WORKING DIRECTORY: LEAN_PROJECT START UTC: 2026-09-05T22:40:11.7222835Z COMMAND: & 'WORKSPACE\tmp\lean_library_definition_audit_2026-09-05\lean-4.34.0-rc2-windows\bin\lake.exe' '--no-cache' 'build' '+ComplementedSubspace:olean' TERMINAL OUTPUT: ✔ [2376/2381] Built ComplementedSubspace.Ambient (95s) ✔ [2377/2383] Built ComplementedSubspace.LocalUnconditional (92s) ✔ [2449/2454] Built ComplementedSubspace.AmbientSeparable (13s) ⚠ [2452/2460] Built ComplementedSubspace.GLRetraction (15s) warning: ComplementedSubspace/GLRetraction.lean:151:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [2454/2463] Built ComplementedSubspace.HilbertOverlap (20s) warning: ComplementedSubspace/HilbertOverlap.lean:27:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.hsSq_nonneg`: [DecidableEq m] [DecidableEq n] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq m] [DecidableEq n] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/HilbertOverlap.lean:31:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.hsSq_transpose`: [DecidableEq m] [DecidableEq n] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq m] [DecidableEq n] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/HilbertOverlap.lean:40:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.sum_sq_mulVec_le`: [DecidableEq m] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq m] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/HilbertOverlap.lean:48:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.hsSq_mul_le`: [DecidableEq k] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq k] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/HilbertOverlap.lean:72:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.diagonal_sq_le_hsSq`: [DecidableEq n] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq n] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/HilbertOverlap.lean:98:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.hsSq_rankOne`: [DecidableEq n] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq n] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/HilbertOverlap.lean:103:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.hsInner_rankOne_eq_diagonal`: [Fintype k] [DecidableEq n] [DecidableEq k] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype k] [DecidableEq n] [DecidableEq k] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/HilbertOverlap.lean:213:4: This simp argument is unused: Matrix.transpose_apply Hint: Omit it from the simp argument list. [apply] simp [hsSq, circleMomentMap, rankOne, Matrix.vecMulVec_apply, Matrix.trace, Matrix.diag, Fin.sum_univ_two, Matrix.one_apply, Matrix.smul_apply] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ✔ [2457/2463] Built ComplementedSubspace.DPRtoGL (14s) ✔ [2458/2464] Built ComplementedSubspace.Parameters (12s) ✔ [2459/2464] Built ComplementedSubspace.TheoremStatement (12s) ✔ [2460/2465] Built ComplementedSubspace.BasisBounds (12s) ✔ [2461/2465] Built ComplementedSubspace.FiniteFrame (17s) ✔ [2462/2465] Built ComplementedSubspace.AmbientLattice (13s) ⚠ [2463/2465] Built ComplementedSubspace.TensorMoment (21s) warning: ComplementedSubspace/TensorMoment.lean:50:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.hsVector_norm_sq`: [DecidableEq m] [DecidableEq n] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq m] [DecidableEq n] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/TensorMoment.lean:51:55: This simp argument is unused: PiLp.toLp_apply Hint: Omit it from the simp argument list. [apply] simp only [hsVector, EuclideanSpace.real_norm_sq_eq, Fintype.sum_prod_type, hsSq] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/TensorMoment.lean:59:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.hsInner_sq_le`: [DecidableEq m] [DecidableEq n] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq m] [DecidableEq n] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/TensorMoment.lean:66:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.rankOne_mixed_hsSq_bound`: [DecidableEq n] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq n] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/TensorMoment.lean:107:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.tensor_hsSq_smul`: [DecidableEq n] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq n] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/TensorMoment.lean:110:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.tensor_hsSq_add`: [DecidableEq n] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq n] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/TensorMoment.lean:116:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.tensor_hsInner_smul_left`: [DecidableEq n] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq n] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/TensorMoment.lean:120:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.tensor_hsInner_smul_right`: [DecidableEq n] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq n] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/TensorMoment.lean:125:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.tensor_hsSq_fromBlocks`: [DecidableEq n] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq n] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ✔ [2574/2583] Built ComplementedSubspace.HilbertComplement (17s) ⚠ [2578/2584] Built ComplementedSubspace.ProjectionPerturbation (21s) warning: ComplementedSubspace/ProjectionPerturbation.lean:46:10: This simp argument is unused: powerEnergyDifference Hint: Omit it from the simp argument list. [apply] simp Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProjectionPerturbation.lean:45:74: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ✔ [2581/2589] Built ComplementedSubspace.BasisTransport (205s) ⚠ [2583/2591] Built ComplementedSubspace.FiniteCorrection (197s) warning: ComplementedSubspace/FiniteCorrection.lean:32:8: automatically included section variable(s) unused in theorem `ComplementedSubspace.finiteRankCorrection_apply`: [DecidableEq ι] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq ι] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/FiniteCorrection.lean:37:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.norm_finiteRankCorrection_le`: [DecidableEq ι] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq ι] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/FiniteCorrection.lean:52:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.exists_extended_basis_coordinates`: [DecidableEq ι] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq ι] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ✔ [2585/2591] Built ComplementedSubspace.ProductFrameIndex (7.5s) ⚠ [2586/2592] Built ComplementedSubspace.FiniteSigns (22s) warning: ComplementedSubspace/FiniteSigns.lean:56:23: This simp argument is unused: Fintype.sum_bool Hint: Omit it from the simp argument list. [apply] simp [finiteAverage] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ⚠ [2588/2592] Built ComplementedSubspace.FiniteApproximation (16s) warning: ComplementedSubspace/FiniteApproximation.lean:52:10: This simp argument is unused: Module.Basis.equivFun_apply Hint: Omit it from the simp argument list. [apply] simp [eq_comm] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/FiniteApproximation.lean:104:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/FiniteApproximation.lean:118:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ✔ [2589/2593] Built ComplementedSubspace.CorollaryStatement (13s) ⚠ [2590/2597] Built ComplementedSubspace.FrameProjectionNorm (24s) warning: ComplementedSubspace/FrameProjectionNorm.lean:19:24: Variable name `i` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _i Note: This linter can be disabled with `set_option linter.unusedVariables false` ⚠ [2591/2597] Built BanLat.Basic (18s) warning: BanLat/Basic.lean:537:2: Try this: haveI̵ The goal is a proposition, so `have` is preferred over `haveI`. The difference between `have` and `haveI` is that `haveI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ✔ [2594/2600] Built ComplementedSubspace.TensorProjection (17s) ⚠ [2595/2602] Built BanLat.LLexpr (16s) warning: BanLat/LLexpr.lean:103:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [2597/2607] Built BanLat.Normed (30s) warning: BanLat/Normed.lean:150:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [2598/2613] Built BanLat.OrderComplete (12s) warning: BanLat/OrderComplete.lean:84:28: `dif_pos` has been deprecated: Use `dite_eq_left` instead warning: BanLat/OrderComplete.lean:88:28: `dif_pos` has been deprecated: Use `dite_eq_left` instead warning: BanLat/OrderComplete.lean:96:28: `dif_pos` has been deprecated: Use `dite_eq_left` instead warning: BanLat/OrderComplete.lean:105:28: `dif_pos` has been deprecated: Use `dite_eq_left` instead warning: BanLat/OrderComplete.lean:126:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/OrderComplete.lean:127:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/OrderComplete.lean:131:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/OrderComplete.lean:244:8: `dif_pos` has been deprecated: Use `dite_eq_left` instead warning: BanLat/OrderComplete.lean:250:8: `dif_pos` has been deprecated: Use `dite_eq_left` instead warning: BanLat/OrderComplete.lean:258:8: `dif_pos` has been deprecated: Use `dite_eq_left` instead warning: BanLat/OrderComplete.lean:269:8: `dif_pos` has been deprecated: Use `dite_eq_left` instead ✔ [2600/2615] Built BanLat.Disjoint (17s) ✔ [2601/2616] Built BanLat.Operators.Positive (19s) ✔ [2602/2616] Built BanLat.OrderUnit (13s) ✔ [2603/2617] Built ComplementedSubspace.DenseContractions (10s) ⚠ [2604/2617] Built BanLat.Substructures.Sublattice (19s) warning: BanLat/Substructures/Sublattice.lean:332:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/Substructures/Sublattice.lean:352:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/Substructures/Sublattice.lean:390:4: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/Substructures/Sublattice.lean:397:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/Substructures/Sublattice.lean:410:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/Substructures/Sublattice.lean:785:4: Try this: haveI̵ The goal is a proposition, so `have` is preferred over `haveI`. The difference between `have` and `haveI` is that `haveI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/Substructures/Sublattice.lean:805:4: `Set.countable_setOf_finite_subset` has been deprecated: Use `Set.countable_ofPred_finite_subset` instead warning: BanLat/Substructures/Sublattice.lean:824:8: `dif_pos` has been deprecated: Use `dite_eq_left` instead warning: BanLat/Substructures/Sublattice.lean:838:8: `dif_pos` has been deprecated: Use `dite_eq_left` instead ⚠ [2605/2618] Built ComplementedSubspace.LocalHilbertCompactness (11s) warning: ComplementedSubspace/LocalHilbertCompactness.lean:107:13: `Set.setOf_and` has been deprecated: Use `Set.ofPred_and` instead warning: ComplementedSubspace/LocalHilbertCompactness.lean:107:24: `Set.setOf_forall` has been deprecated: Use `Set.ofPred_forall` instead warning: ComplementedSubspace/LocalHilbertCompactness.lean:133:34: `Set.setOf_forall` has been deprecated: Use `Set.ofPred_forall` instead warning: ComplementedSubspace/LocalHilbertCompactness.lean:140:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.ApproxParallelogram.mono`: [NormedSpace ℝ E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [NormedSpace ℝ E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/LocalHilbertCompactness.lean:214:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [2606/2618] Built ComplementedSubspace.AmbientBasis (11s) warning: ComplementedSubspace/AmbientBasis.lean:61:38: `ContinuousLinearMap.sum_apply` has been deprecated: Use `sum_apply` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.sum_apply` to `sum_apply x`). warning: ComplementedSubspace/AmbientBasis.lean:64:18: This simp argument is unused: eq_comm Hint: Omit it from the simp argument list. [apply] simp [mul_comm] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/AmbientBasis.lean:96:10: This simp argument is unused: PiLp.smul_apply Hint: Omit it from the simp argument list. [apply] simp [PiLp.single_apply, Pi.single_apply] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/AmbientBasis.lean:96:27: This simp argument is unused: PiLp.single_apply Hint: Omit it from the simp argument list. [apply] simp [PiLp.smul_apply, Pi.single_apply] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/AmbientBasis.lean:123:38: `ContinuousLinearMap.sum_apply` has been deprecated: Use `sum_apply` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.sum_apply` to `sum_apply x`). warning: ComplementedSubspace/AmbientBasis.lean:138:44: `if_pos` has been deprecated: Use `ite_eq_left` instead warning: ComplementedSubspace/AmbientBasis.lean:159:39: `ContinuousLinearMap.sum_apply` has been deprecated: Use `sum_apply` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.sum_apply` to `sum_apply x`). warning: ComplementedSubspace/AmbientBasis.lean:172:35: This simp argument is unused: Pi.single_apply Hint: Omit it from the simp argument list. [apply] simp [hij, eq_comm] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/AmbientBasis.lean:172:57: This simp argument is unused: eq_comm Hint: Omit it from the simp argument list. [apply] simp [Pi.single_apply, hij] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ✔ [2607/2619] Built ComplementedSubspace.LocalHilbertCoordinates (10s) ✔ [2608/2619] Built BanLat.Operators.Hom (14s) ⚠ [2609/2620] Built ComplementedSubspace.ProductFrame (15s) warning: ComplementedSubspace/ProductFrame.lean:50:56: This simp argument is unused: Fintype.card_unit Hint: Omit it from the simp argument list. [apply] simp [realProductFrame, finiteAverage, MomentIndex] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrame.lean:74:49: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ⚠ [2610/2621] Built ComplementedSubspace.ProductFrameMoments (14s) warning: ComplementedSubspace/ProductFrameMoments.lean:91:60: This simp argument is unused: Fintype.card_unit Hint: Omit it from the simp argument list. [apply] simp [productFrameMoment, productFrameFourth, realProductFrame, finiteAverage, tensorMoment, MomentIndex, FrameIndex] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:105:19: This simp argument is unused: productFrameMoment Hint: Omit it from the simp argument list. [apply] simp only [Fintype.sum_sum_type, Finset.sum_add_distrib, ← sideIndex_false, ← sideIndex_true, productFrameFourth_succ] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:107:59: This simp argument is unused: not_false_eq_true Hint: Omit it from the simp argument list. [apply] simp only [Bool.false_eq_true, Bool.true_eq_false, and_self, and_true, and_false, ↓reduceIte, zero_add, add_zero, zero_mul, one_mul, Finset.sum_const_zero, circleBlock, Matrix.smul_apply, Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Matrix.add_apply, Matrix.submatrix_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul, sideIndex, ↓reduceIte] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:109:10: This simp argument is unused: zero_mul Hint: Omit it from the simp argument list. [apply] simp only [Bool.false_eq_true, Bool.true_eq_false, not_false_eq_true, and_self, and_true, and_false, ↓reduceIte, zero_add, add_zero, one_mul, Finset.sum_const_zero, circleBlock, Matrix.smul_apply, Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Matrix.add_apply, Matrix.submatrix_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul, sideIndex, ↓reduceIte] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:109:20: This simp argument is unused: one_mul Hint: Omit it from the simp argument list. [apply] simp only [Bool.false_eq_true, Bool.true_eq_false, not_false_eq_true, and_self, and_true, and_false, ↓reduceIte, zero_add, add_zero, zero_mul, Finset.sum_const_zero, circleBlock, Matrix.smul_apply, Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Matrix.add_apply, Matrix.submatrix_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul, sideIndex, ↓reduceIte] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:109:29: This simp argument is unused: Finset.sum_const_zero Hint: Omit it from the simp argument list. [apply] simp only [Bool.false_eq_true, Bool.true_eq_false, not_false_eq_true, and_self, and_true, and_false, ↓reduceIte, zero_add, add_zero, zero_mul, one_mul, circleBlock, Matrix.smul_apply, Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Matrix.add_apply, Matrix.submatrix_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul, sideIndex, ↓reduceIte] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:112:10: This simp argument is unused: Matrix.submatrix_apply Hint: Omit it from the simp argument list. [apply] simp only [Bool.false_eq_true, Bool.true_eq_false, not_false_eq_true, and_self, and_true, and_false, ↓reduceIte, zero_add, add_zero, zero_mul, one_mul, Finset.sum_const_zero, circleBlock, Matrix.smul_apply, Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Matrix.add_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul, sideIndex, ↓reduceIte] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:112:34: This simp argument is unused: Pi.add_apply Hint: Omit it from the simp argument list. [apply] simp only [Bool.false_eq_true, Bool.true_eq_false, not_false_eq_true, and_self, and_true, and_false, ↓reduceIte, zero_add, add_zero, zero_mul, one_mul, Finset.sum_const_zero, circleBlock, Matrix.smul_apply, Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Matrix.add_apply, Matrix.submatrix_apply, Pi.smul_apply, smul_eq_mul, sideIndex, ↓reduceIte] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:112:48: This simp argument is unused: Pi.smul_apply Hint: Omit it from the simp argument list. [apply] simp only [Bool.false_eq_true, Bool.true_eq_false, not_false_eq_true, and_self, and_true, and_false, ↓reduceIte, zero_add, add_zero, zero_mul, one_mul, Finset.sum_const_zero, circleBlock, Matrix.smul_apply, Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Matrix.add_apply, Matrix.submatrix_apply, Pi.add_apply, smul_eq_mul, sideIndex, ↓reduceIte] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:114:10: This simp argument is unused: Matrix.add_apply Hint: Omit it from the simp argument list. [apply] simp only [productFrameMoment, Matrix.submatrix_apply, Pi.add_apply, mul_add, Finset.sum_add_distrib, Finset.sum_const_zero, zero_add, add_zero, ← Finset.mul_sum, ← Finset.sum_mul] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:115:10: This simp argument is unused: Finset.sum_const_zero Hint: Omit it from the simp argument list. [apply] simp only [productFrameMoment, Matrix.submatrix_apply, Pi.add_apply, Matrix.add_apply, mul_add, Finset.sum_add_distrib, zero_add, add_zero, ← Finset.mul_sum, ← Finset.sum_mul] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:115:33: This simp argument is unused: zero_add Hint: Omit it from the simp argument list. [apply] simp only [productFrameMoment, Matrix.submatrix_apply, Pi.add_apply, Matrix.add_apply, mul_add, Finset.sum_add_distrib, Finset.sum_const_zero, add_zero, ← Finset.mul_sum, ← Finset.sum_mul] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:115:43: This simp argument is unused: add_zero Hint: Omit it from the simp argument list. [apply] simp only [productFrameMoment, Matrix.submatrix_apply, Pi.add_apply, Matrix.add_apply, mul_add, Finset.sum_add_distrib, Finset.sum_const_zero, zero_add, ← Finset.mul_sum, ← Finset.sum_mul] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:115:53: This simp argument is unused: ← Finset.mul_sum Hint: Omit it from the simp argument list. [apply] simp only [productFrameMoment, Matrix.submatrix_apply, Pi.add_apply, Matrix.add_apply, mul_add, Finset.sum_add_distrib, Finset.sum_const_zero, zero_add, add_zero, ← Finset.sum_mul] Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning. Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:116:10: This simp argument is unused: ← Finset.sum_mul Hint: Omit it from the simp argument list. [apply] simp only [productFrameMoment, Matrix.submatrix_apply, Pi.add_apply, Matrix.add_apply, mul_add, Finset.sum_add_distrib, Finset.sum_const_zero, zero_add, add_zero, ← Finset.mul_sum] Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning. Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:118:48: This simp argument is unused: ← Finset.sum_mul Hint: Omit it from the simp argument list. [apply] simp only [mul_assoc, ← Finset.mul_sum, Finset.sum_const_zero, zero_add, add_zero] Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning. Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:119:10: This simp argument is unused: Finset.sum_const_zero Hint: Omit it from the simp argument list. [apply] simp only [mul_assoc, ← Finset.mul_sum, ← Finset.sum_mul, zero_add, add_zero] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:119:33: This simp argument is unused: zero_add Hint: Omit it from the simp argument list. [apply] simp only [mul_assoc, ← Finset.mul_sum, ← Finset.sum_mul, Finset.sum_const_zero, add_zero] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameMoments.lean:119:43: This simp argument is unused: add_zero Hint: Omit it from the simp argument list. [apply] simp only [mul_assoc, ← Finset.mul_sum, ← Finset.sum_mul, Finset.sum_const_zero, zero_add] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ⚠ [2611/2622] Built BanLat.Substructures.Ideal (35s) warning: BanLat/Substructures/Ideal.lean:212:55: `if_pos` has been deprecated: Use `ite_eq_left` instead warning: BanLat/Substructures/Ideal.lean:214:36: `if_neg` has been deprecated: Use `ite_eq_right` instead warning: BanLat/Substructures/Ideal.lean:219:55: `if_pos` has been deprecated: Use `ite_eq_left` instead warning: BanLat/Substructures/Ideal.lean:221:36: `if_neg` has been deprecated: Use `ite_eq_right` instead ✔ [2612/2622] Built ComplementedSubspace.FiniteOverlapMoments (9.7s) ⚠ [2613/2623] Built ComplementedSubspace.ProductFrameLp (9.8s) warning: ComplementedSubspace/ProductFrameLp.lean:27:11: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ✔ [2614/2624] Built BanLat.Substructures.Band.Basic (13s) ✔ [2615/2625] Built ComplementedSubspace.FrameProjectionRange (14s) ✔ [2616/2625] Built BanLat.Substructures.Band.DisjointComplement (14s) ✔ [2617/2625] Built BanLat.Substructures.Band.Lattice (24s) ⚠ [2618/2626] Built ComplementedSubspace.FrameCoefficient (13s) warning: ComplementedSubspace/FrameCoefficient.lean:17:30: Variable name `p` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _p Note: This linter can be disabled with `set_option linter.unusedVariables false` ✔ [2619/2629] Built ComplementedSubspace.FrameCoefficientRange (12s) ⚠ [2620/2629] Built BanLat.Substructures.Band.Generated (14s) warning: BanLat/Substructures/Band/Generated.lean:69:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [2623/2631] Built ComplementedSubspace.FrameCoefficientNorm (9.6s) warning: ComplementedSubspace/FrameCoefficientNorm.lean:23:18: This simp argument is unused: PiLp.toLp_apply Hint: Omit it from the simp argument list. [apply] simp only [hp', Real.norm_eq_abs] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ✔ [2625/2633] Built BanLat.Substructures.Band.Projection (17s) ⚠ [2626/2633] Built ComplementedSubspace.LocalHilbertDual (18s) warning: ComplementedSubspace/LocalHilbertDual.lean:62:27: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/LocalHilbertDual.lean:96:15: `ContinuousLinearMap.add_apply` has been deprecated: Use `add_apply` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.add_apply` to `add_apply x`). warning: ComplementedSubspace/LocalHilbertDual.lean:96:46: `ContinuousLinearMap.sub_apply` has been deprecated: Use `sub_apply` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.sub_apply` to `sub_apply x`). warning: ComplementedSubspace/LocalHilbertDual.lean:107:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.ApproxParallelogram.nonneg_of_nontrivial`: [NormedSpace ℝ E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [NormedSpace ℝ E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/LocalHilbertDual.lean:129:6: This simp argument is unused: zero_add Hint: Omit it from the simp argument list. [apply] simp only [hf, hg, add_zero, sub_self, norm_zero, zero_pow (by decide : 2 ≠ 0), mul_zero, le_refl] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ✔ [2627/2633] Built ComplementedSubspace.LocalHilbert (19s) ✔ [2628/2634] Built ComplementedSubspace.FiniteLpGeometry (18s) ⚠ [2629/2634] Built BanLat.Substructures.Band.PPP (17s) warning: BanLat/Substructures/Band/PPP.lean:60:2: Try this: haveI̵ The goal is a proposition, so `have` is preferred over `haveI`. The difference between `have` and `haveI` is that `haveI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/Substructures/Band/PPP.lean:74:2: Try this: haveI̵ The goal is a proposition, so `have` is preferred over `haveI`. The difference between `have` and `haveI` is that `haveI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [2630/2635] Built ComplementedSubspace.LocalHilbertProjection (12s) warning: ComplementedSubspace/LocalHilbertProjection.lean:84:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ✔ [2631/2636] Built ComplementedSubspace.LpTwoUniformConvex (12s) ✔ [2632/2636] Built ComplementedSubspace.LatticeSpectral (12s) ✔ [2633/2636] Built ComplementedSubspace.AmbientUniformConvex (11s) ✔ [2634/2638] Built ComplementedSubspace.LatticeBasis (14s) ✔ [2635/2640] Built ComplementedSubspace.LpTwoParallelogram (15s) ✔ [2636/2641] Built BanLat.Operators.OrderBounded (17s) ✔ [2637/2643] Built BanLat.RieszDec (14s) ✔ [2642/2649] Built BanLat.Operators.Regular (13s) ⚠ [2644/2652] Built ComplementedSubspace.DPRIsomorphism (15s) warning: ComplementedSubspace/DPRIsomorphism.lean:24:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/DPRIsomorphism.lean:27:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/DPRIsomorphism.lean:48:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [2645/2653] Built ComplementedSubspace.GLDualRetraction (13s) warning: ComplementedSubspace/GLDualRetraction.lean:58:4: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/GLDualRetraction.lean:61:4: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [2646/2653] Built BanLat.Operators.RieszKantorovich (25s) warning: BanLat/Operators/RieszKantorovich.lean:56:20: `if_pos` has been deprecated: Use `ite_eq_left` instead warning: BanLat/Operators/RieszKantorovich.lean:121:2: Try this: haveI̵ The goal is a proposition, so `have` is preferred over `haveI`. The difference between `have` and `haveI` is that `haveI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/Operators/RieszKantorovich.lean:127:2: Try this: haveI̵ The goal is a proposition, so `have` is preferred over `haveI`. The difference between `have` and `haveI` is that `haveI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/Operators/RieszKantorovich.lean:773:2: Try this: haveI̵ The goal is a proposition, so `have` is preferred over `haveI`. The difference between `have` and `haveI` is that `haveI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/Operators/RieszKantorovich.lean:779:2: Try this: haveI̵ The goal is a proposition, so `have` is preferred over `haveI`. The difference between `have` and `haveI` is that `haveI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/Operators/RieszKantorovich.lean:1181:2: Try this: haveI̵ The goal is a proposition, so `have` is preferred over `haveI`. The difference between `have` and `haveI` is that `haveI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: BanLat/Operators/RieszKantorovich.lean:1195:8: `dif_pos` has been deprecated: Use `dite_eq_left` instead warning: BanLat/Operators/RieszKantorovich.lean:1338:8: `dif_pos` has been deprecated: Use `dite_eq_left` instead ⚠ [2647/2653] Built ComplementedSubspace.FiniteParameterGap (15s) warning: ComplementedSubspace/FiniteParameterGap.lean:74:55: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/FiniteParameterGap.lean:77:66: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/FiniteParameterGap.lean:78:33: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/FiniteParameterGap.lean:82:44: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/FiniteParameterGap.lean:103:46: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/FiniteParameterGap.lean:106:46: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/FiniteParameterGap.lean:149:6: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: ComplementedSubspace/FiniteParameterGap.lean:149:6: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: ComplementedSubspace/FiniteParameterGap.lean:158:6: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: ComplementedSubspace/FiniteParameterGap.lean:158:6: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: ComplementedSubspace/FiniteParameterGap.lean:240:2: Unused tactic linter: `congr 1` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: ComplementedSubspace/FiniteParameterGap.lean:256:2: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ⚠ [2648/2653] Built BanLat.Dual (15s) warning: BanLat/Dual.lean:106:6: `dif_pos` has been deprecated: Use `dite_eq_left` instead ⚠ [2649/2655] Built ComplementedSubspace.AmbientSchauder (29s) warning: ComplementedSubspace/AmbientSchauder.lean:29:27: This simp argument is unused: eq_comm Hint: Omit it from the simp argument list. [apply] simp [Pi.single_apply] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/AmbientSchauder.lean:41:40: `ContinuousLinearMap.sum_apply` has been deprecated: Use `sum_apply` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.sum_apply` to `sum_apply x`). ✔ [2650/2655] Built ComplementedSubspace.LatticeApproximation (9.2s) ⚠ [2651/2655] Built ComplementedSubspace.ProductFrameSymmetry (15s) warning: ComplementedSubspace/ProductFrameSymmetry.lean:160:65: This simp argument is unused: Fintype.card_unit Hint: Omit it from the simp argument list. [apply] simp [frameSymmetry, finiteAverage, MomentIndex, FrameIndex] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameSymmetry.lean:173:30: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: ComplementedSubspace/ProductFrameSymmetry.lean:178:30: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: ComplementedSubspace/ProductFrameSymmetry.lean:173:30: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: ComplementedSubspace/ProductFrameSymmetry.lean:178:30: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: ComplementedSubspace/ProductFrameSymmetry.lean:170:31: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/ProductFrameSymmetry.lean:182:31: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ✔ [2652/2655] Built ComplementedSubspace.FiniteHilbertAverage (10s) ⚠ [2653/2657] Built ComplementedSubspace.LatticeNonisomorphism (12s) warning: ComplementedSubspace/LatticeNonisomorphism.lean:23:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/LatticeNonisomorphism.lean:24:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/LatticeNonisomorphism.lean:25:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/LatticeNonisomorphism.lean:26:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/LatticeNonisomorphism.lean:27:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/LatticeNonisomorphism.lean:28:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/LatticeNonisomorphism.lean:29:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [2682/2686] Built ComplementedSubspace.AmbientFiniteApproximation (15s) warning: ComplementedSubspace/AmbientFiniteApproximation.lean:81:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/AmbientFiniteApproximation.lean:82:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/AmbientFiniteApproximation.lean:98:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/AmbientFiniteApproximation.lean:99:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/AmbientFiniteApproximation.lean:100:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/AmbientFiniteApproximation.lean:105:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/AmbientFiniteApproximation.lean:106:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/AmbientFiniteApproximation.lean:107:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [2683/2686] Built ComplementedSubspace.FiniteParameterBounds (12s) warning: ComplementedSubspace/FiniteParameterBounds.lean:79:10: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: ComplementedSubspace/FiniteParameterBounds.lean:79:10: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ⚠ [2684/2690] Built ComplementedSubspace.ProductFrameTrace (12s) warning: ComplementedSubspace/ProductFrameTrace.lean:62:12: This simp argument is unused: Pi.single_apply Hint: Omit it from the simp argument list. [apply] simp [hki] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameTrace.lean:87:27: This simp argument is unused: LinearMap.toMatrix_apply Hint: Omit it from the simp argument list. [apply] simp only [Matrix.trace] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameTrace.lean:88:11: This simp argument is unused: Pi.basisFun_apply Hint: Omit it from the simp argument list. [apply] simp [b, LinearMap.toMatrix'_apply] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ProductFrameTrace.lean:129:51: This simp argument is unused: Finset.sum_ite_eq' Hint: Omit it from the simp argument list. [apply] simp only [mul_ite, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, ite_true] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ✔ [2685/2693] Built ComplementedSubspace.ProductFrameWitness (14s) ✔ [2686/2698] Built ComplementedSubspace.FiniteSignsComplex (13s) ✔ [2687/2698] Built ComplementedSubspace.FiniteTraceSelection (10s) ⚠ [2688/2698] Built ComplementedSubspace.FiniteSignsInterpolation (14s) warning: ComplementedSubspace/FiniteSignsInterpolation.lean:65:13: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/FiniteSignsInterpolation.lean:89:15: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ✔ [2689/2701] Built ComplementedSubspace.LocalHilbertFactorization (15s) ⚠ [2690/2701] Built ComplementedSubspace.FiniteProjectionTrace (16s) warning: ComplementedSubspace/FiniteProjectionTrace.lean:47:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.compressedBasisMap_eq_smulRight`: [FiniteDimensional ℝ E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [FiniteDimensional ℝ E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/FiniteProjectionTrace.lean:81:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.sum_compressedBasisMap`: [FiniteDimensional ℝ E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [FiniteDimensional ℝ E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/FiniteProjectionTrace.lean:98:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.compressedBasisMap_complement_defect`: [FiniteDimensional ℝ E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [FiniteDimensional ℝ E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/FiniteProjectionTrace.lean:120:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.basisComplementCompression_expansion`: [FiniteDimensional ℝ E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [FiniteDimensional ℝ E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/FiniteProjectionTrace.lean:132:38: This simp argument is unused: mul_assoc Hint: Omit it from the simp argument list. [apply] simp only [mul_comm, mul_left_comm] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ⚠ [2691/2701] Built ComplementedSubspace.ProductFrameSignSample (13s) warning: ComplementedSubspace/ProductFrameSignSample.lean:136:10: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: ComplementedSubspace/ProductFrameSignSample.lean:136:10: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: ComplementedSubspace/ProductFrameSignSample.lean:127:13: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ✔ [2692/2701] Built ComplementedSubspace.HilbertTraceTransfer (10s) ⚠ [2693/2704] Built ComplementedSubspace.FiniteOverlapLp (10s) warning: ComplementedSubspace/FiniteOverlapLp.lean:56:63: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/FiniteOverlapLp.lean:63:13: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/FiniteOverlapLp.lean:106:41: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: ComplementedSubspace/FiniteOverlapLp.lean:106:41: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: ComplementedSubspace/FiniteOverlapLp.lean:84:13: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ⚠ [2694/2706] Built ComplementedSubspace.ProductFrameSignContraction (10s) warning: ComplementedSubspace/ProductFrameSignContraction.lean:115:10: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: ComplementedSubspace/ProductFrameSignContraction.lean:115:10: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: ComplementedSubspace/ProductFrameSignContraction.lean:105:13: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ✔ [2695/2706] Built ComplementedSubspace.ProductFrameTraceBound (10s) ✔ [2696/2706] Built ComplementedSubspace.FiniteBasisTraceBound (10s) ⚠ [2697/2707] Built ComplementedSubspace.FiniteOverlapRandomization (9.9s) warning: ComplementedSubspace/FiniteOverlapRandomization.lean:114:10: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: ComplementedSubspace/FiniteOverlapRandomization.lean:114:10: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ⚠ [2698/2707] Built ComplementedSubspace.FiniteOverlapScale (19s) warning: ComplementedSubspace/FiniteOverlapScale.lean:35:2: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/FiniteOverlapScale.lean:57:61: Variable name `hp₃` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hp₃ Note: This linter can be disabled with `set_option linter.unusedVariables false` info: ComplementedSubspace/FiniteOverlapScale.lean:140:4: Try this: [apply] ring_nf The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form. Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead. warning: ComplementedSubspace/FiniteOverlapScale.lean:138:29: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/FiniteOverlapScale.lean:171:23: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ✔ [2699/2708] Built ComplementedSubspace.FiniteOverlapGoodSecond (15s) ⚠ [2700/2708] Built ComplementedSubspace.UnconditionalHilbertSynthesis (14s) warning: ComplementedSubspace/UnconditionalHilbertSynthesis.lean:51:13: Variable name `hD` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hD Note: This linter can be disabled with `set_option linter.unusedVariables false` ✔ [2701/2711] Built ComplementedSubspace.FrameCoefficientHilbert (15s) ⚠ [2702/2711] Built ComplementedSubspace.FiniteOverlapBasisColumns (15s) warning: ComplementedSubspace/FiniteOverlapBasisColumns.lean:15:42: This simp argument is unused: Finset.sum_ite_eq' Hint: Omit it from the simp argument list. [apply] simp only [Real.norm_eq_abs, sq_abs, normalizedFrameSign_covariance, ite_div, zero_div, mul_ite, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, ite_true, real_inner_self_eq_norm_sq] at h Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/FiniteOverlapBasisColumns.lean:17:13: This simp argument is unused: Real.norm_eq_abs Hint: Omit it from the simp argument list. [apply] simp only [sq_abs, one_div, ← Finset.sum_mul] at h Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/FiniteOverlapBasisColumns.lean:17:31: This simp argument is unused: sq_abs Hint: Omit it from the simp argument list. [apply] simp only [Real.norm_eq_abs, one_div, ← Finset.sum_mul] at h Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ✔ [2704/2711] Built ComplementedSubspace.NormalizedHilbertSynthesis (16s) ✔ [2705/2712] Built ComplementedSubspace.FiniteOverlapMatrixNorms (14s) ✔ [2706/2714] Built ComplementedSubspace.FiniteOverlapUpper (17s) ✔ [2707/2714] Built ComplementedSubspace.SelectedCoefficientHilbert (18s) ✔ [2708/2714] Built ComplementedSubspace.FiniteTraceOverlap (18s) ✔ [2709/2714] Built ComplementedSubspace.FiniteOverlapBound (16s) ✔ [2710/2714] Built ComplementedSubspace.ProductFrameRowWitness (20s) ⚠ [2711/2717] Built ComplementedSubspace.SelectedProjectionSetup (27s) warning: ComplementedSubspace/SelectedProjectionSetup.lean:64:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.selectedCoefficientHilbertEquiv_norm_le_one`: [FiniteDimensional ℝ ↥F] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [FiniteDimensional ℝ ↥F] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/SelectedProjectionSetup.lean:164:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.selectedCoefficient_coordinate_sq_le`: [FiniteDimensional ℝ ↥F] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [FiniteDimensional ℝ ↥F] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/SelectedProjectionSetup.lean:180:66: `ContinuousLinearMap.zero_apply` has been deprecated: Use `zero_apply` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.zero_apply` to `zero_apply x`). warning: ComplementedSubspace/SelectedProjectionSetup.lean:174:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.selectedCoefficientHilbert_first_pairing`: [FiniteDimensional ℝ ↥F] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [FiniteDimensional ℝ ↥F] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/SelectedProjectionSetup.lean:185:40: This simp argument is unused: WithLp.ofLp_toLp Hint: Omit it from the simp argument list. [apply] simp only [PiLp.inner_apply, RCLike.inner_apply, conj_trivial, frameCoefficientHilbertEquiv_apply] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ✔ [2712/2717] Built ComplementedSubspace.FiniteOverlapConclusion (12s) ✔ [2713/2719] Built ComplementedSubspace.BasisRestriction (10s) ✔ [2714/2719] Built ComplementedSubspace.ProjectionOverlapLower (11s) ⚠ [2715/2721] Built ComplementedSubspace.FiniteSelectionCoordinates (14s) warning: ComplementedSubspace/FiniteSelectionCoordinates.lean:81:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.basisSubsetProjection_compressed_trace`: [FiniteDimensional ℝ E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [FiniteDimensional ℝ E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ✔ [2716/2722] Built ComplementedSubspace.SelectedHilbertReplacement (23s) ⚠ [2717/2723] Built ComplementedSubspace.FiniteCoordinateSelection (10s) warning: ComplementedSubspace/FiniteCoordinateSelection.lean:42:32: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ComplementedSubspace/FiniteCoordinateSelection.lean:47:24: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ✔ [2718/2723] Built ComplementedSubspace.FiniteSuperspaceSplitting (16s) ⚠ [2719/2723] Built ComplementedSubspace.FiniteSelectedHilbertModel (16s) warning: ComplementedSubspace/FiniteSelectedHilbertModel.lean:46:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/FiniteSelectedHilbertModel.lean:29:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.selected_coordinates_have_hilbert_factorization`: [FiniteDimensional ℝ E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [FiniteDimensional ℝ E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ✔ [2720/2726] Built ComplementedSubspace.FiniteOverlapDualScale (14s) ✔ [2721/2727] Built ComplementedSubspace.NormSqSplitting (15s) ⚠ [2722/2727] Built ComplementedSubspace.DPRObstruction (12s) warning: ComplementedSubspace/DPRObstruction.lean:40:8: Variable name `hVdim` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hVdim Note: This linter can be disabled with `set_option linter.unusedVariables false` ⚠ [2723/2727] Built ComplementedSubspace.LocalHilbertSum (20s) warning: ComplementedSubspace/LocalHilbertSum.lean:140:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ✔ [2724/2727] Built ComplementedSubspace.IsometricProductSplitting (16s) ✔ [2725/2729] Built ComplementedSubspace.FiniteDualBasis (13s) ✔ [2727/2732] Built ComplementedSubspace.LocalHilbertTransport (14s) ✔ [2728/2734] Built ComplementedSubspace.AmbientProjection (15s) ✔ [2729/2736] Built ComplementedSubspace.RecursiveParameters (11s) ✔ [2730/2737] Built ComplementedSubspace.FiniteHeadHilbert (16s) ✔ [2731/2737] Built ComplementedSubspace.ReindexedFrameProjection (16s) ✔ [2732/2737] Built ComplementedSubspace.LocalHilbertProperty (13s) ⚠ [2733/2737] Built ComplementedSubspace.RecursiveHeadHilbert (16s) warning: ComplementedSubspace/RecursiveHeadHilbert.lean:28:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [2734/2737] Built ComplementedSubspace.RecursiveProjection (21s) warning: ComplementedSubspace/RecursiveProjection.lean:98:42: `if_pos` has been deprecated: Use `ite_eq_left` instead warning: ComplementedSubspace/RecursiveProjection.lean:115:41: `if_neg` has been deprecated: Use `ite_eq_right` instead ⚠ [2735/2739] Built ComplementedSubspace.LocalHilbertQuotient (15s) warning: ComplementedSubspace/LocalHilbertQuotient.lean:91:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [2736/2741] Built ComplementedSubspace.LocalHilbertSumDual (23s) warning: ComplementedSubspace/LocalHilbertSumDual.lean:52:27: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ⚠ [2737/2741] Built ComplementedSubspace.LpSubmodule (22s) warning: ComplementedSubspace/LpSubmodule.lean:62:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.lp_two_coordinate_norm_sq`: [(i : ι) → NormedSpace ℝ (E i)] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [(i : ι) → NormedSpace ℝ (E i)] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/LpSubmodule.lean:102:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.lpDiagonalRangeEval_norm_le`: [DecidableEq ι] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq ι] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ⚠ [2738/2744] Built ComplementedSubspace.FrameCoefficientReindexedRange (14s) warning: ComplementedSubspace/FrameCoefficientReindexedRange.lean:44:36: `if_pos` has been deprecated: Use `ite_eq_left` instead warning: ComplementedSubspace/FrameCoefficientReindexedRange.lean:50:36: `if_neg` has been deprecated: Use `ite_eq_right` instead ✔ [2739/2744] Built ComplementedSubspace.LpHeadTail (18s) ⚠ [2740/2747] Built ComplementedSubspace.DiagonalFrameSummand (12s) warning: ComplementedSubspace/DiagonalFrameSummand.lean:58:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.diagonalSummand_RJ`: [DecidableEq ι] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq ι] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: ComplementedSubspace/DiagonalFrameSummand.lean:83:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.diagonalSummand_J_norm`: [DecidableEq ι] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq ι] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ✔ [2741/2748] Built ComplementedSubspace.FiniteCubeBound (8.1s) ✔ [2742/2750] Built ComplementedSubspace.SchauderDPR (15s) ⚠ [2743/2750] Built ComplementedSubspace.ComplexProjectionEnergy (18s) warning: ComplementedSubspace/ComplexProjectionEnergy.lean:45:24: Variable name `i` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _i Note: This linter can be disabled with `set_option linter.unusedVariables false` ⚠ [2744/2750] Built ComplementedSubspace.ProjectionCorollaries (14s) warning: ComplementedSubspace/ProjectionCorollaries.lean:21:4: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/ProjectionCorollaries.lean:24:4: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ✔ [2745/2750] Built ComplementedSubspace.ComplexAmbient (16s) ✔ [2746/2750] Built ComplementedSubspace.DenseContractionsScalar (11s) ✔ [2747/2750] Built ComplementedSubspace.ComplexFrameProjection (16s) ✔ [2748/2754] Built ComplementedSubspace.ComplexTensorProjection (12s) ⚠ [2749/2757] Built ComplementedSubspace.ComplexAmbientSchauder (36s) warning: ComplementedSubspace/ComplexAmbientSchauder.lean:56:45: `ContinuousLinearMap.sum_apply` has been deprecated: Use `sum_apply` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.sum_apply` to `sum_apply x`). warning: ComplementedSubspace/ComplexAmbientSchauder.lean:59:18: This simp argument is unused: eq_comm Hint: Omit it from the simp argument list. [apply] simp [mul_comm] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ComplexAmbientSchauder.lean:103:10: This simp argument is unused: PiLp.smul_apply Hint: Omit it from the simp argument list. [apply] simp [PiLp.single_apply, Pi.single_apply] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ComplexAmbientSchauder.lean:103:27: This simp argument is unused: PiLp.single_apply Hint: Omit it from the simp argument list. [apply] simp [PiLp.smul_apply, Pi.single_apply] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ComplexAmbientSchauder.lean:130:45: `ContinuousLinearMap.sum_apply` has been deprecated: Use `sum_apply` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.sum_apply` to `sum_apply x`). warning: ComplementedSubspace/ComplexAmbientSchauder.lean:145:51: `if_pos` has been deprecated: Use `ite_eq_left` instead warning: ComplementedSubspace/ComplexAmbientSchauder.lean:166:46: `ContinuousLinearMap.sum_apply` has been deprecated: Use `sum_apply` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.sum_apply` to `sum_apply x`). warning: ComplementedSubspace/ComplexAmbientSchauder.lean:179:35: This simp argument is unused: Pi.single_apply Hint: Omit it from the simp argument list. [apply] simp [hij, eq_comm] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ComplexAmbientSchauder.lean:179:57: This simp argument is unused: eq_comm Hint: Omit it from the simp argument list. [apply] simp [Pi.single_apply, hij] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ComplexAmbientSchauder.lean:200:27: This simp argument is unused: eq_comm Hint: Omit it from the simp argument list. [apply] simp [Pi.single_apply] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: ComplementedSubspace/ComplexAmbientSchauder.lean:212:47: `ContinuousLinearMap.sum_apply` has been deprecated: Use `sum_apply` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.sum_apply` to `sum_apply x`). ✔ [2750/2757] Built ComplementedSubspace.FiniteOverlapObstruction (24s) ✔ [2751/2758] Built ComplementedSubspace.RecursiveTailHilbert (10s) ⚠ [2752/2758] Built ComplementedSubspace.FiniteBlockObstruction (10s) warning: ComplementedSubspace/FiniteBlockObstruction.lean:50:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ✔ [2753/2761] Built ComplementedSubspace.RecursiveKernelHilbert (11s) ✔ [2754/2762] Built ComplementedSubspace.FiniteProductObstruction (9.2s) ⚠ [2755/2762] Built ComplementedSubspace.FiniteBlockDPRLower (10s) warning: ComplementedSubspace/FiniteBlockDPRLower.lean:31:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ✔ [2756/2762] Built ComplementedSubspace.FiniteBidual (10s) ✔ [2757/2763] Built ComplementedSubspace.DiagonalFrameProduct (10s) ✔ [2758/2766] Built ComplementedSubspace.InfiniteFrameObstruction (9.4s) ✔ [2759/2766] Built ComplementedSubspace.FiniteDualSuperspace (11s) ✔ [2760/2766] Built ComplementedSubspace.LocalHilbertEmbeddedRenorm (10s) ✔ [2761/2766] Built ComplementedSubspace.RecursiveDiagonalDPR (11s) ⚠ [2762/2766] Built ComplementedSubspace.LocalHilbertHeadRenorm (11s) warning: ComplementedSubspace/LocalHilbertHeadRenorm.lean:22:0: automatically included section variable(s) unused in theorem `ComplementedSubspace.ApproxParallelogram.prodL2`: [NormedSpace ℝ E] [NormedSpace ℝ F] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [NormedSpace ℝ E] [NormedSpace ℝ F] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ⚠ [2763/2769] Built ComplementedSubspace.FiniteDualDPRLower (11s) warning: ComplementedSubspace/FiniteDualDPRLower.lean:33:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/FiniteDualDPRLower.lean:43:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` warning: ComplementedSubspace/FiniteDualDPRLower.lean:44:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ✔ [2764/2771] Built ComplementedSubspace.LocalHilbertRecursiveKernelDual (12s) ⚠ [2765/2771] Built ComplementedSubspace.IsometricProductDPRLower (9.5s) warning: ComplementedSubspace/IsometricProductDPRLower.lean:28:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ✔ [2766/2771] Built ComplementedSubspace.LocalHilbertDualTop (8.0s) ✔ [2767/2771] Built ComplementedSubspace.RecursiveDiagonalDualDPR (10s) ✔ [2768/2774] Built ComplementedSubspace.DPRPredicates (8.1s) ✔ [2769/2774] Built ComplementedSubspace.FiniteBidualDPRLower (9.4s) ✔ [2770/2776] Built ComplementedSubspace.ActualProjectionDPR (9.8s) ✔ [2771/2776] Built ComplementedSubspace.RecursiveDiagonalBidualDPR (10s) ✔ [2772/2776] Built ComplementedSubspace.ActualProjectionDualDPR (10s) ✔ [2773/2779] Built ComplementedSubspace.ActualProjectionBidualDPR (9.9s) ✔ [2774/2779] Built ComplementedSubspace.RealMainTheorem (10s) ⚠ [2775/2780] Built ComplementedSubspace.ComplexFrameCoefficient (10s) warning: ComplementedSubspace/ComplexFrameCoefficient.lean:35:37: Variable name `p` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _p Note: This linter can be disabled with `set_option linter.unusedVariables false` warning: ComplementedSubspace/ComplexFrameCoefficient.lean:123:18: This simp argument is unused: PiLp.toLp_apply Hint: Omit it from the simp argument list. [apply] simp only [hp'] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ⚠ [2776/2780] Built ComplementedSubspace.RealMainConsequences (12s) warning: ComplementedSubspace/RealMainConsequences.lean:27:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ✔ [2777/2782] Built ComplementedSubspace.ComplexFrameRealification (14s) ✔ [2778/2782] Built ComplementedSubspace.ComplexFrameCoefficientRange (15s) ✔ [2779/2785] Built ComplementedSubspace.ComplexReindexedFrameProjection (13s) ✔ [2781/2789] Built ComplementedSubspace.LpSubmoduleScalar (11s) ✔ [2782/2789] Built ComplementedSubspace.LpUniformEquiv (14s) ✔ [2783/2789] Built ComplementedSubspace.ComplexRecursiveProjection (15s) ✔ [2784/2789] Built ComplementedSubspace.ComplexRealDPR (12s) ✔ [2785/2789] Built ComplementedSubspace.PureFrameDPR (12s) ⚠ [2786/2789] Built ComplementedSubspace.ComplexCorollaryAssembly (13s) warning: ComplementedSubspace/ComplexCorollaryAssembly.lean:32:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ✔ [2787/2789] Built ComplementedSubspace.ComplexProjectionRealEquiv (14s) ✔ [2788/2789] Built ComplementedSubspace.ComplexCorollary (10s) ✔ [2789/2789] Built ComplementedSubspace (8.6s) Build completed successfully (2789 jobs). EXIT CODE: 0 END UTC: 2026-09-05T23:08:14.5354564Z