From c1c43e941ec6acb8eb36ca631125f567341bb415 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 20:53:55 -0400 Subject: [PATCH] refactor(Circuit/Rational,Arithmetic): make 51 API and general declarations public again (#926) Earlier privatization passes (mostly #841) hid these declarations because nothing outside their module used them. Under the privatize-by-intent rule of #926 they are library API or general mathematics, so they become public again. Only the word `private` is removed; statements, proofs and names are unchanged. Part of #587. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Circuit/Arithmetic/Power.lean | 2 +- .../Computability/Circuit/Arithmetic/VNP.lean | 2 +- .../Computability/Circuit/Arithmetic/VP.lean | 4 +- .../Arithmetic/Waring/Compilation.lean | 6 +-- .../Circuit/Rational/EncodingBounds.lean | 6 +-- .../Computability/Circuit/Rational/Eval.lean | 6 +-- .../Circuit/Rational/Generator.lean | 2 +- .../Circuit/Rational/IntegralLift.lean | 2 +- .../Circuit/Rational/LaurentReduction.lean | 2 +- .../Circuit/Rational/MatrixEval.lean | 4 +- .../Circuit/Rational/QuantumMatrices.lean | 2 +- .../Circuit/Rational/QuantumSeries.lean | 2 +- .../Circuit/Rational/Runtime/Determinant.lean | 6 +-- .../Circuit/Rational/Runtime/Encode.lean | 6 +-- .../Circuit/Rational/Runtime/Lift.lean | 2 +- .../Circuit/Rational/Runtime/Lift/Defs.lean | 8 ++-- .../Circuit/Rational/SmallExpansion.lean | 2 +- .../Circuit/Rational/Wronskian.lean | 38 +++++++++---------- 18 files changed, 51 insertions(+), 51 deletions(-) diff --git a/Complexity/Computability/Circuit/Arithmetic/Power.lean b/Complexity/Computability/Circuit/Arithmetic/Power.lean index 4b8699dbf..fd6bb2236 100644 --- a/Complexity/Computability/Circuit/Arithmetic/Power.lean +++ b/Complexity/Computability/Circuit/Arithmetic/Power.lean @@ -119,7 +119,7 @@ private theorem binaryPowerCircuit_bit (one : C) (bit : Bool) (e : ℕ) (he : e @[simp] theorem binaryMultiplicationCount_one : binaryMultiplicationCount 1 = 0 := by simp [binaryMultiplicationCount] -private theorem binaryMultiplicationCount_bit (bit : Bool) (e : ℕ) (he : e ≠ 0) : +theorem binaryMultiplicationCount_bit (bit : Bool) (e : ℕ) (he : e ≠ 0) : binaryMultiplicationCount (Nat.bit bit e) = binaryMultiplicationCount e + 1 + bit.toNat := Nat.binaryRecFromOne_eq bit e he diff --git a/Complexity/Computability/Circuit/Arithmetic/VNP.lean b/Complexity/Computability/Circuit/Arithmetic/VNP.lean index ad57b7ece..85fd610bc 100644 --- a/Complexity/Computability/Circuit/Arithmetic/VNP.lean +++ b/Complexity/Computability/Circuit/Arithmetic/VNP.lean @@ -101,7 +101,7 @@ private theorem projection_booleanSum (ρ : Fin k → Fin n ⊕ K) (P : MvPolyno | right i => cases e i <;> simp [booleanAssignment, liftProjection] /-- A Boolean sum has no larger degree than the summed polynomial. -/ -private theorem totalDegree_booleanSum_le (P : MvPolynomial (Fin (n + m)) K) : +theorem totalDegree_booleanSum_le (P : MvPolynomial (Fin (n + m)) K) : (booleanSum m P).totalDegree ≤ P.totalDegree := totalDegree_finsetSum_le fun _ _ => totalDegree_projection_le _ _ diff --git a/Complexity/Computability/Circuit/Arithmetic/VP.lean b/Complexity/Computability/Circuit/Arithmetic/VP.lean index dca1f323b..cfc29a797 100644 --- a/Complexity/Computability/Circuit/Arithmetic/VP.lean +++ b/Complexity/Computability/Circuit/Arithmetic/VP.lean @@ -121,7 +121,7 @@ theorem Circuit.aeval_polynomial {R : Type*} [CommSemiring R] [Algebra K R] /-- Substituting polynomials for the variables of the polynomial computed by a circuit is evaluating the circuit at those polynomials. -/ -private theorem Circuit.aeval_polynomial_mvPolynomial {σ : Type*} +theorem Circuit.aeval_polynomial_mvPolynomial {σ : Type*} (c : Circuit (arithSignature K) n m) (x : Fin n → MvPolynomial σ K) (j : Fin m) : aeval x (c.polynomial j) = c.eval (arithInterpretationWith K C) x j := by @@ -325,7 +325,7 @@ theorem size_projectionCircuit_le (ρ : Fin m → Fin n ⊕ K) : (projectionCirc /-- Feeding the substitution of a projection to a circuit computes the projection of its polynomial. -/ -private theorem polynomial_comp_projectionCircuit (c : Circuit (arithSignature K) m p) +theorem polynomial_comp_projectionCircuit (c : Circuit (arithSignature K) m p) (ρ : Fin m → Fin n ⊕ K) (j : Fin p) : (c.comp (projectionCircuit ρ)).polynomial j = projection ρ (c.polynomial j) := by rw [projection, Circuit.aeval_polynomial_mvPolynomial, Circuit.polynomial, Circuit.eval_comp] diff --git a/Complexity/Computability/Circuit/Arithmetic/Waring/Compilation.lean b/Complexity/Computability/Circuit/Arithmetic/Waring/Compilation.lean index 526a8614d..ddd2655b1 100644 --- a/Complexity/Computability/Circuit/Arithmetic/Waring/Compilation.lean +++ b/Complexity/Computability/Circuit/Arithmetic/Waring/Compilation.lean @@ -79,7 +79,7 @@ theorem Term.eval_toCircuit [Semiring R] (zero one : C) (constant : C → R) rfl /-- Exact weighted term cost, including all coefficient and zero/one constants. -/ -private theorem Term.cost_program_toCircuit (zero one : C) (weight : ArithOp C → ℕ) (t : Term C d) : +theorem Term.cost_program_toCircuit (zero one : C) (weight : ArithOp C → ℕ) (t : Term C d) : (t.toCircuit zero one).program.cost weight = weight (.const zero) + (∑ i, (weight (.const (t.coefficients i)) + weight .mul + weight .add)) + @@ -94,13 +94,13 @@ private theorem Term.cost_program_toCircuit (zero one : C) (weight : ArithOp C def termMultiplicationCount (d : ℕ) : ℕ := d + binaryMultiplicationCount d + 1 /-- Exact term multiplication count, including the final scale multiplication at degree zero. -/ -private theorem Term.mulCost_toCircuit (zero one : C) (t : Term C d) : +theorem Term.mulCost_toCircuit (zero one : C) (t : Term C d) : (t.toCircuit zero one).program.cost ArithOp.mulCost = termMultiplicationCount d := by rw [Term.cost_program_toCircuit] by_cases hd : d = 0 <;> simp [ArithOp.mulCost, termMultiplicationCount, hd] /-- There is one linear-form addition per variable, including the initial addition to zero. -/ -private theorem Term.addCost_toCircuit (zero one : C) (t : Term C d) : +theorem Term.addCost_toCircuit (zero one : C) (t : Term C d) : (t.toCircuit zero one).program.cost ArithOp.addCost = d := by rw [Term.cost_program_toCircuit] simp [ArithOp.addCost] diff --git a/Complexity/Computability/Circuit/Rational/EncodingBounds.lean b/Complexity/Computability/Circuit/Rational/EncodingBounds.lean index 5d8dc3e72..d5da12626 100644 --- a/Complexity/Computability/Circuit/Rational/EncodingBounds.lean +++ b/Complexity/Computability/Circuit/Rational/EncodingBounds.lean @@ -67,12 +67,12 @@ private lemma encodeNat_le (a L : ℕ) (ha : a < 2 ^ L) : (encodeNat a).length exact Nat.add_le_add_right (Nat.mul_le_mul_left 2 ((Nat.digits_length_le_iff (by omega) a).mpr ha)) 1 -private lemma ratio_num_le (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).num.natAbs ≤ a.natAbs := by +lemma ratio_num_le (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).num.natAbs ≤ a.natAbs := by by_cases ha : a = 0 · simp [ha] · exact Int.natAbs_le_of_dvd_ne_zero (Rat.num_dvd a hb) ha -private lemma ratio_den_le (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).den ≤ b.natAbs := by +lemma ratio_den_le (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).den ≤ b.natAbs := by simpa only [Int.natAbs_natCast] using Int.natAbs_le_of_dvd_ne_zero (Rat.den_dvd a b) hb private lemma encodeRat_ratio_le (a b : ℤ) (hb : b ≠ 0) (L : ℕ) @@ -83,7 +83,7 @@ private lemma encodeRat_ratio_le (a b : ℤ) (hb : b ≠ 0) (L : ℕ) simp only [encodeRat, List.length_append, List.length_singleton] omega -private lemma determinant_bound {d : ℕ} (A : Matrix (Fin d) (Fin d) ℤ) (B : ℕ) +lemma determinant_bound {d : ℕ} (A : Matrix (Fin d) (Fin d) ℤ) (B : ℕ) (hA : ∀ i j, |A i j| ≤ B) : |A.det| ≤ (d.factorial : ℤ) * (B : ℤ) ^ d := by have h := Matrix.det_le (abv := AbsoluteValue.abs) (x := (B : ℤ)) (A := A) (by simpa using hA) simpa only [AbsoluteValue.abs_apply, nsmul_eq_mul, Fintype.card_fin] using h diff --git a/Complexity/Computability/Circuit/Rational/Eval.lean b/Complexity/Computability/Circuit/Rational/Eval.lean index 9ea8da563..c23ab3597 100644 --- a/Complexity/Computability/Circuit/Rational/Eval.lean +++ b/Complexity/Computability/Circuit/Rational/Eval.lean @@ -152,14 +152,14 @@ abbrev matMul {l m n : Type*} [Fintype m] (A : Matrix l m R) (B : Matrix m n R) Matrix l n R := A * B /-- An upper unitriangular block matrix is invertible. -/ -private theorem upper_unit (B : Matrix ι κ R) : +theorem upper_unit (B : Matrix ι κ R) : IsUnit (fromBlocks (1 : Matrix ι ι R) B 0 (1 : Matrix κ κ R)) := by apply isUnit_iff_exists.mpr refine ⟨fromBlocks 1 (-B) 0 1, ?_, ?_⟩ <;> simp [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul] /-- A lower unitriangular block matrix is invertible. -/ -private theorem lower_unit (C : Matrix κ ι R) : +theorem lower_unit (C : Matrix κ ι R) : IsUnit (fromBlocks (1 : Matrix ι ι R) 0 C (1 : Matrix κ κ R)) := by apply isUnit_iff_exists.mpr refine ⟨fromBlocks 1 0 (-C) 1, ?_, ?_⟩ <;> @@ -201,7 +201,7 @@ theorem diag_unit_iff (A : Matrix ι ι R) (D : Matrix κ κ R) : simp [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul] /-- The Schur factorization of a block matrix with a zero corner and an invertible corner. -/ -private theorem schur_factor (A A' : Matrix ι ι R) (B : Matrix ι κ R) (C : Matrix κ ι R) +theorem schur_factor (A A' : Matrix ι ι R) (B : Matrix ι κ R) (C : Matrix κ ι R) (hAA' : A * A' = 1) (hA'A : A' * A = 1) : fromBlocks A B C 0 = fromBlocks 1 0 (C * A') 1 * fromBlocks A 0 0 (-C * A' * B) * diff --git a/Complexity/Computability/Circuit/Rational/Generator.lean b/Complexity/Computability/Circuit/Rational/Generator.lean index 2aa589731..fcc3d9c9c 100644 --- a/Complexity/Computability/Circuit/Rational/Generator.lean +++ b/Complexity/Computability/Circuit/Rational/Generator.lean @@ -242,7 +242,7 @@ private lemma condition_degree {n s N e : ℕ} (hs : 1 ≤ s) (f : Formula n) (h gcongr exact ((Formula.certificate_bounds f s hs hf).2 h hh).2) -private lemma integer_grid {K : Type*} [Field K] [CharZero K] (P : List (MvPolynomial (Fin 3) K)) +lemma integer_grid {K : Type*} [Field K] [CharZero K] (P : List (MvPolynomial (Fin 3) K)) (hP : ∀ p ∈ P, p ≠ 0) (d H : ℕ) (hd : ∀ p ∈ P, p.totalDegree ≤ d) (hH : P.length * d < H) : ∃ x : Fin 3 → Fin H, ∀ p ∈ P, eval (fun i => (((x i).val + 1 : ℕ) : K)) p ≠ 0 := by diff --git a/Complexity/Computability/Circuit/Rational/IntegralLift.lean b/Complexity/Computability/Circuit/Rational/IntegralLift.lean index a5d25483d..ab5b4aa3b 100644 --- a/Complexity/Computability/Circuit/Rational/IntegralLift.lean +++ b/Complexity/Computability/Circuit/Rational/IntegralLift.lean @@ -396,7 +396,7 @@ lemma U_bound (n N e H : ℕ) (x : Fin 3 → ℕ) (hH : 1 ≤ H) (hx : ∀ l, x CyclotomicRing.dimension e + 2 * CyclotomicRing.dimension e by omega, pow_add] ring -private lemma scaled_normalization {d : ℕ} (A B : Mat d) (hA : A.det ≠ 0) (c : ℚ) (hc : c ≠ 0) : +lemma scaled_normalization {d : ℕ} (A B : Mat d) (hA : A.det ≠ 0) (c : ℚ) (hc : c ≠ 0) : (c • A)⁻¹ * (c • B) = A⁻¹ * B := by let : Invertible c := invertibleOfNonzero hc have hi : (c • A)⁻¹ = c⁻¹ • A⁻¹ := by diff --git a/Complexity/Computability/Circuit/Rational/LaurentReduction.lean b/Complexity/Computability/Circuit/Rational/LaurentReduction.lean index fbd35750c..a7667caf2 100644 --- a/Complexity/Computability/Circuit/Rational/LaurentReduction.lean +++ b/Complexity/Computability/Circuit/Rational/LaurentReduction.lean @@ -488,7 +488,7 @@ private theorem reduction_weighted_supported {ι : Type*} [Finite ι] exact he ▸ weighted_high_reduction_zero w A (u • x) hnI' hd u⁻¹ (inv_ne_zero hu) (he.symm ▸ hyI) -private lemma exists_independent_subfamily {V : Type*} [AddCommGroup V] [Module K V] +lemma exists_independent_subfamily {V : Type*} [AddCommGroup V] [Module K V] {h : ℕ} (v : Fin h → V) : ∃ (k : ℕ) (a : Fin k → Fin h), Function.Injective a ∧ Submodule.span K (Set.range (v ∘ a)) = Submodule.span K (Set.range v) ∧ diff --git a/Complexity/Computability/Circuit/Rational/MatrixEval.lean b/Complexity/Computability/Circuit/Rational/MatrixEval.lean index 37d89b660..2323da355 100644 --- a/Complexity/Computability/Circuit/Rational/MatrixEval.lean +++ b/Complexity/Computability/Circuit/Rational/MatrixEval.lean @@ -50,11 +50,11 @@ namespace Cslib.Circuits.Rational open Rational.Formula Rational.Output -private theorem matrix_inverse_left {d : ℕ} (a : Mat d) (ha : a.det ≠ 0) : +theorem matrix_inverse_left {d : ℕ} (a : Mat d) (ha : a.det ≠ 0) : a * (a.det⁻¹ • a.adjugate) = 1 := by rw [Matrix.mul_smul, Matrix.mul_adjugate, smul_smul, inv_mul_cancel₀ ha, one_smul] -private theorem matrix_inverse_right {d : ℕ} (a : Mat d) (ha : a.det ≠ 0) : +theorem matrix_inverse_right {d : ℕ} (a : Mat d) (ha : a.det ≠ 0) : (a.det⁻¹ • a.adjugate) * a = 1 := by rw [Matrix.smul_mul, Matrix.adjugate_mul, smul_smul, inv_mul_cancel₀ ha, one_smul] diff --git a/Complexity/Computability/Circuit/Rational/QuantumMatrices.lean b/Complexity/Computability/Circuit/Rational/QuantumMatrices.lean index 5589433f7..6251de7a0 100644 --- a/Complexity/Computability/Circuit/Rational/QuantumMatrices.lean +++ b/Complexity/Computability/Circuit/Rational/QuantumMatrices.lean @@ -57,7 +57,7 @@ open scoped BigOperators noncomputable section variable {Γ R : Type*} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] -private lemma coeff_mul_support_superset (x y : HahnSeries Γ R) (a : Γ) +lemma coeff_mul_support_superset (x y : HahnSeries Γ R) (a : Γ) (s t : Set Γ) (hs : s.IsPWO) (ht : t.IsPWO) (hxs : x.support ⊆ s) (hyt : y.support ⊆ t) : (x * y).coeff a = ∑ ij ∈ Finset.antidiagonal hs ht a, diff --git a/Complexity/Computability/Circuit/Rational/QuantumSeries.lean b/Complexity/Computability/Circuit/Rational/QuantumSeries.lean index c2c780e72..223f8def0 100644 --- a/Complexity/Computability/Circuit/Rational/QuantumSeries.lean +++ b/Complexity/Computability/Circuit/Rational/QuantumSeries.lean @@ -144,7 +144,7 @@ open HahnSeries HahnSeries.SummableFamily Finset Function noncomputable section variable {Γ R : Type*} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] -private theorem power_finite_co_support {x : R⟦Γ⟧} (hx : 0 < x.orderTop) (g : Γ) : +theorem power_finite_co_support {x : R⟦Γ⟧} (hx : 0 < x.orderTop) (g : Γ) : Set.Finite {a | ((fun n ↦ x ^ n) a).coeff g ≠ 0} := by have hpwo : Set.IsPWO (⋃ n, support (x ^ n)) := isPWO_iUnion_support_powers (zero_le_orderTop_iff.mp <| le_of_lt hx) diff --git a/Complexity/Computability/Circuit/Rational/Runtime/Determinant.lean b/Complexity/Computability/Circuit/Rational/Runtime/Determinant.lean index 0b5c322fa..1c6df04b9 100644 --- a/Complexity/Computability/Circuit/Rational/Runtime/Determinant.lean +++ b/Complexity/Computability/Circuit/Rational/Runtime/Determinant.lean @@ -236,7 +236,7 @@ private lemma sum_map_drop_range (d lo : ℕ) (f : ℕ → ℤ) : rw [BirdDet.sumFrom_stop d lo f hlo, List.drop_eq_nil_of_le (by simpa using hlo)] rfl -private lemma sum_map_drop_range_fin {d : ℕ} (i : Fin d) (f : ℕ → ℤ) : +lemma sum_map_drop_range_fin {d : ℕ} (i : Fin d) (f : ℕ → ℤ) : (((List.range d).drop (i.val + 1)).map f).sum = ∑ k ∈ Finset.Ioi i, f k.val := by rw [sum_map_drop_range, DeterminantAlgorithm.sumFrom_fin_tail] @@ -300,7 +300,7 @@ theorem detRows_rowsOf_denote {d : ℕ} (A : DeterminantAlgorithm.Table d) : /-! ### Size bounds -/ -private lemma natAbs_sum_le {l : List ℤ} {C : ℕ} (h : ∀ x ∈ l, x.natAbs ≤ C) : +lemma natAbs_sum_le {l : List ℤ} {C : ℕ} (h : ∀ x ∈ l, x.natAbs ≤ C) : l.sum.natAbs ≤ l.length * C := by induction l with | nil => simp @@ -312,7 +312,7 @@ private lemma natAbs_sum_le {l : List ℤ} {C : ℕ} (h : ∀ x ∈ l, x.natAbs _ = (l.length + 1) * C := by ring /-- Every prefix sum of a list is bounded by its length times a bound on its entries. -/ -private lemma natAbs_take_sum_le {l : List ℤ} {C : ℕ} (h : ∀ x ∈ l, x.natAbs ≤ C) (m : ℕ) : +lemma natAbs_take_sum_le {l : List ℤ} {C : ℕ} (h : ∀ x ∈ l, x.natAbs ≤ C) (m : ℕ) : (l.take m).sum.natAbs ≤ l.length * C := (natAbs_sum_le fun x hx => h x (List.mem_of_mem_take hx)).trans (Nat.mul_le_mul_right _ (List.length_take_le' _ _)) diff --git a/Complexity/Computability/Circuit/Rational/Runtime/Encode.lean b/Complexity/Computability/Circuit/Rational/Runtime/Encode.lean index 29a06d1a4..f8d61e22f 100644 --- a/Complexity/Computability/Circuit/Rational/Runtime/Encode.lean +++ b/Complexity/Computability/Circuit/Rational/Runtime/Encode.lean @@ -125,7 +125,7 @@ theorem divInt_sign (a b : ℤ) (hb : b ≠ 0) : simp [not_lt_of_gt hpa, not_lt_of_gt hpb, not_lt_of_ge hp.le] /-- Reduced numerator magnitude of `Rat.divInt a b` for arbitrary integers `a, b`. -/ -private theorem divInt_num_abs_eq (a b : ℤ) : +theorem divInt_num_abs_eq (a b : ℤ) : (Rat.divInt a b).num.natAbs = if b = 0 then 0 else a.natAbs / Nat.gcd a.natAbs b.natAbs := by by_cases hb : b = 0 @@ -133,7 +133,7 @@ private theorem divInt_num_abs_eq (a b : ℤ) : · simp [hb, divInt_num_abs a b hb] /-- Reduced denominator of `Rat.divInt a b` for arbitrary integers `a, b`. -/ -private theorem divInt_den_eq (a b : ℤ) : +theorem divInt_den_eq (a b : ℤ) : (Rat.divInt a b).den = if b = 0 then 1 else b.natAbs / Nat.gcd a.natAbs b.natAbs := by by_cases hb : b = 0 @@ -141,7 +141,7 @@ private theorem divInt_den_eq (a b : ℤ) : · simp [hb, divInt_den a b hb] /-- Sign bit of `Rat.divInt a b` for arbitrary integers `a, b`. -/ -private theorem divInt_sign_eq (a b : ℤ) : +theorem divInt_sign_eq (a b : ℤ) : decide ((Rat.divInt a b).num < 0) = if a = 0 then false else if b = 0 then false else (decide (a < 0) ^^ decide (b < 0)) := by by_cases hb : b = 0 diff --git a/Complexity/Computability/Circuit/Rational/Runtime/Lift.lean b/Complexity/Computability/Circuit/Rational/Runtime/Lift.lean index fc8df33e5..468b2d0cc 100644 --- a/Complexity/Computability/Circuit/Rational/Runtime/Lift.lean +++ b/Complexity/Computability/Circuit/Rational/Runtime/Lift.lean @@ -66,7 +66,7 @@ namespace Rational /-! ### Magnitude bounds -/ -private lemma natAbs_pow_le {z : ℤ} {H : ℕ} (hH : 1 ≤ H) (hz : z.natAbs ≤ H) {q M : ℕ} +lemma natAbs_pow_le {z : ℤ} {H : ℕ} (hH : 1 ≤ H) (hz : z.natAbs ≤ H) {q M : ℕ} (hq : q ≤ M) : (z ^ q).natAbs ≤ H ^ M := by rw [Int.natAbs_pow] diff --git a/Complexity/Computability/Circuit/Rational/Runtime/Lift/Defs.lean b/Complexity/Computability/Circuit/Rational/Runtime/Lift/Defs.lean index 239d2fc69..194bc5d81 100644 --- a/Complexity/Computability/Circuit/Rational/Runtime/Lift/Defs.lean +++ b/Complexity/Computability/Circuit/Rational/Runtime/Lift/Defs.lean @@ -77,7 +77,7 @@ open Polynomial /-! ### Index bridges -/ -private lemma val_finEquiv {m : ℕ} [NeZero m] (i : Fin m) : (ZMod.finEquiv m i).val = i.val := by +lemma val_finEquiv {m : ℕ} [NeZero m] (i : Fin m) : (ZMod.finEquiv m i).val = i.val := by cases m with | zero => exact (NeZero.ne 0 rfl).elim | succ m => rfl @@ -88,13 +88,13 @@ lemma val_finEquiv_symm {m : ℕ} [NeZero m] (z : ZMod m) : rw [← val_finEquiv, RingEquiv.apply_symm_apply] /-- A sum over `List.range m` is a sum over `Fin m`. -/ -private lemma sum_range_eq_sum_fin {A : Type*} [AddCommMonoid A] (m : ℕ) (f : ℕ → A) : +lemma sum_range_eq_sum_fin {A : Type*} [AddCommMonoid A] (m : ℕ) (f : ℕ → A) : ((List.range m).map f).sum = ∑ i : Fin m, f i := by rw [← List.map_coe_finRange_eq_range, List.map_map, ← List.ofFn_eq_map, List.sum_ofFn] rfl /-- A sum over `List.range m` is a sum over the residues modulo `m`. -/ -private lemma sum_range_eq_sum_zmod {A : Type*} [AddCommMonoid A] (m : ℕ) [NeZero m] (f : ℕ → A) : +lemma sum_range_eq_sum_zmod {A : Type*} [AddCommMonoid A] (m : ℕ) [NeZero m] (f : ℕ → A) : ((List.range m).map f).sum = ∑ z : ZMod m, f z.val := by rw [sum_range_eq_sum_fin] exact Fintype.sum_equiv (ZMod.finEquiv m).toEquiv _ _ fun i => by @@ -102,7 +102,7 @@ private lemma sum_range_eq_sum_zmod {A : Type*} [AddCommMonoid A] (m : ℕ) [NeZ rw [val_finEquiv] /-- Residue subtraction on values, without truncated subtraction below zero. -/ -private lemma val_sub_eq_mod {m : ℕ} [NeZero m] (u v : ZMod m) : +lemma val_sub_eq_mod {m : ℕ} [NeZero m] (u v : ZMod m) : (u - v).val = (u.val + m - v.val) % m := by have hv := v.val_lt rw [← ZMod.val_natCast, Nat.cast_sub (by omega), Nat.cast_add, ZMod.natCast_self, diff --git a/Complexity/Computability/Circuit/Rational/SmallExpansion.lean b/Complexity/Computability/Circuit/Rational/SmallExpansion.lean index fce309c65..243fa80e3 100644 --- a/Complexity/Computability/Circuit/Rational/SmallExpansion.lean +++ b/Complexity/Computability/Circuit/Rational/SmallExpansion.lean @@ -280,7 +280,7 @@ theorem order_reversal_sum (M : ℕ) (a : K) Fintype.card_fin, smul_eq_mul] omega -private lemma sum_fin_val_le_square (h : ℕ) : (∑ j : Fin h, j.val) ≤ h * h := by +lemma sum_fin_val_le_square (h : ℕ) : (∑ j : Fin h, j.val) ≤ h * h := by calc _ ≤ ∑ _j : Fin h, h := Finset.sum_le_sum fun j _ => Nat.le_of_lt j.isLt _ = h * h := by simp diff --git a/Complexity/Computability/Circuit/Rational/Wronskian.lean b/Complexity/Computability/Circuit/Rational/Wronskian.lean index 084f5481a..83a279576 100644 --- a/Complexity/Computability/Circuit/Rational/Wronskian.lean +++ b/Complexity/Computability/Circuit/Rational/Wronskian.lean @@ -67,7 +67,7 @@ def wronskianFamily {K : Type*} [CommRing K] {h : ℕ} (f : Fin h → K[X]) : K[ /-- Factoring prescribed powers from the columns keeps track of the first possible coefficient of a determinant. -/ -private lemma det_factor_column_orders {K ι : Type*} [CommRing K] +lemma det_factor_column_orders {K ι : Type*} [CommRing K] [Fintype ι] [DecidableEq ι] (A : Matrix ι ι K[X]) (d : ι → ℕ) (hd : ∀ i j, X ^ d j ∣ A i j) : ∃ B : Matrix ι ι K[X], @@ -86,7 +86,7 @@ private lemma det_factor_column_orders {K ι : Type*} [CommRing K] rw [hB i j, coeff_X_pow_mul'] simp -private lemma coeff_scaled_derivative_at {K : Type*} [CommRing K] +lemma coeff_scaled_derivative_at {K : Type*} [CommRing K] (f : K[X]) (r d : ℕ) : (X ^ r * derivative^[r] f).coeff d = (d.descFactorial r : K) * f.coeff d := by @@ -96,7 +96,7 @@ private lemma coeff_scaled_derivative_at {K : Type*} [CommRing K] · rw [coeff_X_pow_mul', ite_eq_right hr, Nat.descFactorial_eq_zero_iff_lt.mpr (Nat.lt_of_not_ge hr), Nat.cast_zero, zero_mul] -private lemma scaled_derivative_order {K : Type*} [CommRing K] +lemma scaled_derivative_order {K : Type*} [CommRing K] (f : K[X]) (r : ℕ) : X ^ f.natTrailingDegree ∣ X ^ r * derivative^[r] f := by apply X_pow_dvd_iff.mpr intro a ha @@ -172,7 +172,7 @@ lemma wronskian_order_of_distinct_orders {K : Type*} [Field K] [CharZero K] /-- Polynomial row reduction, derived rather than assumed: every bounded-degree subspace has a basis with distinct largest degrees. -/ -private lemma exists_degree_echelon_family {K : Type*} [Field K] +lemma exists_degree_echelon_family {K : Type*} [Field K] (d : ℕ) (V : Submodule K K[X]) (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) : ∃ (h : ℕ) (f : Fin h → K[X]), LinearIndependent K f ∧ @@ -273,7 +273,7 @@ private def reflectLinearEquiv (K : Type*) [Field K] (N : ℕ) : K[X] ≃ₗ[K] intro c f simpa only [smul_eq_C_mul, RingHom.id_apply] using reflect_C_mul f c N -private lemma order_reflect {K : Type*} [Field K] (N : ℕ) (f : K[X]) +lemma order_reflect {K : Type*} [Field K] (N : ℕ) (f : K[X]) (hf : f ≠ 0) (hd : f.natDegree ≤ N) : (reflect N f).natTrailingDegree = N - f.natDegree := by apply le_antisymm @@ -285,7 +285,7 @@ private lemma order_reflect {K : Type*} [Field K] (N : ℕ) (f : K[X]) rw [coeff_reflect, revAt_le (by omega)] exact coeff_eq_zero_of_natDegree_lt (by omega) -private lemma exists_order_echelon_family {K : Type*} [Field K] +lemma exists_order_echelon_family {K : Type*} [Field K] (d : ℕ) (V : Submodule K K[X]) (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) : ∃ (h : ℕ) (f : Fin h → K[X]), LinearIndependent K f ∧ @@ -326,7 +326,7 @@ private lemma exists_order_echelon_family {K : Type*} [Field K] change (g i).natDegree = (g j).natDegree omega -private lemma wronskian_linearCombination {K : Type*} [CommRing K] {h : ℕ} +lemma wronskian_linearCombination {K : Type*} [CommRing K] {h : ℕ} (f : Fin h → K[X]) (A : Matrix (Fin h) (Fin h) K) : wronskianFamily (fun j => ∑ i, A i j • f i) = wronskianFamily f * C A.det := by have he : (Matrix.of fun r j : Fin h => @@ -347,14 +347,14 @@ private lemma wronskian_linearCombination {K : Type*} [CommRing K] {h : ℕ} congr 1 exact (C.map_det A).symm -private lemma basis_toMatrix_det_ne_zero {K M : Type*} [Field K] [AddCommGroup M] +lemma basis_toMatrix_det_ne_zero {K M : Type*} [Field K] [AddCommGroup M] [Module K M] {h : ℕ} (b b' : Basis (Fin h) K M) : (b.toMatrix b').det ≠ 0 := by have hh := congrArg Matrix.det (b.toMatrix_mul_toMatrix_flip b') rw [Matrix.det_mul, Matrix.det_one] at hh exact left_ne_zero_of_mul_eq_one hh -private lemma wronskian_basis_change {K : Type*} [Field K] {h : ℕ} +lemma wronskian_basis_change {K : Type*} [Field K] {h : ℕ} {V : Submodule K K[X]} (b b' : Basis (Fin h) K V) : wronskianFamily (fun j => (b' j : K[X])) = wronskianFamily (fun j => (b j : K[X])) * C (b.toMatrix b').det := by @@ -365,7 +365,7 @@ private lemma wronskian_basis_change {K : Type*} [Field K] {h : ℕ} simpa only [Submodule.coe_sum, Submodule.coe_smul, Basis.toMatrix_apply] using hh.symm rw [he, wronskian_linearCombination] -private lemma exists_order_echelon_basis {K : Type*} [Field K] +lemma exists_order_echelon_basis {K : Type*} [Field K] (d : ℕ) (V : Submodule K K[X]) {h : ℕ} (b : Basis (Fin h) K V) (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) : ∃ b' : Basis (Fin h) K V, @@ -383,7 +383,7 @@ private lemma exists_order_echelon_basis {K : Type*} [Field K] subst k exact ⟨b', by simpa only [hb'] using hord⟩ -private lemma wronskian_basis_ne_zero {K : Type*} [Field K] [CharZero K] +lemma wronskian_basis_ne_zero {K : Type*} [Field K] [CharZero K] (d : ℕ) {V : Submodule K K[X]} {h : ℕ} (b : Basis (Fin h) K V) (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) : wronskianFamily (fun j => (b j : K[X])) ≠ 0 := by @@ -395,12 +395,12 @@ private lemma wronskian_basis_ne_zero {K : Type*} [Field K] [CharZero K] rw [wronskian_basis_change b b'] at hn exact (mul_ne_zero_iff.mp hn).1 -private lemma derivative_taylor {K : Type*} [CommRing K] (a : K) (f : K[X]) : +lemma derivative_taylor {K : Type*} [CommRing K] (a : K) (f : K[X]) : derivative (taylor a f) = taylor a (derivative f) := by simp only [taylor_apply, derivative_comp, derivative_add, derivative_X, derivative_C, add_zero, one_mul] -private lemma iterate_derivative_taylor {K : Type*} [CommRing K] (a : K) +lemma iterate_derivative_taylor {K : Type*} [CommRing K] (a : K) (f : K[X]) (r : ℕ) : derivative^[r] (taylor a f) = taylor a (derivative^[r] f) := by induction r with @@ -408,7 +408,7 @@ private lemma iterate_derivative_taylor {K : Type*} [CommRing K] (a : K) | succ r ih => rw [Function.iterate_succ_apply', ih, derivative_taylor, Function.iterate_succ_apply'] -private lemma wronskian_taylor {K : Type*} [CommRing K] {h : ℕ} +lemma wronskian_taylor {K : Type*} [CommRing K] {h : ℕ} (a : K) (f : Fin h → K[X]) : wronskianFamily (fun j => taylor a (f j)) = taylor a (wronskianFamily f) := by unfold wronskianFamily @@ -420,7 +420,7 @@ private lemma wronskian_taylor {K : Type*} [CommRing K] {h : ℕ} rw [he] exact ((taylorEquiv a).toRingHom.map_det _).symm -private lemma natDegree_wronskian_le {K : Type*} [CommRing K] {h : ℕ} +lemma natDegree_wronskian_le {K : Type*} [CommRing K] {h : ℕ} (f : Fin h → K[X]) (D : ℕ) (hd : ∀ j, (f j).natDegree ≤ D) : (wronskianFamily f).natDegree ≤ h * D := by unfold wronskianFamily @@ -435,7 +435,7 @@ private lemma natDegree_wronskian_le {K : Type*} [CommRing K] {h : ℕ} (natDegree_iterate_derivative _ _).trans ((Nat.sub_le _ _).trans (hd j)) _ = h * D := by simp -private lemma sum_rootMultiplicity_le_natDegree {K : Type*} [Field K] +lemma sum_rootMultiplicity_le_natDegree {K : Type*} [Field K] (f : K[X]) (s : Finset K) : ∑ a ∈ s, f.rootMultiplicity a ≤ f.natDegree := by classical @@ -447,7 +447,7 @@ private lemma sum_rootMultiplicity_le_natDegree {K : Type*} [Field K] Finset.mem_union_right _ (Multiset.mem_toFinset.mpr ha)) _ ≤ f.natDegree := card_roots' f -private lemma wronskian_order_at {K : Type*} [Field K] [CharZero K] {h : ℕ} +lemma wronskian_order_at {K : Type*} [Field K] [CharZero K] {h : ℕ} (a : K) (f : Fin h → K[X]) (hf : ∀ j, f j ≠ 0) (hd : Function.Injective (fun j => (f j).rootMultiplicity a)) : (wronskianFamily f).rootMultiplicity a + (∑ i : Fin h, i.val) = @@ -461,7 +461,7 @@ private lemma wronskian_order_at {K : Type*} [Field K] [CharZero K] {h : ℕ} rw [wronskian_taylor] at hh simpa only [rootMultiplicity_eq_natTrailingDegree, ← taylor_apply] using hh -private lemma wronskian_basis_rootMultiplicity {K : Type*} [Field K] [CharZero K] +lemma wronskian_basis_rootMultiplicity {K : Type*} [Field K] [CharZero K] (d : ℕ) {V : Submodule K K[X]} {h : ℕ} (b b' : Basis (Fin h) K V) (a : K) (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) : @@ -533,7 +533,7 @@ lemma exists_echelon_basis_at {K : Type*} [Field K] /-- Distinct leading orders make vanishing conditions triangular; no linear combination can cancel its first nonzero echelon term. -/ -private lemma low_coefficients_force_zero {K : Type*} [Field K] {h : ℕ} +lemma low_coefficients_force_zero {K : Type*} [Field K] {h : ℕ} (f : Fin h → K[X]) (hf : ∀ j, f j ≠ 0) (hd : Function.Injective (fun j => (f j).natTrailingDegree)) (c : Fin h → K) (r : ℕ)