From 86669f9f28a395f1588497fd945fae2edbf772a0 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 21:02:46 -0400 Subject: [PATCH] refactor(Foundations,Probability,Languages): make 41 API and general declarations public again (#926) Earlier privatization passes (mostly #628) 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 --- Complexity/Foundations/BooleanAnalysis/Bernoulli.lean | 2 +- Complexity/Foundations/BooleanAnalysis/Fibers.lean | 4 ++-- .../Foundations/BooleanAnalysis/HarmonicTransform.lean | 8 ++++---- .../Foundations/BooleanAnalysis/Hypercontractivity.lean | 2 +- .../BooleanAnalysis/Hypercontractivity/Derivative.lean | 2 +- Complexity/Foundations/BooleanAnalysis/Hypercube.lean | 2 +- .../Foundations/BooleanAnalysis/KahnKalaiLinial.lean | 2 +- Complexity/Foundations/Combinatorics/AffineDisperser.lean | 2 +- .../Combinatorics/AffineDisperser/Threshold.lean | 4 ++-- Complexity/Foundations/Combinatorics/CentralBinomial.lean | 2 +- Complexity/Foundations/Combinatorics/Expander/Walk.lean | 2 +- .../Foundations/Combinatorics/FunctionalGraph/Cycle.lean | 2 +- .../Combinatorics/FunctionalGraph/ForestIntervals.lean | 4 ++-- Complexity/Foundations/Combinatorics/MajorityTree.lean | 2 +- .../Data/BitString/PartialAssignment/Counting.lean | 8 ++++---- Complexity/Foundations/Data/BitString/ShortWords.lean | 2 +- Complexity/Foundations/Data/Code/HammingBound.lean | 2 +- .../Foundations/Data/Nat/Bitwise/Multiplication.lean | 4 ++-- Complexity/Foundations/Data/StackTape.lean | 2 +- .../Foundations/FieldTheory/Finite/BinaryField.lean | 2 +- .../FieldTheory/Finite/LinearizedPolynomial.lean | 2 +- Complexity/Foundations/LinearAlgebra/Matrix/CutRank.lean | 2 +- .../Foundations/LinearAlgebra/Matrix/SubmatrixRobust.lean | 2 +- Complexity/Languages/Probabilistic/LinearHash.lean | 2 +- Complexity/Probability/BitString/LinearHash.lean | 2 +- Complexity/Probability/Conditioning.lean | 2 +- Complexity/Probability/HashIsolation.lean | 2 +- Complexity/Probability/Shearer.lean | 4 ++-- Complexity/Probability/SmallBias/Powering.lean | 4 ++-- 29 files changed, 41 insertions(+), 41 deletions(-) diff --git a/Complexity/Foundations/BooleanAnalysis/Bernoulli.lean b/Complexity/Foundations/BooleanAnalysis/Bernoulli.lean index 0ea70d5e9..854b76520 100644 --- a/Complexity/Foundations/BooleanAnalysis/Bernoulli.lean +++ b/Complexity/Foundations/BooleanAnalysis/Bernoulli.lean @@ -149,7 +149,7 @@ theorem bernoulliAverage_sumElim {ι κ : Type*} [Fintype ι] [Fintype κ] rw [← Sum.elim_comp_inl_inr P] rfl -private theorem bernoulliWeight_split {ι : Type*} [Fintype ι] (p : ℝ) (s x : ι → Bool) : +theorem bernoulliWeight_split {ι : Type*} [Fintype ι] (p : ℝ) (s x : ι → Bool) : bernoulliWeight p x = bernoulliWeight p (fun i : {i // s i = true} => x i) * bernoulliWeight p (fun i : {i // s i ≠ true} => x i) := (Fintype.prod_subtype_mul_prod_subtype (fun i => s i = true) diff --git a/Complexity/Foundations/BooleanAnalysis/Fibers.lean b/Complexity/Foundations/BooleanAnalysis/Fibers.lean index b407b1b03..4c17ae152 100644 --- a/Complexity/Foundations/BooleanAnalysis/Fibers.lean +++ b/Complexity/Foundations/BooleanAnalysis/Fibers.lean @@ -493,7 +493,7 @@ end Projection /-! ### Korten's entropy lemma -/ /-- The log-sum inequality, from Jensen's inequality for `x log x`. -/ -private theorem sum_mul_log_ge {β : Type*} [Fintype β] [Nonempty β] {m : β → ℝ} +theorem sum_mul_log_ge {β : Type*} [Fintype β] [Nonempty β] {m : β → ℝ} (hm : ∀ b, 0 ≤ m b) : (∑ b, m b) * Real.log ((∑ b, m b) / Fintype.card β) ≤ ∑ b, m b * Real.log (m b) := by have hc : (0 : ℝ) < Fintype.card β := by exact_mod_cast Fintype.card_pos @@ -506,7 +506,7 @@ private theorem sum_mul_log_ge {β : Type*} [Fintype β] [Nonempty β] {m : β /-- The logarithm of the size of the fiber of a uniform point of `X` under a map to `β` is on average at least `log |X| - log |β|`. -/ -private theorem expect_log_card_fiber {α β : Type*} [Fintype β] [Nonempty β] [DecidableEq β] +theorem expect_log_card_fiber {α β : Type*} [Fintype β] [Nonempty β] [DecidableEq β] (X : Finset α) (hX : X.Nonempty) (g : α → β) : Real.log X.card - Real.log (Fintype.card β) ≤ 𝔼 x ∈ X, Real.log (X.filter (fun y => g y = g x)).card := by diff --git a/Complexity/Foundations/BooleanAnalysis/HarmonicTransform.lean b/Complexity/Foundations/BooleanAnalysis/HarmonicTransform.lean index 5b630fd62..72dff3d98 100644 --- a/Complexity/Foundations/BooleanAnalysis/HarmonicTransform.lean +++ b/Complexity/Foundations/BooleanAnalysis/HarmonicTransform.lean @@ -183,7 +183,7 @@ private theorem resample_cons {n : ℕ} (s y x : Fin n → Bool) (a b c : Bool) funext i refine Fin.cases ?_ (fun j => ?_) i <;> simp [resample, Set.piecewise] -private theorem projectionAverage_cons_false {n : ℕ} +theorem projectionAverage_cons_false {n : ℕ} (f : (Fin (n + 1) → Bool) → ℝ) (selected x : Fin n → Bool) (b : Bool) : projectionAverage f (Fin.cons false selected) (Fin.cons b x) = projectionAverage (fun x => (f (Fin.cons false x) + f (Fin.cons true x)) / 2) @@ -193,7 +193,7 @@ private theorem projectionAverage_cons_false {n : ℕ} simp only [resample_cons, Bool.false_eq_true, ite_false] rw [← expect_div, expect_add_distrib] -private theorem projectionAverage_cons_true {n : ℕ} +theorem projectionAverage_cons_true {n : ℕ} (f : (Fin (n + 1) → Bool) → ℝ) (selected x : Fin n → Bool) (b : Bool) : projectionAverage f (Fin.cons true selected) (Fin.cons b x) = projectionAverage (fun x => f (Fin.cons b x)) selected x := by @@ -202,7 +202,7 @@ private theorem projectionAverage_cons_true {n : ℕ} simp only [resample_cons, ite_true] ring -private theorem harmonicTransform_cons_false {n : ℕ} +theorem harmonicTransform_cons_false {n : ℕ} (f : (Fin (n + 1) → Bool) → ℝ) (selected : Fin n → Bool) : harmonicTransform f (Fin.cons false selected) = harmonicTransform @@ -214,7 +214,7 @@ private theorem harmonicTransform_cons_false {n : ℕ} simp_rw [projectionAverage_cons_false] simp [harmonicMean, Fintype.expect_prod_type] -private theorem harmonicTransform_cons_true {n : ℕ} +theorem harmonicTransform_cons_true {n : ℕ} {f : (Fin (n + 1) → Bool) → ℝ} (hf : ∀ x, 0 ≤ f x) (selected : Fin n → Bool) : harmonicTransform f (Fin.cons true selected) = 2 * harmonicTransform (fun x => f (Fin.cons false x)) selected * diff --git a/Complexity/Foundations/BooleanAnalysis/Hypercontractivity.lean b/Complexity/Foundations/BooleanAnalysis/Hypercontractivity.lean index 13b48b2e9..caa0d02a9 100644 --- a/Complexity/Foundations/BooleanAnalysis/Hypercontractivity.lean +++ b/Complexity/Foundations/BooleanAnalysis/Hypercontractivity.lean @@ -82,7 +82,7 @@ theorem expect_mul_noiseOp_mul (ρ σ : ℝ) (f g : (ι → Bool) → ℝ) : rw [← noiseOp_noiseOp, expect_mul_noiseOp_comm] /-- The expectation of `f` against `T_{ρ σ} g` is at most `‖T_ρ f‖_2 ‖T_σ g‖_2`. -/ -private theorem expect_mul_noiseOp_mul_le (ρ σ : ℝ) (f g : (ι → Bool) → ℝ) : +theorem expect_mul_noiseOp_mul_le (ρ σ : ℝ) (f g : (ι → Bool) → ℝ) : 𝔼 x, f x * noiseOp (ρ * σ) g x ≤ lpNorm 2 (noiseOp ρ f) * lpNorm 2 (noiseOp σ g) := by rw [expect_mul_noiseOp_mul, lpNorm_two, lpNorm_two] exact Real.expect_mul_le_sqrt_mul_sqrt _ _ _ diff --git a/Complexity/Foundations/BooleanAnalysis/Hypercontractivity/Derivative.lean b/Complexity/Foundations/BooleanAnalysis/Hypercontractivity/Derivative.lean index 0d6b3afda..34697d7df 100644 --- a/Complexity/Foundations/BooleanAnalysis/Hypercontractivity/Derivative.lean +++ b/Complexity/Foundations/BooleanAnalysis/Hypercontractivity/Derivative.lean @@ -39,7 +39,7 @@ variable {ι : Type*} [Fintype ι] [DecidableEq ι] omit [Fintype ι] in /-- A power of the absolute value of the derivative of a Boolean function, read as signs, is the absolute value: the derivative takes the values `0` and `±1`. -/ -private theorem abs_derivative_signVal_rpow (f : (ι → Bool) → Bool) (i : ι) (x : ι → Bool) {p : ℝ} +theorem abs_derivative_signVal_rpow (f : (ι → Bool) → Bool) (i : ι) (x : ι → Bool) {p : ℝ} (hp : p ≠ 0) : |derivative i (fun x => signVal (f x)) x| ^ p = |derivative i (fun x => signVal (f x)) x| := by simp only [derivative] diff --git a/Complexity/Foundations/BooleanAnalysis/Hypercube.lean b/Complexity/Foundations/BooleanAnalysis/Hypercube.lean index 416de73de..b54ffaec2 100644 --- a/Complexity/Foundations/BooleanAnalysis/Hypercube.lean +++ b/Complexity/Foundations/BooleanAnalysis/Hypercube.lean @@ -63,7 +63,7 @@ open Finset Function Module variable {ι : Type*} /-- Flipping a bit of `T` negates the character of `T`. -/ -private theorem chi_update_not_of_mem {R : Type*} [CommRing R] [DecidableEq ι] {T : Finset ι} +theorem chi_update_not_of_mem {R : Type*} [CommRing R] [DecidableEq ι] {T : Finset ι} {i : ι} (hi : i ∈ T) (x : ι → Bool) : chi R T (update x i (!x i)) = -chi R T x := by have h := chi_update_of_mem (R := R) hi x (x i) diff --git a/Complexity/Foundations/BooleanAnalysis/KahnKalaiLinial.lean b/Complexity/Foundations/BooleanAnalysis/KahnKalaiLinial.lean index 843694503..ce971a7ea 100644 --- a/Complexity/Foundations/BooleanAnalysis/KahnKalaiLinial.lean +++ b/Complexity/Foundations/BooleanAnalysis/KahnKalaiLinial.lean @@ -112,7 +112,7 @@ private theorem sum_sum_filter_mem_fourierCoeff_sq_div_card (f : (ι → Bool) · simp [not_not.1 hS] /-- The weight `∑_{S ∋ i} f̂(S) ^ 2 / |S|` is at most the influence of `i`. -/ -private theorem sum_filter_mem_fourierCoeff_sq_div_card_le_influence (f : (ι → Bool) → ℝ) (i : ι) : +theorem sum_filter_mem_fourierCoeff_sq_div_card_le_influence (f : (ι → Bool) → ℝ) (i : ι) : ∑ S with i ∈ S, fourierCoeff f S ^ 2 / #S ≤ influence i f := by rw [influence_eq_sum_fourierCoeff_sq] refine sum_le_sum fun S hS => div_le_self (sq_nonneg _) ?_ diff --git a/Complexity/Foundations/Combinatorics/AffineDisperser.lean b/Complexity/Foundations/Combinatorics/AffineDisperser.lean index a84dc92bd..8620ed000 100644 --- a/Complexity/Foundations/Combinatorics/AffineDisperser.lean +++ b/Complexity/Foundations/Combinatorics/AffineDisperser.lean @@ -143,7 +143,7 @@ theorem eq_of_covering {r : ℕ} (k : Fin r → ℕ) (hk : StrictAnti k) (hk0 : /-- **Averaging**: some `t`-element subset `I` of `S` carries at least a `t / |S|` share of `∑_{i ∈ S} d i`. -/ -private theorem exists_subset_card_eq_mul_sum_le {ι : Type*} (S : Finset ι) (d : ι → ℕ) +theorem exists_subset_card_eq_mul_sum_le {ι : Type*} (S : Finset ι) (d : ι → ℕ) {t : ℕ} (ht : t ≤ S.card) : ∃ I ⊆ S, I.card = t ∧ t * ∑ i ∈ S, d i ≤ S.card * ∑ i ∈ I, d i := by classical diff --git a/Complexity/Foundations/Combinatorics/AffineDisperser/Threshold.lean b/Complexity/Foundations/Combinatorics/AffineDisperser/Threshold.lean index ba7a8ca69..bf162be12 100644 --- a/Complexity/Foundations/Combinatorics/AffineDisperser/Threshold.lean +++ b/Complexity/Foundations/Combinatorics/AffineDisperser/Threshold.lean @@ -54,7 +54,7 @@ namespace Cslib.AffineDisperser open Filter Explicit /-- Exponentials beat polynomials: `c * (n + 1) ^ k ≤ 2 ^ n` for all large `n`. -/ -private theorem eventually_mul_pow_le_two_pow (c k : ℕ) : +theorem eventually_mul_pow_le_two_pow (c k : ℕ) : ∀ᶠ n : ℕ in atTop, c * (n + 1) ^ k ≤ 2 ^ n := by filter_upwards [Nat.eventually_mul_pow_le_pow (c * 2 ^ k) k one_lt_two, eventually_ge_atTop 1] with n hn hn1 @@ -92,7 +92,7 @@ private theorem eventually_chebyshevFactor_le : _ = 2 ^ (s + q * (8 * s + 10)) := by rw [← pow_mul, ← pow_add] _ ≤ 2 ^ L := Nat.pow_le_pow_right two_pos h3 -private theorem tendsto_log_two_atTop : Tendsto (Nat.log 2) atTop atTop := +theorem tendsto_log_two_atTop : Tendsto (Nat.log 2) atTop atTop := tendsto_atTop_atTop.2 fun b => ⟨2 ^ b, fun _ hN => Nat.le_log_of_pow_le one_lt_two hN⟩ /-- Decomposing `explicitThreshold N` into the budget `N / (⌊log₂ N⌋ + 1) ^ 2`, the block-count diff --git a/Complexity/Foundations/Combinatorics/CentralBinomial.lean b/Complexity/Foundations/Combinatorics/CentralBinomial.lean index 180533dd6..d69abadb4 100644 --- a/Complexity/Foundations/Combinatorics/CentralBinomial.lean +++ b/Complexity/Foundations/Combinatorics/CentralBinomial.lean @@ -128,7 +128,7 @@ theorem two_mul_card_small_le (n : ℕ) : /-- Subsets of size between `n / 2` and `n / 2 + t` number at most `(t + 1) · C(n, ⌊n/2⌋)`. -/ -private theorem card_middle_le (n t : ℕ) : +theorem card_middle_le (n t : ℕ) : (univ.filter fun S : Finset (Fin n) => n ≤ 2 * S.card ∧ S.card ≤ n / 2 + t).card ≤ (t + 1) * n.choose (n / 2) := by classical diff --git a/Complexity/Foundations/Combinatorics/Expander/Walk.lean b/Complexity/Foundations/Combinatorics/Expander/Walk.lean index c17ae3821..fc35d994a 100644 --- a/Complexity/Foundations/Combinatorics/Expander/Walk.lean +++ b/Complexity/Foundations/Combinatorics/Expander/Walk.lean @@ -485,7 +485,7 @@ variable [Fintype D] /-- From a fixed start `v`, the `i`-th dart of a uniformly random walk leaves the vertex reached by the random walk after `i` steps along a uniformly random label: the average of `f` over it is `(G.walk ^ i) (fun w ↦ 𝔼 a, f (w, a)) v`. -/ -private theorem expect_walkDart_mk (v : V) (i : Fin t) (f : V × D → ℝ) : +theorem expect_walkDart_mk (v : V) (i : Fin t) (f : V × D → ℝ) : 𝔼 k : Fin t → D, f (G.walkDart (v, k) i) = (G.walk ^ (i : ℕ)) (fun w ↦ 𝔼 a, f (w, a)) v := by rcases isEmpty_or_nonempty D with hD | hD · have : IsEmpty (Fin t → D) := ⟨fun k ↦ hD.false (k i)⟩ diff --git a/Complexity/Foundations/Combinatorics/FunctionalGraph/Cycle.lean b/Complexity/Foundations/Combinatorics/FunctionalGraph/Cycle.lean index 3ac7cbcea..ba42c30b7 100644 --- a/Complexity/Foundations/Combinatorics/FunctionalGraph/Cycle.lean +++ b/Complexity/Foundations/Combinatorics/FunctionalGraph/Cycle.lean @@ -61,7 +61,7 @@ variable {α : Type u} [Finite α] (f : α → α) omit [Finite α] in /-- Periodic points reached at different times along one orbit have the same minimal period. -/ -private theorem minimalPeriod_eq_of_periodic_iterates (x : α) {a b : ℕ} +theorem minimalPeriod_eq_of_periodic_iterates (x : α) {a b : ℕ} (ha : f^[a] x ∈ periodicPts f) (hb : f^[b] x ∈ periodicPts f) : minimalPeriod f (f^[a] x) = minimalPeriod f (f^[b] x) := by rcases le_total a b with h | h diff --git a/Complexity/Foundations/Combinatorics/FunctionalGraph/ForestIntervals.lean b/Complexity/Foundations/Combinatorics/FunctionalGraph/ForestIntervals.lean index 127e161e9..5d0a0ca15 100644 --- a/Complexity/Foundations/Combinatorics/FunctionalGraph/ForestIntervals.lean +++ b/Complexity/Foundations/Combinatorics/FunctionalGraph/ForestIntervals.lean @@ -106,7 +106,7 @@ theorem forestPath_injective : Function.Injective (forestPath f) := by theorem self_mem_forestPath (x : α) : x ∈ forestPath f x := (mem_forestPath f x x).mpr ⟨0, Nat.zero_le _, rfl⟩ -private theorem forestPath_step (x : α) (hx : 0 < transientDepth f x) : +theorem forestPath_step (x : α) (hx : 0 < transientDepth f x) : forestPath f x = forestPath f (f x) ++ [x] := by have hd : transientDepth f (f x) + 1 = transientDepth f x := by have hh := transientDepth_iterate f x 1 @@ -117,7 +117,7 @@ private theorem forestPath_step (x : α) (hx : 0 < transientDepth f x) : (forestTrace f (f x) (transientDepth f (f x) + 1)).reverse ++ [x] rw [hd] -private theorem forestPath_iterate_prefix (x : α) {t : ℕ} (ht : t ≤ transientDepth f x) : +theorem forestPath_iterate_prefix (x : α) {t : ℕ} (ht : t ≤ transientDepth f x) : forestPath f (f^[t] x) <+: forestPath f x := by induction t generalizing x with | zero => exact ⟨[], List.append_nil _⟩ diff --git a/Complexity/Foundations/Combinatorics/MajorityTree.lean b/Complexity/Foundations/Combinatorics/MajorityTree.lean index 231dd21ff..7245c68b4 100644 --- a/Complexity/Foundations/Combinatorics/MajorityTree.lean +++ b/Complexity/Foundations/Combinatorics/MajorityTree.lean @@ -62,7 +62,7 @@ variable {α : Type*} [DecidableEq α] def maj3 (a b c : α) : α := if a = b then a else c /-- If `maj3 a b c` misses `y`, then two of `a`, `b`, `c` miss `y`. -/ -private theorem two_ne_of_maj3_ne {a b c y : α} (h : maj3 a b c ≠ y) : +theorem two_ne_of_maj3_ne {a b c y : α} (h : maj3 a b c ≠ y) : (a ≠ y ∧ b ≠ y) ∨ (a ≠ y ∧ c ≠ y) ∨ (b ≠ y ∧ c ≠ y) := by unfold maj3 at h split_ifs at h with hab diff --git a/Complexity/Foundations/Data/BitString/PartialAssignment/Counting.lean b/Complexity/Foundations/Data/BitString/PartialAssignment/Counting.lean index b10de21c9..768f8ab2a 100644 --- a/Complexity/Foundations/Data/BitString/PartialAssignment/Counting.lean +++ b/Complexity/Foundations/Data/BitString/PartialAssignment/Counting.lean @@ -83,7 +83,7 @@ free. -/ /-- For a fixed subset `S ∈ powersetCard ℓ ρ₀.free`, there are `2 ^ (#ρ₀.free - ℓ)` extensions in `ρ₀.extensions ℓ` whose free set is `S`. -/ -private theorem card_filter_extensions_free_eq (ρ₀ : PartialAssignment ι) (ℓ : ℕ) +theorem card_filter_extensions_free_eq (ρ₀ : PartialAssignment ι) (ℓ : ℕ) {S : Finset ι} (hS : S ∈ powersetCard ℓ ρ₀.free) : #{ρ ∈ ρ₀.extensions ℓ | ρ.free = S} = 2 ^ (#ρ₀.free - ℓ) := by obtain ⟨hSsub, hScard⟩ := mem_powersetCard.1 hS @@ -158,7 +158,7 @@ theorem card_filter_extensions_free_subset (ρ₀ : PartialAssignment ι) (ℓ : /-- The number of extensions in `ρ₀.extensions ℓ` that fix every coordinate of `B ⊆ ρ₀.free` is `C(#ρ₀.free - |B|, ℓ) * 2 ^ (#ρ₀.free - ℓ)`. -/ -private theorem card_filter_extensions_not_nonempty_inter (ρ₀ : PartialAssignment ι) (ℓ : ℕ) +theorem card_filter_extensions_not_nonempty_inter (ρ₀ : PartialAssignment ι) (ℓ : ℕ) {B : Finset ι} (hB : B ⊆ ρ₀.free) : #{ρ ∈ ρ₀.extensions ℓ | ¬(ρ.free ∩ B).Nonempty} = (#ρ₀.free - #B).choose ℓ * 2 ^ (#ρ₀.free - ℓ) := by @@ -199,7 +199,7 @@ theorem card_withFree (ℓ : ℕ) : /-- A partial assignment with `ℓ'` free coordinates extends `C(|ι| - ℓ', ℓ - ℓ')` of the ones with `ℓ ≥ ℓ'` free coordinates: those that free `ℓ - ℓ'` of its fixed coordinates. -/ -private theorem card_filter_extends_withFree {ρ' : PartialAssignment ι} {ℓ : ℕ} +theorem card_filter_extends_withFree {ρ' : PartialAssignment ι} {ℓ : ℕ} (hℓ : #ρ'.free ≤ ℓ) : #((withFree ι ℓ).filter fun ρ => ρ'.Extends ρ) = (Fintype.card ι - #ρ'.free).choose (ℓ - #ρ'.free) := by @@ -241,7 +241,7 @@ private theorem card_filter_extends_withFree {ρ' : PartialAssignment ι} {ℓ : /-- The words agreeing with a partial assignment outside its free coordinates: `2 ^ ℓ` of them for `ℓ` free coordinates. -/ -private theorem card_filter_outside_eq (ρ : PartialAssignment ι) : +theorem card_filter_outside_eq (ρ : PartialAssignment ι) : #{z : ι → Bool | outside ρ.free z = ρ} = 2 ^ #ρ.free := by rw [← card_filter_forall_notMem_eq ρ.free (ρ.fill fun _ => false)] congr 1 diff --git a/Complexity/Foundations/Data/BitString/ShortWords.lean b/Complexity/Foundations/Data/BitString/ShortWords.lean index 7a44328f2..edb2f3523 100644 --- a/Complexity/Foundations/Data/BitString/ShortWords.lean +++ b/Complexity/Foundations/Data/BitString/ShortWords.lean @@ -95,7 +95,7 @@ theorem nil_mem_shortWords (L : ℕ) : [] ∈ shortWords L := by simp /-- The binary words of length at most `L` are the words `List.ofFn r` for `r : Fin m → Bool` and `m ≤ L`. -/ -private theorem shortWords_eq_biUnion (L : ℕ) : +theorem shortWords_eq_biUnion (L : ℕ) : shortWords L = (range (L + 1)).biUnion fun m => univ.image (List.ofFn : (Fin m → Bool) → _) := by ext w diff --git a/Complexity/Foundations/Data/Code/HammingBound.lean b/Complexity/Foundations/Data/Code/HammingBound.lean index a74035b95..49bf7b2fc 100644 --- a/Complexity/Foundations/Data/Code/HammingBound.lean +++ b/Complexity/Foundations/Data/Code/HammingBound.lean @@ -66,7 +66,7 @@ variable {ι : Type*} [Fintype ι] [DecidableEq ι] {β : ι → Type*} [∀ i, /-- The words differing from `x` exactly at the positions `S`: a different letter at each position of `S`. -/ -private theorem card_filter_filter_ne_eq (x : ∀ i, β i) (S : Finset ι) : +theorem card_filter_filter_ne_eq (x : ∀ i, β i) (S : Finset ι) : #{y : ∀ i, β i | ({i | x i ≠ y i} : Finset ι) = S} = ∏ i ∈ S, (Fintype.card (β i) - 1) := by have h : #{y : ∀ i, β i | ({i | x i ≠ y i} : Finset ι) = S} = Fintype.card (∀ i, {b : β i // (i ∈ S ↔ x i ≠ b)}) := by diff --git a/Complexity/Foundations/Data/Nat/Bitwise/Multiplication.lean b/Complexity/Foundations/Data/Nat/Bitwise/Multiplication.lean index 77ae2eded..e05e45195 100644 --- a/Complexity/Foundations/Data/Nat/Bitwise/Multiplication.lean +++ b/Complexity/Foundations/Data/Nat/Bitwise/Multiplication.lean @@ -105,7 +105,7 @@ private theorem sum_pairs (x y : ℕ) : /-- The weighted contribution of all columns strictly below `k`. -/ def mulPrefix (x y k : ℕ) : ℕ := ∑ j ∈ range k, mulColumn x y j * 2 ^ j -private theorem mulPrefix_succ (x y k : ℕ) : +theorem mulPrefix_succ (x y k : ℕ) : mulPrefix x y (k + 1) = mulPrefix x y k + mulColumn x y k * 2 ^ k := sum_range_succ _ _ private theorem mulPrefix_eq_filter (x y k : ℕ) : @@ -162,7 +162,7 @@ def mulCarry (x y k : ℕ) : ℕ := mulPrefix x y k / 2 ^ k /-- No carry enters column `0`. -/ @[simp] theorem mulCarry_zero (x y : ℕ) : mulCarry x y 0 = 0 := by simp [mulCarry, mulPrefix] -private theorem mulCarry_succ (x y k : ℕ) : +theorem mulCarry_succ (x y k : ℕ) : mulCarry x y (k + 1) = (mulCarry x y k + mulColumn x y k) / 2 := by simp only [mulCarry, mulPrefix_succ, pow_succ, ← Nat.div_div_eq_div_mul, Nat.add_mul_div_right _ _ (Nat.two_pow_pos k)] diff --git a/Complexity/Foundations/Data/StackTape.lean b/Complexity/Foundations/Data/StackTape.lean index 79b514541..ac7c24d56 100644 --- a/Complexity/Foundations/Data/StackTape.lean +++ b/Complexity/Foundations/Data/StackTape.lean @@ -148,7 +148,7 @@ lemma ofList_append_replicate_none (l : List (Option Symbol)) (n : ℕ) : ofList (l.map some) = mapSome l := by exact ofList_toList (mapSome l) -private lemma listBlank_mk_cons_toList (a : Option Symbol) (tape : StackTape Symbol) : +lemma listBlank_mk_cons_toList (a : Option Symbol) (tape : StackTape Symbol) : _root_.Turing.ListBlank.mk (cons a tape).toList = _root_.Turing.ListBlank.cons a (_root_.Turing.ListBlank.mk tape.toList) := by cases a with diff --git a/Complexity/Foundations/FieldTheory/Finite/BinaryField.lean b/Complexity/Foundations/FieldTheory/Finite/BinaryField.lean index 8000790e5..5f96451e4 100644 --- a/Complexity/Foundations/FieldTheory/Finite/BinaryField.lean +++ b/Complexity/Foundations/FieldTheory/Finite/BinaryField.lean @@ -155,7 +155,7 @@ noncomputable def leastIrreducible (p : ℕ) : (ZMod 2)[X] := polyOfCode (Nat.find h) else X -private theorem exists_code_irreducible {p : ℕ} (hp : p ≠ 0) : +theorem exists_code_irreducible {p : ℕ} (hp : p ≠ 0) : ∃ m, Irreducible (polyOfCode m) ∧ (polyOfCode m).natDegree = p := by obtain ⟨g, hg, hgp⟩ := exists_irreducible_natDegree_eq hp obtain ⟨m, rfl⟩ := polyOfCode_surjective g diff --git a/Complexity/Foundations/FieldTheory/Finite/LinearizedPolynomial.lean b/Complexity/Foundations/FieldTheory/Finite/LinearizedPolynomial.lean index b774ad674..09309146e 100644 --- a/Complexity/Foundations/FieldTheory/Finite/LinearizedPolynomial.lean +++ b/Complexity/Foundations/FieldTheory/Finite/LinearizedPolynomial.lean @@ -352,7 +352,7 @@ theorem linearizedEval_pow_two_pow [Finite F] {n : ℕ} [NeZero n] (hn : finrank pow_two_pow_mod hn x (j.val + k), ZMod.val_add, ZMod.val_natCast, Nat.add_mod_mod] omit [Algebra (ZMod 2) F] in -private theorem linearizedEval_sub_mul {n : ℕ} [NeZero n] (a b : ZMod n → F) (c x : F) : +theorem linearizedEval_sub_mul {n : ℕ} [NeZero n] (a b : ZMod n → F) (c x : F) : linearizedEval (fun j => b j - c * a j) x = linearizedEval b x - c * linearizedEval a x := by simp only [linearizedEval, sub_mul, Finset.sum_sub_distrib, Finset.mul_sum, mul_assoc] diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/CutRank.lean b/Complexity/Foundations/LinearAlgebra/Matrix/CutRank.lean index dd37ddf7f..4860e2e43 100644 --- a/Complexity/Foundations/LinearAlgebra/Matrix/CutRank.lean +++ b/Complexity/Foundations/LinearAlgebra/Matrix/CutRank.lean @@ -88,7 +88,7 @@ theorem blockRank_eq_rank [Finite m] (S : Set m) (T : Set n) [Fintype T] : /-- Restricting the columns of a block maps its row space onto the row space of the smaller block. -/ -private theorem span_range_row_submatrix_eq_map (S : Set m) {T T' : Set n} (h : T' ⊆ T) : +theorem span_range_row_submatrix_eq_map (S : Set m) {T T' : Set n} (h : T' ⊆ T) : span K (range (M.submatrix ((↑) : S → m) ((↑) : T' → n)).row) = (span K (range (M.submatrix ((↑) : S → m) ((↑) : T → n)).row)).map (LinearMap.funLeft K K (inclusion h)) := by diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/SubmatrixRobust.lean b/Complexity/Foundations/LinearAlgebra/Matrix/SubmatrixRobust.lean index 435768dc1..8199275e5 100644 --- a/Complexity/Foundations/LinearAlgebra/Matrix/SubmatrixRobust.lean +++ b/Complexity/Foundations/LinearAlgebra/Matrix/SubmatrixRobust.lean @@ -356,7 +356,7 @@ theorem add_blockRank_le_cutRank_add_transpose [Finite ι] omega /-- Two injective maps with disjoint ranges pull back at most `|V|` elements of `V`. -/ -private theorem ncard_preimage_add_ncard_preimage_le [Finite ι] {f : κ → ι} {g : κ' → ι} +theorem ncard_preimage_add_ncard_preimage_le [Finite ι] {f : κ → ι} {g : κ' → ι} (hf : Function.Injective f) (hg : Function.Injective g) (hfg : Disjoint (range f) (range g)) (V : Set ι) : (f ⁻¹' V).ncard + (g ⁻¹' V).ncard ≤ V.ncard := by rw [← ncard_image_of_injective _ hf, ← ncard_image_of_injective _ hg, diff --git a/Complexity/Languages/Probabilistic/LinearHash.lean b/Complexity/Languages/Probabilistic/LinearHash.lean index b97c3a4d1..d2f90fe0a 100644 --- a/Complexity/Languages/Probabilistic/LinearHash.lean +++ b/Complexity/Languages/Probabilistic/LinearHash.lean @@ -77,7 +77,7 @@ theorem eval_extract_bind {n m : ℕ} (source : PMF (BitString n)) : wordHash_eq_ofFn, ofList_ofFn, blocksEquiv_apply] /-- The word extractor's exact finite law on one fixed-width input. -/ -private theorem eval_extract_ofFn {n m : ℕ} (input : BitString n) : +theorem eval_extract_ofFn {n m : ℕ} (input : BitString n) : ProbComp.eval (extract m (List.ofFn input)) = (PMF.uniformOfFintype (BitString (m * n))).map (fun seed => List.ofFn seed ++ diff --git a/Complexity/Probability/BitString/LinearHash.lean b/Complexity/Probability/BitString/LinearHash.lean index cefdd3e67..399a81b15 100644 --- a/Complexity/Probability/BitString/LinearHash.lean +++ b/Complexity/Probability/BitString/LinearHash.lean @@ -99,7 +99,7 @@ theorem isTwoUniversal (n m : ℕ) : (isDeltaUniversalHash n m).isTwoUniversal /-- Any initial block of a uniform matrix is itself uniform. Unused rows may remain public. -/ -private theorem uniform_prefix {n m count : ℕ} (h : m ≤ count) : +theorem uniform_prefix {n m count : ℕ} (h : m ≤ count) : (PMF.uniformOfFintype (Fin count → BitString n)).map (fun rows => rows ∘ Fin.castLE h) = PMF.uniformOfFintype (Fin m → BitString n) := by diff --git a/Complexity/Probability/Conditioning.lean b/Complexity/Probability/Conditioning.lean index 8fd6aeef4..faca6d699 100644 --- a/Complexity/Probability/Conditioning.lean +++ b/Complexity/Probability/Conditioning.lean @@ -55,7 +55,7 @@ theorem map_fst_apply (joint : PMF (α × β)) (a : α) : simp [Ne.symm hx] /-- Each joint mass is at most the corresponding marginal mass. -/ -private theorem apply_le_map_fst (joint : PMF (α × β)) (a : α) (b : β) : +theorem apply_le_map_fst (joint : PMF (α × β)) (a : α) (b : β) : joint (a, b) ≤ (joint.map Prod.fst) a := le_map_apply joint Prod.fst (a, b) diff --git a/Complexity/Probability/HashIsolation.lean b/Complexity/Probability/HashIsolation.lean index 9fd650bcf..92d0c3a59 100644 --- a/Complexity/Probability/HashIsolation.lean +++ b/Complexity/Probability/HashIsolation.lean @@ -158,7 +158,7 @@ theorem IsTwoUniversal.conditionalEntropy_hash_le [Finite Seed] {seed : PMF Seed omit [Fintype Seed] [Fintype Output] in /-- Averaging over hash lengths `1, …, count` leaves at most the average logarithmic fiber size plus two bits, divided by `count`. This is the entropy bound in Holenstein's Lemma 3. -/ -private theorem mean_conditionalEntropy_hash_le [Finite Seed] (count : ℕ) (seed : PMF Seed) +theorem mean_conditionalEntropy_hash_le [Finite Seed] (count : ℕ) (seed : PMF Seed) (source : PMF Input) (f : Input → Image) (hash : (i : Fin count) → Seed → Input → (Fin (i.val + 1) → Bool)) (hhash : ∀ i, IsTwoUniversal seed (hash i)) (predicate : Fin count → Seed → Input → Bool) : diff --git a/Complexity/Probability/Shearer.lean b/Complexity/Probability/Shearer.lean index f2187985e..7f09a8050 100644 --- a/Complexity/Probability/Shearer.lean +++ b/Complexity/Probability/Shearer.lean @@ -57,7 +57,7 @@ namespace Cslib.Probability.PMF variable {ι : Type*} {α : ι → Type*} [∀ i, Finite (α i)] /-- Conditioning a coordinate on a larger set of coordinates cannot increase its entropy. -/ -private theorem conditionalEntropy_map_restrict_le (P : PMF (∀ i, α i)) {s t : Finset ι} +theorem conditionalEntropy_map_restrict_le (P : PMF (∀ i, α i)) {s t : Finset ι} (hst : s ⊆ t) (i : ι) : conditionalEntropy (P.map fun x => (t.restrict x, x i)) ≤ conditionalEntropy (P.map fun x => (s.restrict x, x i)) := by @@ -120,7 +120,7 @@ theorem entropy_map_restrict_eq_sum [LinearOrder ι] (P : PMF (∀ i, α i)) (s rw [hfilter] /-- The restriction of a tuple to all coordinates carries the tuple's entropy. -/ -private theorem entropy_map_restrict_univ [Fintype ι] (P : PMF (∀ i, α i)) : +theorem entropy_map_restrict_univ [Fintype ι] (P : PMF (∀ i, α i)) : entropy (P.map (univ : Finset ι).restrict) = entropy P := by apply entropy_map_of_injective intro x y hxy diff --git a/Complexity/Probability/SmallBias/Powering.lean b/Complexity/Probability/SmallBias/Powering.lean index 6ba4668a5..2b6a199d7 100644 --- a/Complexity/Probability/SmallBias/Powering.lean +++ b/Complexity/Probability/SmallBias/Powering.lean @@ -81,7 +81,7 @@ private theorem chi_powering (S : Finset (Fin n)) (s : F × F) : /-- The inner product of `bits a` with the bits of a uniformly random field element is unbiased unless `a = 0`. -/ -private theorem expect_signVal_dotProduct [DecidableEq F] (a : F) : +theorem expect_signVal_dotProduct [DecidableEq F] (a : F) : 𝔼 y, signVal (bits a ⬝ᵥ bits y) = if a = 0 then 1 else 0 := by rw [Fintype.expect_equiv bits.toEquiv (fun y => signVal (bits a ⬝ᵥ bits y)) (fun v => signVal (bits a ⬝ᵥ v)) fun _ => rfl] @@ -102,7 +102,7 @@ theorem bias_powering [DecidableEq F] (S : Finset (Fin n)) : /-- A nonempty sum of distinct powers `x ^ i`, `i < n`, vanishes at fewer than `n` points of a field. -/ -private theorem card_filter_sum_pow_eq_zero_le [DecidableEq F] {S : Finset (Fin n)} +theorem card_filter_sum_pow_eq_zero_le [DecidableEq F] {S : Finset (Fin n)} (hS : S.Nonempty) : #{x : F | ∑ i ∈ S, x ^ (i : ℕ) = 0} ≤ n - 1 := by classical