From b5050e4a57e5dd6b2960d11a758188fba5ac64e5 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 16:49:08 +0000 Subject: [PATCH 1/2] refactor(Combinatorics): align namespaces with upstream markers and factor proof steps (#614) --- .../Computability/Circuit/Boolean/LMN.lean | 4 +- .../Communication/Disjointness.lean | 6 +- .../Combinatorics/CentralBinomial.lean | 3 +- .../Combinatorics/Expander/Hitting.lean | 187 +++---- .../Combinatorics/Hypergeometric.lean | 130 +++-- .../Combinatorics/PowersetTail.lean | 286 +++++------ .../Data/Code/LocalListDecoding.lean | 468 ++++++++---------- ComplexityTests/RandomizedDisjointness.lean | 4 +- 8 files changed, 541 insertions(+), 547 deletions(-) diff --git a/Complexity/Computability/Circuit/Boolean/LMN.lean b/Complexity/Computability/Circuit/Boolean/LMN.lean index c097247566..1d0b408678 100644 --- a/Complexity/Computability/Circuit/Boolean/LMN.lean +++ b/Complexity/Computability/Circuit/Boolean/LMN.lean @@ -34,7 +34,7 @@ stage leaves a `1 / (16 s + 1)` fraction of the free bits (as in The proof draws a random set `J` of `ℓ = ⌊n / (16 s + 1) ^ d⌋` coordinates and fixes the others to a random word `z`, a random restriction (partial assignment) (`PartialAssignment.sum_card_filter_outside`). A set `U` of at least `k` coordinates meets `J` in at -least `s` of them for at least half of the `J` (`Finset.two_mul_card_filter_card_inter_lt_le`), so +least `s` of them for at least half of the `J` (`Cslib.two_mul_card_filter_card_inter_lt_le`), so the weight on such `U` is at most twice the expected weight of the restriction on sets of at least `s` coordinates (`BitString.expect_sum_fourierCoeff_piecewise_sq`). That is zero when the restriction has a decision tree of depth below `s` (`DecisionTree.fourierCoeff_eq_zero_of_depth_lt`) @@ -168,7 +168,7 @@ theorem sum_fourierCoeff_sq_le_of_computes {f : BooleanFunction n} {C : Circuit rw [hswap, mul_sum, sum_filter] refine sum_le_sum fun U _ => ?_ split_ifs with hU - · have hcount := Finset.two_mul_card_filter_card_inter_lt_le (s := univ) (U := U) (ℓ := ℓ) + · have hcount := two_mul_card_filter_card_inter_lt_le (s := univ) (U := U) (ℓ := ℓ) (m := s) (subset_univ U) (by simpa using hn0) (by have : 8 * n ≤ k * ℓ := (Nat.mul_le_mul_right _ (le_max_left _ _)).trans hk diff --git a/Complexity/Computability/Communication/Disjointness.lean b/Complexity/Computability/Communication/Disjointness.lean index 6120c7b4e3..b0fb478459 100644 --- a/Complexity/Computability/Communication/Disjointness.lean +++ b/Complexity/Computability/Communication/Disjointness.lean @@ -37,7 +37,7 @@ mass the average of `a₁ b₁`, where `a₁` and `b₁` are the fractions of th containing `i` in `A` and of `Ty ∪ {i}` in `B`. Call the partition bad for `A` if `a₁ < a₀ / 3`. Once `Ty` is fixed, `i` is a uniformly random point outside `Ty` and `b₀` is fixed, and a family of subsets of the complement of `Ty` for which many points are bad is small -(`Finset.four_mul_sum_card_filter_notMem_le`, proved by Markov's inequality and counting subsets of +(`Cslib.four_mul_sum_card_filter_notMem_le`, proved by Markov's inequality and counting subsets of a cube). So the partitions bad for `A` or, symmetrically, for `B` carry at most half of the mass of the disjoint pairs, up to an exponentially small error, while on the others `a₁ b₁ ≥ a₀ b₀ / 9`. This is *Razborov's corruption lemma* (`Disjointness.corrupted_hardDist`): on every rectangle the @@ -205,7 +205,7 @@ private theorem low_le_two_pow (A : Finset (Finset U)) (s : Finset U) : low A s rw [← card_powerset] exact card_le_card fun x hx => mem_powerset.mpr (mem_filter.mp hx).2 -/-- The error terms of `Finset.four_mul_sum_card_filter_notMem_le` for `j = 12 r` and +/-- The error terms of `Cslib.four_mul_sum_card_filter_notMem_le` for `j = 12 r` and `#S ≥ 48 r`. -/ private theorem slack_le {r s : ℕ} (hs : 48 * r ≤ s) (hs1 : 1 ≤ s) : 8 * s * (27 / 32 : ℝ) ^ r + (((12 * r : ℕ) : ℝ) + 1) * 2 ^ (12 * r) * (3 / 4) ^ s ≤ @@ -510,7 +510,7 @@ variable (m) in `x ⊆ Tx` and `y ⊆ Ty`; with probability `1 / 2` output the disjoint pair `(x, y)`, and otherwise the pair `(x ∪ {i}, y ∪ {i})`, which meets in exactly `i`. Razborov draws subsets of fixed size `m / 2` instead; drawing all subsets lets the corruption bound be proved by counting subsets of -a cube (`Finset.four_mul_sum_card_filter_notMem_le`). -/ +a cube (`Cslib.four_mul_sum_card_filter_notMem_le`). -/ noncomputable def hardDist (hU : Fintype.card U = 2 * m + 1) : PMF (Finset U × Finset U) := PMF.ofFintype (fun q => ENNReal.ofReal (hardWeight m q)) (by diff --git a/Complexity/Foundations/Combinatorics/CentralBinomial.lean b/Complexity/Foundations/Combinatorics/CentralBinomial.lean index a4314253ec..180533dd6b 100644 --- a/Complexity/Foundations/Combinatorics/CentralBinomial.lean +++ b/Complexity/Foundations/Combinatorics/CentralBinomial.lean @@ -5,7 +5,7 @@ Authors: Samuel Schlesinger -/ module --- upstream: candidate (the central binomial bounds to Mathlib's `Mathlib/Combinatorics/Choose`) +-- upstream: candidate public import Complexity.Init public import Mathlib.Data.Nat.Choose.Central @@ -29,6 +29,7 @@ binomial coefficients), are at most `6 / 10` of all sets when `100 (t + 1)² ≤ ## Main results +* `Cslib.centralBinom_sq_mul_le`: `C(2m, m)² (2m + 1) ≤ 16 ^ m`. * `Cslib.choose_half_sq_mul_le`: `C(n, ⌊n/2⌋)² (n + 1) ≤ 4 ^ n`. * `Cslib.ten_mul_card_filter_card_le_le`: few sets are much larger than half. diff --git a/Complexity/Foundations/Combinatorics/Expander/Hitting.lean b/Complexity/Foundations/Combinatorics/Expander/Hitting.lean index f8dd034364..e472a1b9f7 100644 --- a/Complexity/Foundations/Combinatorics/Expander/Hitting.lean +++ b/Complexity/Foundations/Combinatorics/Expander/Hitting.lean @@ -125,7 +125,62 @@ end WeightedWalk section Hitting -variable [Fintype V] [Fintype D] [DecidableEq V] +variable [Fintype V] [Fintype D] + +/-- The second moment of a constant restricted to `B` is `dens B` times its square. -/ +private theorem expect_ite_const_sq [DecidableEq V] (B : Finset V) (α : ℝ) : + 𝔼 v, (if v ∈ B then α else 0) ^ 2 = dens B * α ^ 2 := by + have h : (𝔼 v, if v ∈ B then (1 : ℝ) else 0) = dens B := by + simpa using (Fintype.expect_boole (𝕜 := ℝ) fun v => v ∈ B) + rw [← h, expect_mul] + exact expect_congr rfl fun v _ => by split_ifs <;> simp + +/-- By Cauchy–Schwarz, the squared average of a function vanishing outside `C` is at most the +density of `C` times its second moment. -/ +private theorem sq_expect_le_dens_mul_expect_sq {C : Finset V} {x : V → ℝ} + (hx : ∀ v ∉ C, x v = 0) : + (𝔼 v, x v) ^ 2 ≤ dens C * 𝔼 v, x v ^ 2 := by + classical + have h := expect_mul_sq_le_sq_mul_sq univ (fun v => if v ∈ C then (1 : ℝ) else 0) x + have h₁ : 𝔼 v, (if v ∈ C then (1 : ℝ) else 0) * x v = 𝔼 v, x v := + expect_congr rfl fun v _ => by by_cases hv : v ∈ C <;> simp [hv, hx] + have h₂ : 𝔼 v, (if v ∈ C then (1 : ℝ) else 0) ^ 2 = dens C := by + simpa using expect_ite_const_sq C 1 + rwa [h₁, h₂] at h + +/-- Subtracting `(1 - λ(G))` times the mean from `G.walk x` leaves second moment at most +`λ(G) ^ 2` times the second moment of `x`. -/ +private theorem expect_walk_sub_one_sub_spectralExpansion_sq_le [Nonempty V] [Nonempty D] + (x : V → ℝ) : + 𝔼 v, (G.walk x v - (1 - G.spectralExpansion) * 𝔼 u, x u) ^ 2 ≤ + G.spectralExpansion ^ 2 * 𝔼 v, x v ^ 2 := by + set ℓ := G.spectralExpansion + set α := 𝔼 v, x v + set w : V → ℝ := G.walk (fun v => x v - α) + have hw₀ : 𝔼 v, (x v - α) = 0 := Fintype.expect_balance x + have hw : 𝔼 v, w v = 0 := G.expect_walk_eq_zero hw₀ + have hw₂ : 𝔼 v, w v ^ 2 ≤ ℓ ^ 2 * 𝔼 v, (x v - α) ^ 2 := + expect_walk_sq_le_spectralExpansion_sq_mul hw₀ + have hyw (v : V) : G.walk x v - (1 - ℓ) * α = ℓ * α + w v := by + have : G.walk x = (fun _ => α) + w := by + rw [← G.walk_const α, ← map_add] + exact congrArg G.walk (funext fun _ => by simp) + simp only [this, Pi.add_apply] + ring + have hvar : 𝔼 v, (x v - α) ^ 2 = 𝔼 v, x v ^ 2 - α ^ 2 := by + have : ∀ v, (x v - α) ^ 2 = x v ^ 2 - 2 * α * x v + α ^ 2 := fun _ => by ring + simp only [this, expect_add_distrib, expect_sub_distrib, ← mul_expect, Fintype.expect_const] + ring + calc 𝔼 v, (G.walk x v - (1 - ℓ) * α) ^ 2 + = ℓ ^ 2 * α ^ 2 + 2 * (ℓ * α) * 𝔼 v, w v + 𝔼 v, w v ^ 2 := by + have : ∀ v, (G.walk x v - (1 - ℓ) * α) ^ 2 = + ℓ ^ 2 * α ^ 2 + 2 * (ℓ * α) * w v + w v ^ 2 := fun v => by rw [hyw]; ring + simp only [this, expect_add_distrib, ← mul_expect, Fintype.expect_const] + _ ≤ ℓ ^ 2 * α ^ 2 + 2 * (ℓ * α) * 0 + ℓ ^ 2 * (𝔼 v, x v ^ 2 - α ^ 2) := by + rw [hw, ← hvar]; gcongr + _ = ℓ ^ 2 * 𝔼 v, x v ^ 2 := by ring + +variable [DecidableEq V] /-- One step of a walk restricted to a small set: if `x` vanishes outside a set `C`, and `B` and `C` have density at most `μ`, then restricting `G.walk x` to `B` gives second moment at most @@ -141,60 +196,57 @@ theorem expect_ite_mem_walk_sq_le [Nonempty D] {B C : Finset V} {μ : ℝ} (hB : have hℓ₁ := G.spectralExpansion_le_one have hμ : 0 ≤ μ := (by positivity : (0 : ℝ) ≤ dens B).trans hB set α := 𝔼 v, x v - -- the average of a function supported on `C` is small - have hα : α ^ 2 ≤ dens C * 𝔼 v, x v ^ 2 := by - have h := expect_mul_sq_le_sq_mul_sq univ (fun v => if v ∈ C then (1 : ℝ) else 0) x - have h₁ : 𝔼 v, (if v ∈ C then (1 : ℝ) else 0) * x v = α := - expect_congr rfl fun v _ => by by_cases hv : v ∈ C <;> simp [hv, hx] - have h₂ : 𝔼 v, (if v ∈ C then (1 : ℝ) else 0) ^ 2 = dens C := - Fintype.expect_boole_mem_sq C - rwa [h₁, h₂] at h - -- the walk operator is `(1 - λ)` times the average plus an operator of norm at most `λ` set y : V → ℝ := fun v => G.walk x v - (1 - ℓ) * α - have hy : 𝔼 v, y v ^ 2 ≤ ℓ ^ 2 * 𝔼 v, x v ^ 2 := by - set w : V → ℝ := G.walk (fun v => x v - α) - have hw₀ : 𝔼 v, (x v - α) = 0 := Fintype.expect_balance x - have hw : 𝔼 v, w v = 0 := G.expect_walk_eq_zero hw₀ - have hw₂ : 𝔼 v, w v ^ 2 ≤ ℓ ^ 2 * 𝔼 v, (x v - α) ^ 2 := - expect_walk_sq_le_spectralExpansion_sq_mul hw₀ - have hyw (v : V) : y v = ℓ * α + w v := by - have : G.walk x = (fun _ => α) + w := by - rw [← G.walk_const α, ← map_add] - congr 1 - funext v - simp - simp only [y, this, Pi.add_apply] - ring - have hvar : 𝔼 v, (x v - α) ^ 2 = 𝔼 v, x v ^ 2 - α ^ 2 := by - have : ∀ v, (x v - α) ^ 2 = x v ^ 2 - 2 * α * x v + α ^ 2 := fun v => by ring - simp only [this, expect_add_distrib, expect_sub_distrib, ← mul_expect, - Fintype.expect_const] - ring - calc 𝔼 v, y v ^ 2 = ℓ ^ 2 * α ^ 2 + 2 * (ℓ * α) * 𝔼 v, w v + 𝔼 v, w v ^ 2 := by - have : ∀ v, y v ^ 2 = ℓ ^ 2 * α ^ 2 + 2 * (ℓ * α) * w v + w v ^ 2 := fun v => by - rw [hyw]; ring - simp only [this, expect_add_distrib, ← mul_expect, Fintype.expect_const] - _ ≤ ℓ ^ 2 * α ^ 2 + 2 * (ℓ * α) * 0 + ℓ ^ 2 * (𝔼 v, x v ^ 2 - α ^ 2) := by - rw [hw, ← hvar] - gcongr - _ = ℓ ^ 2 * 𝔼 v, x v ^ 2 := by ring - -- so the restriction to `B` is the restriction of `(1 - λ) α` plus a function of norm `λ ‖x‖` have hsplit (v : V) : (if v ∈ B then G.walk x v else 0) = (1 - ℓ) * (if v ∈ B then α else 0) + 1 * (if v ∈ B then y v else 0) := by split_ifs <;> simp [y] simp only [hsplit] refine Fintype.expect_add_sq_le (by linarith) zero_le_one hμ hℓ₀ (expect_nonneg fun _ _ => sq_nonneg _) ?_ ?_ |>.trans_eq (by ring) - · calc 𝔼 v, (if v ∈ B then α else 0) ^ 2 = dens B * α ^ 2 := by - rw [← Fintype.expect_boole_mem B, expect_mul] - exact expect_congr rfl fun v _ => by split_ifs <;> simp + · calc 𝔼 v, (if v ∈ B then α else 0) ^ 2 = dens B * α ^ 2 := expect_ite_const_sq B α _ ≤ μ * (μ * 𝔼 v, x v ^ 2) := by have := expect_nonneg (s := (univ : Finset V)) fun v _ => sq_nonneg (x v) gcongr - exact hα.trans (by gcongr) + exact (sq_expect_le_dens_mul_expect_sq hx).trans (by gcongr) _ = μ ^ 2 * 𝔼 v, x v ^ 2 := by ring - · refine le_trans (expect_le_expect fun v _ => ?_) hy - split_ifs <;> simp [sq_nonneg] + · refine le_trans (expect_le_expect fun v _ => ?_) + (G.expect_walk_sub_one_sub_spectralExpansion_sq_le x) + by_cases hv : v ∈ B <;> simp [hv, y, ℓ, α, sq_nonneg] + +omit [Fintype V] in +/-- The indicator-weighted walk vanishes outside `B 0`. -/ +private theorem weightedWalk_ite_eq_zero_of_notMem (t : ℕ) (B : ℕ → Finset V) {v : V} + (hv : v ∉ B 0) : + G.weightedWalk t (fun i v => if v ∈ B i then (1 : ℝ) else 0) v = 0 := by + obtain ⟨c, hc⟩ := G.weightedWalk_eq_mul t (fun i v => if v ∈ B i then (1 : ℝ) else 0) v + simp [hc, hv] + +/-- The second moment of the indicator-weighted walk decays by `((1 - λ(G)) μ + λ(G)) ^ 2` at each +step when every set `B i` has density at most `μ`. -/ +private theorem expect_weightedWalk_ite_sq_le [Nonempty D] {μ : ℝ} (t : ℕ) : + ∀ B : ℕ → Finset V, (∀ i, (dens (B i) : ℝ) ≤ μ) → + 𝔼 v, G.weightedWalk t (fun i v => if v ∈ B i then (1 : ℝ) else 0) v ^ 2 ≤ + ((1 - G.spectralExpansion) * μ + G.spectralExpansion) ^ (2 * t) * μ := by + set c := (1 - G.spectralExpansion) * μ + G.spectralExpansion + induction t with + | zero => + intro B hB + rw [weightedWalk_zero, expect_ite_const_sq] + simpa using hB 0 + | succ t ih => + intro B hB + have hstep := G.expect_ite_mem_walk_sq_le (hB 0) (hB 1) fun _ => + G.weightedWalk_ite_eq_zero_of_notMem t (fun i => B (i + 1)) + have heq (v : V) : G.weightedWalk (t + 1) (fun i v => if v ∈ B i then (1 : ℝ) else 0) v = + if v ∈ B 0 then G.walk (G.weightedWalk t + (fun i v => if v ∈ B (i + 1) then (1 : ℝ) else 0)) v else 0 := by + rw [weightedWalk_succ, Pi.mul_apply] + split_ifs <;> simp + simp only [heq] + calc _ ≤ c ^ 2 * 𝔼 v, G.weightedWalk t + (fun i v => if v ∈ B (i + 1) then (1 : ℝ) else 0) v ^ 2 := hstep + _ ≤ c ^ 2 * (c ^ (2 * t) * μ) := by gcongr; exact ih _ fun i => hB (i + 1) + _ = c ^ (2 * (t + 1)) * μ := by ring /-- **The hitting property of expander walks**, following [Vadhan, Theorem 4.17][Vadhan2012] (the sharp bound is due to [Kahale][Kahale1995]), with varying sets and the initial density @@ -213,57 +265,16 @@ theorem dens_filter_forall_walkAt_mem_le [Nonempty D] {B : ℕ → Finset V} {μ have := G.spectralExpansion_nonneg positivity set h : ℕ → V → ℝ := fun i v => if v ∈ B i then 1 else 0 - -- the weighted walk of the indicators vanishes outside the first set - have hsupp (t : ℕ) (B : ℕ → Finset V) (v : V) (hv : v ∉ B 0) : - G.weightedWalk t (fun i v => if v ∈ B i then (1 : ℝ) else 0) v = 0 := by - obtain ⟨c, hc⟩ := G.weightedWalk_eq_mul t (fun i v => if v ∈ B i then (1 : ℝ) else 0) v - simp [hc, hv] - -- and its second moment decays by `c ^ 2` with every step - have hmoment (t : ℕ) : ∀ B : ℕ → Finset V, (∀ i, (dens (B i) : ℝ) ≤ μ) → - 𝔼 v, G.weightedWalk t (fun i v => if v ∈ B i then (1 : ℝ) else 0) v ^ 2 ≤ - c ^ (2 * t) * μ := by - induction t with - | zero => - intro B hB - simp only [weightedWalk_zero, pow_zero, mul_zero, one_mul] - calc 𝔼 v, (if v ∈ B 0 then (1 : ℝ) else 0) ^ 2 = dens (B 0) := - Fintype.expect_boole_mem_sq (B 0) - _ ≤ μ := hB 0 - | succ t ih => - intro B hB - have hstep := G.expect_ite_mem_walk_sq_le (hB 0) (hB 1) (hsupp t (fun i => B (i + 1))) - have heq (v : V) : G.weightedWalk (t + 1) (fun i v => if v ∈ B i then (1 : ℝ) else 0) v = - if v ∈ B 0 then G.walk (G.weightedWalk t - (fun i v => if v ∈ B (i + 1) then (1 : ℝ) else 0)) v else 0 := by - rw [weightedWalk_succ, Pi.mul_apply] - split_ifs <;> simp - simp only [heq] - calc _ ≤ c ^ 2 * 𝔼 v, G.weightedWalk t - (fun i v => if v ∈ B (i + 1) then (1 : ℝ) else 0) v ^ 2 := hstep - _ ≤ c ^ 2 * (c ^ (2 * t) * μ) := by gcongr; exact ih _ fun i => hB (i + 1) - _ = c ^ (2 * (t + 1)) * μ := by ring - -- the probability is the average of the weighted walk, which is small by Cauchy–Schwarz have hprob : (dens {p : V × (Fin t → D) | ∀ i ≤ t, G.walkAt p i ∈ B i} : ℝ) = 𝔼 v, G.weightedWalk t h v := by rw [expect_weightedWalk, ← Fintype.expect_boole] refine expect_congr rfl fun p _ => ?_ simp only [h, prod_ite_zero, prod_const_one, mem_range, Nat.lt_succ_iff] rw [hprob] - have hCS := expect_mul_sq_le_sq_mul_sq univ (fun v => if v ∈ B 0 then (1 : ℝ) else 0) - (G.weightedWalk t h) - have h₁ : 𝔼 v, (if v ∈ B 0 then (1 : ℝ) else 0) * G.weightedWalk t h v = - 𝔼 v, G.weightedWalk t h v := - expect_congr rfl fun v _ => by - by_cases hv : v ∈ B 0 - · simp [hv] - · simp only [hv, ↓reduceIte, zero_mul] - exact (hsupp t B v hv).symm - have h₂ : 𝔼 v, (if v ∈ B 0 then (1 : ℝ) else 0) ^ 2 = dens (B 0) := - Fintype.expect_boole_mem_sq (B 0) - rw [h₁, h₂] at hCS have hbound : (𝔼 v, G.weightedWalk t h v) ^ 2 ≤ (μ * c ^ t) ^ 2 := - hCS.trans <| (mul_le_mul (hB 0) (hmoment t B hB) (expect_nonneg fun _ _ => sq_nonneg _) - hμ).trans_eq (by ring) + (sq_expect_le_dens_mul_expect_sq fun _ => G.weightedWalk_ite_eq_zero_of_notMem t B).trans <| + (mul_le_mul (hB 0) (G.expect_weightedWalk_ite_sq_le t B hB) + (expect_nonneg fun _ _ => sq_nonneg _) hμ).trans_eq (by ring) calc 𝔼 v, G.weightedWalk t h v ≤ μ * c ^ t := (abs_le_of_sq_le_sq' hbound (by positivity)).2 _ = μ * (μ + ℓ * (1 - μ)) ^ t := by ring diff --git a/Complexity/Foundations/Combinatorics/Hypergeometric.lean b/Complexity/Foundations/Combinatorics/Hypergeometric.lean index db38bfc881..2108083c4e 100644 --- a/Complexity/Foundations/Combinatorics/Hypergeometric.lean +++ b/Complexity/Foundations/Combinatorics/Hypergeometric.lean @@ -32,17 +32,42 @@ Chebyshev's inequality `X < m ≤ μ` with probability at most `μ / (μ - m)²` ## Main results -* `Finset.sum_card_inter_powersetCard`, `Finset.sum_card_inter_mul_sub_one_powersetCard`: the +* `Cslib.mul_card_filter_le_sum`, `Cslib.card_filter_mul_le_sum`: Markov's inequality for a + `Finset` sum. +* `Cslib.sum_card_inter_powersetCard`, `Cslib.sum_card_inter_mul_sub_one_powersetCard`: the first two factorial moments of `#(U ∩ J)` over the `ℓ`-subsets `J`. -* `Finset.sum_card_inter_sub_sq_le`: the variance is at most the mean. -* `Finset.card_filter_card_inter_lt_mul_sq_le`: Chebyshev's inequality. -* `Finset.two_mul_card_filter_card_inter_lt_le`: most `ℓ`-subsets meet `U` in at least half the +* `Cslib.sum_card_inter_sub_sq_le`: the variance is at most the mean. +* `Cslib.card_filter_card_inter_lt_mul_sq_le`: Chebyshev's inequality. +* `Cslib.two_mul_card_filter_card_inter_lt_le`: most `ℓ`-subsets meet `U` in at least half the expected number of elements. -/ @[expose] public section -namespace Finset +namespace Cslib + +open Finset + +/-- **Markov's inequality** for a `Finset` sum: if `m ≤ f x` whenever `x ∈ s` satisfies `p x`, +then `m * #{x ∈ s | p x} ≤ ∑ x ∈ s, f x`. -/ +theorem mul_card_filter_le_sum {α : Type*} (s : Finset α) (p : α → Prop) + [DecidablePred p] (f : α → ℕ) {m : ℕ} (hm : ∀ x ∈ s, p x → m ≤ f x) : + m * #{x ∈ s | p x} ≤ ∑ x ∈ s, f x := by + rw [mul_comm, ← smul_eq_mul] + exact ((s.filter p).card_nsmul_le_sum f m fun x hx => + hm x (mem_filter.mp hx).1 (mem_filter.mp hx).2).trans + (sum_le_sum_of_subset (filter_subset p s)) + +/-- **Markov's inequality** for a nonnegative `Finset` sum: if `0 ≤ f x` on `s` and `m ≤ f x` +whenever `x ∈ s` satisfies `p x`, then `#{x ∈ s | p x} * m ≤ ∑ x ∈ s, f x`. -/ +theorem card_filter_mul_le_sum {α R : Type*} [Semiring R] [PartialOrder R] [IsOrderedAddMonoid R] + (s : Finset α) (p : α → Prop) [DecidablePred p] (f : α → R) {m : R} + (hf : ∀ x ∈ s, 0 ≤ f x) (hm : ∀ x ∈ s, p x → m ≤ f x) : + (#{x ∈ s | p x} : R) * m ≤ ∑ x ∈ s, f x := by + rw [← nsmul_eq_mul] + exact ((s.filter p).card_nsmul_le_sum f m fun x hx => + hm x (mem_filter.mp hx).1 (mem_filter.mp hx).2).trans + (sum_le_sum_of_subset_of_nonneg (filter_subset p s) fun x hx _ => hf x hx) variable {α : Type*} [DecidableEq α] {s U : Finset α} {ℓ : ℕ} @@ -143,13 +168,55 @@ private theorem natCast_mul_natCast_sub_one (x : ℕ) : · push_cast [Nat.add_sub_cancel] ring +/-- The second factorial moment of `#(U ∩ J)` is at most the square of the first moment: +`(#s)² ∑_J #(U ∩ J) (#(U ∩ J) - 1) ≤ (#U)² ℓ² C(#s, ℓ)`. -/ +private theorem sq_card_mul_sum_card_inter_mul_sub_one_powersetCard_le (hU : U ⊆ s) : + (#s : ℝ) ^ 2 * ∑ J ∈ s.powersetCard ℓ, (#(U ∩ J) : ℝ) * ((#(U ∩ J) : ℝ) - 1) ≤ + (#U : ℝ) ^ 2 * (ℓ : ℝ) ^ 2 * (#s).choose ℓ := by + set P := s.powersetCard ℓ + set X : Finset α → ℝ := fun J => (#(U ∩ J) : ℝ) + set c : ℝ := (#s : ℝ) + set a : ℝ := (#U : ℝ) + set b : ℝ := (ℓ : ℝ) + set M : ℝ := ((#s).choose ℓ : ℝ) + have hM : 0 ≤ M := by positivity + have hS₂ : c * (c - 1) * ∑ J ∈ P, X J * (X J - 1) = a * (a - 1) * (b * (b - 1)) * M := by + have h := congrArg (Nat.cast (R := ℝ)) + (card_mul_sum_card_inter_mul_sub_one_powersetCard (ℓ := ℓ) hU) + simp only [Nat.cast_mul, Nat.cast_sum, natCast_mul_natCast_sub_one] at h + exact h + rcases Nat.lt_or_ge #s 2 with hs | hs + · rw [sum_eq_zero fun J _ => ?_] + · simp only [mul_zero] + positivity + have : #(U ∩ J) ≤ 1 := (card_le_card inter_subset_left).trans ((card_le_card hU).trans + (by omega)) + rcases Nat.le_one_iff_eq_zero_or_eq_one.1 this with h | h <;> simp [h] + have hc : (2 : ℝ) ≤ c := by simp only [c]; exact_mod_cast hs + have hac : a ≤ c := by simp only [a, c]; exact_mod_cast card_le_card hU + have ha : 0 ≤ a := by positivity + have hb : 0 ≤ b := by positivity + -- `(c - 1) a² b² - c a (a - 1) b (b - 1) = a b ((c - a) (b - 1) + a (c - 1)) ≥ 0` + have hfac : 0 ≤ a * b * ((c - a) * (b - 1) + a * (c - 1)) := by + rcases Nat.eq_zero_or_pos ℓ with h | h + · simp [b, h] + have hb1 : (1 : ℝ) ≤ b := by simp only [b]; exact_mod_cast h + exact mul_nonneg (mul_nonneg ha hb) (add_nonneg (mul_nonneg (sub_nonneg.2 hac) + (sub_nonneg.2 hb1)) (mul_nonneg ha (by linarith))) + have h₁ : (c - 1) * (c ^ 2 * ∑ J ∈ P, X J * (X J - 1)) ≤ (c - 1) * (a ^ 2 * b ^ 2 * M) := by + have : (c - 1) * (c ^ 2 * ∑ J ∈ P, X J * (X J - 1)) = + c * (a * (a - 1) * (b * (b - 1)) * M) := by + rw [← hS₂] + ring + rw [this] + nlinarith [mul_nonneg hM hfac] + exact le_of_mul_le_mul_left h₁ (by linarith) + /-- **The variance of `#(U ∩ J)` is at most its mean**: over the `ℓ`-subsets `J` of `s`, with `n = #s`, `∑_J (n #(U ∩ J) - #U ℓ)² ≤ n #U ℓ C(n, ℓ)`. -/ theorem sum_card_inter_sub_sq_le (hU : U ⊆ s) : ∑ J ∈ s.powersetCard ℓ, ((#s : ℝ) * #(U ∩ J) - #U * ℓ) ^ 2 ≤ #s * #U * ℓ * (#s).choose ℓ := by - rcases Nat.lt_or_ge #s ℓ with hℓs | hℓs - · simp [powersetCard_eq_empty.2 hℓs, Nat.choose_eq_zero_of_lt hℓs] set P := s.powersetCard ℓ set X : Finset α → ℝ := fun J => (#(U ∩ J) : ℝ) set c : ℝ := (#s : ℝ) @@ -157,53 +224,18 @@ theorem sum_card_inter_sub_sq_le (hU : U ⊆ s) : set b : ℝ := (ℓ : ℝ) set M : ℝ := ((#s).choose ℓ : ℝ) have hP : (#P : ℝ) = M := by simp [P, M] - have hM : 0 ≤ M := by positivity - -- the factorial moments have hS₁ : c * ∑ J ∈ P, X J = a * b * M := by have h := congrArg (Nat.cast (R := ℝ)) (card_mul_sum_card_inter_powersetCard (ℓ := ℓ) hU) simp only [Nat.cast_mul, Nat.cast_sum] at h exact h - have hS₂ : c * (c - 1) * ∑ J ∈ P, X J * (X J - 1) = a * (a - 1) * (b * (b - 1)) * M := by - have h := congrArg (Nat.cast (R := ℝ)) - (card_mul_sum_card_inter_mul_sub_one_powersetCard (ℓ := ℓ) hU) - simp only [Nat.cast_mul, Nat.cast_sum, natCast_mul_natCast_sub_one] at h - exact h - -- the sum of squares in terms of the factorial moments have hexp : ∑ J ∈ P, (c * X J - a * b) ^ 2 = c ^ 2 * ∑ J ∈ P, X J * (X J - 1) + (c - 2 * a * b) * (c * ∑ J ∈ P, X J) + #P * (a ^ 2 * b ^ 2) := by rw [sum_congr rfl fun J _ => show (c * X J - a * b) ^ 2 = c ^ 2 * (X J * (X J - 1)) + (c - 2 * a * b) * (c * X J) + a ^ 2 * b ^ 2 by ring] simp only [sum_add_distrib, ← mul_sum, sum_const, nsmul_eq_mul] ring - -- it remains to bound the second factorial moment - have hkey : c ^ 2 * ∑ J ∈ P, X J * (X J - 1) ≤ a ^ 2 * b ^ 2 * M := by - rcases Nat.lt_or_ge #s 2 with hs | hs - · -- `U ∩ J` has at most one element - rw [sum_eq_zero fun J _ => ?_] - · simp only [mul_zero] - positivity - have : #(U ∩ J) ≤ 1 := (card_le_card inter_subset_left).trans ((card_le_card hU).trans - (by omega)) - rcases Nat.le_one_iff_eq_zero_or_eq_one.1 this with h | h <;> simp [X, h] - have hc : (2 : ℝ) ≤ c := by simp only [c]; exact_mod_cast hs - have hac : a ≤ c := by simp only [a, c]; exact_mod_cast card_le_card hU - have ha : 0 ≤ a := by positivity - have hb : 0 ≤ b := by positivity - -- `(c - 1) a² b² - c a (a - 1) b (b - 1) = a b ((c - a) (b - 1) + a (c - 1)) ≥ 0` - have hfac : 0 ≤ a * b * ((c - a) * (b - 1) + a * (c - 1)) := by - rcases Nat.eq_zero_or_pos ℓ with h | h - · simp [b, h] - have hb1 : (1 : ℝ) ≤ b := by simp only [b]; exact_mod_cast h - exact mul_nonneg (mul_nonneg ha hb) (add_nonneg (mul_nonneg (sub_nonneg.2 hac) - (sub_nonneg.2 hb1)) (mul_nonneg ha (by linarith))) - have h₁ : (c - 1) * (c ^ 2 * ∑ J ∈ P, X J * (X J - 1)) ≤ (c - 1) * (a ^ 2 * b ^ 2 * M) := by - have : (c - 1) * (c ^ 2 * ∑ J ∈ P, X J * (X J - 1)) = - c * (a * (a - 1) * (b * (b - 1)) * M) := by - rw [← hS₂] - ring - rw [this] - nlinarith [mul_nonneg hM hfac] - exact le_of_mul_le_mul_left h₁ (by linarith) + have hkey : c ^ 2 * ∑ J ∈ P, X J * (X J - 1) ≤ a ^ 2 * b ^ 2 * M := + sq_card_mul_sum_card_inter_mul_sub_one_powersetCard_le hU change ∑ J ∈ P, (c * X J - a * b) ^ 2 ≤ c * a * b * M rw [hexp, hS₁, hP] nlinarith [hkey] @@ -214,11 +246,9 @@ the mean), the `ℓ`-subsets `J` of `s` meeting `U` in fewer than `m` elements n theorem card_filter_card_inter_lt_mul_sq_le (hU : U ⊆ s) {m : ℕ} (hm : #s * m ≤ #U * ℓ) : (#{J ∈ s.powersetCard ℓ | #(U ∩ J) < m} : ℝ) * ((#U : ℝ) * ℓ - #s * m) ^ 2 ≤ #s * #U * ℓ * (#s).choose ℓ := by - refine le_trans ?_ (sum_card_inter_sub_sq_le hU) - rw [← nsmul_eq_mul, ← sum_const] - refine (sum_le_sum fun J hJ => ?_).trans - (sum_le_sum_of_subset_of_nonneg (filter_subset _ _) fun _ _ _ => sq_nonneg _) - have hX : (#(U ∩ J) : ℝ) ≤ m := by exact_mod_cast (mem_filter.1 hJ).2.le + refine (card_filter_mul_le_sum _ _ _ (fun _ _ => sq_nonneg _) fun J _ hJ => ?_).trans + (sum_card_inter_sub_sq_le hU) + have hX : (#(U ∩ J) : ℝ) ≤ m := by exact_mod_cast hJ.le have hmR : (#s : ℝ) * m ≤ #U * ℓ := by exact_mod_cast hm have hcX : (#s : ℝ) * #(U ∩ J) ≤ #s * m := mul_le_mul_of_nonneg_left hX (by positivity) calc ((#U : ℝ) * ℓ - #s * m) ^ 2 ≤ (#U * ℓ - #s * #(U ∩ J)) ^ 2 := @@ -254,4 +284,4 @@ theorem two_mul_card_filter_card_inter_lt_le (hU : U ⊆ s) (hs : 0 < #s) le_of_mul_le_mul_right (by nlinarith : K * μ * μ ≤ 4 * c * M * μ) hμ0 exact le_of_mul_le_mul_left (by nlinarith : 4 * c * (2 * K) ≤ 4 * c * M) (by linarith) -end Finset +end Cslib diff --git a/Complexity/Foundations/Combinatorics/PowersetTail.lean b/Complexity/Foundations/Combinatorics/PowersetTail.lean index e9e9a59479..2a3fc08b8e 100644 --- a/Complexity/Foundations/Combinatorics/PowersetTail.lean +++ b/Complexity/Foundations/Combinatorics/PowersetTail.lean @@ -11,6 +11,7 @@ public import Complexity.Init public import Mathlib.Data.Finset.Powerset public import Mathlib.Algebra.BigOperators.Group.Finset.Defs public import Mathlib.Basic.Real.Basic +import Complexity.Foundations.Combinatorics.Hypergeometric import Mathlib.Algebra.BigOperators.Ring.Finset import Mathlib.Algebra.Group.Action.Defs import Mathlib.Algebra.Order.BigOperators.Group.Finset @@ -25,26 +26,26 @@ import Mathlib.Tactic.Ring A uniformly random subset `x` of a finite set `S` meets a fixed `K ⊆ S` in about `#K / 2` points. Weighting each subset `x` by `2 ^ #(K \ x)` gives total weight `3 ^ #K 2 ^ #(S \ K)` -(`Finset.sum_powerset_two_pow_card_sdiff`), and every subset meeting `K` in at most `j` points has +(`Cslib.sum_powerset_two_pow_card_sdiff`), and every subset meeting `K` in at most `j` points has weight at least `2 ^ (#K - j)`. So at most a `(3 / 4) ^ #K 2 ^ j` fraction of the subsets of `S` -meet `K` in at most `j` points (`Finset.two_pow_mul_card_filter_card_inter_le`); for instance at +meet `K` in at most `j` points (`Cslib.two_pow_mul_card_filter_card_inter_le`); for instance at most a `(27 / 32) ^ r / 2` fraction meet a set of `3 r` points in fewer than `r` points. Weighting by `2 ^ #x` instead bounds the subsets missing at most `j` points of `S` -(`Finset.two_pow_mul_card_filter_card_sdiff_le`). This is the exponential-moment (Chernoff) bound +(`Cslib.two_pow_mul_card_filter_card_sdiff_le`). This is the exponential-moment (Chernoff) bound with the single weight `2` [Alon and Spencer, Appendix A][AlonSpencer2016], stated by counting; for the subsets of `K` itself, Hoeffding's bound for fair coins (`Cslib.BitString.card_filter_le_card_filter_sub_half_le`) is sharper. A family of sets for which many points of `S` are avoided by most of its members inside `S` is -therefore small (`Finset.four_mul_sum_card_filter_notMem_le`): by Markov's inequality, many of its +therefore small (`Cslib.four_mul_sum_card_filter_notMem_le`): by Markov's inequality, many of its members meet the avoided points in few points, or miss few points of `S`. This is the counting step of Razborov's corruption bound for disjointness [Razborov1992]. ## Main results -* `Finset.two_pow_mul_card_filter_card_inter_le`: few subsets of `S` meet `K` in few points. -* `Finset.two_pow_mul_card_filter_card_sdiff_le`: few subsets of `S` miss few of its points. -* `Finset.four_mul_sum_card_filter_notMem_le`: families avoiding many points are small. +* `Cslib.two_pow_mul_card_filter_card_inter_le`: few subsets of `S` meet `K` in few points. +* `Cslib.two_pow_mul_card_filter_card_sdiff_le`: few subsets of `S` miss few of its points. +* `Cslib.four_mul_sum_card_filter_notMem_le`: families avoiding many points are small. ## References @@ -54,7 +55,9 @@ step of Razborov's corruption bound for disjointness [Razborov1992]. @[expose] public section -namespace Finset +namespace Cslib + +open Finset variable {U : Type*} [DecidableEq U] @@ -87,12 +90,9 @@ theorem sum_powerset_two_pow_card_sdiff {K S : Finset U} (hKS : K ⊆ S) : most `3 ^ #K 2 ^ #(S \ K)`. -/ theorem two_pow_mul_card_filter_card_inter_le {K S : Finset U} (hKS : K ⊆ S) (j : ℕ) : 2 ^ (#K - j) * #{x ∈ S.powerset | #(K ∩ x) ≤ j} ≤ 3 ^ #K * 2 ^ (#S - #K) := by - rw [← sum_powerset_two_pow_card_sdiff hKS, mul_comm, ← smul_eq_mul] - refine (card_nsmul_le_sum _ _ _ fun x hx => ?_).trans - (sum_le_sum_of_subset_of_nonneg (filter_subset _ _) fun _ _ _ => Nat.zero_le _) - refine Nat.pow_le_pow_right (Nat.succ_pos 1) ?_ + rw [← sum_powerset_two_pow_card_sdiff hKS] + refine mul_card_filter_le_sum _ _ _ fun x _ hx => Nat.pow_le_pow_right (Nat.succ_pos 1) ?_ have h := card_sdiff_add_card_inter K x - have := (mem_filter.mp hx).2 omega /-- Few subsets of `S` miss at most `j` of its points: `2 ^ (#S - j)` times their number is at @@ -101,16 +101,112 @@ theorem two_pow_mul_card_filter_card_sdiff_le (S : Finset U) (j : ℕ) : 2 ^ (#S - j) * #{x ∈ S.powerset | #(S \ x) ≤ j} ≤ 3 ^ #S := by have h := sum_pow_mul_eq_add_pow (2 : ℕ) 1 S simp only [one_pow, mul_one] at h - rw [show (3 : ℕ) = 2 + 1 from rfl, ← h, mul_comm, ← smul_eq_mul] - refine (card_nsmul_le_sum _ _ _ fun x hx => ?_).trans - (sum_le_sum_of_subset_of_nonneg (filter_subset _ _) fun _ _ _ => Nat.zero_le _) - refine Nat.pow_le_pow_right (Nat.succ_pos 1) ?_ - obtain ⟨hx, hj⟩ := mem_filter.mp hx + rw [show (3 : ℕ) = 2 + 1 from rfl, ← h] + refine mul_card_filter_le_sum _ _ _ fun x hx hj => Nat.pow_le_pow_right (Nat.succ_pos 1) ?_ have := card_sdiff_add_card_eq_card (mem_powerset.mp hx) omega /-! ### Families of sets that avoid many points -/ +/-- If `S` contains at least `3 * r` points `i` with `4 * #{x ∈ AS | i ∈ x} ≤ #AS`, where +`AS = A.filter (· ⊆ S)`, then `#AS * 32 ^ r ≤ 2 * 27 ^ r * 2 ^ #S`. -/ +private theorem card_filter_subset_mul_pow_le (A : Finset (Finset U)) (S : Finset U) {r : ℕ} + (hbad : 3 * r ≤ #{i ∈ S | 4 * #{x ∈ A.filter (· ⊆ S) | i ∈ x} ≤ #(A.filter (· ⊆ S))}) : + #(A.filter (· ⊆ S)) * 32 ^ r ≤ 2 * 27 ^ r * 2 ^ #S := by + set AS := A.filter (· ⊆ S) + have hASsub : AS ⊆ S.powerset := fun x hx => mem_powerset.mpr (mem_filter.mp hx).2 + rcases Nat.eq_zero_or_pos r with rfl | hr + · have := (card_le_card hASsub).trans (card_powerset S).le + simp only [pow_zero, mul_one]; omega + obtain ⟨K, hKbad, hKcard⟩ := exists_subset_card_eq hbad + have hKS : K ⊆ S := hKbad.trans (filter_subset _ _) + have h4sum : 4 * ∑ x ∈ AS, #(K ∩ x) ≤ 3 * r * #AS := by + have hsumK : ∑ i ∈ K, #{x ∈ AS | i ∈ x} = ∑ x ∈ AS, #(K ∩ x) := by + rw [show ∑ i ∈ K, #{x ∈ AS | i ∈ x} = ∑ x ∈ AS, #{i ∈ K | i ∈ x} from + sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow _] + exact sum_congr rfl fun x _ => by rw [filter_mem_eq_inter] + rw [← hsumK, mul_sum] + calc ∑ i ∈ K, 4 * #{x ∈ AS | i ∈ x} ≤ ∑ _i ∈ K, #AS := + sum_le_sum fun i hi => (mem_filter.mp (hKbad hi)).2 + _ = 3 * r * #AS := by rw [sum_const, hKcard, smul_eq_mul] + have hG : r * #{x ∈ AS | r ≤ #(K ∩ x)} ≤ ∑ x ∈ AS, #(K ∩ x) := + mul_card_filter_le_sum _ _ _ fun _ _ => id + have h4G : 4 * #{x ∈ AS | r ≤ #(K ∩ x)} ≤ 3 * #AS := Nat.le_of_mul_le_mul_left (by nlinarith) hr + have hGL : #{x ∈ AS | r ≤ #(K ∩ x)} + #{x ∈ AS | ¬r ≤ #(K ∩ x)} = #AS := + card_filter_add_card_filter_not _ + have hL : #{x ∈ AS | ¬r ≤ #(K ∩ x)} ≤ #{x ∈ S.powerset | #(K ∩ x) ≤ r - 1} := + card_le_card fun x hx => mem_filter.mpr ⟨hASsub (mem_filter.mp hx).1, by + have := (mem_filter.mp hx).2; omega⟩ + have hcount := two_pow_mul_card_filter_card_inter_le hKS (r - 1) + rw [hKcard, show 3 * r - (r - 1) = 2 * r + 1 by omega] at hcount + have key : 2 ^ (2 * r + 1) * #AS ≤ 4 * (3 ^ (3 * r) * 2 ^ (#S - 3 * r)) := + (Nat.mul_le_mul_left _ (show #AS ≤ 4 * #{x ∈ S.powerset | #(K ∩ x) ≤ r - 1} by omega)).trans + (by rw [mul_left_comm]; exact Nat.mul_le_mul_left _ hcount) + have h2S : 2 ^ (#S - 3 * r) * 2 ^ (3 * r) = 2 ^ #S := by + rw [← pow_add, Nat.sub_add_cancel (hKcard ▸ card_le_card hKS)] + have h32 : (32 : ℕ) ^ r = 2 ^ (2 * r) * 2 ^ (3 * r) := by + rw [← pow_add, show 2 * r + 3 * r = 5 * r by ring, pow_mul]; norm_num + have h27 : (27 : ℕ) ^ r = 3 ^ (3 * r) := by rw [pow_mul]; norm_num + rw [h32, h27]; refine Nat.le_of_mul_le_mul_left ?_ (two_pos : 0 < 2) + calc 2 * (#AS * (2 ^ (2 * r) * 2 ^ (3 * r))) = 2 ^ (2 * r + 1) * #AS * 2 ^ (3 * r) := by ring + _ ≤ 4 * (3 ^ (3 * r) * 2 ^ (#S - 3 * r)) * 2 ^ (3 * r) := Nat.mul_le_mul_right _ key + _ = 2 * (2 * 3 ^ (3 * r) * (2 ^ (#S - 3 * r) * 2 ^ (3 * r))) := by ring + _ = 2 * (2 * 3 ^ (3 * r) * 2 ^ #S) := by rw [h2S] + +/-- In `ℝ`, the subsets of `S` missing at most `j` points number at most +`2 ^ #S * (2 ^ j * (3 / 4) ^ #S)`. -/ +private theorem card_filter_card_sdiff_le_real (S : Finset U) (j : ℕ) : + (#{x ∈ S.powerset | #(S \ x) ≤ j} : ℝ) ≤ 2 ^ #S * (2 ^ j * (3 / 4) ^ #S) := by + have hcount : 2 ^ #S * #{x ∈ S.powerset | #(S \ x) ≤ j} ≤ 2 ^ j * 3 ^ #S := + calc 2 ^ #S * #{x ∈ S.powerset | #(S \ x) ≤ j} + ≤ 2 ^ j * 2 ^ (#S - j) * #{x ∈ S.powerset | #(S \ x) ≤ j} := + Nat.mul_le_mul_right _ (by + rw [← pow_add] + exact Nat.pow_le_pow_right two_pos (by omega)) + _ ≤ 2 ^ j * 3 ^ #S := by + rw [mul_assoc] + exact Nat.mul_le_mul_left _ (two_pow_mul_card_filter_card_sdiff_le S j) + have hcountR : (2 : ℝ) ^ #S * #{x ∈ S.powerset | #(S \ x) ≤ j} ≤ 2 ^ j * 3 ^ #S := by + exact_mod_cast hcount + have h34 : (2 : ℝ) ^ #S * (2 ^ #S * (2 ^ j * (3 / 4) ^ #S)) = 2 ^ j * 3 ^ #S := by + calc (2 : ℝ) ^ #S * (2 ^ #S * (2 ^ j * (3 / 4) ^ #S)) + = 2 ^ j * ((2 * (2 * (3 / 4))) ^ #S) := by rw [mul_pow, mul_pow]; ring + _ = 2 ^ j * 3 ^ #S := by norm_num + exact le_of_mul_le_mul_left (hcountR.trans_eq h34.symm) (by positivity) + +/-- If `4 * #bad ≤ j + 1`, then `4` times the sum of avoidance counts over `bad` is at most the +sum over `S` plus `(j + 1) * #{x ∈ S.powerset | #(S \ x) ≤ j}`. -/ +private theorem four_mul_sum_bad_le_sum_add (A : Finset (Finset U)) (S : Finset U) {j : ℕ} + {bad : Finset U} (hbad : 4 * #bad ≤ j + 1) : + 4 * ∑ i ∈ bad, #{x ∈ A | x ⊆ S ∧ i ∉ x} ≤ + ∑ i ∈ S, #{x ∈ A | x ⊆ S ∧ i ∉ x} + (j + 1) * #{x ∈ S.powerset | #(S \ x) ≤ j} := by + set AS := A.filter (· ⊆ S) with hAS + have hASsub : AS ⊆ S.powerset := fun x hx => mem_powerset.mpr (mem_filter.mp hx).2 + have havoid (i : U) : #{x ∈ A | x ⊆ S ∧ i ∉ x} = #{x ∈ AS | i ∉ x} := by rw [hAS, filter_filter] + have hsum_bad : ∑ i ∈ bad, #{x ∈ A | x ⊆ S ∧ i ∉ x} ≤ #bad * #AS := + (sum_le_sum fun i _ => (show #{x ∈ A | x ⊆ S ∧ i ∉ x} ≤ #AS by + rw [havoid]; exact card_filter_le _ _)).trans_eq (by rw [sum_const, smul_eq_mul]) + have hS : ∑ i ∈ S, #{x ∈ A | x ⊆ S ∧ i ∉ x} = ∑ x ∈ AS, #(S \ x) := by + simp only [havoid] + rw [show ∑ i ∈ S, #{x ∈ AS | i ∉ x} = ∑ x ∈ AS, #{i ∈ S | i ∉ x} from + sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow _] + exact sum_congr rfl fun x _ => by rw [sdiff_eq_filter] + have hH : (j + 1) * #{x ∈ AS | j < #(S \ x)} ≤ ∑ x ∈ AS, #(S \ x) := + mul_card_filter_le_sum _ _ _ fun _ _ => id + have hHH : #{x ∈ AS | j < #(S \ x)} + #{x ∈ AS | ¬j < #(S \ x)} = #AS := + card_filter_add_card_filter_not _ + have hH' : #{x ∈ AS | ¬j < #(S \ x)} ≤ #{x ∈ S.powerset | #(S \ x) ≤ j} := + card_le_card fun x hx => mem_filter.mpr ⟨hASsub (mem_filter.mp hx).1, by + have := (mem_filter.mp hx).2; omega⟩ + rw [hS] + calc 4 * ∑ i ∈ bad, #{x ∈ A | x ⊆ S ∧ i ∉ x} ≤ 4 * (#bad * #AS) := + Nat.mul_le_mul_left _ hsum_bad + _ ≤ (j + 1) * #AS := by rw [← mul_assoc]; exact Nat.mul_le_mul_right _ hbad + _ = (j + 1) * #{x ∈ AS | j < #(S \ x)} + (j + 1) * #{x ∈ AS | ¬j < #(S \ x)} := by + rw [← hHH, mul_add] + _ ≤ ∑ x ∈ AS, #(S \ x) + (j + 1) * #{x ∈ S.powerset | #(S \ x) ≤ j} := + Nat.add_le_add hH (Nat.mul_le_mul_left _ hH') + /-- **A family of sets that avoid many points is small.** Let `A` be a family of sets and `S` a finite set, and call a point `i ∈ S` *bad* if the members of `A` inside `S` containing `i` are fewer than a third of those avoiding it. Then the pairs of a member of `A` inside `S` and a bad @@ -130,158 +226,44 @@ theorem four_mul_sum_card_filter_notMem_le (A : Finset (Finset U)) (S : Finset U (#{x ∈ A | x ⊆ S ∧ i ∉ x} : ℝ) ≤ ∑ i ∈ S, (#{x ∈ A | x ⊆ S ∧ i ∉ x} : ℝ) + 2 ^ #S * (8 * #S * (27 / 32) ^ r + (j + 1) * 2 ^ j * (3 / 4) ^ #S) := by - set AS := A.filter (· ⊆ S) with hAS - set N := #AS with hNdef - have hASsub : AS ⊆ S.powerset := fun x hx => mem_powerset.mpr (mem_filter.mp hx).2 - have hN : N ≤ 2 ^ #S := (card_le_card hASsub).trans (card_powerset S).le - have havoid (i : U) : #{x ∈ A | x ⊆ S ∧ i ∉ x} = #{x ∈ AS | i ∉ x} := by - rw [hAS, filter_filter] - have hcontain (i : U) : #{x ∈ A | i ∈ x ∧ x ⊆ S} = #{x ∈ AS | i ∈ x} := by - rw [hAS, filter_filter] - congr 1 - exact filter_congr fun x _ => and_comm + set AS := A.filter (· ⊆ S) with hAS; set N := #AS + have havoid (i : U) : #{x ∈ A | x ⊆ S ∧ i ∉ x} = #{x ∈ AS | i ∉ x} := by rw [hAS, filter_filter] have hsplit (i : U) : #{x ∈ AS | i ∈ x} + #{x ∈ AS | i ∉ x} = N := card_filter_add_card_filter_not _ - have havoid_le (i : U) : #{x ∈ A | x ⊆ S ∧ i ∉ x} ≤ N := by - have := hsplit i - rw [havoid] - omega set bad := S.filter fun i => 3 * #{x ∈ A | i ∈ x ∧ x ⊆ S} < #{x ∈ A | x ⊆ S ∧ i ∉ x} - with hbaddef - have hsum_bad : ∑ i ∈ bad, #{x ∈ A | x ⊆ S ∧ i ∉ x} ≤ #bad * N := - (sum_le_sum fun i _ => havoid_le i).trans_eq (by rw [sum_const, smul_eq_mul]) have hpos : (0 : ℝ) ≤ ∑ i ∈ S, (#{x ∈ A | x ⊆ S ∧ i ∉ x} : ℝ) := sum_nonneg fun _ _ => Nat.cast_nonneg _ by_cases hbad : 3 * r ≤ #bad · -- Many bad points: the family is small. + have hsum_bad : ∑ i ∈ bad, #{x ∈ A | x ⊆ S ∧ i ∉ x} ≤ #bad * N := + (sum_le_sum fun i _ => (show #{x ∈ A | x ⊆ S ∧ i ∉ x} ≤ N by + rw [havoid]; exact card_filter_le _ _)).trans_eq (by rw [sum_const, smul_eq_mul]) have hsmall : N * 32 ^ r ≤ 2 * 27 ^ r * 2 ^ #S := by - rcases Nat.eq_zero_or_pos r with rfl | hr - · simp only [pow_zero, mul_one] - omega - obtain ⟨K, hKbad, hKcard⟩ := exists_subset_card_eq hbad - have hKS : K ⊆ S := hKbad.trans (filter_subset _ _) - have hK4 (i : U) (hi : i ∈ K) : 4 * #{x ∈ AS | i ∈ x} ≤ N := by - have := (mem_filter.mp (hKbad hi)).2 - have := hsplit i - rw [hcontain, havoid] at * - omega - have hsumK : ∑ i ∈ K, #{x ∈ AS | i ∈ x} = ∑ x ∈ AS, #(K ∩ x) := by - rw [show ∑ i ∈ K, #{x ∈ AS | i ∈ x} = ∑ x ∈ AS, #{i ∈ K | i ∈ x} from - sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow _] - exact sum_congr rfl fun x _ => by rw [filter_mem_eq_inter] - have h4sum : 4 * ∑ x ∈ AS, #(K ∩ x) ≤ 3 * r * N := by - rw [← hsumK, mul_sum] - calc ∑ i ∈ K, 4 * #{x ∈ AS | i ∈ x} ≤ ∑ _i ∈ K, N := sum_le_sum hK4 - _ = 3 * r * N := by rw [sum_const, hKcard, smul_eq_mul] - -- Markov's inequality: few members meet `K` in at least `r` points. - set G := AS.filter fun x => r ≤ #(K ∩ x) - have hG : r * #G ≤ ∑ x ∈ AS, #(K ∩ x) := by - rw [mul_comm, ← smul_eq_mul] - exact (card_nsmul_le_sum _ _ _ fun x hx => (mem_filter.mp hx).2).trans - (sum_le_sum_of_subset_of_nonneg (filter_subset _ _) fun _ _ _ => Nat.zero_le _) - have h4G : 4 * #G ≤ 3 * N := - Nat.le_of_mul_le_mul_left (by nlinarith) hr - have hGL : #G + #{x ∈ AS | ¬r ≤ #(K ∩ x)} = N := card_filter_add_card_filter_not _ - have hL : #{x ∈ AS | ¬r ≤ #(K ∩ x)} ≤ #{x ∈ S.powerset | #(K ∩ x) ≤ r - 1} := by - refine card_le_card fun x hx => ?_ - obtain ⟨hx, hxr⟩ := mem_filter.mp hx - exact mem_filter.mpr ⟨hASsub hx, by omega⟩ - have hcount := two_pow_mul_card_filter_card_inter_le hKS (r - 1) - rw [hKcard, show 3 * r - (r - 1) = 2 * r + 1 by omega] at hcount - have h3r : 3 * r ≤ #S := hKcard ▸ card_le_card hKS - have key : 2 ^ (2 * r + 1) * N ≤ 4 * (3 ^ (3 * r) * 2 ^ (#S - 3 * r)) := by - calc 2 ^ (2 * r + 1) * N ≤ 2 ^ (2 * r + 1) * (4 * #{x ∈ S.powerset | #(K ∩ x) ≤ r - 1}) := - Nat.mul_le_mul_left _ (by omega) - _ ≤ 4 * (3 ^ (3 * r) * 2 ^ (#S - 3 * r)) := by - rw [mul_left_comm] - exact Nat.mul_le_mul_left _ hcount - have h2S : 2 ^ (#S - 3 * r) * 2 ^ (3 * r) = 2 ^ #S := by - rw [← pow_add, Nat.sub_add_cancel h3r] - have h32 : (32 : ℕ) ^ r = 2 ^ (2 * r) * 2 ^ (3 * r) := by - rw [← pow_add, show 2 * r + 3 * r = 5 * r by ring, pow_mul] - norm_num - have h27 : (27 : ℕ) ^ r = 3 ^ (3 * r) := by - rw [pow_mul] - norm_num - have h := Nat.mul_le_mul_right (2 ^ (3 * r)) key - rw [h32, h27] - refine Nat.le_of_mul_le_mul_left ?_ (two_pos : 0 < 2) - calc 2 * (N * (2 ^ (2 * r) * 2 ^ (3 * r))) = 2 ^ (2 * r + 1) * N * 2 ^ (3 * r) := by ring - _ ≤ 4 * (3 ^ (3 * r) * 2 ^ (#S - 3 * r)) * 2 ^ (3 * r) := h - _ = 2 * (2 * 3 ^ (3 * r) * (2 ^ (#S - 3 * r) * 2 ^ (3 * r))) := by ring - _ = 2 * (2 * 3 ^ (3 * r) * 2 ^ #S) := by rw [h2S] + refine card_filter_subset_mul_pow_le A S (hbad.trans (card_le_card fun i hi => ?_)) + obtain ⟨hiS, hlt⟩ := mem_filter.mp hi + have hcontain : #{x ∈ A | i ∈ x ∧ x ⊆ S} = #{x ∈ AS | i ∈ x} := by + rw [hAS, filter_filter]; exact congrArg card (filter_congr fun _ _ => and_comm) + rw [hcontain, havoid] at hlt; have := hsplit i + exact mem_filter.mpr ⟨hiS, by rw [← hAS]; omega⟩ have hNr : (N : ℝ) ≤ 2 * (27 / 32) ^ r * 2 ^ #S := by have h : (N : ℝ) * 32 ^ r ≤ 2 * 27 ^ r * 2 ^ #S := by exact_mod_cast hsmall - rw [div_pow, mul_div_assoc', div_mul_eq_mul_div, le_div_iff₀ (by positivity)] - linarith - have hbadS : #bad ≤ #S := card_le_card (filter_subset _ _) - have h1 : (∑ i ∈ bad, (#{x ∈ A | x ⊆ S ∧ i ∉ x} : ℝ)) ≤ #S * N := by - have : (∑ i ∈ bad, (#{x ∈ A | x ⊆ S ∧ i ∉ x} : ℝ)) ≤ #bad * N := by - exact_mod_cast hsum_bad - exact this.trans (mul_le_mul_of_nonneg_right (by exact_mod_cast hbadS) (by positivity)) + rw [div_pow, mul_div_assoc', div_mul_eq_mul_div, le_div_iff₀ (by positivity)]; linarith + have h1 : (∑ i ∈ bad, (#{x ∈ A | x ⊆ S ∧ i ∉ x} : ℝ)) ≤ #S * N := + (by exact_mod_cast hsum_bad : (∑ i ∈ bad, (#{x ∈ A | x ⊆ S ∧ i ∉ x} : ℝ)) ≤ #bad * N).trans + (mul_le_mul_of_nonneg_right (by exact_mod_cast card_le_card (filter_subset _ S)) + (by positivity)) have h2 : (0 : ℝ) ≤ 2 ^ #S * ((j + 1) * 2 ^ j * (3 / 4) ^ #S) := by positivity have h3 : (#S : ℝ) * N ≤ #S * (2 * (27 / 32) ^ r * 2 ^ #S) := mul_le_mul_of_nonneg_left hNr (by positivity) nlinarith · -- Few bad points: most members of the family avoid many points. - push Not at hbad - have hS : ∑ i ∈ S, #{x ∈ A | x ⊆ S ∧ i ∉ x} = ∑ x ∈ AS, #(S \ x) := by - simp only [havoid] - rw [show ∑ i ∈ S, #{x ∈ AS | i ∉ x} = ∑ x ∈ AS, #{i ∈ S | i ∉ x} from - sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow _] - exact sum_congr rfl fun x _ => by rw [sdiff_eq_filter] - set H := AS.filter fun x => j < #(S \ x) - have hH : (j + 1) * #H ≤ ∑ x ∈ AS, #(S \ x) := by - rw [mul_comm, ← smul_eq_mul] - exact (card_nsmul_le_sum _ _ _ fun x hx => (mem_filter.mp hx).2).trans - (sum_le_sum_of_subset_of_nonneg (filter_subset _ _) fun _ _ _ => Nat.zero_le _) - have hHH : #H + #{x ∈ AS | ¬j < #(S \ x)} = N := card_filter_add_card_filter_not _ - have hH' : #{x ∈ AS | ¬j < #(S \ x)} ≤ #{x ∈ S.powerset | #(S \ x) ≤ j} := by - refine card_le_card fun x hx => ?_ - obtain ⟨hx, hxj⟩ := mem_filter.mp hx - exact mem_filter.mpr ⟨hASsub hx, by omega⟩ - have hcount := two_pow_mul_card_filter_card_sdiff_le S j - have hcount' : 2 ^ #S * #{x ∈ S.powerset | #(S \ x) ≤ j} ≤ 2 ^ j * 3 ^ #S := by - calc 2 ^ #S * #{x ∈ S.powerset | #(S \ x) ≤ j} - ≤ 2 ^ j * 2 ^ (#S - j) * #{x ∈ S.powerset | #(S \ x) ≤ j} := - Nat.mul_le_mul_right _ (by - rw [← pow_add] - exact Nat.pow_le_pow_right two_pos (by omega)) - _ ≤ 2 ^ j * 3 ^ #S := by rw [mul_assoc]; exact Nat.mul_le_mul_left _ hcount - -- The bad points carry at most `3 r N ≤ (j + 1) N / 4` incidences. - have hmain : 4 * ∑ i ∈ bad, #{x ∈ A | x ⊆ S ∧ i ∉ x} ≤ - ∑ i ∈ S, #{x ∈ A | x ⊆ S ∧ i ∉ x} + (j + 1) * #{x ∈ S.powerset | #(S \ x) ≤ j} := by - rw [hS] - have h12 : 4 * (#bad * N) ≤ (j + 1) * N := by - rw [← mul_assoc] - exact Nat.mul_le_mul_right _ (by omega) - calc 4 * ∑ i ∈ bad, #{x ∈ A | x ⊆ S ∧ i ∉ x} ≤ 4 * (#bad * N) := - Nat.mul_le_mul_left _ hsum_bad - _ ≤ (j + 1) * N := h12 - _ = (j + 1) * #H + (j + 1) * #{x ∈ AS | ¬j < #(S \ x)} := by rw [← hHH, mul_add] - _ ≤ ∑ x ∈ AS, #(S \ x) + (j + 1) * #{x ∈ S.powerset | #(S \ x) ≤ j} := - Nat.add_le_add hH (Nat.mul_le_mul_left _ hH') have hmainR : 4 * ∑ i ∈ bad, (#{x ∈ A | x ⊆ S ∧ i ∉ x} : ℝ) ≤ ∑ i ∈ S, (#{x ∈ A | x ⊆ S ∧ i ∉ x} : ℝ) + (j + 1) * #{x ∈ S.powerset | #(S \ x) ≤ j} := by - exact_mod_cast hmain - have hcountR : (2 : ℝ) ^ #S * #{x ∈ S.powerset | #(S \ x) ≤ j} ≤ 2 ^ j * 3 ^ #S := by - exact_mod_cast hcount' - have h34 : (2 : ℝ) ^ #S * (2 ^ #S * (3 / 4) ^ #S) = 3 ^ #S := by - rw [← mul_assoc, ← mul_pow, ← mul_pow] - norm_num - have hQ : ((j : ℝ) + 1) * #{x ∈ S.powerset | #(S \ x) ≤ j} ≤ - 2 ^ #S * ((j + 1) * 2 ^ j * (3 / 4) ^ #S) := by - have h2pos : (0 : ℝ) < 2 ^ #S := by positivity - rw [← mul_le_mul_iff_of_pos_left h2pos] - calc (2 : ℝ) ^ #S * (((j : ℝ) + 1) * #{x ∈ S.powerset | #(S \ x) ≤ j}) - = ((j : ℝ) + 1) * (2 ^ #S * #{x ∈ S.powerset | #(S \ x) ≤ j}) := by ring - _ ≤ ((j : ℝ) + 1) * (2 ^ j * 3 ^ #S) := - mul_le_mul_of_nonneg_left hcountR (by positivity) - _ = 2 ^ #S * (2 ^ #S * ((j + 1) * 2 ^ j * (3 / 4) ^ #S)) := by - rw [← h34] - ring + exact_mod_cast four_mul_sum_bad_le_sum_add A S (bad := bad) (by omega) + have hQ := mul_le_mul_of_nonneg_left (card_filter_card_sdiff_le_real S j) + (by positivity : (0 : ℝ) ≤ j + 1) have h8 : (0 : ℝ) ≤ 2 ^ #S * (8 * #S * (27 / 32) ^ r) := by positivity nlinarith -end Finset +end Cslib diff --git a/Complexity/Foundations/Data/Code/LocalListDecoding.lean b/Complexity/Foundations/Data/Code/LocalListDecoding.lean index 2527ebe392..4563c74e27 100644 --- a/Complexity/Foundations/Data/Code/LocalListDecoding.lean +++ b/Complexity/Foundations/Data/Code/LocalListDecoding.lean @@ -9,6 +9,7 @@ module public import Complexity.Foundations.Data.Code.HintDecoding public import Complexity.Foundations.Data.Code.LocalDecoding +import Complexity.Foundations.Combinatorics.Hypergeometric import Mathlib.Tactic.Linarith import Mathlib.Tactic.Positivity @@ -153,122 +154,114 @@ private theorem card_seeds_mem_mem (A : Finset (Fin m → F)) {t t' : F} (htt : obtain ⟨h₁, h₂⟩ := line_through hsub y y' exact Prod.ext h₁ h₂ -/-- **Random lines sample a set well.** Over all points `x` and nonzero directions `u`, the -number of pairs for which the line `t ↦ x + t • u` has at most `D` points in `A` is at most -`q * a * (Q - 1) / (μ - D) ^ 2`, where `a = #A`, `Q = q ^ m` and `μ = q * a / Q > D` is the mean -number of points of a line in `A`. -/ -theorem card_filter_lineAgree_le_mul_sq_le (A : Finset (Fin m → F)) {D : ℝ} - (hD : D < Fintype.card F * #A / Fintype.card F ^ m) : - (#{xu : (Fin m → F) × (Fin m → F) | xu.2 ≠ 0 ∧ (lineAgree A xu.1 xu.2 : ℝ) ≤ D} : ℝ) * - (Fintype.card F * #A / Fintype.card F ^ m - D) ^ 2 ≤ +/-- The first moment of `lineAgree A` over `seeds m F`. -/ +private theorem sum_lineAgree_seeds (A : Finset (Fin m → F)) : + ∑ xu ∈ seeds m F, (lineAgree A xu.1 xu.2 : ℝ) = + Fintype.card F * (#A * ((Fintype.card F : ℝ) ^ m - 1)) := by + have hN (xu : (Fin m → F) × (Fin m → F)) : + (lineAgree A xu.1 xu.2 : ℝ) = ∑ t : F, if xu.1 + t • xu.2 ∈ A then (1 : ℝ) else 0 := by + simp [lineAgree, sum_boole] + simp only [hN] + rw [sum_comm] + simp only [sum_boole] + rw [sum_congr rfl fun t _ => by rw [card_seeds_mem A t], sum_const, card_univ, nsmul_eq_mul, + Nat.cast_mul, Nat.cast_sub (Nat.one_le_pow _ _ Fintype.card_pos)] + simp + +/-- The second moment of `lineAgree A` over `seeds m F`. -/ +private theorem sum_lineAgree_sq_seeds (A : Finset (Fin m → F)) : + ∑ xu ∈ seeds m F, (lineAgree A xu.1 xu.2 : ℝ) ^ 2 = + Fintype.card F * (#A * ((Fintype.card F : ℝ) ^ m - 1)) + + Fintype.card F * (Fintype.card F - 1) * (#A * #A - #A) := by + have hdiagN (t : F) : ∑ t' : F, + #{xu ∈ seeds m F | xu.1 + t • xu.2 ∈ A ∧ xu.1 + t' • xu.2 ∈ A} = + #A * (Fintype.card F ^ m - 1) + (Fintype.card F - 1) * (#A * #A - #A) := by + rw [← add_sum_erase _ _ (mem_univ t)] + simp only [and_self, card_seeds_mem A t] + rw [sum_congr rfl fun t' ht' => card_seeds_mem_mem A (Ne.symm (ne_of_mem_erase ht')), + sum_const, card_erase_of_mem (mem_univ _), card_univ, smul_eq_mul] + have hsq (xu : (Fin m → F) × (Fin m → F)) : + (lineAgree A xu.1 xu.2 : ℝ) ^ 2 = ∑ t : F, ∑ t' : F, + if xu.1 + t • xu.2 ∈ A ∧ xu.1 + t' • xu.2 ∈ A then (1 : ℝ) else 0 := by + have hN : (lineAgree A xu.1 xu.2 : ℝ) = + ∑ t : F, if xu.1 + t • xu.2 ∈ A then (1 : ℝ) else 0 := by simp [lineAgree, sum_boole] + rw [hN, sq, sum_mul_sum] + refine sum_congr rfl fun t _ => sum_congr rfl fun t' _ => ?_ + split_ifs <;> simp_all + simp only [hsq] + rw [sum_comm] + refine (sum_congr rfl fun _ _ => sum_comm).trans ?_ + simp only [sum_boole] + have hrow (t : F) : ∑ t' : F, + ((#{xu ∈ seeds m F | xu.1 + t • xu.2 ∈ A ∧ xu.1 + t' • xu.2 ∈ A} : ℕ) : ℝ) = + #A * ((Fintype.card F : ℝ) ^ m - 1) + (Fintype.card F - 1) * (#A * #A - #A) := by + rw [← Nat.cast_sum, hdiagN t, Nat.cast_add, Nat.cast_mul, Nat.cast_mul, + Nat.cast_sub (Nat.one_le_pow _ _ Fintype.card_pos), Nat.cast_sub Fintype.card_pos, + Nat.cast_sub (Nat.le_mul_self _)] + simp + rw [sum_congr rfl fun t _ => hrow t, sum_const, card_univ, nsmul_eq_mul] + ring + +/-- The centered second moment of `lineAgree A` over `seeds m F`. -/ +private theorem sum_lineAgree_sub_sq_le (A : Finset (Fin m → F)) : + ∑ xu ∈ seeds m F, + ((lineAgree A xu.1 xu.2 : ℝ) - Fintype.card F * #A / Fintype.card F ^ m) ^ 2 ≤ Fintype.card F * #A * (Fintype.card F ^ m - 1) := by set q : ℝ := (Fintype.card F : ℝ) set Q : ℝ := (Fintype.card F : ℝ) ^ m set a : ℝ := (#A : ℝ) set μ := q * a / Q have hQpos : (0 : ℝ) < Q := by positivity - have hQ1 : (1 : ℝ) ≤ Q := one_le_pow₀ (by exact_mod_cast Fintype.card_pos) have haQ : a ≤ Q := by - have := card_le_univ A - rw [Fintype.card_fun, Fintype.card_fin] at this - simp only [a, Q] - exact_mod_cast this - have hq1 : (1 : ℝ) ≤ q := by - simp only [q] - exact_mod_cast Fintype.card_pos - -- the number of points of a line in `A`, as a sum of indicators + have := card_le_univ A; rw [Fintype.card_fun, Fintype.card_fin] at this + simp only [a, Q]; exact_mod_cast this + have hq1 : (1 : ℝ) ≤ q := by simp only [q]; exact_mod_cast Fintype.card_pos let N : (Fin m → F) × (Fin m → F) → ℝ := fun xu => lineAgree A xu.1 xu.2 - have hN : ∀ xu, N xu = ∑ t : F, if xu.1 + t • xu.2 ∈ A then (1 : ℝ) else 0 := fun xu => by - simp [N, lineAgree, sum_boole] have hcardS : (#(seeds m F) : ℝ) = Q * (Q - 1) := by - rw [card_seeds, Nat.cast_mul, Nat.cast_sub (Nat.one_le_pow _ _ Fintype.card_pos)] - simp [Q] - -- the first moment - have h1 : ∑ xu ∈ seeds m F, N xu = q * (a * (Q - 1)) := by - simp only [hN] - rw [sum_comm] - simp only [sum_boole] - rw [sum_congr rfl fun t _ => by rw [card_seeds_mem A t], sum_const, card_univ, nsmul_eq_mul, - Nat.cast_mul, Nat.cast_sub (Nat.one_le_pow _ _ Fintype.card_pos)] - simp [q, a, Q] - -- the second moment - have hdiagN : ∀ t : F, ∑ t' : F, - #{xu ∈ seeds m F | xu.1 + t • xu.2 ∈ A ∧ xu.1 + t' • xu.2 ∈ A} = - #A * (Fintype.card F ^ m - 1) + (Fintype.card F - 1) * (#A * #A - #A) := by - intro t - rw [← add_sum_erase _ _ (mem_univ t)] - simp only [and_self, card_seeds_mem A t] - rw [sum_congr rfl fun t' ht' => card_seeds_mem_mem A (Ne.symm (ne_of_mem_erase ht')), - sum_const, card_erase_of_mem (mem_univ _), card_univ, smul_eq_mul] - have c1 : ((Fintype.card F ^ m - 1 : ℕ) : ℝ) = Q - 1 := by - rw [Nat.cast_sub (Nat.one_le_pow _ _ Fintype.card_pos)] - simp [Q] - have c2 : ((Fintype.card F - 1 : ℕ) : ℝ) = q - 1 := by - rw [Nat.cast_sub Fintype.card_pos] - simp [q] - have c3 : ((#A * #A - #A : ℕ) : ℝ) = a * a - a := by - rw [Nat.cast_sub (Nat.le_mul_self _)] - simp [a] - have h2 : ∑ xu ∈ seeds m F, N xu ^ 2 = q * (a * (Q - 1)) + q * (q - 1) * (a * a - a) := by - have hsq : ∀ xu, N xu ^ 2 = ∑ t : F, ∑ t' : F, - if xu.1 + t • xu.2 ∈ A ∧ xu.1 + t' • xu.2 ∈ A then (1 : ℝ) else 0 := fun xu => by - rw [hN, sq, sum_mul_sum] - refine sum_congr rfl fun t _ => sum_congr rfl fun t' _ => ?_ - split_ifs <;> simp_all - simp only [hsq] - rw [sum_comm] - refine (sum_congr rfl fun t _ => sum_comm).trans ?_ - simp only [sum_boole] - have : ∀ t : F, ∑ t' : F, - ((#{xu ∈ seeds m F | xu.1 + t • xu.2 ∈ A ∧ xu.1 + t' • xu.2 ∈ A} : ℕ) : ℝ) = - a * (Q - 1) + (q - 1) * (a * a - a) := fun t => by - rw [← Nat.cast_sum, hdiagN t, Nat.cast_add, Nat.cast_mul, Nat.cast_mul, c1, c2, c3] - rw [sum_congr rfl fun t _ => this t, sum_const, card_univ, nsmul_eq_mul] + rw [card_seeds, Nat.cast_mul, Nat.cast_sub (Nat.one_le_pow _ _ Fintype.card_pos)]; simp [Q] + have hexp : ∑ xu ∈ seeds m F, (N xu - μ) ^ 2 = + ∑ xu ∈ seeds m F, N xu ^ 2 - 2 * μ * ∑ xu ∈ seeds m F, N xu + μ ^ 2 * #(seeds m F) := by + simp only [sub_sq, sum_add_distrib, sum_sub_distrib, sum_const, nsmul_eq_mul, ← sum_mul, + ← mul_sum] ring - -- the variance - have hvar : ∑ xu ∈ seeds m F, (N xu - μ) ^ 2 ≤ q * a * (Q - 1) := by - have hexp : ∑ xu ∈ seeds m F, (N xu - μ) ^ 2 = - ∑ xu ∈ seeds m F, N xu ^ 2 - 2 * μ * ∑ xu ∈ seeds m F, N xu + - μ ^ 2 * #(seeds m F) := by - simp only [sub_sq, sum_add_distrib, sum_sub_distrib, sum_const, nsmul_eq_mul, ← sum_mul, - ← mul_sum] - ring - rw [hexp, h1, h2, hcardS] - simp only [μ] - rcases eq_or_lt_of_le (show (0 : ℝ) ≤ a by positivity) with ha0 | hapos - · rw [← ha0] - field_simp - nlinarith - have ha1 : 1 ≤ a := by - have : 0 < #A := by - simp only [a] at hapos - exact_mod_cast hapos - simp only [a] - exact_mod_cast this - have key : q * (q - 1) * (a * a - a) * Q ≤ q * q * a * a * (Q - 1) := by - have h₀ : (q - 1) * (a - 1) * Q ≤ q * a * (Q - 1) := by nlinarith - have h' := mul_le_mul_of_nonneg_left h₀ (show (0 : ℝ) ≤ q * a by positivity) - calc q * (q - 1) * (a * a - a) * Q = q * a * ((q - 1) * (a - 1) * Q) := by ring - _ ≤ q * a * (q * a * (Q - 1)) := h' - _ = _ := by ring - have hfin : q * (q - 1) * (a * a - a) ≤ q * q * a * a * (Q - 1) / Q := by - rw [le_div_iff₀ hQpos] - linarith - have e1 : (q * a / Q) ^ 2 * (Q * (Q - 1)) = q * q * a * a * (Q - 1) / Q := by - field_simp - have e2 : 2 * (q * a / Q) * (q * (a * (Q - 1))) = 2 * (q * q * a * a * (Q - 1) / Q) := by - field_simp - rw [e1, e2] - linarith - -- Chebyshev - have hcheb : (#{xu : (Fin m → F) × (Fin m → F) | xu.2 ≠ 0 ∧ (N xu : ℝ) ≤ D} : ℝ) * - (μ - D) ^ 2 ≤ ∑ xu ∈ seeds m F, (N xu - μ) ^ 2 := by - rw [← nsmul_eq_mul, ← sum_const] - refine (sum_le_sum fun xu hxu => ?_).trans (sum_le_sum_of_subset_of_nonneg - (fun xu hxu => ?_) fun _ _ _ => sq_nonneg _) - · exact (mem_filter.1 hxu).2.2 |> fun h => by nlinarith [sq_nonneg (N xu - μ)] - · exact mem_filter.2 ⟨mem_univ _, (mem_filter.1 hxu).2.1⟩ - exact hcheb.trans hvar + change ∑ xu ∈ seeds m F, (N xu - μ) ^ 2 ≤ q * a * (Q - 1) + rw [hexp, sum_lineAgree_seeds A, sum_lineAgree_sq_seeds A, hcardS] + change q * (a * (Q - 1)) + q * (q - 1) * (a * a - a) - 2 * μ * (q * (a * (Q - 1))) + + μ ^ 2 * (Q * (Q - 1)) ≤ q * a * (Q - 1) + simp only [μ] + rcases eq_or_lt_of_le (show (0 : ℝ) ≤ a by positivity) with ha0 | hapos + · rw [← ha0]; field_simp; nlinarith + have ha1 : 1 ≤ a := by + have : 0 < #A := by simp only [a] at hapos; exact_mod_cast hapos + simp only [a]; exact_mod_cast this + have h₀ : (q - 1) * (a - 1) * Q ≤ q * a * (Q - 1) := by nlinarith + have key : q * (q - 1) * (a * a - a) * Q ≤ q * q * a * a * (Q - 1) := + calc q * (q - 1) * (a * a - a) * Q = q * a * ((q - 1) * (a - 1) * Q) := by ring + _ ≤ q * a * (q * a * (Q - 1)) := mul_le_mul_of_nonneg_left h₀ (by positivity) + _ = _ := by ring + have hfin : q * (q - 1) * (a * a - a) ≤ q * q * a * a * (Q - 1) / Q := + (le_div_iff₀ hQpos).2 (by linarith) + have e1 : (q * a / Q) ^ 2 * (Q * (Q - 1)) = q * q * a * a * (Q - 1) / Q := by field_simp + have e2 : 2 * (q * a / Q) * (q * (a * (Q - 1))) = 2 * (q * q * a * a * (Q - 1) / Q) := by + field_simp + rw [e1, e2]; linarith + +/-- **Random lines sample a set well.** Over all points `x` and nonzero directions `u`, the +number of pairs for which the line `t ↦ x + t • u` has at most `D` points in `A` is at most +`q * a * (Q - 1) / (μ - D) ^ 2`, where `a = #A`, `Q = q ^ m` and `μ = q * a / Q > D` is the mean +number of points of a line in `A`. -/ +theorem card_filter_lineAgree_le_mul_sq_le (A : Finset (Fin m → F)) {D : ℝ} + (hD : D < Fintype.card F * #A / Fintype.card F ^ m) : + (#{xu : (Fin m → F) × (Fin m → F) | xu.2 ≠ 0 ∧ (lineAgree A xu.1 xu.2 : ℝ) ≤ D} : ℝ) * + (Fintype.card F * #A / Fintype.card F ^ m - D) ^ 2 ≤ + Fintype.card F * #A * (Fintype.card F ^ m - 1) := by + have hfilter : ({xu : (Fin m → F) × (Fin m → F) | + xu.2 ≠ 0 ∧ (lineAgree A xu.1 xu.2 : ℝ) ≤ D} : Finset _) = + {xu ∈ seeds m F | (lineAgree A xu.1 xu.2 : ℝ) ≤ D} := by rw [seeds, filter_filter] + rw [hfilter] + refine (card_filter_mul_le_sum _ _ _ (fun _ _ => sq_nonneg _) fun xu _ hxu => ?_).trans + (sum_lineAgree_sub_sq_le A) + nlinarith [sq_nonneg ((lineAgree A xu.1 xu.2 : ℝ) - Fintype.card F * #A / Fintype.card F ^ m)] /-! ### The decoder -/ @@ -351,6 +344,106 @@ private theorem card_normDirs_mul_le : rwa [card_product, card_erase_of_mem (mem_univ _), card_erase_of_mem (mem_univ _), card_univ, card_univ, Fintype.card_fun, Fintype.card_fin] at h +/-- For a fixed `x`, at most `#(normDirs m F) * (D - d)` points `z ≠ x` lie on a line through `x` +with more than `D` agreements yet make `lineListDecode` fail at `x`. -/ +private theorem card_filter_lineListDecode_ne_of_lt_lineAgree_le {d D : ℕ} (hd : 1 ≤ d) + (hn : Fintype.card F < #(Sudan.monomials d D)) (hDq : D < Fintype.card F) + {p : (Fin m → F) → F} (hp : p ∈ reedMuller F m d) (g : (Fin m → F) → F) (x : Fin m → F) : + #{z | z ≠ x ∧ D < lineAgree {y | g y = p y} x (z - x) ∧ + lineListDecode g d D z (p z) x ≠ p x} ≤ #(normDirs m F) * (D - d) := by + set A : Finset (Fin m → F) := {y | g y = p y} + let bad (v : Fin m → F) : Finset F := + {τ | hintDecode id (fun t : F => g (x + t • v)) d D τ (p (x + τ • v)) ≠ p x} + calc #{z | z ≠ x ∧ D < lineAgree A x (z - x) ∧ lineListDecode g d D z (p z) x ≠ p x} + ≤ #(((normDirs m F).filter (fun v => D < lineAgree A x v)).sigma bad) := by + refine card_le_card_of_injOn + (fun z => ⟨(firstNonzero (z - x))⁻¹ • (z - x), firstNonzero (z - x)⟩) + (fun z hz => ?_) (fun z hz z' hz' heq => ?_) + · simp only [coe_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hz + obtain ⟨hne, hD, hdec⟩ := hz + have hl : firstNonzero (z - x) ≠ 0 := + firstNonzero_eq_zero_iff.not.2 (sub_ne_zero.2 hne) + simp only [coe_sigma, Set.mem_sigma_iff, mem_coe, mem_filter, normDirs, mem_univ, + true_and, bad] + rw [lineListDecode_eq g p d D hne] at hdec + exact ⟨⟨by rw [firstNonzero_smul, inv_mul_cancel₀ hl], + by rwa [lineAgree_smul A _ _ (inv_ne_zero hl)]⟩, hdec⟩ + · simp only [coe_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hz hz' + have e1 := firstNonzero_smul_inv_smul (sub_ne_zero.2 hz.1) + have e2 := firstNonzero_smul_inv_smul (sub_ne_zero.2 hz'.1) + have h1 := congrArg Sigma.fst heq + have h2 := congrArg Sigma.snd heq + simp only at h1 h2 + have hsub : z - x = z' - x := by rw [← e1, h1, h2, e2] + exact sub_left_injective hsub + _ = ∑ v ∈ (normDirs m F).filter (fun v => D < lineAgree A x v), #(bad v) := card_sigma _ _ + _ ≤ ∑ v ∈ (normDirs m F).filter (fun v => D < lineAgree A x v), (D - d) := + sum_le_sum fun v hv => card_hintDecode_line_ne_le hd hn hDq hp g x v (mem_filter.1 hv).2 + _ ≤ #(normDirs m F) * (D - d) := by + rw [sum_const, smul_eq_mul] + exact Nat.mul_le_mul_right _ (card_filter_le _ _) + +/-- Over all pairs `(x, z)`, the number of pairs where `lineListDecode` fails is at most the +diagonal (`q ^ m`), plus the pairs on lines with at most `D` agreements, plus at most +`q ^ m * #(normDirs m F) * (D - d)` pairs on good lines with a bad hint position. -/ +private theorem sum_card_filter_lineListDecode_ne_le {d D : ℕ} (hd : 1 ≤ d) + (hn : Fintype.card F < #(Sudan.monomials d D)) (hDq : D < Fintype.card F) + {p : (Fin m → F) → F} (hp : p ∈ reedMuller F m d) (g : (Fin m → F) → F) : + ∑ z : Fin m → F, #{x | lineListDecode g d D z (p z) x ≠ p x} ≤ + Fintype.card F ^ m + + #{xu : (Fin m → F) × (Fin m → F) | + xu.2 ≠ 0 ∧ (lineAgree {y | g y = p y} xu.1 xu.2 : ℝ) ≤ (D : ℝ)} + + Fintype.card F ^ m * (#(normDirs m F) * (D - d)) := by + set A : Finset (Fin m → F) := {y | g y = p y} + have hswap : (∑ z : Fin m → F, #{x | lineListDecode g d D z (p z) x ≠ p x}) = + ∑ x : Fin m → F, #{z | lineListDecode g d D z (p z) x ≠ p x} := by + simp only [card_eq_sum_ones, sum_filter]; exact sum_comm + have hpt (x : Fin m → F) : #{z | lineListDecode g d D z (p z) x ≠ p x} ≤ + 1 + #{u : Fin m → F | u ≠ 0 ∧ (lineAgree A x u : ℝ) ≤ (D : ℝ)} + + #(normDirs m F) * (D - d) := by + have hsub : ({z | lineListDecode g d D z (p z) x ≠ p x} : Finset _) ⊆ + ({x} : Finset _) ∪ ({z | z ≠ x ∧ lineAgree A x (z - x) ≤ D} : Finset _) ∪ + ({z | z ≠ x ∧ D < lineAgree A x (z - x) ∧ + lineListDecode g d D z (p z) x ≠ p x} : Finset _) := by + intro z hz + simp only [mem_filter, mem_univ, true_and, mem_union, mem_singleton] at hz ⊢ + by_cases hzx : z = x; · exact Or.inl (Or.inl hzx) + by_cases hlow : lineAgree A x (z - x) ≤ D; · exact Or.inl (Or.inr ⟨hzx, hlow⟩) + exact Or.inr ⟨hzx, not_le.1 hlow, hz⟩ + have hshift : #{z | z ≠ x ∧ lineAgree A x (z - x) ≤ D} = + #{u : Fin m → F | u ≠ 0 ∧ (lineAgree A x u : ℝ) ≤ (D : ℝ)} := by + simp only [card_eq_sum_ones, sum_filter] + exact Fintype.sum_equiv (Equiv.subRight x) _ _ fun z => by + simp [Equiv.subRight_apply, sub_ne_zero] + calc #{z | lineListDecode g d D z (p z) x ≠ p x} + ≤ #({x} : Finset _) + #{z | z ≠ x ∧ lineAgree A x (z - x) ≤ D} + + #{z | z ≠ x ∧ D < lineAgree A x (z - x) ∧ lineListDecode g d D z (p z) x ≠ p x} := + (card_le_card hsub).trans + ((card_union_le _ _).trans (Nat.add_le_add_right (card_union_le _ _) _)) + _ ≤ 1 + #{u : Fin m → F | u ≠ 0 ∧ (lineAgree A x u : ℝ) ≤ (D : ℝ)} + + #(normDirs m F) * (D - d) := by + rw [card_singleton, hshift] + exact Nat.add_le_add_left + (card_filter_lineListDecode_ne_of_lt_lineAgree_le hd hn hDq hp g x) _ + have hS₂ : (∑ x : Fin m → F, #{u : Fin m → F | u ≠ 0 ∧ (lineAgree A x u : ℝ) ≤ (D : ℝ)}) = + #{xu : (Fin m → F) × (Fin m → F) | xu.2 ≠ 0 ∧ (lineAgree A xu.1 xu.2 : ℝ) ≤ (D : ℝ)} := by + simp only [card_eq_sum_ones, sum_filter, Fintype.sum_prod_type] + rw [hswap]; refine (sum_le_sum fun x _ => hpt x).trans ?_ + simp only [sum_add_distrib, sum_const, card_univ, Fintype.card_fun, Fintype.card_fin, smul_eq_mul, + mul_one, hS₂, le_rfl] + +/-- In `ℝ`, the number of normalized directions is at most `(q ^ m - 1) / (q - 1)`. -/ +private theorem card_normDirs_le_real : + (#(normDirs m F) : ℝ) ≤ ((Fintype.card F : ℝ) ^ m - 1) / (Fintype.card F - 1) := by + have hq1 : (1 : ℝ) < Fintype.card F := by exact_mod_cast Fintype.one_lt_card + rw [le_div_iff₀ (by linarith)] + have h := card_normDirs_mul_le (m := m) (F := F) + have h1 : ((Fintype.card F - 1 : ℕ) : ℝ) = Fintype.card F - 1 := by + rw [Nat.cast_sub Fintype.card_pos, Nat.cast_one] + have h2 : ((Fintype.card F ^ m - 1 : ℕ) : ℝ) = (Fintype.card F : ℝ) ^ m - 1 := by + rw [Nat.cast_sub (Nat.one_le_pow _ _ Fintype.card_pos), Nat.cast_pow, Nat.cast_one] + rw [← h1, ← h2]; exact_mod_cast h + /-- **Local list decoding of Reed–Muller codes**, a variant of [SudanTrevisanVadhan2001]. Let `p` be a codeword of the Reed–Muller code of degree `d ≥ 1` in `m` variables over a field with `q` elements, `Q = q ^ m`, and let `g` agree with `p` on `a` points. Let `D < q` be such that there @@ -372,160 +465,37 @@ theorem exists_card_lineListDecode_ne_le {d D : ℕ} (hd : 1 ≤ d) set Q : ℝ := (Fintype.card F : ℝ) ^ m set μ := q * #A / Q have hQpos : (0 : ℝ) < Q := by positivity - have hq1 : (1 : ℝ) < q := by - simp only [q] - exact_mod_cast Fintype.one_lt_card - -- the bad hint positions on each line - let bad : (Fin m → F) → (Fin m → F) → Finset F := fun x v => - {τ | hintDecode id (fun t : F => g (x + t • v)) d D τ (p (x + τ • v)) ≠ p x} - -- the three kinds of failing pairs - let S₁ : Finset ((Fin m → F) × (Fin m → F)) := univ.filter fun xz => xz.2 = xz.1 - let S₂ : Finset ((Fin m → F) × (Fin m → F)) := univ.filter fun xz => - xz.2 ≠ xz.1 ∧ lineAgree A xz.1 (xz.2 - xz.1) ≤ D - let S₃ : Finset ((Fin m → F) × (Fin m → F)) := univ.filter fun xz => xz.2 ≠ xz.1 ∧ - D < lineAgree A xz.1 (xz.2 - xz.1) ∧ - firstNonzero (xz.2 - xz.1) ∈ bad xz.1 ((firstNonzero (xz.2 - xz.1))⁻¹ • (xz.2 - xz.1)) - let fail : Finset ((Fin m → F) × (Fin m → F)) := - univ.filter fun xz => lineListDecode g d D xz.2 (p xz.2) xz.1 ≠ p xz.1 - have hfail : fail ⊆ S₁ ∪ S₂ ∪ S₃ := by - rintro ⟨x, z⟩ hxz - simp only [fail, mem_filter, mem_univ, true_and] at hxz - simp only [S₁, S₂, S₃, mem_union, mem_filter, mem_univ, true_and] - by_cases hzx : z = x - · exact Or.inl (Or.inl hzx) - by_cases hlow : lineAgree A x (z - x) ≤ D - · exact Or.inl (Or.inr ⟨hzx, hlow⟩) - refine Or.inr ⟨hzx, not_le.1 hlow, ?_⟩ - simp only [bad, mem_filter, mem_univ, true_and] - rwa [lineListDecode_eq g p d D hzx] at hxz - -- the diagonal - have hdiag : #S₁ = Fintype.card F ^ m := by - have : #S₁ = #(univ : Finset (Fin m → F)) := by - refine card_nbij' Prod.fst (fun x => (x, x)) (fun _ _ => mem_coe.2 (mem_univ _)) - (fun x _ => by simp [S₁]) (fun xz hxz => ?_) (fun x _ => rfl) - simp only [S₁, coe_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hxz - exact Prod.ext rfl hxz.symm - rw [this, card_univ, Fintype.card_fun, Fintype.card_fin] - -- the lines with few agreements - have hlow : (#S₂ : ℝ) * (μ - D) ^ 2 ≤ q * #A * (Q - 1) := by - have hcard : #S₂ = - #{xu : (Fin m → F) × (Fin m → F) | xu.2 ≠ 0 ∧ (lineAgree A xu.1 xu.2 : ℝ) ≤ D} := by - refine card_nbij' (fun xz => (xz.1, xz.2 - xz.1)) (fun xu => (xu.1, xu.2 + xu.1)) - (fun xz h => ?_) (fun xu h => ?_) (fun xz _ => by simp) (fun xu _ => by simp) - · simp only [S₂, coe_filter, mem_univ, true_and, Set.mem_ofPred_eq] at h ⊢ - exact ⟨sub_ne_zero.2 h.1, by exact_mod_cast h.2⟩ - · simp only [S₂, coe_filter, mem_univ, true_and, Set.mem_ofPred_eq, - add_sub_cancel_right] at h ⊢ - exact ⟨fun h' => h.1 (by simpa using h'), by exact_mod_cast h.2⟩ - rw [hcard] + have hμD : 0 < μ - D := by linarith + have hlow : (#{xu : (Fin m → F) × (Fin m → F) | + xu.2 ≠ 0 ∧ (lineAgree A xu.1 xu.2 : ℝ) ≤ (D : ℝ)} : ℝ) ≤ + q * #A * (Q - 1) / (μ - D) ^ 2 := by + rw [le_div_iff₀ (by positivity)] exact card_filter_lineAgree_le_mul_sq_le A hμ - -- the bad hint positions - have hfib : ∀ x : Fin m → F, #(S₃.filter fun xz => xz.1 = x) ≤ #(normDirs m F) * (D - d) := by - intro x - calc #(S₃.filter fun xz => xz.1 = x) - ≤ #(((normDirs m F).filter (fun v => D < lineAgree A x v)).sigma fun v => bad x v) := by - refine card_le_card_of_injOn - (fun xz => ⟨(firstNonzero (xz.2 - x))⁻¹ • (xz.2 - x), firstNonzero (xz.2 - x)⟩) - (fun xz hxz => ?_) (fun xz hxz xz' hxz' heq => ?_) - · simp only [S₃, coe_filter, mem_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hxz - obtain ⟨⟨hne, hD, hb⟩, rfl⟩ := hxz - have hu : xz.2 - xz.1 ≠ 0 := sub_ne_zero.2 hne - have hl : firstNonzero (xz.2 - xz.1) ≠ 0 := firstNonzero_eq_zero_iff.not.2 hu - simp only [coe_sigma, Set.mem_sigma_iff, mem_coe, mem_filter, normDirs, mem_univ, - true_and] - refine ⟨⟨by rw [firstNonzero_smul, inv_mul_cancel₀ hl], ?_⟩, hb⟩ - rw [lineAgree_smul A _ _ (inv_ne_zero hl)] - exact hD - · simp only [S₃, coe_filter, mem_filter, mem_univ, true_and, - Set.mem_ofPred_eq] at hxz hxz' - obtain ⟨⟨hne, -, -⟩, hx⟩ := hxz - obtain ⟨⟨hne', -, -⟩, hx'⟩ := hxz' - subst hx - have h1 := congrArg Sigma.fst heq - have h2 := congrArg Sigma.snd heq - simp only at h1 h2 - rw [hx'] at hne' - have e1 := firstNonzero_smul_inv_smul (sub_ne_zero.2 hne) - have e2 := firstNonzero_smul_inv_smul (sub_ne_zero.2 hne') - have : xz.2 - xz.1 = xz'.2 - xz.1 := by rw [← e1, h1, h2, e2] - exact Prod.ext hx'.symm (sub_left_injective this) - _ = ∑ v ∈ (normDirs m F).filter (fun v => D < lineAgree A x v), #(bad x v) := - card_sigma _ _ - _ ≤ ∑ v ∈ (normDirs m F).filter (fun v => D < lineAgree A x v), (D - d) := - sum_le_sum fun v hv => card_hintDecode_line_ne_le hd hn hDq hp g x v - (mem_filter.1 hv).2 - _ ≤ #(normDirs m F) * (D - d) := by - rw [sum_const, smul_eq_mul] - exact Nat.mul_le_mul_right _ (card_filter_le _ _) - have hbad : (#S₃ : ℝ) ≤ Q * (#(normDirs m F) * (D - d : ℕ)) := by - rw [card_eq_sum_card_fiberwise (f := Prod.fst) (t := univ) fun _ _ => mem_univ _, - Nat.cast_sum] - calc (∑ x : Fin m → F, (#(S₃.filter fun xz => xz.1 = x) : ℝ)) - ≤ ∑ _x : Fin m → F, ((#(normDirs m F) * (D - d) : ℕ) : ℝ) := - sum_le_sum fun x _ => by exact_mod_cast hfib x - _ = Q * (#(normDirs m F) * (D - d : ℕ)) := by - rw [sum_const, card_univ, Fintype.card_fun, Fintype.card_fin, nsmul_eq_mul] - push_cast - rfl - have hnorm : (#(normDirs m F) : ℝ) ≤ (Q - 1) / (q - 1) := by - rw [le_div_iff₀ (by linarith)] - have h := card_normDirs_mul_le (m := m) (F := F) - have : ((Fintype.card F - 1 : ℕ) : ℝ) = q - 1 := by - rw [Nat.cast_sub Fintype.card_pos] - simp [q] - have h' : ((Fintype.card F ^ m - 1 : ℕ) : ℝ) = Q - 1 := by - rw [Nat.cast_sub (Nat.one_le_pow _ _ Fintype.card_pos)] - simp [Q] - rw [← this, ← h'] - exact_mod_cast h - -- averaging over the advice point + have hbad : Q * (#(normDirs m F) * (D - d : ℕ)) ≤ Q * (Q - 1) * (D - d : ℕ) / (q - 1) := by + rw [mul_assoc, mul_div_assoc] + refine mul_le_mul_of_nonneg_left ?_ hQpos.le + rw [mul_div_right_comm] + exact mul_le_mul_of_nonneg_right (card_normDirs_le_real (m := m) (F := F)) (by positivity) + have htot : (∑ z : Fin m → F, (#{x | lineListDecode g d D z (p z) x ≠ p x} : ℝ)) ≤ + Q + (#{xu : (Fin m → F) × (Fin m → F) | + xu.2 ≠ 0 ∧ (lineAgree A xu.1 xu.2 : ℝ) ≤ (D : ℝ)} : ℝ) + + Q * (#(normDirs m F) * (D - d : ℕ)) := by + have hle := Nat.cast_le (α := ℝ).2 (sum_card_filter_lineListDecode_ne_le hd hn hDq hp g) + simpa [Q] using hle have hsum : (∑ z : Fin m → F, (#{x | lineListDecode g d D z (p z) x ≠ p x} : ℝ)) ≤ Q * (1 + (q * #A * (Q - 1) / (μ - D) ^ 2 + Q * (Q - 1) * (D - d : ℕ) / (q - 1)) / Q) := by - have hcount : (∑ z : Fin m → F, (#{x | lineListDecode g d D z (p z) x ≠ p x} : ℝ)) = - #fail := by - rw [← Nat.cast_sum] - congr 1 - rw [card_eq_sum_card_fiberwise (f := Prod.snd) (t := univ) fun _ _ => mem_univ _] - refine sum_congr rfl fun z _ => ?_ - refine card_nbij' (fun x => (x, z)) Prod.fst (fun x hx => ?_) (fun xz hxz => ?_) - (fun x _ => rfl) (fun xz hxz => ?_) - · simp_all [fail] - · simp only [coe_filter, mem_univ, true_and, Set.mem_ofPred_eq, fail, mem_filter] at hxz ⊢ - rw [← hxz.2] - exact hxz.1 - · simp only [coe_filter, mem_univ, true_and, Set.mem_ofPred_eq, fail, mem_filter] at hxz - exact Prod.ext rfl hxz.2.symm - rw [hcount] - have hμD : 0 < μ - D := by linarith - have hlow' : (#S₂ : ℝ) ≤ q * #A * (Q - 1) / (μ - D) ^ 2 := by - rw [le_div_iff₀ (by positivity)] - exact hlow - have hbad' : Q * (#(normDirs m F) * (D - d : ℕ)) ≤ Q * (Q - 1) * (D - d : ℕ) / (q - 1) := by - rw [mul_assoc, mul_div_assoc] - refine mul_le_mul_of_nonneg_left ?_ hQpos.le - rw [mul_div_right_comm] - exact mul_le_mul_of_nonneg_right hnorm (by positivity) - have hunion : (#fail : ℝ) ≤ #S₁ + #S₂ + #S₃ := by - exact_mod_cast (card_le_card hfail).trans - ((card_union_le _ _).trans (Nat.add_le_add_right (card_union_le _ _) _)) - have hS₁ : (#S₁ : ℝ) = Q := by - rw [hdiag] - push_cast - rfl - calc (#fail : ℝ) ≤ Q + q * #A * (Q - 1) / (μ - D) ^ 2 + - Q * (Q - 1) * (D - d : ℕ) / (q - 1) := by linarith + calc (∑ z : Fin m → F, (#{x | lineListDecode g d D z (p z) x ≠ p x} : ℝ)) + ≤ Q + q * #A * (Q - 1) / (μ - D) ^ 2 + Q * (Q - 1) * (D - d : ℕ) / (q - 1) := by linarith _ = Q * (1 + (q * #A * (Q - 1) / (μ - D) ^ 2 + Q * (Q - 1) * (D - d : ℕ) / (q - 1)) / Q) := by - rw [mul_add, mul_one, mul_div_cancel₀ _ hQpos.ne'] - ring + rw [mul_add, mul_one, mul_div_cancel₀ _ hQpos.ne']; ring obtain ⟨z, -, hz⟩ := exists_le_of_sum_le (s := (univ : Finset (Fin m → F))) univ_nonempty (f := fun z => (#{x | lineListDecode g d D z (p z) x ≠ p x} : ℝ)) (g := fun _ => 1 + (q * #A * (Q - 1) / (μ - D) ^ 2 + Q * (Q - 1) * (D - d : ℕ) / (q - 1)) / Q) (by rw [sum_const, card_univ, Fintype.card_fun, Fintype.card_fin, nsmul_eq_mul] - push_cast - exact hsum) + push_cast; exact hsum) exact ⟨z, hz⟩ end Cslib.Code diff --git a/ComplexityTests/RandomizedDisjointness.lean b/ComplexityTests/RandomizedDisjointness.lean index fcd7c5b59b..ff537eea57 100644 --- a/ComplexityTests/RandomizedDisjointness.lean +++ b/ComplexityTests/RandomizedDisjointness.lean @@ -125,11 +125,11 @@ info: 'Cslib.Communication.Disjointness.corrupted_hardDist' depends on axioms: #print axioms Cslib.Communication.Disjointness.corrupted_hardDist /-- -info: 'Finset.four_mul_sum_card_filter_notMem_le' depends on axioms: +info: 'Cslib.four_mul_sum_card_filter_notMem_le' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in -#print axioms Finset.four_mul_sum_card_filter_notMem_le +#print axioms Cslib.four_mul_sum_card_filter_notMem_le /-- info: 'Cslib.Communication.PublicCoin.div_le_mul_ecomplexityFun_disjoint_add' depends on axioms: From 3438457315a4c4db9cbfbfa53bc7d610943c7abc Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 17:24:09 +0000 Subject: [PATCH 2/2] refactor(Combinatorics): address review feedback and nits on #830 (#614) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Extract Finset.mul_card_filter_le_sum and Finset.card_filter_mul_le_sum into Foundations/Data/Finset/Markov.lean, deriving the ℕ specialization from the Semiring version and recording its Mathlib placement in UPSTREAM.md - Derive sq_expect_le_dens_mul_expect_sq from Fintype.sq_expect_le_dens_mul_expect_sq and Finset.dens_le_dens, and use Fintype.expect_boole_mem and Fintype.expect_boole_mem_sq from #820 in Expander/Hitting.lean - Make Cslib.RotationMap.expect_walk_sub_one_sub_spectralExpansion_sq_le public and cite [Vadhan2012] - Remove extra Mathlib destination line from CentralBinomial.lean header --- Complexity.lean | 1 + .../Complexity/PolyTime/RotationMap/Walk.lean | 14 ++--- .../Combinatorics/Expander/Hitting.lean | 38 +++++------ .../Combinatorics/Expander/KilledWalk.lean | 63 ++++++++++--------- .../Combinatorics/Hypergeometric.lean | 24 +------ .../Combinatorics/PowersetTail.lean | 2 +- .../Data/Code/LocalListDecoding.lean | 2 +- .../Foundations/Data/Finset/Markov.lean | 54 ++++++++++++++++ ComplexityTests/Axioms.lean | 4 +- ComplexityTests/PCPEncodedAmplification.lean | 6 +- ComplexityTests/RotationWalk.lean | 12 ++-- UPSTREAM.md | 4 +- 12 files changed, 131 insertions(+), 93 deletions(-) create mode 100644 Complexity/Foundations/Data/Finset/Markov.lean diff --git a/Complexity.lean b/Complexity.lean index cb8034dcf5..cc65f5443b 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1704,6 +1704,7 @@ public import Complexity.Foundations.Data.Fin.Append public import Complexity.Foundations.Data.Fin.Order public import Complexity.Foundations.Data.Fin.Tuple public import Complexity.Foundations.Data.Finset.Expect +public import Complexity.Foundations.Data.Finset.Markov public import Complexity.Foundations.Data.Finset.Quantile public import Complexity.Foundations.Data.Finset.Sampling public import Complexity.Foundations.Data.Finset.SymmDiff diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Walk.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Walk.lean index 15068fa92e..93b6fb328c 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Walk.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Walk.lean @@ -195,24 +195,24 @@ theorem rotationMap_killedPowRotWithInput (T q : ℕ) [NeZero q] (signal : Fin q (encPair input (encPair vertex (encPair (encPi label) (encPi signal)))) (encPair vertex (encPair (encPi label) (encPi signal))) := by have hprefix : ComputableTidilyInPolyTime - (fun k : Fin T → D => Fin.take _ (RotationMap.killTime_le c) k) + (fun k : Fin T → D => Fin.take _ (killTime_le c) k) (encPi label) (encPi label) := - pi fun i : Fin (RotationMap.killTime c) => - pi_apply label (⟨i.val, i.isLt.trans_le (RotationMap.killTime_le c)⟩ : Fin T) + pi fun i : Fin (killTime c) => + pi_apply label (⟨i.val, i.isLt.trans_le (killTime_le c)⟩ : Fin T) have hwalk : ComputableTidilyInPolyTime (fun p : P × (V × ((Fin T → D) × (Fin T → Fin q))) => - RotationMap.powRotWithInput rotate (RotationMap.killTime c) - (p.1, p.2.1, Fin.take _ (RotationMap.killTime_le c) p.2.2.1)) + RotationMap.powRotWithInput rotate (killTime c) + (p.1, p.2.1, Fin.take _ (killTime_le c) p.2.2.1)) (encPair input (encPair vertex (encPair (encPi label) (encPi signal)))) (encPair vertex (encPi label)) := - (rotationMap_powRotWithInput hrotate (RotationMap.killTime c)).comp + (rotationMap_powRotWithInput hrotate (killTime c)).comp ((fst _ _).prod (((snd _ _).fst').prod (hprefix.comp ((snd _ _).snd'.fst')))) dsimp only [RotationMap.killedPowRotWithInput] apply hwalk.fst'.prod apply prod ?_ (const c) apply pi intro i - by_cases hi : i.val < RotationMap.killTime c + by_cases hi : i.val < killTime c · simpa only [dite_eq_left hi, Function.comp_def] using (pi_apply label ⟨i.val, hi⟩).comp hwalk.snd' · simpa only [dite_eq_right hi, Function.comp_def] using diff --git a/Complexity/Foundations/Combinatorics/Expander/Hitting.lean b/Complexity/Foundations/Combinatorics/Expander/Hitting.lean index e472a1b9f7..2c6f97c3c3 100644 --- a/Complexity/Foundations/Combinatorics/Expander/Hitting.lean +++ b/Complexity/Foundations/Combinatorics/Expander/Hitting.lean @@ -34,8 +34,9 @@ the walk operator with multiplication by the weights (`Cslib.RotationMap.weighte `Cslib.RotationMap.expect_prod_walkAt`). For indicator weights, each step multiplies the second moment of a function supported on a set of density at most `μ` by at most `((1 - λ) μ + λ) ^ 2`: the walk operator is `(1 - λ)` times the projection onto the constants plus -an operator of norm at most `λ`, and the projection of a function supported on a small set is small -(`Cslib.RotationMap.expect_ite_mem_walk_sq_le`). +an operator of norm at most `λ` +(`Cslib.RotationMap.expect_walk_sub_one_sub_spectralExpansion_sq_le`), and the projection of a +function supported on a small set is small (`Cslib.RotationMap.expect_ite_mem_walk_sq_le`). ## Main definitions @@ -45,6 +46,8 @@ an operator of norm at most `λ`, and the projection of a function supported on * `Cslib.RotationMap.expect_prod_walkAt`: the expected product of weights along a walk from a vertex is the weighted walk. +* `Cslib.RotationMap.expect_walk_sub_one_sub_spectralExpansion_sq_le`: subtracting `(1 - λ)` times + the mean from `G.walk x` leaves second moment at most `λ ^ 2` times the second moment of `x`. * `Cslib.RotationMap.expect_ite_mem_walk_sq_le`: one step of a walk restricted to a small set. * `Cslib.RotationMap.dens_filter_forall_walkAt_mem_le`: the hitting property. * `Cslib.RotationMap.dens_filter_forall_walkAt_mem_le_pow`: the usual power bound for remaining @@ -127,30 +130,21 @@ section Hitting variable [Fintype V] [Fintype D] -/-- The second moment of a constant restricted to `B` is `dens B` times its square. -/ -private theorem expect_ite_const_sq [DecidableEq V] (B : Finset V) (α : ℝ) : - 𝔼 v, (if v ∈ B then α else 0) ^ 2 = dens B * α ^ 2 := by - have h : (𝔼 v, if v ∈ B then (1 : ℝ) else 0) = dens B := by - simpa using (Fintype.expect_boole (𝕜 := ℝ) fun v => v ∈ B) - rw [← h, expect_mul] - exact expect_congr rfl fun v _ => by split_ifs <;> simp - -/-- By Cauchy–Schwarz, the squared average of a function vanishing outside `C` is at most the -density of `C` times its second moment. -/ +/-- By the second moment method (`Fintype.sq_expect_le_dens_mul_expect_sq`), the squared average +of a function vanishing outside `C` is at most the density of `C` times its second moment. -/ private theorem sq_expect_le_dens_mul_expect_sq {C : Finset V} {x : V → ℝ} (hx : ∀ v ∉ C, x v = 0) : (𝔼 v, x v) ^ 2 ≤ dens C * 𝔼 v, x v ^ 2 := by classical - have h := expect_mul_sq_le_sq_mul_sq univ (fun v => if v ∈ C then (1 : ℝ) else 0) x - have h₁ : 𝔼 v, (if v ∈ C then (1 : ℝ) else 0) * x v = 𝔼 v, x v := - expect_congr rfl fun v _ => by by_cases hv : v ∈ C <;> simp [hv, hx] - have h₂ : 𝔼 v, (if v ∈ C then (1 : ℝ) else 0) ^ 2 = dens C := by - simpa using expect_ite_const_sq C 1 - rwa [h₁, h₂] at h + refine (Fintype.sq_expect_le_dens_mul_expect_sq x).trans ?_ + have hsub : ({v : V | x v ≠ 0} : Finset V) ⊆ C := fun v hv => + by_contra fun hvC => (mem_filter.mp hv).2 (hx v hvC) + exact mul_le_mul_of_nonneg_right (by exact_mod_cast dens_le_dens hsub) + (expect_nonneg fun _ _ => sq_nonneg _) /-- Subtracting `(1 - λ(G))` times the mean from `G.walk x` leaves second moment at most `λ(G) ^ 2` times the second moment of `x`. -/ -private theorem expect_walk_sub_one_sub_spectralExpansion_sq_le [Nonempty V] [Nonempty D] +theorem expect_walk_sub_one_sub_spectralExpansion_sq_le [Nonempty V] [Nonempty D] (x : V → ℝ) : 𝔼 v, (G.walk x v - (1 - G.spectralExpansion) * 𝔼 u, x u) ^ 2 ≤ G.spectralExpansion ^ 2 * 𝔼 v, x v ^ 2 := by @@ -203,7 +197,9 @@ theorem expect_ite_mem_walk_sq_le [Nonempty D] {B C : Finset V} {μ : ℝ} (hB : simp only [hsplit] refine Fintype.expect_add_sq_le (by linarith) zero_le_one hμ hℓ₀ (expect_nonneg fun _ _ => sq_nonneg _) ?_ ?_ |>.trans_eq (by ring) - · calc 𝔼 v, (if v ∈ B then α else 0) ^ 2 = dens B * α ^ 2 := expect_ite_const_sq B α + · calc 𝔼 v, (if v ∈ B then α else 0) ^ 2 = dens B * α ^ 2 := by + rw [← Fintype.expect_boole_mem B, expect_mul] + exact expect_congr rfl fun v _ => by split_ifs <;> simp _ ≤ μ * (μ * 𝔼 v, x v ^ 2) := by have := expect_nonneg (s := (univ : Finset V)) fun v _ => sq_nonneg (x v) gcongr @@ -231,7 +227,7 @@ private theorem expect_weightedWalk_ite_sq_le [Nonempty D] {μ : ℝ} (t : ℕ) induction t with | zero => intro B hB - rw [weightedWalk_zero, expect_ite_const_sq] + rw [weightedWalk_zero, Fintype.expect_boole_mem_sq] simpa using hB 0 | succ t ih => intro B hB diff --git a/Complexity/Foundations/Combinatorics/Expander/KilledWalk.lean b/Complexity/Foundations/Combinatorics/Expander/KilledWalk.lean index dd7ed5455b..af8d7262b0 100644 --- a/Complexity/Foundations/Combinatorics/Expander/KilledWalk.lean +++ b/Complexity/Foundations/Combinatorics/Expander/KilledWalk.lean @@ -40,19 +40,19 @@ that the reverse is killed at the same step. ## Main definitions -* `Cslib.RotationMap.killTime`: the step at which a walk with given kill signals is killed. +* `Cslib.killTime`: the step at which a walk with given kill signals is killed. * `Cslib.RotationMap.killedPow`: the killed power of a rotation map. ## Main results -* `Cslib.RotationMap.killTime_cons`: a walk survives its first step unless its first signal is `0`, +* `Cslib.killTime_cons`: a walk survives its first step unless its first signal is `0`, and is then killed one step after the walk along its remaining signals. -* `Cslib.RotationMap.card_filter_killTime_eq`, `Cslib.RotationMap.card_filter_le_killTime`: the +* `Cslib.card_filter_killTime_eq`, `Cslib.card_filter_le_killTime`: the truncated geometric law of the kill time. -* `Cslib.RotationMap.sum_ite_killTime_eq`, `Cslib.RotationMap.card_filter_killTime_eq_and`: given +* `Cslib.sum_ite_killTime_eq`, `Cslib.card_filter_killTime_eq_and`: given its kill time, a killed walk is a uniformly random walk of that length. -* `Cslib.RotationMap.expect_killTime_eq`, `Cslib.RotationMap.expect_le_killTime`, - `Cslib.RotationMap.expect_ite_killTime_eq`, `Cslib.RotationMap.expect_prod_ite_killTime_eq`: the +* `Cslib.expect_killTime_eq`, `Cslib.expect_le_killTime`, + `Cslib.expect_ite_killTime_eq`, `Cslib.expect_prod_ite_killTime_eq`: the law of killed walks, as uniform averages. * `Cslib.RotationMap.card_filter_killTime_eq_and_splitWalk`: the crossing count for killed walks. * `Cslib.RotationMap.neighbor_killedPow`, `Cslib.RotationMap.rot_pow_killTime`: the edges of the @@ -67,12 +67,12 @@ that the reverse is killed at the same step. @[expose] public section -namespace Cslib.RotationMap +namespace Cslib open Finset open scoped BigOperators -variable {V D : Type*} (G : RotationMap V D) +variable {V D : Type*} section KillTime @@ -203,25 +203,6 @@ theorem card_filter_killTime_eq_and {ℓ : ℕ} (hℓ : ℓ < T) (P : V × (Fin rw [card_filter, card_filter, mul_comm, ← smul_eq_mul, ← sum_ite_killTime_eq hℓ] simp only [ite_and] -/-- **The crossing count for killed walks.** Counted by the dart `d` crossed at step `i`, the walks -of length `T` and kill signals for which the walk is killed at its step `ℓ < T`, crosses `d` at its -step `i < ℓ`, the reverse of its first `i` steps satisfies `P d` and its steps from `i + 1` to `ℓ` -satisfy `Q d` are counted by independent factors and the weight of the length `ℓ`. -/ -theorem card_filter_killTime_eq_and_splitWalk {ℓ : ℕ} (hℓ : ℓ < T) (i : Fin ℓ) - (P : V × D → (Fin i → D) → Prop) (Q : V × D → (Fin (ℓ - (i + 1)) → D) → Prop) - [∀ d, DecidablePred (P d)] [∀ d, DecidablePred (Q d)] : - #{x : V × (Fin T → D) × (Fin T → Fin q) | killTime x.2.2 = ℓ ∧ - (P (G.walkDart (x.1, Fin.take ℓ hℓ.le x.2.1) i) - ((G.pow i).rot (x.1, Fin.take i i.isLt.le (Fin.take ℓ hℓ.le x.2.1))).2 ∧ - Q (G.walkDart (x.1, Fin.take ℓ hℓ.le x.2.1) i) - (G.walkDrop (x.1, Fin.take ℓ hℓ.le x.2.1) (i + 1)).2)} = - (∑ d, #{r | P d r} * #{s | Q d s}) * - (Fintype.card D ^ (T - ℓ) * ((q - 1) ^ ℓ * q ^ (T - (ℓ + 1)))) := by - rw [← G.card_filter_splitWalk i P Q] - exact card_filter_killTime_eq_and hℓ fun w ↦ - P (G.walkDart w i) ((G.pow i).rot (w.1, Fin.take i i.isLt.le w.2)).2 ∧ - Q (G.walkDart w i) (G.walkDrop w (i + 1)).2 - end Law section Expect @@ -291,6 +272,30 @@ theorem expect_prod_ite_killTime_eq [Fintype V] [Nonempty D] {ℓ : ℕ} (hℓ : end Expect +namespace RotationMap + +variable (G : RotationMap V D) + +/-- **The crossing count for killed walks.** Counted by the dart `d` crossed at step `i`, the walks +of length `T` and kill signals for which the walk is killed at its step `ℓ < T`, crosses `d` at its +step `i < ℓ`, the reverse of its first `i` steps satisfies `P d` and its steps from `i + 1` to `ℓ` +satisfy `Q d` are counted by independent factors and the weight of the length `ℓ`. -/ +theorem card_filter_killTime_eq_and_splitWalk {T q : ℕ} [NeZero q] [Fintype V] [Fintype D] + {ℓ : ℕ} (hℓ : ℓ < T) (i : Fin ℓ) + (P : V × D → (Fin i → D) → Prop) (Q : V × D → (Fin (ℓ - (i + 1)) → D) → Prop) + [∀ d, DecidablePred (P d)] [∀ d, DecidablePred (Q d)] : + #{x : V × (Fin T → D) × (Fin T → Fin q) | killTime x.2.2 = ℓ ∧ + (P (G.walkDart (x.1, Fin.take ℓ hℓ.le x.2.1) i) + ((G.pow i).rot (x.1, Fin.take i i.isLt.le (Fin.take ℓ hℓ.le x.2.1))).2 ∧ + Q (G.walkDart (x.1, Fin.take ℓ hℓ.le x.2.1) i) + (G.walkDrop (x.1, Fin.take ℓ hℓ.le x.2.1) (i + 1)).2)} = + (∑ d, #{r | P d r} * #{s | Q d s}) * + (Fintype.card D ^ (T - ℓ) * ((q - 1) ^ ℓ * q ^ (T - (ℓ + 1)))) := by + rw [← G.card_filter_splitWalk i P Q] + exact card_filter_killTime_eq_and hℓ fun w ↦ + P (G.walkDart w i) ((G.pow i).rot (w.1, Fin.take i i.isLt.le w.2)).2 ∧ + Q (G.walkDart w i) (G.walkDrop w (i + 1)).2 + section KilledPow /-- Overwriting the first `n` labels with `r` leaves `r` as the first `n` labels. -/ @@ -345,4 +350,6 @@ theorem rot_pow_killTime (p : V × (Fin T → D) × (Fin T → Fin q)) : end KilledPow -end Cslib.RotationMap +end RotationMap + +end Cslib diff --git a/Complexity/Foundations/Combinatorics/Hypergeometric.lean b/Complexity/Foundations/Combinatorics/Hypergeometric.lean index 2108083c4e..ba914b4ce6 100644 --- a/Complexity/Foundations/Combinatorics/Hypergeometric.lean +++ b/Complexity/Foundations/Combinatorics/Hypergeometric.lean @@ -11,6 +11,7 @@ public import Complexity.Init public import Mathlib.Data.Finset.Powerset public import Mathlib.Algebra.BigOperators.Group.Finset.Defs public import Mathlib.Basic.Real.Basic +import Complexity.Foundations.Data.Finset.Markov import Mathlib.Algebra.BigOperators.Ring.Finset import Mathlib.Algebra.Order.BigOperators.Group.Finset import Mathlib.Data.Finset.Prod @@ -32,8 +33,6 @@ Chebyshev's inequality `X < m ≤ μ` with probability at most `μ / (μ - m)²` ## Main results -* `Cslib.mul_card_filter_le_sum`, `Cslib.card_filter_mul_le_sum`: Markov's inequality for a - `Finset` sum. * `Cslib.sum_card_inter_powersetCard`, `Cslib.sum_card_inter_mul_sub_one_powersetCard`: the first two factorial moments of `#(U ∩ J)` over the `ℓ`-subsets `J`. * `Cslib.sum_card_inter_sub_sq_le`: the variance is at most the mean. @@ -48,27 +47,6 @@ namespace Cslib open Finset -/-- **Markov's inequality** for a `Finset` sum: if `m ≤ f x` whenever `x ∈ s` satisfies `p x`, -then `m * #{x ∈ s | p x} ≤ ∑ x ∈ s, f x`. -/ -theorem mul_card_filter_le_sum {α : Type*} (s : Finset α) (p : α → Prop) - [DecidablePred p] (f : α → ℕ) {m : ℕ} (hm : ∀ x ∈ s, p x → m ≤ f x) : - m * #{x ∈ s | p x} ≤ ∑ x ∈ s, f x := by - rw [mul_comm, ← smul_eq_mul] - exact ((s.filter p).card_nsmul_le_sum f m fun x hx => - hm x (mem_filter.mp hx).1 (mem_filter.mp hx).2).trans - (sum_le_sum_of_subset (filter_subset p s)) - -/-- **Markov's inequality** for a nonnegative `Finset` sum: if `0 ≤ f x` on `s` and `m ≤ f x` -whenever `x ∈ s` satisfies `p x`, then `#{x ∈ s | p x} * m ≤ ∑ x ∈ s, f x`. -/ -theorem card_filter_mul_le_sum {α R : Type*} [Semiring R] [PartialOrder R] [IsOrderedAddMonoid R] - (s : Finset α) (p : α → Prop) [DecidablePred p] (f : α → R) {m : R} - (hf : ∀ x ∈ s, 0 ≤ f x) (hm : ∀ x ∈ s, p x → m ≤ f x) : - (#{x ∈ s | p x} : R) * m ≤ ∑ x ∈ s, f x := by - rw [← nsmul_eq_mul] - exact ((s.filter p).card_nsmul_le_sum f m fun x hx => - hm x (mem_filter.mp hx).1 (mem_filter.mp hx).2).trans - (sum_le_sum_of_subset_of_nonneg (filter_subset p s) fun x hx _ => hf x hx) - variable {α : Type*} [DecidableEq α] {s U : Finset α} {ℓ : ℕ} /-- Double counting: summed over the `t ∈ P`, `#(A ∩ f t)` counts every `a ∈ A` once for each `t` diff --git a/Complexity/Foundations/Combinatorics/PowersetTail.lean b/Complexity/Foundations/Combinatorics/PowersetTail.lean index 2a3fc08b8e..88f997e4fe 100644 --- a/Complexity/Foundations/Combinatorics/PowersetTail.lean +++ b/Complexity/Foundations/Combinatorics/PowersetTail.lean @@ -11,7 +11,7 @@ public import Complexity.Init public import Mathlib.Data.Finset.Powerset public import Mathlib.Algebra.BigOperators.Group.Finset.Defs public import Mathlib.Basic.Real.Basic -import Complexity.Foundations.Combinatorics.Hypergeometric +import Complexity.Foundations.Data.Finset.Markov import Mathlib.Algebra.BigOperators.Ring.Finset import Mathlib.Algebra.Group.Action.Defs import Mathlib.Algebra.Order.BigOperators.Group.Finset diff --git a/Complexity/Foundations/Data/Code/LocalListDecoding.lean b/Complexity/Foundations/Data/Code/LocalListDecoding.lean index 4563c74e27..f8ee424468 100644 --- a/Complexity/Foundations/Data/Code/LocalListDecoding.lean +++ b/Complexity/Foundations/Data/Code/LocalListDecoding.lean @@ -9,7 +9,7 @@ module public import Complexity.Foundations.Data.Code.HintDecoding public import Complexity.Foundations.Data.Code.LocalDecoding -import Complexity.Foundations.Combinatorics.Hypergeometric +import Complexity.Foundations.Data.Finset.Markov import Mathlib.Tactic.Linarith import Mathlib.Tactic.Positivity diff --git a/Complexity/Foundations/Data/Finset/Markov.lean b/Complexity/Foundations/Data/Finset/Markov.lean new file mode 100644 index 0000000000..991b54a2a5 --- /dev/null +++ b/Complexity/Foundations/Data/Finset/Markov.lean @@ -0,0 +1,54 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Algebra.Order.BigOperators.Group.Finset +public import Mathlib.Algebra.Order.Ring.Defs +import Mathlib.Algebra.BigOperators.Ring.Finset + +/-! +# Markov's inequality for finite sums + +If a nonnegative function `f` on a finite set `s` is at least `m` on `{x ∈ s | p x}`, then `m` +times the cardinality of that subset is at most `∑ x ∈ s, f x` +(`Finset.mul_card_filter_le_sum`, `Finset.card_filter_mul_le_sum`). + +## Main results + +* `Finset.mul_card_filter_le_sum`: `m * #{x ∈ s | p x} ≤ ∑ x ∈ s, f x` for `f : α → ℕ`. +* `Finset.card_filter_mul_le_sum`: `(#{x ∈ s | p x} : R) * m ≤ ∑ x ∈ s, f x` for `0 ≤ f x`. +-/ + +@[expose] public section + +open scoped BigOperators + +namespace Finset + +variable {α : Type*} + +/-- **Markov's inequality** for a nonnegative `Finset` sum: if `0 ≤ f x` on `s` and `m ≤ f x` +whenever `x ∈ s` satisfies `p x`, then `#{x ∈ s | p x} * m ≤ ∑ x ∈ s, f x`. -/ +theorem card_filter_mul_le_sum {R : Type*} [Semiring R] [PartialOrder R] [IsOrderedAddMonoid R] + (s : Finset α) (p : α → Prop) [DecidablePred p] (f : α → R) {m : R} + (hf : ∀ x ∈ s, 0 ≤ f x) (hm : ∀ x ∈ s, p x → m ≤ f x) : + (#{x ∈ s | p x} : R) * m ≤ ∑ x ∈ s, f x := by + rw [← nsmul_eq_mul] + exact ((s.filter p).card_nsmul_le_sum f m fun x hx => + hm x (mem_filter.mp hx).1 (mem_filter.mp hx).2).trans + (sum_le_sum_of_subset_of_nonneg (filter_subset p s) fun x hx _ => hf x hx) + +/-- **Markov's inequality** for a `Finset` sum: if `m ≤ f x` whenever `x ∈ s` satisfies `p x`, +then `m * #{x ∈ s | p x} ≤ ∑ x ∈ s, f x`. -/ +theorem mul_card_filter_le_sum (s : Finset α) (p : α → Prop) [DecidablePred p] (f : α → ℕ) + {m : ℕ} (hm : ∀ x ∈ s, p x → m ≤ f x) : + m * #{x ∈ s | p x} ≤ ∑ x ∈ s, f x := + Nat.mul_comm _ _ ▸ s.card_filter_mul_le_sum p f (fun _ _ => Nat.zero_le _) hm + +end Finset diff --git a/ComplexityTests/Axioms.lean b/ComplexityTests/Axioms.lean index c877c841a6..fe042279f0 100644 --- a/ComplexityTests/Axioms.lean +++ b/ComplexityTests/Axioms.lean @@ -2405,10 +2405,10 @@ info: 'Cslib.RotationMap.sq_expect_walkDart_mul_walkDart_sub_le' depends on axio #print axioms Cslib.RotationMap.sq_expect_walkDart_mul_walkDart_sub_le /-- -info: 'Cslib.RotationMap.card_filter_killTime_eq' depends on axioms: [propext, Classical.choice, Quot.sound] +info: 'Cslib.card_filter_killTime_eq' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in -#print axioms Cslib.RotationMap.card_filter_killTime_eq +#print axioms Cslib.card_filter_killTime_eq /-- info: 'Cslib.RotationMap.card_filter_killTime_eq_and_splitWalk' depends on axioms: [propext, Classical.choice, Quot.sound] diff --git a/ComplexityTests/PCPEncodedAmplification.lean b/ComplexityTests/PCPEncodedAmplification.lean index a7e7659c60..56ebd355f4 100644 --- a/ComplexityTests/PCPEncodedAmplification.lean +++ b/ComplexityTests/PCPEncodedAmplification.lean @@ -91,9 +91,9 @@ example : (powered exampleGraph).edges.length = 16 := by decide example : (exampleGraph.powerPreprocessEdge evalConstraint false rotateReflection 1 2 ((0, false), (fun _ => cloud), (fun _ => 1))).constraint (fun _ => false) (fun _ => true) = false := by - have hkill : RotationMap.killTime (fun _ : Fin 1 => (1 : Fin 2)) = 1 := - le_antisymm (RotationMap.killTime_le _) (Nat.succ_le_iff.mpr - ((RotationMap.lt_killTime_iff _ (by decide)).mpr (by decide))) + have hkill : killTime (fun _ : Fin 1 => (1 : Fin 2)) = 1 := + le_antisymm (killTime_le _) (Nat.succ_le_iff.mpr + ((lt_killTime_iff _ (by decide)).mpr (by decide))) simp [Graph.powerPreprocessEdge, RegularConstraintGraph.powerRelationWithInput, hkill, Graph.preprocessRelation, cloud, List.finRange_succ, List.finRange_zero] diff --git a/ComplexityTests/RotationWalk.lean b/ComplexityTests/RotationWalk.lean index fb2ce2cdf5..d288bb0562 100644 --- a/ComplexityTests/RotationWalk.lean +++ b/ComplexityTests/RotationWalk.lean @@ -54,24 +54,24 @@ example (T selected : ℕ) (v : ℕ × Bool) (k : Fin T → Bool) : example : RotationMap.killedPowRotWithInput rotate 4 2 (4, (4, false), ![false, false, true, false], ![1, 1, 1, 0]) = ((4, true), ![false, true, true, false], ![1, 1, 1, 0]) := by - have hkill : RotationMap.killTime (![1, 1, 1, 0] : Fin 4 → Fin 2) = 3 := - (RotationMap.killTime_eq_iff _ (by decide)).mpr (by decide) + have hkill : killTime (![1, 1, 1, 0] : Fin 4 → Fin 2) = 3 := + (killTime_eq_iff _ (by decide)).mpr (by decide) rw [RotationMap.killedPowRotWithInput_of_killTime rotate _ (by decide) hkill] decide example : RotationMap.killedPowRotWithInput rotate 3 2 (4, (4, false), ![false, false, true], ![0, 1, 1]) = ((4, false), ![false, false, true], ![0, 1, 1]) := by - have hkill : RotationMap.killTime (![0, 1, 1] : Fin 3 → Fin 2) = 0 := - (RotationMap.killTime_eq_iff _ (by decide)).mpr (by decide) + have hkill : killTime (![0, 1, 1] : Fin 3 → Fin 2) = 0 := + (killTime_eq_iff _ (by decide)).mpr (by decide) rw [RotationMap.killedPowRotWithInput_of_killTime rotate _ (by decide) hkill] decide example : RotationMap.killedPowRotWithInput rotate 2 1 (4, (4, false), ![true, false], ![0, 0]) = ((4, false), ![true, false], ![0, 0]) := by - have hkill : RotationMap.killTime (![0, 0] : Fin 2 → Fin 1) = 0 := - (RotationMap.killTime_eq_iff _ (by decide)).mpr (by decide) + have hkill : killTime (![0, 0] : Fin 2 → Fin 1) = 0 := + (killTime_eq_iff _ (by decide)).mpr (by decide) rw [RotationMap.killedPowRotWithInput_of_killTime rotate _ (by decide) hkill] decide diff --git a/UPSTREAM.md b/UPSTREAM.md index 53ddd62007..9928f540f6 100644 --- a/UPSTREAM.md +++ b/UPSTREAM.md @@ -206,8 +206,10 @@ agreement during upstream review. | `Foundations/BooleanAnalysis/Fourier` | Consider Mathlib beside `Analysis/Fourier/FiniteAbelian`. | | `Foundations/BooleanAnalysis/{Bernoulli,CoordinateSampling,Fibers,HarmonicTransform,LightPatterns,MirrorSets}`, `Foundations/Analysis/HarmonicMean` | Consider Mathlib probability APIs; generic finite-type `harmonicMean` is split into `Foundations/Analysis/HarmonicMean` (#317). | | `Foundations/BooleanAnalysis/HadamardTester` | Consider the PCP hierarchy. | -| `Foundations/Combinatorics/{FiniteCover,Hypergeometric,Sunflower}` | Consider Mathlib combinatorics; probabilistic-method lemmas belong near `Combinatorics/Probabilistic`. | +| `Foundations/Combinatorics/CentralBinomial` | Consider Mathlib's `Data/Nat/Choose/Central` (`Nat.centralBinom_sq_mul_le`) and `Combinatorics/Choose`. | +| `Foundations/Combinatorics/{FiniteCover,Hypergeometric,PowersetTail,Sunflower}` | Consider Mathlib combinatorics; probabilistic-method lemmas belong near `Combinatorics/Probabilistic`. | | `Foundations/Data/Finset/Expect` | Product-type expectation helpers extracted from `Foundations/Combinatorics/Expander/Products` (#317); Mathlib candidates. | +| `Foundations/Data/Finset/Markov` | Mathlib candidate: `Algebra/Order/BigOperators/Group/Finset` (`Finset.card_filter_mul_le_sum`, `Finset.mul_card_filter_le_sum`). | | `Foundations/Data/Matrix/Permanent` | Mathlib candidate: Laplace expansion of the permanent along row and column 0, beside `LinearAlgebra/Matrix/Permanent` (mirroring `Matrix.det_succ_row_zero`). | | `Foundations/LinearAlgebra/{Rank,Matrix/CutRank,Matrix/Lindsey}` | Mathlib candidates: `LinearAlgebra/Dimension/LinearMap` and `LinearAlgebra/Matrix/Rank`; placement of Lindsey's lemma needs agreement. | | `Probability/PairwiseIndependentHash/Shift` | Consider integration into `PairwiseIndependentHash`. |