diff --git a/Complexity.lean b/Complexity.lean index ced41512e..e9ed8c9a2 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2350,7 +2350,9 @@ public import Complexity.Foundations.Analysis.InnerProductSpace.Basic public import Complexity.Foundations.Analysis.LpNorm public import Complexity.Foundations.Analysis.LpNormMeasure public import Complexity.Foundations.Analysis.MarkovBrothersInequality +public import Complexity.Foundations.Analysis.RootError public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos +public import Complexity.Foundations.Analysis.SpecialFunctions.SmoothSwitch public import Complexity.Foundations.BooleanAnalysis.Bernoulli public import Complexity.Foundations.BooleanAnalysis.Bonami public import Complexity.Foundations.BooleanAnalysis.BucketWeight @@ -2719,13 +2721,16 @@ public import Complexity.Foundations.NumberTheory.SqrtPrimeWindow public import Complexity.Foundations.Order.BooleanSubalgebra public import Complexity.Foundations.Order.Changes public import Complexity.Foundations.Order.UpperLower +public import Complexity.Foundations.Probability.AtomCutoffs public import Complexity.Foundations.Probability.ColumnDetector +public import Complexity.Foundations.Probability.CorrectionAtom public import Complexity.Foundations.Probability.DetectedHierarchy public import Complexity.Foundations.Probability.DetectedStage public import Complexity.Foundations.Probability.Gaussian.Multivariate public import Complexity.Foundations.Probability.Gaussian.Real public import Complexity.Foundations.Probability.Gaussian.Sheppard public import Complexity.Foundations.Probability.HierarchyParams +public import Complexity.Foundations.Probability.RootMetric public import Complexity.Foundations.Probability.SecondMoment public import Complexity.Foundations.Probability.StochasticAtom public import Complexity.Foundations.Quantum.Measurement @@ -2991,6 +2996,7 @@ public import Complexity.Probability.PMF.UniformSubset public import Complexity.Probability.PairwiseIndependent public import Complexity.Probability.PairwiseIndependentHash public import Complexity.Probability.PairwiseIndependentHash.Affine +public import Complexity.Probability.PairwiseIndependentHash.AtomChannels public import Complexity.Probability.PairwiseIndependentHash.DetectorChannels public import Complexity.Probability.PairwiseIndependentHash.HierarchyChannels public import Complexity.Probability.PairwiseIndependentHash.Retention diff --git a/Complexity/Foundations/Analysis/RootError.lean b/Complexity/Foundations/Analysis/RootError.lean new file mode 100644 index 000000000..f11115eb5 --- /dev/null +++ b/Complexity/Foundations/Analysis/RootError.lean @@ -0,0 +1,307 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Analysis.SpecialFunctions.Pow.Real +import Mathlib.Algebra.BigOperators.Field +import Mathlib.Analysis.MeanInequalitiesPow +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.GCongr +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# Root errors and the homogeneous loss + +The estimators of the OpenAI preprint measure the error of a nonnegative quantity by the +difference of `s`-th roots, `|H^{1/s} - H'^{1/s}|`, rather than by `|H - H'|` +[OpenAI2026LogSpace, Sections 5.6 and 7.3]. This file collects the scalar facts behind that choice. + +**Ordinary versus root error** [OpenAI2026LogSpace, (5.21)]. For `0 ≤ z, w ≤ C`, +`|z - w| ≤ s C^{(s-1)/s} |z^{1/s} - w^{1/s}|` (`Cslib.abs_sub_le_mul_abs_rpow_inv_sub`). + +**The homogeneous loss** [OpenAI2026LogSpace, (7.6), Lemma 7.2]. For nonnegative `H`, `H'`, +`L(H, H') = |H - H'|^s / (H + H')^{s-1}` (`Cslib.homogeneousLoss`; for `s ≥ 1`, Lean's division +by zero gives the preprint's value `0` at `H = H' = 0`). It is homogeneous of degree one. It is +comparable to the root error, +`|H^{1/s} - H'^{1/s}|^s / 2^{s-1} ≤ L(H, H') ≤ s^s |H^{1/s} - H'^{1/s}|^s` +(`Cslib.rpow_inv_sub_pow_le_homogeneousLoss`, `Cslib.homogeneousLoss_le_rpow_inv_sub_pow`). +Unlike the root error, it contracts under nonnegative mixtures +(`Cslib.homogeneousLoss_sum_le`), so it passes through conditional expectations. Finally it +controls a clipped relative error: if `0 ≤ H ≤ C₀ G`, then for every `a > 0` and `H' ≥ 0`, +`a · min (1, |H - H'| / (a + G))^s ≤ 2 (3 C₀ + 3)^{s-1} L(H, H')` +(`Cslib.mul_min_pow_le_homogeneousLoss`, (7.7)). + +## Main definitions + +* `Cslib.homogeneousLoss`: the loss `|H - H'|^s / (H + H')^{s-1}`. + +## Main results + +* `Cslib.abs_sub_le_mul_abs_rpow_inv_sub`: ordinary error is controlled by root error. +* `Cslib.homogeneousLoss_nonneg`, `Cslib.homogeneousLoss_self`, `Cslib.homogeneousLoss_comm`, + `Cslib.homogeneousLoss_mul`: basic properties. +* `Cslib.rpow_inv_sub_pow_le_homogeneousLoss`, `Cslib.homogeneousLoss_le_rpow_inv_sub_pow`: + comparability with the root error. +* `Cslib.homogeneousLoss_sum_le`: contraction under nonnegative mixtures and sums. +* `Cslib.mul_min_pow_le_homogeneousLoss`: the clipped relative error bound. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + (5.21), (7.6), (7.7) and Lemma 7.2 (preprint, not peer reviewed) +-/ + +public section + +open Finset + +namespace Cslib + +/-- **Ordinary error is controlled by root error** [OpenAI2026LogSpace, (5.21)]. For +`0 ≤ z, w ≤ C` and `s ≥ 1`, `|z - w| ≤ s C^{(s-1)/s} |z^{1/s} - w^{1/s}|`. -/ +theorem abs_sub_le_mul_abs_rpow_inv_sub {s : ℕ} (hs : s ≠ 0) {z w C : ℝ} (hz : 0 ≤ z) + (hw : 0 ≤ w) (hzC : z ≤ C) (hwC : w ≤ C) : + |z - w| ≤ s * C ^ (((s : ℝ) - 1) / s) * |z ^ (s⁻¹ : ℝ) - w ^ (s⁻¹ : ℝ)| := by + have hC : 0 ≤ C := hz.trans hzC + have hroot : C ^ (((s : ℝ) - 1) / s) = (C ^ (s⁻¹ : ℝ)) ^ (s - 1) := by + rw [← Real.rpow_natCast, ← Real.rpow_mul hC, Nat.cast_sub (Nat.one_le_iff_ne_zero.2 hs), + Nat.cast_one, div_eq_inv_mul] + have hmax : max |z ^ (s⁻¹ : ℝ)| |w ^ (s⁻¹ : ℝ)| ≤ C ^ (s⁻¹ : ℝ) := by + have hs' : (0 : ℝ) ≤ (s : ℝ)⁻¹ := by positivity + rw [abs_of_nonneg (Real.rpow_nonneg hz _), abs_of_nonneg (Real.rpow_nonneg hw _)] + exact max_le (Real.rpow_le_rpow hz hzC hs') (Real.rpow_le_rpow hw hwC hs') + calc |z - w| = |(z ^ (s⁻¹ : ℝ)) ^ s - (w ^ (s⁻¹ : ℝ)) ^ s| := by + rw [Real.rpow_inv_natCast_pow hz hs, Real.rpow_inv_natCast_pow hw hs] + _ ≤ |z ^ (s⁻¹ : ℝ) - w ^ (s⁻¹ : ℝ)| * s * max |z ^ (s⁻¹ : ℝ)| |w ^ (s⁻¹ : ℝ)| ^ (s - 1) := + abs_pow_sub_pow_le _ _ _ + _ ≤ |z ^ (s⁻¹ : ℝ) - w ^ (s⁻¹ : ℝ)| * s * (C ^ (s⁻¹ : ℝ)) ^ (s - 1) := by gcongr + _ = s * C ^ (((s : ℝ) - 1) / s) * |z ^ (s⁻¹ : ℝ) - w ^ (s⁻¹ : ℝ)| := by rw [hroot]; ring + +/-- The **homogeneous loss** `L(H, H') = |H - H'|^s / (H + H')^{s-1}` of the OpenAI preprint +[OpenAI2026LogSpace, (7.6)]. On nonnegative arguments with `s ≥ 1` it agrees with the preprint's +definition, which sets `L(0, 0) = 0`. -/ +noncomputable def homogeneousLoss (s : ℕ) (H H' : ℝ) : ℝ := + |H - H'| ^ s / (H + H') ^ (s - 1) + +variable {s : ℕ} {H H' : ℝ} + +theorem homogeneousLoss_nonneg (hH : 0 ≤ H) (hH' : 0 ≤ H') : 0 ≤ homogeneousLoss s H H' := by + unfold homogeneousLoss; positivity + +@[simp] +theorem homogeneousLoss_self (hs : s ≠ 0) (H : ℝ) : homogeneousLoss s H H = 0 := by + simp [homogeneousLoss, hs] + +theorem homogeneousLoss_comm (s : ℕ) (H H' : ℝ) : + homogeneousLoss s H H' = homogeneousLoss s H' H := by + rw [homogeneousLoss, homogeneousLoss, abs_sub_comm, add_comm] + +/-- The loss is homogeneous of degree one. -/ +theorem homogeneousLoss_mul (hs : s ≠ 0) {c : ℝ} (hc : 0 ≤ c) (H H' : ℝ) : + homogeneousLoss s (c * H) (c * H') = c * homogeneousLoss s H H' := by + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hs + rcases hc.eq_or_lt with rfl | hc + · simp [homogeneousLoss] + simp only [homogeneousLoss, ← mul_sub, ← mul_add, abs_mul, abs_of_pos hc, mul_pow, + Nat.add_sub_cancel] + rw [mul_div_mul_comm, pow_succ, mul_div_cancel_left₀ _ (pow_ne_zero k hc.ne')] + +/-- The loss in terms of the roots `a = H^{1/s}` and `b = H'^{1/s}`, with `b ≤ a`. -/ +private theorem homogeneousLoss_pow_pow {a b : ℝ} (hb : 0 ≤ b) (hba : b ≤ a) : + homogeneousLoss s (a ^ s) (b ^ s) = (a ^ s - b ^ s) ^ s / (a ^ s + b ^ s) ^ (s - 1) := by + rw [homogeneousLoss, abs_of_nonneg (sub_nonneg.2 (pow_le_pow_left₀ hb hba s))] + +/-- `a^{s-1} (a - b) ≤ a^s - b^s ≤ s a^{s-1} (a - b)` for `0 ≤ b ≤ a`. -/ +private theorem pow_sub_pow_bounds {a b : ℝ} (hb : 0 ≤ b) (hba : b ≤ a) (hs : s ≠ 0) : + a ^ (s - 1) * (a - b) ≤ a ^ s - b ^ s ∧ a ^ s - b ^ s ≤ s * a ^ (s - 1) * (a - b) := by + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hs + have ha : 0 ≤ a := hb.trans hba + have hk : b ^ k ≤ a ^ k := pow_le_pow_left₀ hb hba k + simp only [Nat.add_sub_cancel] + constructor + · simp only [pow_succ] + nlinarith [mul_le_mul_of_nonneg_right hk hb] + · have h := abs_pow_sub_pow_le a b (k + 1) + rw [abs_of_nonneg (sub_nonneg.2 (pow_le_pow_left₀ hb hba _)), abs_of_nonneg (sub_nonneg.2 hba), + abs_of_nonneg ha, abs_of_nonneg hb, max_eq_left hba, Nat.add_sub_cancel] at h + exact h.trans (le_of_eq (by ring)) + +/-- Comparability in terms of the roots, with `b ≤ a`. -/ +private theorem homogeneousLoss_pow_pow_bounds {a b : ℝ} (hb : 0 ≤ b) (hba : b ≤ a) + (hs : s ≠ 0) : + (a - b) ^ s / 2 ^ (s - 1) ≤ homogeneousLoss s (a ^ s) (b ^ s) ∧ + homogeneousLoss s (a ^ s) (b ^ s) ≤ (s : ℝ) ^ s * (a - b) ^ s := by + have ha : 0 ≤ a := hb.trans hba + rw [homogeneousLoss_pow_pow hb hba] + rcases ha.eq_or_lt with rfl | ha + · have : b = 0 := le_antisymm hba hb + subst this + simp [zero_pow hs] + obtain ⟨hlo, hhi⟩ := pow_sub_pow_bounds hb hba hs + have hab : 0 ≤ a - b := sub_nonneg.2 hba + have hden : 0 < (a ^ s + b ^ s) ^ (s - 1) := by positivity + have hbs : b ^ s ≤ a ^ s := pow_le_pow_left₀ hb hba s + have key : (a ^ (s - 1)) ^ s = (a ^ s) ^ (s - 1) := by rw [← pow_mul, ← pow_mul, mul_comm] + constructor + · rw [div_le_div_iff₀ (by positivity) hden] + calc (a - b) ^ s * (a ^ s + b ^ s) ^ (s - 1) ≤ (a - b) ^ s * (2 * a ^ s) ^ (s - 1) := by + gcongr; linarith + _ = (a ^ (s - 1) * (a - b)) ^ s * 2 ^ (s - 1) := by rw [mul_pow, mul_pow, key]; ring + _ ≤ (a ^ s - b ^ s) ^ s * 2 ^ (s - 1) := by gcongr + · rw [div_le_iff₀ hden] + calc (a ^ s - b ^ s) ^ s ≤ (s * a ^ (s - 1) * (a - b)) ^ s := by + gcongr + _ = (s : ℝ) ^ s * (a - b) ^ s * (a ^ s) ^ (s - 1) := by rw [mul_pow, mul_pow, key]; ring + _ ≤ (s : ℝ) ^ s * (a - b) ^ s * (a ^ s + b ^ s) ^ (s - 1) := by + gcongr; linarith [pow_nonneg hb s] + +/-- Reduce a statement about `H, H'` to their roots in decreasing order. -/ +private theorem homogeneousLoss_bounds (hs : s ≠ 0) (hH : 0 ≤ H) (hH' : 0 ≤ H') : + |H ^ (s⁻¹ : ℝ) - H' ^ (s⁻¹ : ℝ)| ^ s / 2 ^ (s - 1) ≤ homogeneousLoss s H H' ∧ + homogeneousLoss s H H' ≤ (s : ℝ) ^ s * |H ^ (s⁻¹ : ℝ) - H' ^ (s⁻¹ : ℝ)| ^ s := by + wlog hle : H' ≤ H generalizing H H' + · rw [homogeneousLoss_comm, abs_sub_comm] + exact this hH' hH (le_of_not_ge hle) + have hb : 0 ≤ H' ^ (s⁻¹ : ℝ) := Real.rpow_nonneg hH' _ + have hba : H' ^ (s⁻¹ : ℝ) ≤ H ^ (s⁻¹ : ℝ) := Real.rpow_le_rpow hH' hle (by positivity) + have h := homogeneousLoss_pow_pow_bounds hb hba hs + rw [Real.rpow_inv_natCast_pow hH hs, Real.rpow_inv_natCast_pow hH' hs] at h + rwa [abs_of_nonneg (sub_nonneg.2 hba)] + +/-- The homogeneous loss bounds the root error from above [OpenAI2026LogSpace, Lemma 7.2]. -/ +theorem rpow_inv_sub_pow_le_homogeneousLoss (hs : s ≠ 0) (hH : 0 ≤ H) (hH' : 0 ≤ H') : + |H ^ (s⁻¹ : ℝ) - H' ^ (s⁻¹ : ℝ)| ^ s ≤ 2 ^ (s - 1) * homogeneousLoss s H H' := by + have h := (homogeneousLoss_bounds hs hH hH').1 + rwa [div_le_iff₀ (by positivity), mul_comm] at h + +/-- The root error bounds the homogeneous loss from above [OpenAI2026LogSpace, Lemma 7.2]. -/ +theorem homogeneousLoss_le_rpow_inv_sub_pow (hs : s ≠ 0) (hH : 0 ≤ H) (hH' : 0 ≤ H') : + homogeneousLoss s H H' ≤ (s : ℝ) ^ s * |H ^ (s⁻¹ : ℝ) - H' ^ (s⁻¹ : ℝ)| ^ s := + (homogeneousLoss_bounds hs hH hH').2 + +/-- **Mixture contraction** [OpenAI2026LogSpace, Lemma 7.2]: the homogeneous loss of two +nonnegative mixtures is at most the mixture of the losses. With unit weights this is +subadditivity over finite sums. -/ +theorem homogeneousLoss_sum_le {ι : Type*} (t : Finset ι) (hs : s ≠ 0) {w F F' : ι → ℝ} + (hw : ∀ i ∈ t, 0 ≤ w i) (hF : ∀ i ∈ t, 0 ≤ F i) (hF' : ∀ i ∈ t, 0 ≤ F' i) : + homogeneousLoss s (∑ i ∈ t, w i * F i) (∑ i ∈ t, w i * F' i) ≤ + ∑ i ∈ t, w i * homogeneousLoss s (F i) (F' i) := by + set S : ι → ℝ := fun i => F i + F' i + set D : ι → ℝ := fun i => |F i - F' i| + set A := ∑ i ∈ t, w i * S i + have hS : ∀ i ∈ t, 0 ≤ S i := fun i hi => add_nonneg (hF i hi) (hF' i hi) + have hD : ∀ i ∈ t, D i ≤ S i := fun i hi => + (abs_sub _ _).trans (by rw [abs_of_nonneg (hF i hi), abs_of_nonneg (hF' i hi)]) + have hrhs : 0 ≤ ∑ i ∈ t, w i * homogeneousLoss s (F i) (F' i) := + sum_nonneg fun i hi => mul_nonneg (hw i hi) (homogeneousLoss_nonneg (hF i hi) (hF' i hi)) + have hdiff : |∑ i ∈ t, w i * F i - ∑ i ∈ t, w i * F' i| ≤ ∑ i ∈ t, w i * D i := by + rw [← sum_sub_distrib] + refine (abs_sum_le_sum_abs _ _).trans (le_of_eq (sum_congr rfl fun i hi => ?_)) + rw [← mul_sub, abs_mul, abs_of_nonneg (hw i hi)] + have hsumS : ∑ i ∈ t, w i * F i + ∑ i ∈ t, w i * F' i = A := by + rw [← sum_add_distrib]; exact sum_congr rfl fun i _ => by simp only [S]; ring + have hA : 0 ≤ A := sum_nonneg fun i hi => mul_nonneg (hw i hi) (hS i hi) + rcases hA.eq_or_lt with hA0 | hApos + · -- Every weighted pair vanishes, so the left side is `L(0, 0) = 0`. + have hzero : ∀ i ∈ t, w i * S i = 0 := + (sum_eq_zero_iff_of_nonneg fun i hi => mul_nonneg (hw i hi) (hS i hi)).1 hA0.symm + have hD0 : ∑ i ∈ t, w i * D i = 0 := sum_eq_zero fun i hi => by + have := mul_le_mul_of_nonneg_left (hD i hi) (hw i hi) + have := mul_nonneg (hw i hi) (abs_nonneg (F i - F' i)) + linarith [hzero i hi] + have hl : |∑ i ∈ t, w i * F i - ∑ i ∈ t, w i * F' i| = 0 := + le_antisymm (hD0 ▸ hdiff) (abs_nonneg _) + rw [homogeneousLoss, hl, zero_pow hs, zero_div] + exact hrhs + -- Jensen's inequality for `x ↦ x^s` with weights `w i S i / A` at the points `D i / S i`. + set lam : ι → ℝ := fun i => w i * S i / A + set x : ι → ℝ := fun i => D i / S i + have hlam : ∀ i ∈ t, 0 ≤ lam i := fun i hi => div_nonneg (mul_nonneg (hw i hi) (hS i hi)) hA + have hlam1 : ∑ i ∈ t, lam i = 1 := by rw [← sum_div, div_self hApos.ne'] + have hx : ∀ i ∈ t, 0 ≤ x i := fun i hi => div_nonneg (abs_nonneg _) (hS i hi) + have hjensen := Real.pow_arith_mean_le_arith_mean_pow t lam x hlam hlam1 hx s + have hmean : ∑ i ∈ t, lam i * x i = (∑ i ∈ t, w i * D i) / A := by + rw [sum_div] + refine sum_congr rfl fun i hi => ?_ + rcases (hS i hi).eq_or_lt with h0 | hpos + · have : D i = 0 := le_antisymm (h0 ▸ hD i hi) (abs_nonneg _) + simp only [lam, x, this, ← h0]; simp + · simp only [lam, x]; field_simp + have hmeanpow : ∑ i ∈ t, lam i * x i ^ s = + (∑ i ∈ t, w i * homogeneousLoss s (F i) (F' i)) / A := by + rw [sum_div] + refine sum_congr rfl fun i hi => ?_ + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hs + rcases (hS i hi).eq_or_lt with h0 | hpos + · have : D i = 0 := le_antisymm (h0 ▸ hD i hi) (abs_nonneg _) + simp only [lam, x, homogeneousLoss, this, ← h0] + simp only [show |F i - F' i| = 0 from this]; simp + · simp only [lam, x, homogeneousLoss, Nat.add_sub_cancel, D, S] at * + rw [div_pow, pow_succ (F i + F' i) k] + field_simp + rw [hmean, hmeanpow, div_pow, div_le_div_iff₀ (by positivity) hApos] at hjensen + rw [homogeneousLoss, hsumS] + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hs + rw [Nat.add_sub_cancel, div_le_iff₀ (by positivity)] + have hk := pow_le_pow_left₀ (abs_nonneg _) hdiff (k + 1) + rw [pow_succ A k, ← mul_assoc] at hjensen + exact hk.trans (le_of_mul_le_mul_right hjensen hApos) + +/-- **The clipped relative error** [OpenAI2026LogSpace, (7.7)]. If `0 ≤ H ≤ C₀ G`, then for every +`a > 0` and `H' ≥ 0`, `a · min (1, |H - H'| / (a + G))^s ≤ 2 (3 C₀ + 3)^{s-1} L(H, H')`. -/ +theorem mul_min_pow_le_homogeneousLoss (hs : s ≠ 0) {C₀ G a : ℝ} (hC₀ : 0 ≤ C₀) (hG : 0 ≤ G) + (ha : 0 < a) (hH : 0 ≤ H) (hHG : H ≤ C₀ * G) (hH' : 0 ≤ H') : + a * min 1 (|H - H'| / (a + G)) ^ s ≤ 2 * (3 * C₀ + 3) ^ (s - 1) * homogeneousLoss s H H' := by + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hs + simp only [Nat.add_sub_cancel, homogeneousLoss] + have haG : 0 < a + G := by positivity + have hmin0 : 0 ≤ min 1 (|H - H'| / (a + G)) := le_min zero_le_one (by positivity) + have hC : (3 : ℝ) ^ k ≤ (3 * C₀ + 3) ^ k := pow_le_pow_left₀ (by norm_num) (by linarith) k + by_cases hcase : H' ≤ 2 * H + a + · -- `H + H' ≤ (3 C₀ + 3) (a + G)`, and `a / (a + G)^{k+1} ≤ 1 / (a + G)^k`. + have hsum : H + H' ≤ (3 * C₀ + 3) * (a + G) := by nlinarith + rcases (add_nonneg hH hH').eq_or_lt with h0 | hpos + · have h1 : H = 0 := by linarith + have h2 : H' = 0 := by linarith + simp [h1, h2] + have hd : 0 ≤ |H - H'| := abs_nonneg _ + calc a * min 1 (|H - H'| / (a + G)) ^ (k + 1) + ≤ a * (|H - H'| / (a + G)) ^ (k + 1) := by gcongr; exact min_le_right _ _ + _ ≤ |H - H'| ^ (k + 1) / (a + G) ^ k := by + rw [div_pow, ← mul_div_assoc, div_le_div_iff₀ (by positivity) (by positivity), + pow_succ (a + G) k] + have hX : 0 ≤ |H - H'| ^ (k + 1) * (a + G) ^ k := by positivity + nlinarith [mul_le_mul_of_nonneg_left (show a ≤ a + G by linarith) hX] + _ = (3 * C₀ + 3) ^ k * (|H - H'| ^ (k + 1) / ((3 * C₀ + 3) * (a + G)) ^ k) := by + rw [mul_pow]; field_simp + _ ≤ (3 * C₀ + 3) ^ k * (|H - H'| ^ (k + 1) / (H + H') ^ k) := by gcongr + _ ≤ 2 * (3 * C₀ + 3) ^ k * (|H - H'| ^ (k + 1) / (H + H') ^ k) := by + have : 0 ≤ (3 * C₀ + 3) ^ k * (|H - H'| ^ (k + 1) / (H + H') ^ k) := by positivity + linarith + · -- `|H - H'| > H' / 2`, `H + H' < 3 H' / 2` and `H' > a`, so the loss is at least + -- `H' / (2 · 3^k) ≥ a / (2 · 3^k)`. + push Not at hcase + have hH'pos : 0 < H' := by linarith + have hd : H' / 2 ≤ |H - H'| := by rw [abs_sub_comm, abs_of_pos (by linarith)]; linarith + have hden : 0 < (H + H') ^ k := by positivity + have hlow : H' / (2 * 3 ^ k) ≤ |H - H'| ^ (k + 1) / (H + H') ^ k := by + rw [div_le_div_iff₀ (by positivity) hden] + calc H' * (H + H') ^ k ≤ H' * (3 * (H' / 2)) ^ k := by gcongr; linarith + _ = 2 * 3 ^ k * (H' / 2) ^ (k + 1) := by rw [mul_pow, pow_succ]; ring + _ ≤ |H - H'| ^ (k + 1) * (2 * 3 ^ k) := by + rw [mul_comm]; gcongr + calc a * min 1 (|H - H'| / (a + G)) ^ (k + 1) ≤ a * 1 := by + gcongr + exact pow_le_one₀ hmin0 (min_le_left _ _) + _ ≤ 2 * 3 ^ k * (H' / (2 * 3 ^ k)) := by field_simp; linarith + _ ≤ 2 * (3 * C₀ + 3) ^ k * (|H - H'| ^ (k + 1) / (H + H') ^ k) := by + gcongr + +end Cslib diff --git a/Complexity/Foundations/Analysis/SpecialFunctions/SmoothSwitch.lean b/Complexity/Foundations/Analysis/SpecialFunctions/SmoothSwitch.lean new file mode 100644 index 000000000..90e2d253c --- /dev/null +++ b/Complexity/Foundations/Analysis/SpecialFunctions/SmoothSwitch.lean @@ -0,0 +1,186 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Analysis.SpecialFunctions.SmoothTransition +public import Mathlib.Analysis.SpecialFunctions.Pow.Real +public import Mathlib.Topology.MetricSpace.Lipschitz +import Mathlib.Analysis.Calculus.ContDiff.RCLike +import Mathlib.Analysis.SpecialFunctions.Pow.Deriv +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Positivity + +/-! +# Smooth switches with Lipschitz roots + +A *switch* `χ_{α,β}` is a nondecreasing function that vanishes on `(-∞, α]` and is one on +`[β, ∞)`. The stochastic atoms of the OpenAI preprint need switches such that `χ_{α,β} ^ (1/s)` +and `(1 - χ_{α,β}) ^ (1/s)` are Lipschitz, so that errors in the root metrics of the later +estimates propagate linearly through every cutoff [OpenAI2026LogSpace, Section 5.1]. + +We take Mathlib's `Real.smoothTransition`, rescaled to `[α, β]` (`Cslib.smoothSwitch`). The +preprint instead rescales a normalized integral of `z^{s-1} (1 - z)^{s-1}`; any fixed switch with +these properties serves. Every positive power of `Real.smoothTransition` is again continuously +differentiable, since `exp (-1/x) ^ p = exp (-1/(x/p))`, and it is constant outside `[0, 1]`. Hence +every positive power is Lipschitz (`Real.smoothTransition.exists_lipschitzWith_rpow`). +The complement is the reflection +`1 - smoothTransition x = smoothTransition (1 - x)` (`Real.smoothTransition.one_sub`), so its powers +are Lipschitz too. + +## Main definitions + +* `Cslib.smoothSwitch`: the switch `χ_{α,β}`. + +## Main results + +* `Real.smoothTransition.one_sub`: the complement of the transition is its reflection. +* `Real.smoothTransition.exists_lipschitzWith_rpow`, + `Real.smoothTransition.exists_lipschitzWith_one_sub_rpow`: positive powers of the transition + and of its complement are Lipschitz. +* `Cslib.smoothSwitch_eq_zero_iff`, `Cslib.smoothSwitch_eq_one_iff`, `Cslib.smoothSwitch_nonneg`, + `Cslib.smoothSwitch_le_one`, `Cslib.monotone_smoothSwitch`: the switch properties. +* `Cslib.exists_lipschitzWith_smoothSwitch_rpow`, + `Cslib.exists_lipschitzWith_one_sub_smoothSwitch_rpow`: the root-Lipschitz properties. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 5.1 (preprint, not peer reviewed) +-/ + +public section + +open Set + +namespace Real.smoothTransition + +/-- The complement of the smooth transition is its reflection at `1/2`. -/ +theorem one_sub (x : ℝ) : 1 - smoothTransition x = smoothTransition (1 - x) := by + have hD := pos_denom x + simp only [smoothTransition, sub_sub_cancel] + rw [add_comm (expNegInvGlue (1 - x)), eq_div_iff hD.ne', sub_mul, div_mul_cancel₀ _ hD.ne'] + ring + +/-- A positive power of `expNegInvGlue` is a rescaling of it. -/ +private theorem expNegInvGlue_rpow {p : ℝ} (hp : 0 < p) (x : ℝ) : + expNegInvGlue x ^ p = expNegInvGlue (x / p) := by + rcases le_or_gt x 0 with hx | hx + · rw [expNegInvGlue.zero_of_nonpos hx, expNegInvGlue.zero_of_nonpos + (div_nonpos_of_nonpos_of_nonneg hx hp.le), Real.zero_rpow hp.ne'] + · have hxp : ¬ x / p ≤ 0 := not_le.2 (div_pos hx hp) + simp only [expNegInvGlue, not_le.2 hx, hxp, ite_false, ← Real.exp_mul] + congr 1 + field_simp + +/-- Positive powers of the smooth transition are smooth. -/ +private theorem contDiff_rpow {p : ℝ} (hp : 0 < p) : + ContDiff ℝ 1 fun x => smoothTransition x ^ p := by + have h : (fun x => smoothTransition x ^ p) = fun x => + expNegInvGlue (x / p) / (expNegInvGlue x + expNegInvGlue (1 - x)) ^ p := by + funext x + rw [smoothTransition, Real.div_rpow (expNegInvGlue.nonneg x) (pos_denom x).le, + expNegInvGlue_rpow hp] + rw [h] + refine (expNegInvGlue.contDiff.comp (contDiff_id.div_const p)).div ?_ fun x => + (Real.rpow_pos_of_pos (pos_denom x) p).ne' + exact (expNegInvGlue.contDiff.add (expNegInvGlue.contDiff.comp + (contDiff_const.sub contDiff_id))).rpow_const_of_ne fun x => (pos_denom x).ne' + +/-- A function of the smooth transition that is `C¹` is Lipschitz, since the transition is +constant outside `[0, 1]`. -/ +private theorem exists_lipschitzWith_comp {g : ℝ → ℝ} + (hg : ContDiff ℝ 1 fun x => g (smoothTransition x)) : + ∃ K, LipschitzWith K fun x => g (smoothTransition x) := by + obtain ⟨K, hK⟩ := hg.contDiffOn.exists_lipschitzOnWith (s := Icc (0 : ℝ) 1) one_ne_zero + (convex_Icc 0 1) isCompact_Icc + refine ⟨K, LipschitzWith.of_dist_le_mul fun x y => ?_⟩ + have hproj := (LipschitzWith.projIcc (zero_le_one' ℝ)).dist_le_mul x y + rw [← smoothTransition.projIcc (x := x), ← smoothTransition.projIcc (x := y)] + refine (hK.dist_le_mul _ (projIcc 0 1 _ x).2 _ (projIcc 0 1 _ y).2).trans ?_ + rw [Subtype.dist_eq] at hproj + simp only [NNReal.coe_one, one_mul] at hproj + exact mul_le_mul_of_nonneg_left hproj K.2 + +/-- Every positive power of the smooth transition is Lipschitz. -/ +theorem exists_lipschitzWith_rpow {p : ℝ} (hp : 0 < p) : + ∃ K, LipschitzWith K fun x => smoothTransition x ^ p := + exists_lipschitzWith_comp (g := fun t => t ^ p) (contDiff_rpow hp) + +/-- Every positive power of the complement of the smooth transition is Lipschitz. -/ +theorem exists_lipschitzWith_one_sub_rpow {p : ℝ} (hp : 0 < p) : + ∃ K, LipschitzWith K fun x => (1 - smoothTransition x) ^ p := by + obtain ⟨K, hK⟩ := exists_lipschitzWith_rpow hp + refine ⟨K, LipschitzWith.of_dist_le_mul fun x y => ?_⟩ + simp only [one_sub] + simpa only [dist_sub_left] using hK.dist_le_mul (1 - x) (1 - y) + +end smoothTransition + +end Real + +namespace Cslib + +open Real + +/-- The switch `χ_{α,β}`: `Real.smoothTransition` rescaled from `[0, 1]` to `[α, β]`. It vanishes +on `(-∞, α]`, is one on `[β, ∞)` and is nondecreasing [OpenAI2026LogSpace, Section 5.1]. -/ +noncomputable def smoothSwitch (α β t : ℝ) : ℝ := + smoothTransition ((t - α) / (β - α)) + +variable {α β t : ℝ} + +theorem smoothSwitch_nonneg (α β t : ℝ) : 0 ≤ smoothSwitch α β t := + smoothTransition.nonneg _ + +theorem smoothSwitch_le_one (α β t : ℝ) : smoothSwitch α β t ≤ 1 := + smoothTransition.le_one _ + +theorem smoothSwitch_eq_zero_iff (hαβ : α < β) : smoothSwitch α β t = 0 ↔ t ≤ α := by + rw [smoothSwitch, smoothTransition.zero_iff_nonpos, div_le_iff₀ (sub_pos.2 hαβ), zero_mul, + sub_nonpos] + +theorem smoothSwitch_eq_one_iff (hαβ : α < β) : smoothSwitch α β t = 1 ↔ β ≤ t := by + rw [smoothSwitch, smoothTransition.eq_one_iff_one_le, one_le_div (sub_pos.2 hαβ), + sub_le_sub_iff_right] + +theorem smoothSwitch_of_le (hαβ : α < β) (ht : t ≤ α) : smoothSwitch α β t = 0 := + (smoothSwitch_eq_zero_iff hαβ).2 ht + +theorem smoothSwitch_of_ge (hαβ : α < β) (ht : β ≤ t) : smoothSwitch α β t = 1 := + (smoothSwitch_eq_one_iff hαβ).2 ht + +theorem monotone_smoothSwitch (hαβ : α ≤ β) : Monotone (smoothSwitch α β) := + fun _ _ h => smoothTransition.monotone + (div_le_div_of_nonneg_right (sub_le_sub_right h α) (sub_nonneg.2 hαβ)) + +/-- Rescaling the argument of a Lipschitz function. -/ +private theorem lipschitzWith_comp_rescale {g : ℝ → ℝ} {K : NNReal} (hg : LipschitzWith K g) + (hαβ : α < β) : + LipschitzWith (K * (β - α)⁻¹.toNNReal) fun t => g ((t - α) / (β - α)) := by + refine LipschitzWith.of_dist_le_mul fun x y => ?_ + refine (hg.dist_le_mul _ _).trans (le_of_eq ?_) + rw [NNReal.coe_mul, Real.coe_toNNReal _ (inv_nonneg.2 (sub_pos.2 hαβ).le), Real.dist_eq, + Real.dist_eq, ← sub_div, sub_sub_sub_cancel_right, abs_div, abs_of_pos (sub_pos.2 hαβ), + div_eq_mul_inv] + ring + +/-- Every positive power of a switch is Lipschitz; for `p = 1/s` this is the root-Lipschitz +property of [OpenAI2026LogSpace, Section 5.1]. -/ +theorem exists_lipschitzWith_smoothSwitch_rpow (hαβ : α < β) {p : ℝ} (hp : 0 < p) : + ∃ K, LipschitzWith K fun t => smoothSwitch α β t ^ p := by + obtain ⟨K, hK⟩ := smoothTransition.exists_lipschitzWith_rpow hp + exact ⟨_, lipschitzWith_comp_rescale hK hαβ⟩ + +/-- Every positive power of the complement of a switch is Lipschitz. -/ +theorem exists_lipschitzWith_one_sub_smoothSwitch_rpow (hαβ : α < β) {p : ℝ} (hp : 0 < p) : + ∃ K, LipschitzWith K fun t => (1 - smoothSwitch α β t) ^ p := by + obtain ⟨K, hK⟩ := smoothTransition.exists_lipschitzWith_one_sub_rpow hp + exact ⟨_, lipschitzWith_comp_rescale hK hαβ⟩ + +end Cslib diff --git a/Complexity/Foundations/Data/Finset/KthLargest.lean b/Complexity/Foundations/Data/Finset/KthLargest.lean index b1198aef3..33b6107d3 100644 --- a/Complexity/Foundations/Data/Finset/KthLargest.lean +++ b/Complexity/Foundations/Data/Finset/KthLargest.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Init +public import Mathlib.Algebra.Order.Group.Abs public import Mathlib.Data.Finset.Max /-! @@ -31,6 +32,8 @@ is at least `t` exactly when at least `k` values are at least `t` (`Finset.le_kt * `Finset.kthLargest_nonneg`, `Finset.kthLargest_le`: bounds. * `Finset.lt_kthLargest_iff`, `Finset.le_kthLargest_iff`: the threshold characterizations. +* `Finset.kthLargest_le_kthLargest_add`, `Finset.abs_kthLargest_sub_kthLargest_le`: stability + under perturbation of the values. ## References @@ -113,4 +116,37 @@ theorem le_kthLargest_iff (hk : 0 < k) (ht : 0 < t) : obtain ⟨x, hxs, htx, hkx⟩ := exists_le_card hk (t ≤ ·) hcard exact htx.trans (le_kthLargest_of_le_card hxs hkx) +section Stability + +variable {R : Type*} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] {k : ℕ} + {s : Finset α} {h₁ h₂ : α → R} {ε : R} + +/-- **Rank stability, one side** [OpenAI2026LogSpace, (5.4)]: if every value of `h₁` exceeds the +corresponding value of `h₂` by at most `ε ≥ 0`, so does the `k`-th largest value. -/ +theorem kthLargest_le_kthLargest_add (hk : 0 < k) (hε : 0 ≤ ε) (h : ∀ x ∈ s, h₁ x ≤ h₂ x + ε) : + kthLargest k s h₁ ≤ kthLargest k s h₂ + ε := by + set r := kthLargest k s h₁ + rcases le_or_gt r ε with hr | hr + · exact hr.trans (le_add_of_nonneg_left kthLargest_nonneg) + have hr0 : 0 < r := hε.trans_lt hr + have hcard := (le_kthLargest_iff hk hr0).mp le_rfl + have hlo : r - ε ≤ kthLargest k s h₂ := by + refine (le_kthLargest_iff hk (sub_pos.mpr hr)).mpr (hcard.trans (card_le_card fun x hx => ?_)) + rw [mem_filter] at hx ⊢ + exact ⟨hx.1, sub_le_iff_le_add.mpr (hx.2.trans (h x hx.1))⟩ + exact sub_le_iff_le_add.mp hlo + +/-- **Rank stability** [OpenAI2026LogSpace, (5.4)]: `|rank_k h₁ − rank_k h₂| ≤ sup |h₁ − h₂|`. +If the values differ by at most `ε ≥ 0` everywhere on `s`, so do their `k`-th largest values. -/ +theorem abs_kthLargest_sub_kthLargest_le (hk : 0 < k) (hε : 0 ≤ ε) + (h : ∀ x ∈ s, |h₁ x - h₂ x| ≤ ε) : |kthLargest k s h₁ - kthLargest k s h₂| ≤ ε := by + rw [abs_sub_le_iff] + constructor + · exact sub_le_iff_le_add'.mpr (kthLargest_le_kthLargest_add hk hε fun x hx => + sub_le_iff_le_add'.mp (le_of_abs_le (h x hx))) + · exact sub_le_iff_le_add'.mpr (kthLargest_le_kthLargest_add hk hε fun x hx => + sub_le_iff_le_add'.mp (le_of_abs_le ((abs_sub_comm _ _).trans_le (h x hx)))) + +end Stability + end Finset diff --git a/Complexity/Foundations/Probability/AtomCutoffs.lean b/Complexity/Foundations/Probability/AtomCutoffs.lean new file mode 100644 index 000000000..5494d4687 --- /dev/null +++ b/Complexity/Foundations/Probability/AtomCutoffs.lean @@ -0,0 +1,195 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Analysis.SpecialFunctions.SmoothSwitch +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# Smooth cutoffs of the stochastic atoms + +The dense and correction atoms (`Complexity.Foundations.Probability.StochasticAtom`, +`Complexity.Foundations.Probability.CorrectionAtom`) take their cutoff functions as parameters, +with only the threshold properties each statement uses. This file supplies the preprint's explicit +choices, built from the smooth switches `Cslib.smoothSwitch` [OpenAI2026LogSpace, (5.5), (5.12)]. +Fix a lower support threshold `ϑ > 0` of a main row function, and let `v` be a scaled entry and `r` +the `K`-th rank of its row: + +* the preparatory factor `h_ϑ(v) = χ_{ϑ/2, 3ϑ/4}(v)` (`Cslib.prepCutoff`); +* the row gate `R_ϑ(r) = 1 - χ_{ϑ/1000, ϑ/500}(r)` (`Cslib.rowCutoff`); +* the auxiliary score `I_ϑ(v, r) = χ_{ϑ/8, ϑ/4}(v) (1 - χ_{ϑ/100, ϑ/50}(r))` (`Cslib.auxCutoff`); +* the incoming cutoff `1 - χ_{1/4, 1/2}` (`Cslib.incomingCutoff`). + +Each lemma below is a hypothesis of the atom identities or support bounds; for example +`Cslib.auxCutoff_eq_one_of_rowCutoff_ne_zero` is the hypothesis of the incoming cap +(`Matrix.card_filter_correctionAtom_col_ne_zero_lt`) for a main function supported above `ϑ/4`. +Every positive power of each cutoff is Lipschitz, the auxiliary score jointly in both arguments +[OpenAI2026LogSpace, Section 5.1: "Products of bounded functions with Lipschitz `s`th roots again +have Lipschitz `s`th roots"]. + +## Main definitions + +* `Cslib.prepCutoff`, `Cslib.rowCutoff`, `Cslib.auxCutoff`, `Cslib.incomingCutoff`. + +## Main results + +* `Cslib.prepCutoff_eq_one`, `Cslib.rowCutoff_eq_one`, `Cslib.rowCutoff_eq_zero_iff`, + `Cslib.auxCutoff_eq_zero`, `Cslib.auxCutoff_eq_one_of_rowCutoff_ne_zero`, + `Cslib.incomingCutoff_eq_one`, `Cslib.incomingCutoff_eq_zero`: the thresholds. +* `Cslib.exists_lipschitzWith_prepCutoff_rpow`, `Cslib.exists_lipschitzWith_rowCutoff_rpow`, + `Cslib.exists_lipschitzWith_incomingCutoff_rpow`, `Cslib.exists_abs_auxCutoff_rpow_sub_le`: the + root-Lipschitz properties. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Sections 5.1 and 5.3 (preprint, not peer reviewed) +-/ + +public section + +namespace Cslib + +/-- The preparatory factor `h_ϑ = χ_{ϑ/2, 3ϑ/4}` [OpenAI2026LogSpace, (5.5)]. -/ +noncomputable def prepCutoff (ϑ v : ℝ) : ℝ := + smoothSwitch (ϑ / 2) (3 * ϑ / 4) v + +/-- The row gate `R_ϑ = 1 - χ_{ϑ/1000, ϑ/500}`, applied to the `K`-th rank of a row +[OpenAI2026LogSpace, (5.5)]. -/ +noncomputable def rowCutoff (ϑ r : ℝ) : ℝ := + 1 - smoothSwitch (ϑ / 1000) (ϑ / 500) r + +/-- The auxiliary score `I_ϑ(v, r) = χ_{ϑ/8, ϑ/4}(v) (1 - χ_{ϑ/100, ϑ/50}(r))` of an entry `v` with +row rank `r` [OpenAI2026LogSpace, (5.5)]. -/ +noncomputable def auxCutoff (ϑ v r : ℝ) : ℝ := + smoothSwitch (ϑ / 8) (ϑ / 4) v * (1 - smoothSwitch (ϑ / 100) (ϑ / 50) r) + +/-- The incoming cutoff `1 - χ_{1/4, 1/2}`, applied to the `K_c`-th auxiliary rank of a column +[OpenAI2026LogSpace, (5.12)]. -/ +noncomputable def incomingCutoff (r : ℝ) : ℝ := + 1 - smoothSwitch (1 / 4) (1 / 2) r + +variable {ϑ v r : ℝ} + +/-! ### Thresholds -/ + +theorem prepCutoff_eq_one (hϑ : 0 < ϑ) (hv : 3 * ϑ / 4 ≤ v) : prepCutoff ϑ v = 1 := + smoothSwitch_of_ge (by linarith) hv + +theorem prepCutoff_eq_zero (hϑ : 0 < ϑ) (hv : v ≤ ϑ / 2) : prepCutoff ϑ v = 0 := + smoothSwitch_of_le (by linarith) hv + +theorem rowCutoff_nonneg (ϑ r : ℝ) : 0 ≤ rowCutoff ϑ r := + sub_nonneg.2 (smoothSwitch_le_one _ _ _) + +theorem rowCutoff_le_one (ϑ r : ℝ) : rowCutoff ϑ r ≤ 1 := + sub_le_self _ (smoothSwitch_nonneg _ _ _) + +theorem rowCutoff_eq_one (hϑ : 0 < ϑ) (hr : r ≤ ϑ / 1000) : rowCutoff ϑ r = 1 := by + rw [rowCutoff, smoothSwitch_of_le (by linarith) hr, sub_zero] + +theorem rowCutoff_eq_zero_iff (hϑ : 0 < ϑ) : rowCutoff ϑ r = 0 ↔ ϑ / 500 ≤ r := by + rw [rowCutoff, sub_eq_zero, eq_comm, smoothSwitch_eq_one_iff (by linarith)] + +theorem rowCutoff_eq_zero (hϑ : 0 < ϑ) (hr : ϑ / 500 ≤ r) : rowCutoff ϑ r = 0 := + (rowCutoff_eq_zero_iff hϑ).2 hr + +theorem auxCutoff_nonneg (ϑ v r : ℝ) : 0 ≤ auxCutoff ϑ v r := + mul_nonneg (smoothSwitch_nonneg _ _ _) (sub_nonneg.2 (smoothSwitch_le_one _ _ _)) + +theorem auxCutoff_le_one (ϑ v r : ℝ) : auxCutoff ϑ v r ≤ 1 := + (mul_le_of_le_one_right (smoothSwitch_nonneg _ _ _) + (sub_le_self _ (smoothSwitch_nonneg _ _ _))).trans (smoothSwitch_le_one _ _ _) + +theorem auxCutoff_eq_zero (hϑ : 0 < ϑ) (hv : v ≤ ϑ / 8) : auxCutoff ϑ v r = 0 := by + rw [auxCutoff, smoothSwitch_of_le (by linarith) hv, zero_mul] + +theorem auxCutoff_eq_one (hϑ : 0 < ϑ) (hv : ϑ / 4 ≤ v) (hr : r ≤ ϑ / 100) : + auxCutoff ϑ v r = 1 := by + rw [auxCutoff, smoothSwitch_of_ge (by linarith) hv, smoothSwitch_of_le (by linarith) hr] + norm_num + +/-- Where the row gate is open and the entry is at least `ϑ/4`, the auxiliary score is one. This +is the hypothesis of the incoming cap [OpenAI2026LogSpace, proof of Lemma 5.6]. -/ +theorem auxCutoff_eq_one_of_rowCutoff_ne_zero (hϑ : 0 < ϑ) (hv : ϑ / 4 ≤ v) + (hr : rowCutoff ϑ r ≠ 0) : auxCutoff ϑ v r = 1 := by + refine auxCutoff_eq_one hϑ hv ?_ + have := mt (rowCutoff_eq_zero hϑ) hr + linarith + +theorem incomingCutoff_nonneg (r : ℝ) : 0 ≤ incomingCutoff r := + sub_nonneg.2 (smoothSwitch_le_one _ _ _) + +theorem incomingCutoff_le_one (r : ℝ) : incomingCutoff r ≤ 1 := + sub_le_self _ (smoothSwitch_nonneg _ _ _) + +theorem incomingCutoff_eq_one (hr : r ≤ 1 / 4) : incomingCutoff r = 1 := by + rw [incomingCutoff, smoothSwitch_of_le (by norm_num) hr, sub_zero] + +theorem incomingCutoff_eq_zero (hr : 1 / 2 ≤ r) : incomingCutoff r = 0 := by + rw [incomingCutoff, smoothSwitch_of_ge (by norm_num) hr, sub_self] + +/-! ### Lipschitz roots -/ + +variable {p : ℝ} + +theorem exists_lipschitzWith_prepCutoff_rpow (hϑ : 0 < ϑ) (hp : 0 < p) : + ∃ K, LipschitzWith K fun v => prepCutoff ϑ v ^ p := + exists_lipschitzWith_smoothSwitch_rpow (by linarith) hp + +theorem exists_lipschitzWith_rowCutoff_rpow (hϑ : 0 < ϑ) (hp : 0 < p) : + ∃ K, LipschitzWith K fun r => rowCutoff ϑ r ^ p := + exists_lipschitzWith_one_sub_smoothSwitch_rpow (by linarith) hp + +theorem exists_lipschitzWith_incomingCutoff_rpow (hp : 0 < p) : + ∃ K, LipschitzWith K fun r => incomingCutoff r ^ p := + exists_lipschitzWith_one_sub_smoothSwitch_rpow (by norm_num) hp + +/-- The positive powers of the auxiliary score are Lipschitz in both arguments. -/ +theorem exists_abs_auxCutoff_rpow_sub_le (hϑ : 0 < ϑ) (hp : 0 < p) : + ∃ L : ℝ, ∀ v r v' r', |auxCutoff ϑ v r ^ p - auxCutoff ϑ v' r' ^ p| ≤ + L * (|v - v'| + |r - r'|) := by + obtain ⟨Ka, hKa⟩ := exists_lipschitzWith_smoothSwitch_rpow (α := ϑ / 8) (β := ϑ / 4) + (by linarith) hp + obtain ⟨Kb, hKb⟩ := exists_lipschitzWith_one_sub_smoothSwitch_rpow (α := ϑ / 100) + (β := ϑ / 50) (by linarith) hp + refine ⟨max Ka Kb, fun v r v' r' => ?_⟩ + set a : ℝ → ℝ := fun v => smoothSwitch (ϑ / 8) (ϑ / 4) v + set b : ℝ → ℝ := fun r => 1 - smoothSwitch (ϑ / 100) (ϑ / 50) r + have ha0 : ∀ v, 0 ≤ a v := fun v => smoothSwitch_nonneg _ _ _ + have hb0 : ∀ r, 0 ≤ b r := fun r => sub_nonneg.2 (smoothSwitch_le_one _ _ _) + have ha1 : ∀ v, a v ^ p ≤ 1 := fun v => + Real.rpow_le_one (ha0 v) (smoothSwitch_le_one _ _ _) hp.le + have hb1 : ∀ r, b r ^ p ≤ 1 := fun r => + Real.rpow_le_one (hb0 r) (sub_le_self _ (smoothSwitch_nonneg _ _ _)) hp.le + have hda : |a v ^ p - a v' ^ p| ≤ Ka * |v - v'| := by + simpa only [Real.dist_eq] using hKa.dist_le_mul v v' + have hdb : |b r ^ p - b r' ^ p| ≤ Kb * |r - r'| := by + simpa only [Real.dist_eq] using hKb.dist_le_mul r r' + have hsplit : auxCutoff ϑ v r ^ p - auxCutoff ϑ v' r' ^ p = + (a v ^ p - a v' ^ p) * b r ^ p + a v' ^ p * (b r ^ p - b r' ^ p) := by + simp only [auxCutoff, Real.mul_rpow (ha0 _) (hb0 _), a, b] + ring + rw [hsplit] + have hbp : 0 ≤ b r ^ p := Real.rpow_nonneg (hb0 r) p + have hap : 0 ≤ a v' ^ p := Real.rpow_nonneg (ha0 v') p + calc |(a v ^ p - a v' ^ p) * b r ^ p + a v' ^ p * (b r ^ p - b r' ^ p)| + ≤ |a v ^ p - a v' ^ p| * b r ^ p + a v' ^ p * |b r ^ p - b r' ^ p| := by + refine (abs_add_le _ _).trans (le_of_eq ?_) + rw [abs_mul, abs_mul, abs_of_nonneg hbp, abs_of_nonneg hap] + _ ≤ |a v ^ p - a v' ^ p| * 1 + 1 * |b r ^ p - b r' ^ p| := by + gcongr + exacts [hb1 r, ha1 v'] + _ ≤ Ka * |v - v'| + Kb * |r - r'| := by rw [mul_one, one_mul]; exact add_le_add hda hdb + _ ≤ max Ka Kb * (|v - v'| + |r - r'|) := by + rw [mul_add] + gcongr + exacts [le_max_left (Ka : ℝ) Kb, le_max_right (Ka : ℝ) Kb] + +end Cslib diff --git a/Complexity/Foundations/Probability/CorrectionAtom.lean b/Complexity/Foundations/Probability/CorrectionAtom.lean new file mode 100644 index 000000000..80776f529 --- /dev/null +++ b/Complexity/Foundations/Probability/CorrectionAtom.lean @@ -0,0 +1,415 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Probability.StochasticAtom +import Complexity.Foundations.Data.Finset.Markov +import Mathlib.Algebra.Order.BigOperators.Expect +import Mathlib.Algebra.BigOperators.Field +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# Correction atoms with an incoming gate + +A *correction atom* represents an entry `Q (G x y / f) · g₀(y)` of a correction matrix as the +conditional mean of a bounded table, like the dense atoms of +`Complexity.Foundations.Probability.StochasticAtom`. Its table also has few nonzero entries in each +*column*. That bound is what lets later error estimates sum over the sources of a column. This is +idea 6 in issue #474, following the OpenAI preprint [OpenAI2026LogSpace, Sections 5.3 and 5.5]. + +**The incoming gate.** A draw is a pair `(s, t)` of independent seeds: `s` for the start channel +`X`, which retains sources, and `t` for the terminal channel (rank channel `Y`, usage channel +`Yt`). The *auxiliary score* of a source `x'` at column `y` is `I (G x' y / f, rank_K {G x' w / f : +Y t w})` (`Matrix.auxScore`). The *incoming gate* of column `y` is +`τ (rank_{K_c} {aux x' y : X s x'})` (`Matrix.incomingGate`) [OpenAI2026LogSpace, (5.12)]. The atom +is +`1{Yt t y} · Q (G x y / f) · R · T_y / c(q_y) · g₀(y)` (`Matrix.correctionAtom`), where `R` is the +row gate of `x`, `T_y` the incoming gate, `c(q) = max (1/2) (min 1 q)`, and `q_y` the conditional +mean of the preparatory value `h (G x y / f) · R · T_y` given `X(x)` and `Yt(y)` +(`Matrix.correctionPrep`, `Matrix.correctionNormalizer`) [OpenAI2026LogSpace, (5.13), (5.14)]. + +**The identity** [OpenAI2026LogSpace, Lemma 5.3]. The conditional mean of the atom is exactly +`Q (G x y / f) · g₀(y)` (`Matrix.expect_correctionAtom`). The row gate fails on at most a quarter +of the conditioning draws, by `Matrix.card_filter_rowGate_lt_one_mul_le`. The auxiliary score can +exceed the gate's threshold only on a fixed set `D` of sources, and the incoming gate fails only +if `K_c` members of `D` are retained (`Matrix.card_filter_incomingGate_lt_one_mul_le`). When +`g₀(y) ≠ 0`, the hypothesis `p · #D ≤ B` (the preprint's column bound (5.2)) makes this rare too. +When `g₀(y) = 0` both sides vanish and no bound on `D` is needed. Both gates are then full on half +of the draws, and the normalization principle (`Finset.expect_mul_div_clip_eq`) applies. The +failure bounds use no independence between gates. + +**The incoming cap** [OpenAI2026LogSpace, (5.18), Lemma 5.6]. If `I = 1` wherever `Q` and `ρ` are +both nonzero, and `τ` vanishes from `g ≤ 1` on, then on every draw a column has fewer than `K_c` +retained sources with a nonzero atom (`Matrix.card_filter_correctionAtom_col_ne_zero_lt`). `K_c` +such sources would all have score one, which closes the incoming gate +(`Matrix.incomingGate_eq_zero`). Rows have fewer than `K` nonzero atoms, as for dense atoms +(`Matrix.card_filter_correctionAtom_row_ne_zero_lt`). + +## Main definitions + +* `Matrix.auxScore`, `Matrix.incomingGate`: the auxiliary score and the incoming gate. +* `Matrix.correctionPrep`, `Matrix.correctionNormalizer`, `Matrix.correctionAtom`: the atom. + +## Main results + +* `Finset.expect_mul_div_clip_eq`: the normalization principle. +* `Finset.card_filter_le_card_filter_mul_le`: few draws retain many members of a sparse set. +* `Matrix.card_filter_incomingGate_lt_one_mul_le`: the incoming gate rarely fails. +* `Matrix.expect_correctionAtom`: the correction atom identity. +* `Matrix.abs_correctionAtom_le`: the atom is bounded. +* `Matrix.incomingGate_eq_zero`, `Matrix.card_filter_correctionAtom_col_ne_zero_lt`, + `Matrix.card_filter_correctionAtom_row_ne_zero_lt`: the incoming cap and the support bounds. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Sections 5.1, 5.3 and 5.5 (preprint, not peer reviewed) +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Finset + +variable {Ω : Type*} + +/-- **The normalization principle** [OpenAI2026LogSpace, Section 5.1]. Let a gate `γ` take values +in `[0, 1]` on a nonempty finite set `S` of draws, and be below one on at most half of them. Then +dividing by its clipped mean `c(q) = max (1/2) (min 1 q)` removes the gate's bias: +`𝔼_S [m · γ / c(𝔼_S γ)] = m`. -/ +theorem expect_mul_div_clip_eq {S : Finset Ω} (hS : S.Nonempty) {γ : Ω → ℝ} + (hγ0 : ∀ s ∈ S, 0 ≤ γ s) (hγ1 : ∀ s ∈ S, γ s ≤ 1) (hfail : 2 * (#{s ∈ S | γ s < 1} : ℝ) ≤ #S) + (m : ℝ) : 𝔼 s ∈ S, m * γ s / max (1 / 2) (min 1 (𝔼 s ∈ S, γ s)) = m := by + have hSr : (0 : ℝ) < #S := by exact_mod_cast hS.card_pos + have hγ : ∀ s ∈ S, 1 - (if γ s < 1 then 1 else 0) ≤ γ s := fun s hs => by + split_ifs with h + · rw [sub_self]; exact hγ0 s hs + · simpa using not_lt.mp h + have hlo : 1 / 2 ≤ 𝔼 s ∈ S, γ s := by + rw [expect_eq_sum_div_card, le_div_iff₀ hSr] + calc 1 / 2 * (#S : ℝ) ≤ #S - #{s ∈ S | γ s < 1} := by linarith + _ = ∑ s ∈ S, (1 - (if γ s < 1 then 1 else 0)) := by + rw [sum_sub_distrib, sum_boole, sum_const, nsmul_eq_mul, mul_one] + _ ≤ ∑ s ∈ S, γ s := sum_le_sum hγ + have hhi : 𝔼 s ∈ S, γ s ≤ 1 := expect_le hS hγ1 + have hpos : 0 < 𝔼 s ∈ S, γ s := lt_of_lt_of_le (by norm_num) hlo + rw [min_eq_right hhi, max_eq_right hlo] + simp only [mul_div_assoc] + rw [← mul_expect, ← expect_div, div_self hpos.ne', mul_one] + +variable {V : Type*} + +/-- **Few draws retain many members of a sparse set** (Markov's inequality). Let every member +`w ≠ x` of `D` be retained on at most a `p` fraction of the draws in `S`. Then at most a +`(1 + p #D) / K` fraction of the draws retain `K > 0` members of `D`. The vertex `x` itself +contributes at most one per draw. -/ +theorem card_filter_le_card_filter_mul_le {ι : Type*} (X : ι → V → Prop) [∀ s v, Decidable (X s v)] + (S : Finset ι) (D : Finset V) (x : V) {p : ℝ} (hp : 0 ≤ p) + (hpair : ∀ w ∈ D, w ≠ x → (#{s ∈ S | X s w} : ℝ) ≤ p * #S) (K : ℕ) : + (#{s ∈ S | K ≤ #{w ∈ D | X s w}} : ℝ) * K ≤ #S * (1 + p * #D) := by + classical + have hMarkov : (#{s ∈ S | K ≤ #{w ∈ D | X s w}} : ℝ) * K ≤ ∑ s ∈ S, (#{w ∈ D | X s w} : ℝ) := + card_filter_mul_le_sum S _ _ (fun _ _ => by positivity) fun s _ hs => by exact_mod_cast hs + have hswap : ∑ s ∈ S, (#{w ∈ D | X s w} : ℝ) = ∑ w ∈ D, (#{s ∈ S | X s w} : ℝ) := by + simp only [natCast_card_filter] + exact sum_comm + have hterm : ∀ w ∈ D, (#{s ∈ S | X s w} : ℝ) ≤ (if x = w then (#S : ℝ) else 0) + p * #S := by + intro w hw + by_cases hxw : x = w + · have hle : (#{s ∈ S | X s w} : ℝ) ≤ #S := by exact_mod_cast card_filter_le _ _ + have : 0 ≤ p * #S := by positivity + simp only [hxw, ↓reduceIte] + linarith + · simp only [hxw, ↓reduceIte, zero_add] + exact hpair w hw (Ne.symm hxw) + calc (#{s ∈ S | K ≤ #{w ∈ D | X s w}} : ℝ) * K + ≤ ∑ w ∈ D, ((if x = w then (#S : ℝ) else 0) + p * #S) := + hMarkov.trans (hswap ▸ sum_le_sum hterm) + _ = (if x ∈ D then (#S : ℝ) else 0) + #D * (p * #S) := by + rw [sum_add_distrib, sum_ite_eq, sum_const, nsmul_eq_mul] + _ ≤ #S * (1 + p * #D) := by + have : (if x ∈ D then (#S : ℝ) else 0) ≤ #S := by split_ifs <;> [exact le_rfl; positivity] + nlinarith + +end Finset + +namespace Matrix + +variable {V ι κ : Type*} [Fintype V] + +section Definitions + +variable (I : ℝ → ℝ → ℝ) (τ : ℝ → ℝ) (K Kc : ℕ) (f : ℝ) (G : Matrix V V ℝ) + +/-- The **auxiliary score** of the entry `(x, y)` for the retained set `T` of the rank channel: +`I (G x y / f, rank_K {G x w / f : w ∈ T})` [OpenAI2026LogSpace, (5.5)]. -/ +@[expose] noncomputable def auxScore (T : Finset V) (x y : V) : ℝ := + I (G x y / f) (kthLargest K T fun w => G x w / f) + +/-- The **incoming gate** of column `y`: `τ (rank_{K_c} {auxScore x y : x ∈ S})` over the retained +set `S` of sources [OpenAI2026LogSpace, (5.12)]. -/ +@[expose] noncomputable def incomingGate (S T : Finset V) (y : V) : ℝ := + τ (kthLargest Kc S fun x => auxScore I K f G T x y) + +variable {ι κ : Type*} [Fintype ι] [Fintype κ] (X : ι → V → Prop) (Y Yt : κ → V → Prop) + [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Y t v)] [∀ t v, Decidable (Yt t v)] + (Q h ρ : ℝ → ℝ) (g₀ : V → ℝ) + +/-- The **preparatory value** of a correction atom: `h (G x y / f) · R · T_y`, with the row gate +`R` and the incoming gate `T_y` [OpenAI2026LogSpace, (5.13)]. -/ +@[expose] noncomputable def correctionPrep (S T : Finset V) (x y : V) : ℝ := + h (G x y / f) * rowGate ρ K f G T x * incomingGate I τ K Kc f G S T y + +/-- The **normalizer** `q_y` of a correction atom: the mean of the preparatory value over the +draws that retain `x` in the start channel and `y` in the usage channel +[OpenAI2026LogSpace, (5.13)]. -/ +@[expose] noncomputable def correctionNormalizer (x y : V) : ℝ := + 𝔼 d ∈ ({s | X s x} : Finset ι) ×ˢ ({t | Yt t y} : Finset κ), + correctionPrep I τ K Kc f G h ρ {w | X d.1 w} {w | Y d.2 w} x y + +/-- The **correction atom** at `(x, y)` on the draw `d = (s, t)`: +`1{Yt t y} · Q (G x y / f) · R · T_y / c(q_y) · g₀(y)` [OpenAI2026LogSpace, (5.14)]. -/ +@[expose] noncomputable def correctionAtom (d : ι × κ) (x y : V) : ℝ := + if Yt d.2 y then + Q (G x y / f) * (rowGate ρ K f G {w | Y d.2 w} x * + incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y) / + max (1 / 2) (min 1 (correctionNormalizer I τ K Kc f G X Y Yt h ρ x y)) * g₀ y + else 0 + +end Definitions + +variable {I : ℝ → ℝ → ℝ} {τ : ℝ → ℝ} {K Kc : ℕ} {f : ℝ} {G : Matrix V V ℝ} + +omit [Fintype V] in +/-- **The incoming cap** [OpenAI2026LogSpace, Lemma 5.6]: if `τ` vanishes from `g ≤ 1` on and at +least `K_c > 0` retained sources have auxiliary score at least one at column `y`, the incoming +gate of `y` is closed. -/ +theorem incomingGate_eq_zero {S T : Finset V} {y : V} (hKc : 0 < Kc) {g : ℝ} (hg : g ≤ 1) + (hτ : ∀ r, g ≤ r → τ r = 0) (hcard : Kc ≤ #{x ∈ S | 1 ≤ auxScore I K f G T x y}) : + incomingGate I τ K Kc f G S T y = 0 := + hτ _ (hg.trans ((le_kthLargest_iff hKc one_pos).mpr hcard)) + +/-- **The incoming gate rarely fails** [OpenAI2026LogSpace, proof of Lemma 5.3]. Let `τ` be one +through `τ₀ ≥ 0` and `I` vanish when its first argument is at most `e`, so a score above `τ₀` +needs a source in `D = {x' | e < G x' y / f}`. If every member `w ≠ x` of `D` is retained on at +most a `p` fraction of the draws in `S`, then for every terminal set `T` the incoming gate is +below one on at most a `(1 + p #D) / K_c` fraction of `S`. -/ +theorem card_filter_incomingGate_lt_one_mul_le (X : ι → V → Prop) + [∀ s v, Decidable (X s v)] (S : Finset ι) (T : Finset V) (x y : V) (hKc : 0 < Kc) + {τ₀ : ℝ} (hτ₀ : 0 ≤ τ₀) (hττ : ∀ r, r ≤ τ₀ → τ r = 1) {e : ℝ} + (hI : ∀ v r, v ≤ e → I v r = 0) {p : ℝ} (hp : 0 ≤ p) + (hpair : ∀ w, e < G w y / f → w ≠ x → (#{s ∈ S | X s w} : ℝ) ≤ p * #S) : + (#{s ∈ S | incomingGate I τ K Kc f G {w | X s w} T y < 1} : ℝ) * Kc ≤ + #S * (1 + p * #({w | e < G w y / f} : Finset V)) := by + set D : Finset V := {w | e < G w y / f} + refine le_trans ?_ (card_filter_le_card_filter_mul_le X S D x hp + (fun w hw hwx => hpair w (by simpa [D] using hw) hwx) Kc) + refine mul_le_mul_of_nonneg_right ?_ (by positivity) + refine Nat.cast_le.mpr (card_le_card fun s hs => ?_) + rw [mem_filter] at hs ⊢ + refine ⟨hs.1, ?_⟩ + have hlt : τ₀ < kthLargest Kc {w | X s w} fun w => auxScore I K f G T w y := by + by_contra hle + rw [incomingGate, hττ _ (not_lt.mp hle)] at hs + exact lt_irrefl _ hs.2 + refine ((lt_kthLargest_iff hKc hτ₀).mp hlt).trans (card_le_card fun w hw => ?_) + rw [mem_filter] at hw ⊢ + refine ⟨?_, by simpa using hw.1⟩ + simp only [D, mem_filter, mem_univ, true_and] + by_contra hle + rw [auxScore, hI _ _ (not_lt.mp hle)] at hw + exact absurd hw.2 (not_lt.mpr hτ₀) + +omit [Fintype V] in +/-- A product of two gates with values in `[0, 1]` is at most one. -/ +private theorem mul_le_one_of_gate {r t : ℝ} (hr : r ≤ 1) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : + r * t ≤ 1 := + (mul_le_mul_of_nonneg_right hr ht0).trans (by rw [one_mul]; exact ht1) + +variable [Fintype ι] [Fintype κ] {X : ι → V → Prop} {Y Yt : κ → V → Prop} + [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Y t v)] [∀ t v, Decidable (Yt t v)] + {Q h ρ : ℝ → ℝ} {g₀ : V → ℝ} + +/-- **The correction atom is bounded**: `|F(x, y)| ≤ 2 |Q (G x y / f)| |g₀(y)|` on every draw, +when the row and incoming gate functions take values in `[0, 1]`. -/ +theorem abs_correctionAtom_le (hρ0 : ∀ r, 0 ≤ ρ r) (hρ1 : ∀ r, ρ r ≤ 1) (hτ0 : ∀ r, 0 ≤ τ r) + (hτ1 : ∀ r, τ r ≤ 1) (d : ι × κ) (x y : V) : + |correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ d x y| ≤ 2 * |Q (G x y / f)| * |g₀ y| := by + rw [correctionAtom] + split_ifs + · set γ := rowGate ρ K f G {w | Y d.2 w} x * + incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y + have hγ0 : 0 ≤ γ := mul_nonneg (hρ0 _) (hτ0 _) + have hγ1 : γ ≤ 1 := mul_le_one_of_gate (hρ1 _) (hτ0 _) (hτ1 _) + set c := max (1 / 2) (min 1 (correctionNormalizer I τ K Kc f G X Y Yt h ρ x y)) + have hc : (1 / 2 : ℝ) ≤ c := le_max_left _ _ + have hc0 : 0 < c := lt_of_lt_of_le (by norm_num) hc + rw [abs_mul, abs_div, abs_mul, abs_of_nonneg hγ0, abs_of_pos hc0] + refine mul_le_mul_of_nonneg_right ?_ (abs_nonneg _) + rw [div_le_iff₀ hc0] + calc |Q (G x y / f)| * γ ≤ |Q (G x y / f)| * 1 := mul_le_mul_of_nonneg_left hγ1 (abs_nonneg _) + _ = 2 * |Q (G x y / f)| * (1 / 2) := by ring + _ ≤ _ := mul_le_mul_of_nonneg_left hc (by positivity) + · rw [abs_zero]; positivity + +/-- **Row support** [OpenAI2026LogSpace, Lemma 5.6]: if `Q` vanishes through `e ≥ 0` and `ρ` +vanishes from `g ≤ e` on, then on every draw fewer than `K > 0` correction atoms of a row are +nonzero among the vertices the rank channel retains. -/ +theorem card_filter_correctionAtom_row_ne_zero_lt (hK : 0 < K) {e g : ℝ} (he : 0 ≤ e) + (hQ : ∀ v, v ≤ e → Q v = 0) (hg : g ≤ e) (hρ : ∀ r, g ≤ r → ρ r = 0) (d : ι × κ) (x : V) : + #{y ∈ ({w | Y d.2 w} : Finset V) | correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ d x y ≠ 0} < + K := by + refine lt_of_le_of_lt (card_le_card fun y hy => ?_) + (card_filter_mul_rowGate_ne_zero_lt (a := f) (G := G) {w | Y d.2 w} x hK he hQ hg hρ) + rw [mem_filter] at hy ⊢ + refine ⟨hy.1, fun h0 => hy.2 ?_⟩ + rw [correctionAtom] + split_ifs + · rw [← mul_assoc, h0, zero_mul, zero_div, zero_mul] + · rfl + +/-- **Column support: the incoming cap** [OpenAI2026LogSpace, (5.18), Lemma 5.6]. Suppose the +auxiliary score is one wherever `Q` and `ρ` are both nonzero, and `τ` vanishes from `g ≤ 1` on. +Then on every draw fewer than `K_c > 0` retained sources have a nonzero atom in column `y`: +`K_c` of them would close the incoming gate, which makes the whole column zero. -/ +theorem card_filter_correctionAtom_col_ne_zero_lt (hKc : 0 < Kc) + (hIQ : ∀ v r, Q v ≠ 0 → ρ r ≠ 0 → I v r = 1) {g : ℝ} (hg : g ≤ 1) + (hτ : ∀ r, g ≤ r → τ r = 0) (d : ι × κ) (y : V) : + #{x ∈ ({w | X d.1 w} : Finset V) | correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ d x y ≠ 0} < + Kc := by + by_contra hle + rw [not_lt] at hle + have hgate : incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y = 0 := by + refine incomingGate_eq_zero hKc hg hτ (hle.trans (card_le_card fun x hx => ?_)) + rw [mem_filter] at hx ⊢ + refine ⟨hx.1, le_of_eq (hIQ _ _ (fun hQ => hx.2 ?_) (fun hρ => hx.2 ?_)).symm⟩ + · rw [correctionAtom]; split_ifs <;> simp [hQ] + · rw [correctionAtom]; split_ifs <;> simp [rowGate, hρ] + obtain ⟨x, hx⟩ := card_pos.mp (hKc.trans_le hle) + rw [mem_filter, correctionAtom, hgate] at hx + split_ifs at hx <;> simp at hx + +/-- **The correction atom identity, including zero multipliers** [OpenAI2026LogSpace, Lemma 5.3]. +Let `h = 1` wherever `Q ≠ 0`; let `ρ, τ ∈ [0, 1]`, with `ρ` one through `η > 0` and `τ` one +through `τ₀ ≥ 0`; and let `I` vanish when its first argument is at most `e`. Let row `x` of +`G ≥ 0` have mass at most `M`. Suppose the draws retaining `x` in `X` and `y` in `Yt` are +nonempty, and two pair bounds hold. Every `w ≠ y` is retained by `Y` on at most a `c f` fraction +of the draws with `Yt(y)`. Every `w ≠ x` is retained by `X` on at most a `p` fraction of the draws +with `X(x)`. If `g₀(y) ≠ 0`, let the sources that can score satisfy +`p · #{w | e < G w y / f} ≤ B`. Then, for `K ≥ 4 (1 + c M / η)` and `K_c ≥ 4 (1 + B)`, the +conditional mean of the atom is exactly `Q (G x y / f) · g₀(y)`. -/ +theorem expect_correctionAtom {x y : V} (hSx : ({s | X s x} : Finset ι).Nonempty) + (hSy : ({t | Yt t y} : Finset κ).Nonempty) (hQh : ∀ v, Q v ≠ 0 → h v = 1) + (hρ0 : ∀ r, 0 ≤ ρ r) (hρ1 : ∀ r, ρ r ≤ 1) {η : ℝ} (hη : 0 < η) (hρη : ∀ r, r ≤ η → ρ r = 1) + (hτ0 : ∀ r, 0 ≤ τ r) (hτ1 : ∀ r, τ r ≤ 1) {τ₀ : ℝ} (hτ₀ : 0 ≤ τ₀) + (hττ : ∀ r, r ≤ τ₀ → τ r = 1) {e : ℝ} (hI : ∀ v r, v ≤ e → I v r = 0) (hf : 0 < f) + (hG0 : ∀ w, 0 ≤ G x w) {M : ℝ} (hGM : ∑ w, G x w ≤ M) {c : ℝ} (hc : 0 ≤ c) + (hK : 4 * (1 + c * M / η) ≤ K) + (hpairY : ∀ w, w ≠ y → (#{t | Yt t y ∧ Y t w} : ℝ) ≤ c * f * #{t | Yt t y}) {p : ℝ} + (hp : 0 ≤ p) (hpairX : ∀ w, w ≠ x → (#{s | X s x ∧ X s w} : ℝ) ≤ p * #{s | X s x}) {B : ℝ} + (hB : g₀ y ≠ 0 → p * #({w | e < G w y / f} : Finset V) ≤ B) (hKc : 4 * (1 + B) ≤ Kc) : + 𝔼 d ∈ ({s | X s x} : Finset ι) ×ˢ ({t | Yt t y} : Finset κ), + correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ d x y = Q (G x y / f) * g₀ y := by + set Sx : Finset ι := {s | X s x} + set Sy : Finset κ := {t | Yt t y} + set C := Sx ×ˢ Sy + set γ : ι × κ → ℝ := fun d => rowGate ρ K f G {w | Y d.2 w} x * + incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y + -- trivial cases: a zero entry or a zero multiplier + by_cases hz : Q (G x y / f) * g₀ y = 0 + · rw [hz] + refine expect_eq_zero fun d _ => ?_ + rw [correctionAtom] + split_ifs + · rcases mul_eq_zero.mp hz with h0 | h0 <;> simp [h0] + · rfl + obtain ⟨hQ0, hg0⟩ := mul_ne_zero_iff.mp hz + have hh1 : h (G x y / f) = 1 := hQh _ hQ0 + have hSxr : (0 : ℝ) < #Sx := by exact_mod_cast hSx.card_pos + have hSyr : (0 : ℝ) < #Sy := by exact_mod_cast hSy.card_pos + have hM : 0 ≤ M := (sum_nonneg fun w _ => hG0 w).trans hGM + have hKr : (0 : ℝ) < K := by + have : 0 ≤ c * M / η := by positivity + linarith + have hBnn : 0 ≤ B := (by positivity : (0 : ℝ) ≤ p * #({w | e < G w y / f} : Finset V)).trans + (hB hg0) + have hKcr : (0 : ℝ) < Kc := by linarith + -- the row gate fails on at most a quarter of the terminal draws + have hR : (#{t ∈ Sy | rowGate ρ K f G {w | Y t w} x < 1} : ℝ) * 4 ≤ #Sy := by + have h := card_filter_rowGate_lt_one_mul_le Sy x hf hη hρη hG0 hGM (by exact_mod_cast hKr) hc + fun w hwy => by + have hset : ({t ∈ Sy | Y t w} : Finset κ) = ({t | Yt t y ∧ Y t w} : Finset κ) := by + ext t; simp only [Sy, mem_filter, mem_univ, true_and] + rw [hset] + exact hpairY w hwy + nlinarith + -- the incoming gate fails on at most a quarter of the start draws, for every terminal set + have hT : ∀ T : Finset V, + (#{s ∈ Sx | incomingGate I τ K Kc f G {w | X s w} T y < 1} : ℝ) * 4 ≤ #Sx := by + intro T + have h := card_filter_incomingGate_lt_one_mul_le (τ := τ) (K := K) (f := f) (G := G) X Sx T x + y (by exact_mod_cast hKcr) hτ₀ hττ + hI hp fun w _ hwx => by + have hset : ({s ∈ Sx | X s w} : Finset ι) = ({s | X s x ∧ X s w} : Finset ι) := by + ext s; simp only [Sx, mem_filter, mem_univ, true_and] + rw [hset] + exact hpairX w hwx + have h1 : #Sx * (1 + p * #({w | e < G w y / f} : Finset V)) ≤ #Sx * (1 + B) := by + have := hB hg0 + gcongr + nlinarith + -- so the product gate fails on at most half of the conditioning draws + have hfail : 2 * (#{d ∈ C | γ d < 1} : ℝ) ≤ #C := by + have hsplit : ∀ d, (if γ d < 1 then (1 : ℝ) else 0) ≤ + (if rowGate ρ K f G {w | Y d.2 w} x < 1 then 1 else 0) + + (if incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y < 1 then 1 else 0) := by + intro d + by_cases h1 : rowGate ρ K f G {w | Y d.2 w} x < 1 + · split_ifs <;> norm_num + by_cases h2 : incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y < 1 + · split_ifs <;> norm_num + have hr : rowGate ρ K f G {w | Y d.2 w} x = 1 := le_antisymm (hρ1 _) (not_lt.mp h1) + have ht : incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y = 1 := + le_antisymm (hτ1 _) (not_lt.mp h2) + simp only [γ, hr, ht, mul_one, lt_irrefl, ↓reduceIte] + norm_num + have hcount : (#{d ∈ C | γ d < 1} : ℝ) ≤ + #Sx * #{t ∈ Sy | rowGate ρ K f G {w | Y t w} x < 1} + + ∑ t ∈ Sy, (#{s ∈ Sx | incomingGate I τ K Kc f G {w | X s w} {w | Y t w} y < 1} : ℝ) := by + rw [natCast_card_filter] + refine (sum_le_sum fun d _ => hsplit d).trans_eq ?_ + rw [sum_add_distrib, sum_product, sum_product_right] + simp only [sum_const, nsmul_eq_mul, ← natCast_card_filter] + have hsum : (∑ t ∈ Sy, + (#{s ∈ Sx | incomingGate I τ K Kc f G {w | X s w} {w | Y t w} y < 1} : ℝ)) * 4 ≤ + #Sy * #Sx := by + rw [sum_mul] + calc ∑ t ∈ Sy, (#{s ∈ Sx | incomingGate I τ K Kc f G {w | X s w} {w | Y t w} y < 1} : + ℝ) * 4 ≤ ∑ _t ∈ Sy, (#Sx : ℝ) := sum_le_sum fun t _ => hT _ + _ = #Sy * #Sx := by rw [sum_const, nsmul_eq_mul] + have hC : (#C : ℝ) = #Sx * #Sy := by rw [card_product]; push_cast; ring + rw [hC] + nlinarith [mul_le_mul_of_nonneg_left hR hSxr.le] + -- the normalizer is the mean of the product gate, and the normalization principle applies + have hq : correctionNormalizer I τ K Kc f G X Y Yt h ρ x y = 𝔼 d ∈ C, γ d := by + simp only [correctionNormalizer, correctionPrep, hh1, one_mul, γ, C, Sx, Sy] + have hterm : ∀ d ∈ C, correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ d x y = + Q (G x y / f) * γ d / max (1 / 2) (min 1 (𝔼 d ∈ C, γ d)) * g₀ y := fun d hd => by + have hd' : Yt d.2 y := by simpa [C, Sy] using (mem_product.mp hd).2 + simp only [correctionAtom, hd', ↓reduceIte, hq, γ] + have key : 𝔼 d ∈ C, Q (G x y / f) * γ d / max (1 / 2) (min 1 (𝔼 d ∈ C, γ d)) = + Q (G x y / f) := + expect_mul_div_clip_eq (hSx.product hSy) (fun d _ => mul_nonneg (hρ0 _) (hτ0 _)) + (fun d _ => mul_le_one_of_gate (hρ1 _) (hτ0 _) (hτ1 _)) hfail _ + rw [expect_congr rfl hterm, ← expect_mul, key] + +end Matrix diff --git a/Complexity/Foundations/Probability/RootMetric.lean b/Complexity/Foundations/Probability/RootMetric.lean new file mode 100644 index 000000000..419b8cccd --- /dev/null +++ b/Complexity/Foundations/Probability/RootMetric.lean @@ -0,0 +1,170 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Algebra.BigOperators.Expect +public import Mathlib.Analysis.SpecialFunctions.Pow.Real +import Complexity.Foundations.Analysis.RootError +import Mathlib.Algebra.Order.BigOperators.Expect +import Mathlib.Tactic.GCongr +import Mathlib.Tactic.Positivity + +/-! +# Integrated norms and root metrics of random tables + +The estimators of the OpenAI preprint compare random row tables and vertex arrays by integrated +`s`-th power norms over a shared environment `σ` [OpenAI2026LogSpace, Section 5.6]. Let `σ` range +uniformly over a finite type `Ω`, let `X` and `Y` be channels (`X σ x` means that `x` is retained +on the draw `σ`), and fix a normalization `N` and a nominal rate `u`. For a random table +`Z : Ω → V → V → ℝ` and a random vertex array `v : Ω → V → ℝ`, + +* `‖Z‖^s_{u,a;s} = (N u)⁻¹ 𝔼_σ ∑_{X σ x} ∑_{Y σ y} |Z σ x y|^s` (`Cslib.rowNormPow`, (5.19)); +* `d_{u,a}(H, H')^s = ‖H^{1/s} - H'^{1/s}‖^s_{u,a;s}` (`Cslib.rootDistPow`, (5.19)); +* `‖v‖^s_{u;s} = (N u)⁻¹ 𝔼_σ ∑_{X σ x} |v σ x|^s` (`Cslib.vertexNormPow`, (5.20)). + +Here the channel `Y` plays the role of the preprint's `Y_a`, and values outside the retained sets +are ignored, which is the preprint's convention of extending them by zero. We work with the +`s`-th powers of the norms throughout, as every estimate of the preprint does. + +The ordinary norm of a difference of bounded nonnegative tables is controlled by their root +distance (`Cslib.rowNormPow_sub_le_rootDistPow`, from (5.21)). A table with bounded values and +fewer than `K` nonzero entries per retained row has norm at most `K B^s ‖1‖^s_{u;s}` +(`Cslib.rowNormPow_le_of_card_le`). This is the uniform bound of [OpenAI2026LogSpace, Section 5.6]. + +## Main definitions + +* `Cslib.rowNormPow`, `Cslib.rootDistPow`, `Cslib.vertexNormPow`. + +## Main results + +* `Cslib.rowNormPow_nonneg`, `Cslib.vertexNormPow_nonneg`, `Cslib.rootDistPow_comm`, + `Cslib.rootDistPow_self`: basic properties. +* `Cslib.rowNormPow_le_mul`: comparison of norms from a pointwise comparison. +* `Cslib.rowNormPow_sub_le_rootDistPow`: ordinary error is controlled by root error. +* `Cslib.rowNormPow_le_of_card_le`: the uniform bound for bounded sparse tables. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 5.6, (5.19)–(5.21) (preprint, not peer reviewed) +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Cslib + +variable {Ω V : Type*} [Fintype Ω] [Fintype V] + +section Definitions + +variable (s : ℕ) (N u : ℝ) (X Y : Ω → V → Prop) [∀ σ v, Decidable (X σ v)] + [∀ σ v, Decidable (Y σ v)] + +/-- The `s`-th power `‖Z‖^s_{u,a;s}` of the integrated row norm of a random table +[OpenAI2026LogSpace, (5.19)]. -/ +noncomputable def rowNormPow (Z : Ω → V → V → ℝ) : ℝ := + (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), |Z σ x y| ^ s + +/-- The `s`-th power `d_{u,a}(H, H')^s` of the root distance of two random tables +[OpenAI2026LogSpace, (5.19)]. -/ +noncomputable def rootDistPow (H H' : Ω → V → V → ℝ) : ℝ := + rowNormPow s N u X Y fun σ x y => H σ x y ^ (s⁻¹ : ℝ) - H' σ x y ^ (s⁻¹ : ℝ) + +/-- The `s`-th power `‖v‖^s_{u;s}` of the integrated norm of a random vertex array +[OpenAI2026LogSpace, (5.20)]. -/ +noncomputable def vertexNormPow (v : Ω → V → ℝ) : ℝ := + (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), |v σ x| ^ s + +end Definitions + +variable {s : ℕ} {N u : ℝ} {X Y : Ω → V → Prop} [∀ σ v, Decidable (X σ v)] + [∀ σ v, Decidable (Y σ v)] + +theorem rowNormPow_nonneg (hNu : 0 ≤ N * u) (Z : Ω → V → V → ℝ) : 0 ≤ rowNormPow s N u X Y Z := by + unfold rowNormPow; positivity + +theorem vertexNormPow_nonneg (hNu : 0 ≤ N * u) (v : Ω → V → ℝ) : + 0 ≤ vertexNormPow s N u X v := by + unfold vertexNormPow; positivity + +theorem rootDistPow_comm (H H' : Ω → V → V → ℝ) : + rootDistPow s N u X Y H H' = rootDistPow s N u X Y H' H := by + simp only [rootDistPow, rowNormPow, abs_sub_comm] + +@[simp] +theorem rootDistPow_self (hs : s ≠ 0) (H : Ω → V → V → ℝ) : rootDistPow s N u X Y H H = 0 := by + simp [rootDistPow, rowNormPow, hs] + +/-- A pointwise comparison of `s`-th powers on the retained pairs gives a comparison of the +norms. -/ +theorem rowNormPow_le_mul (hNu : 0 ≤ N * u) {c : ℝ} {Z Z' : Ω → V → V → ℝ} + (h : ∀ σ x y, X σ x → Y σ y → |Z σ x y| ^ s ≤ c * |Z' σ x y| ^ s) : + rowNormPow s N u X Y Z ≤ c * rowNormPow s N u X Y Z' := by + unfold rowNormPow + calc (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), + |Z σ x y| ^ s + ≤ (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), + c * |Z' σ x y| ^ s := by + refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (inv_nonneg.2 hNu) + refine sum_le_sum fun x hx => sum_le_sum fun y hy => ?_ + simp only [mem_filter, mem_univ, true_and] at hx hy + exact h σ x y hx hy + _ = _ := by simp only [← mul_sum, ← mul_expect]; ring + +/-- **Ordinary error is controlled by root error** [OpenAI2026LogSpace, (5.21)], integrated: for +tables with values in `[0, C]` on the retained pairs, +`‖H - H'‖^s ≤ (s C^{(s-1)/s})^s d(H, H')^s`. -/ +theorem rowNormPow_sub_le_rootDistPow (hs : s ≠ 0) (hNu : 0 ≤ N * u) {C : ℝ} + {H H' : Ω → V → V → ℝ} + (hH : ∀ σ x y, X σ x → Y σ y → 0 ≤ H σ x y ∧ H σ x y ≤ C) + (hH' : ∀ σ x y, X σ x → Y σ y → 0 ≤ H' σ x y ∧ H' σ x y ≤ C) : + rowNormPow s N u X Y (fun σ x y => H σ x y - H' σ x y) ≤ + (s * C ^ (((s : ℝ) - 1) / s)) ^ s * rootDistPow s N u X Y H H' := by + refine rowNormPow_le_mul hNu fun σ x y hx hy => ?_ + obtain ⟨h0, h1⟩ := hH σ x y hx hy + obtain ⟨h0', h1'⟩ := hH' σ x y hx hy + have hk : 0 ≤ (s : ℝ) * C ^ (((s : ℝ) - 1) / s) := + mul_nonneg (Nat.cast_nonneg s) (Real.rpow_nonneg (h0.trans h1) _) + rw [← mul_pow] + exact pow_le_pow_left₀ (abs_nonneg _) (abs_sub_le_mul_abs_rpow_inv_sub hs h0 h0' h1 h1') s + +/-- **The uniform bound** [OpenAI2026LogSpace, Section 5.6]. A table with values bounded by `B` +and at most `K` nonzero entries in each retained row has `‖Z‖^s ≤ K B^s ‖1‖^s`. -/ +theorem rowNormPow_le_of_card_le (hs : s ≠ 0) (hNu : 0 ≤ N * u) {B : ℝ} (hB0 : 0 ≤ B) {K : ℕ} + {Z : Ω → V → V → ℝ} (hB : ∀ σ x y, |Z σ x y| ≤ B) + (hK : ∀ σ x, X σ x → #{y ∈ ({y | Y σ y} : Finset V) | Z σ x y ≠ 0} ≤ K) : + rowNormPow s N u X Y Z ≤ K * B ^ s * vertexNormPow s N u X fun _ _ => 1 := by + unfold rowNormPow vertexNormPow + have hrow : ∀ σ, ∀ x ∈ ({x | X σ x} : Finset V), + ∑ y ∈ ({y | Y σ y} : Finset V), |Z σ x y| ^ s ≤ K * B ^ s := fun σ x hx => by + simp only [mem_filter, mem_univ, true_and] at hx + rw [← sum_filter_of_ne (p := fun y => Z σ x y ≠ 0) fun y _ h hy => + h (by rw [hy, abs_zero, zero_pow hs])] + calc ∑ y ∈ ({y | Y σ y} : Finset V) with Z σ x y ≠ 0, |Z σ x y| ^ s + ≤ ∑ y ∈ ({y | Y σ y} : Finset V) with Z σ x y ≠ 0, B ^ s := + sum_le_sum fun y _ => pow_le_pow_left₀ (abs_nonneg _) (hB σ x y) s + _ ≤ K * B ^ s := by + rw [sum_const, nsmul_eq_mul] + gcongr + exact_mod_cast hK σ x hx + calc (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), + |Z σ x y| ^ s + ≤ (N * u)⁻¹ * 𝔼 σ, (#({x | X σ x} : Finset V) : ℝ) * (K * B ^ s) := by + refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (inv_nonneg.2 hNu) + rw [← nsmul_eq_mul, ← sum_const] + exact sum_le_sum (hrow σ) + _ = _ := by + rw [← expect_mul] + simp only [abs_one, one_pow, sum_const, nsmul_eq_mul, mul_one] + ring + +end Cslib diff --git a/Complexity/Probability/PairwiseIndependentHash/AtomChannels.lean b/Complexity/Probability/PairwiseIndependentHash/AtomChannels.lean new file mode 100644 index 000000000..f62d31ce6 --- /dev/null +++ b/Complexity/Probability/PairwiseIndependentHash/AtomChannels.lean @@ -0,0 +1,117 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Probability.StochasticAtom +public import Complexity.Probability.PairwiseIndependentHash.RetentionChannel + +/-! +# Dense atoms over affine channels at two rates + +A dense atom (`Matrix.denseAtom`) ranks its row over a channel at the atom's scale `f` and is +masked by a *usage* channel at a lower rate `t ≤ f` [OpenAI2026LogSpace, (5.11)]. For the affine +retention channels over `𝔽_P` both are one seed with two boxes: the usage channel has a smaller +side `L_t ≤ ⌈P a⌉`. So it retains a subset (`Cslib.Probability.affineRetains_of_le`). Given that +the usage channel retains `y`, another identifier `w` is retained at rate `f = a ^ H` with +probability at most `2 ^ H f`, by pairwise independence at two rates +(`Cslib.Probability.card_affineRetains_and_affineRetains_le`). This is the cross-rate pair bound +of [OpenAI2026LogSpace, Lemma 3.1] used in the proof of Lemma 5.1. With it, the dense atom +identity holds for these channels at two rates (`Cslib.Probability.expect_denseAtom_affineRetains`). + +## Main results + +* `Cslib.Probability.card_filter_and_le_of_dens_le`: a conditional probability bound as a count. +* `Cslib.Probability.card_affineRetains_and_affineRetains_le`: the cross-rate pair bound. +* `Cslib.Probability.expect_denseAtom_affineRetains`: the dense atom identity at two rates. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Lemma 3.1 and Lemma 5.1 (preprint, not peer reviewed) +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Cslib.Probability + +variable {V : Type*} {P H : ℕ} [Fact P.Prime] + +omit [Fact P.Prime] in +/-- A **conditional probability bound as a count**: if `Pr[B ∧ A] ≤ q Pr[A]` for uniform seeds, +then among the seeds satisfying `A`, at most a `q` fraction also satisfy `B`. -/ +theorem card_filter_and_le_of_dens_le {Ω : Type*} [Fintype Ω] {A B : Ω → Prop} [DecidablePred A] + [DecidablePred B] {q : ℝ} (h : (dens {t | B t ∧ A t} : ℝ) ≤ q * dens {t | A t}) : + (#{t | A t ∧ B t} : ℝ) ≤ q * #{t | A t} := by + have hcard : ∀ T : Finset Ω, ((dens T : ℚ≥0) : ℝ) = #T / Fintype.card Ω := fun T => by + rw [dens_eq_card_div_card]; push_cast; rfl + rw [hcard, hcard, ← mul_div_assoc] at h + have hset : ({t | A t ∧ B t} : Finset Ω) = ({t | B t ∧ A t} : Finset Ω) := + filter_congr fun _ _ => and_comm + rw [hset] + rcases (Fintype.card Ω).eq_zero_or_pos with h0 | h0 + · have : (univ : Finset Ω) = ∅ := univ_eq_empty_iff.mpr (Fintype.card_eq_zero_iff.mp h0) + simp [this] + · exact (div_le_div_iff_of_pos_right (by exact_mod_cast h0)).mp h + +/-- **The cross-rate pair bound for affine channels.** Let `ident : V → ZMod P` be injective, +`1 ≤ P a`, `a ≤ 1`, and `L_t ≤ P`. Among the seeds whose box of side `L_t` retains `y`, those +whose box of side `⌈P a⌉` also retains `w ≠ y` form at most a `2 ^ H a ^ H` fraction. -/ +theorem card_affineRetains_and_affineRetains_le {ident : V → ZMod P} + (hident : Function.Injective ident) {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) {Lt : ℕ} + (hLt : Lt ≤ P) {w y : V} (hwy : w ≠ y) : + (#{s | affineRetains P H Lt s (ident y) ∧ affineRetains P H ⌈P * a⌉₊ s (ident w)} : ℝ) ≤ + 2 ^ H * a ^ H * #{s | affineRetains P H Lt s (ident y)} := by + obtain ⟨hL, -, hup, -, -⟩ := affineRetains_rates (H := H) hPa ha + refine card_filter_and_le_of_dens_le ?_ + rw [dens_affineRetains_and_affineRetains hL hLt (hident.ne hwy), dens_affineRetains hLt] + push_cast + exact mul_le_mul_of_nonneg_right hup (by positivity) + +/-- **The dense atom identity for affine channels at two rates** [OpenAI2026LogSpace, Lemma 5.1]. +The rank channel retains with side `⌈P a⌉` (rate `f = a ^ H`), the usage channel with a side +`0 < L_t ≤ ⌈P a⌉`. For every nonnegative row of mass at most `M`, the conditional mean of the +dense atom given the usage channel is `k (G x y / f)`, once `K ≥ 2 (1 + 2 ^ H M / η)`. -/ +theorem expect_denseAtom_affineRetains [Fintype V] {ident : V → ZMod P} + (hident : Function.Injective ident) {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) {Lt : ℕ} + (hLt0 : 0 < Lt) (hLt : Lt ≤ ⌈P * a⌉₊) {k h ρ : ℝ → ℝ} {K : ℕ} {G : Matrix V V ℝ} {x y : V} + (hkh : ∀ d, k d ≠ 0 → h d = 1) (hρ0 : ∀ r, 0 ≤ ρ r) (hρ1 : ∀ r, ρ r ≤ 1) {η : ℝ} + (hη : 0 < η) (hρη : ∀ r, r ≤ η → ρ r = 1) (hG0 : ∀ w, 0 ≤ G x w) {M : ℝ} + (hGM : ∑ w, G x w ≤ M) (hK : 2 * (1 + 2 ^ H * M / η) ≤ K) : + 𝔼 s ∈ ({s | affineRetains P H Lt s (ident y)} : + Finset (Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P))), + Matrix.denseAtom (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) + (fun s v => affineRetains P H Lt s (ident v)) k h ρ K (a ^ H) G s x y = + k (G x y / a ^ H) := by + obtain ⟨hL, -, -, -, -⟩ := affineRetains_rates (H := H) hPa ha + have hLtP : Lt ≤ P := hLt.trans hL + have ha0 : 0 < a := by + by_contra h0 + have hP : (0 : ℝ) ≤ P := Nat.cast_nonneg _ + nlinarith [mul_nonpos_of_nonneg_of_nonpos hP (not_lt.mp h0)] + have hS : ({s | affineRetains P H Lt s (ident y)} : + Finset (Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P))).Nonempty := by + rw [← card_pos] + by_contra h0 + have h := dens_affineRetains (H := H) hLtP (ident y) + rw [dens_eq_card_div_card, Nat.eq_zero_of_not_pos h0, Nat.cast_zero, zero_div] at h + have : (0 : ℚ≥0) < ((Lt : ℚ≥0) / P) ^ H := by + have : (0 : ℚ≥0) < P := by exact_mod_cast (Fact.out : P.Prime).pos + positivity + exact absurd h this.ne + have hp : ∀ w, w ≠ y → (#{s | affineRetains P H Lt s (ident y) ∧ + affineRetains P H ⌈P * a⌉₊ s (ident w)} : ℝ) ≤ + 2 ^ H * a ^ H * #{s | affineRetains P H Lt s (ident y)} := fun w hwy => + card_affineRetains_and_affineRetains_le hident hPa ha hLtP hwy + exact Matrix.expect_denseAtom (Y := fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) + (Yt := fun s v => affineRetains P H Lt s (ident v)) (c := 2 ^ H) hS hkh hρ0 hρ1 hη hρη + (pow_pos ha0 H) hG0 hGM (by positivity) hK hp + +end Cslib.Probability diff --git a/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean b/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean index 7b243567c..1efd0065f 100644 --- a/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean +++ b/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean @@ -53,6 +53,8 @@ only for the later averaging walks, so they are not needed here. * `Cslib.Probability.card_retentionBox`: the box has `L ^ H` points. * `Cslib.Probability.dens_affineRetains`, `Cslib.Probability.dens_affineRetains_and`: exact retention probabilities of one identifier and of two distinct ones. +* `Cslib.Probability.affineRetains_of_le`, `Cslib.Probability.dens_affineRetains_and_affineRetains`: + nested boxes and the joint retention probability at two rates. * `Cslib.Probability.dens_two_mul_card_filter_affineRetains_lt_le`: the lower tail of the number of retained identifiers of a set. * `Cslib.Probability.dens_filter_fst_and_snd`: events about independent seeds are independent. @@ -150,6 +152,31 @@ theorem dens_affineRetains_and (hL : L ≤ P) {w y : ZMod P} (hwy : w ≠ y) : push_cast rfl +omit [Fact P.Prime] in +/-- **Nested boxes**: an identifier retained with side `L₂` is retained with every side +`L₁ ≥ L₂`, by the same seed. So a channel at a lower rate retains a subset. -/ +theorem affineRetains_of_le {L₁ L₂ : ℕ} (hL : L₂ ≤ L₁) {s} {y : ZMod P} + (h : affineRetains P H L₂ s y) : affineRetains P H L₁ s y := by + simp only [affineRetains, retentionBox, Fintype.mem_piFinset, mem_filter, mem_univ, + true_and] at h ⊢ + exact fun j => (h j).trans_le hL + +/-- **Pairwise independent retention at two rates**: for distinct identifiers `w ≠ y`, the seed +retains `w` with side `L₁` and `y` with side `L₂` with probability +`(L₁ / P) ^ H * (L₂ / P) ^ H`. -/ +theorem dens_affineRetains_and_affineRetains {L₁ L₂ : ℕ} (hL₁ : L₁ ≤ P) (hL₂ : L₂ ≤ P) + {w y : ZMod P} (hwy : w ≠ y) : + dens {s | affineRetains P H L₁ s w ∧ affineRetains P H L₂ s y} = + ((L₁ : ℚ≥0) / P) ^ H * ((L₂ : ℚ≥0) / P) ^ H := by + have h := isPairwiseIndependentHash_affineIdentifier.dens_filter_apply_mem_and_apply_mem hwy + (retentionBox P H L₁) (retentionBox P H L₂) + rw [card_retentionBox hL₁, card_retentionBox hL₂, Fintype.card_fun, Fintype.card_fin, + ZMod.card] at h + unfold affineRetains + rw [h, div_pow, div_pow] + push_cast + rfl + /-- **Lower tail of the retained count**: a set `A` of identifiers retains fewer than half of its expected number `#A π`, with `π = (L / P) ^ H`, with probability at most `4 / (#A π)`. -/ theorem dens_two_mul_card_filter_affineRetains_lt_le (hL : L ≤ P) (A : Finset (ZMod P)) diff --git a/ComplexityTests/AtomChannels.lean b/ComplexityTests/AtomChannels.lean new file mode 100644 index 000000000..87a60bb42 --- /dev/null +++ b/ComplexityTests/AtomChannels.lean @@ -0,0 +1,66 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexity.Probability.PairwiseIndependentHash.AtomChannels +import Mathlib.Tactic.NormNum.Prime + +/-! +# Tests for dense atoms over affine channels at two rates + +* The joint retention probability at two rates over `𝔽₃`, exactly. +* Nested boxes. +* The dense atom identity at two rates for a concrete walk over `𝔽₅`. +-/ + +namespace ComplexityTests.AtomChannels + +open Finset Cslib.Probability +open scoped BigOperators + +instance : Fact (Nat.Prime 3) := ⟨by norm_num⟩ +instance : Fact (Nat.Prime 5) := ⟨by norm_num⟩ + +-- Over `𝔽₃` in one coordinate, `0` lands in the box of side `2` and `1` in the box of side `1` +-- with probability `2/3 · 1/3 = 2/9`. +example : dens {s | affineRetains 3 1 2 s 0 ∧ affineRetains 3 1 1 s 1} = 2 / 9 := by + rw [dens_affineRetains_and_affineRetains (by norm_num) (by norm_num) (by decide)] + norm_num + +-- A seed that retains `y` with side `1` retains it with side `2`. +example (s : Matrix (Fin 2) (Fin 1) (ZMod 5) × (Fin 2 → ZMod 5)) (y : ZMod 5) + (h : affineRetains 5 2 1 s y) : affineRetains 5 2 2 s y := + affineRetains_of_le (by norm_num) h + +/-- The `½`-walk `x → x + 1` on `ZMod 5`. -/ +private noncomputable def W : Matrix (ZMod 5) (ZMod 5) ℝ := + fun x w => if w = x + 1 then 1 / 2 else 0 + +/-- Main function zero through `1/2`. -/ +private noncomputable def k : ℝ → ℝ := fun d => if d ≤ 1 / 2 then 0 else d + +/-- Gate function: one below `1/1000`. -/ +private noncomputable def ρ : ℝ → ℝ := fun r => if r < 1 / 1000 then 1 else 0 + +private theorem row_mass (x : ZMod 5) : ∑ w, W x w ≤ 1 / 2 := by + simp [W, Finset.sum_ite_eq'] + +-- Rank channel of side `⌈5 · 1/2⌉ = 3` in `𝔽₅²` (rate `f = 1/4`), usage channel of side `1`: +-- the atom at `(0, 1)` has conditional mean `k (W 0 1 / f) = k 2 = 2`, for `K = 8002`. +example : 𝔼 s ∈ ({s | affineRetains 5 2 1 s (id 1)} : + Finset (Matrix (Fin 2) (Fin 1) (ZMod 5) × (Fin 2 → ZMod 5))), + Matrix.denseAtom (fun s v => affineRetains 5 2 ⌈(5 : ℕ) * (1 / 2 : ℝ)⌉₊ s (id v)) + (fun s v => affineRetains 5 2 1 s (id v)) k (fun _ => 1) ρ 8002 ((1 / 2 : ℝ) ^ 2) W s 0 1 = + 2 := by + have hceil : ⌈(5 : ℕ) * (1 / 2 : ℝ)⌉₊ = 3 := by + rw [Nat.ceil_eq_iff (by norm_num)]; norm_num + rw [expect_denseAtom_affineRetains (V := ZMod 5) (ident := id) Function.injective_id + (by norm_num) (by norm_num) (Lt := 1) (by norm_num) (by rw [hceil]; norm_num) + (fun _ _ => rfl) (fun r => by unfold ρ; split_ifs <;> norm_num) + (fun r => by unfold ρ; split_ifs <;> norm_num) (by norm_num : (0 : ℝ) < 1 / 2000) + (fun r hr => by unfold ρ; rw [ite_eq_left_iff]; exact fun h => absurd (by linarith) h) + (fun w => by unfold W; split_ifs <;> norm_num) (row_mass 0) (by norm_num)] + norm_num [k, W] + +end ComplexityTests.AtomChannels diff --git a/ComplexityTests/CorrectionAtom.lean b/ComplexityTests/CorrectionAtom.lean new file mode 100644 index 000000000..4db52159a --- /dev/null +++ b/ComplexityTests/CorrectionAtom.lean @@ -0,0 +1,217 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexity.Foundations.Probability.CorrectionAtom +import Complexity.Probability.PairwiseIndependentHash.DetectorChannels +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Tests for the correction atoms + +* The normalization principle on a concrete gate. +* The incoming cap on a concrete column, and the column and row support bounds. +* The correction atom identity with every hypothesis discharged, for a concrete matrix and for every + matrix under the affine retention channels over `𝔽_P`. +* Rank stability on concrete values. +-/ + +namespace ComplexityTests.CorrectionAtom + +open Finset Matrix Cslib Cslib.Probability +open scoped BigOperators + +/-- Correction cutoff: zero through `1/4`. -/ +private noncomputable def Q : ℝ → ℝ := fun v => if v ≤ 1 / 4 then 0 else v + +/-- Row gate: one below `1/1000`. -/ +private noncomputable def ρ : ℝ → ℝ := fun r => if r < 1 / 1000 then 1 else 0 + +/-- Incoming gate: one below `1/4`. -/ +private noncomputable def τ : ℝ → ℝ := fun r => if r < 1 / 4 then 1 else 0 + +/-- Auxiliary score: one above entry `1/8`, ignoring the rank. -/ +private noncomputable def I : ℝ → ℝ → ℝ := fun v _ => if v ≤ 1 / 8 then 0 else 1 + +private theorem ρ_nonneg (r : ℝ) : 0 ≤ ρ r := by unfold ρ; split_ifs <;> norm_num +private theorem ρ_le_one (r : ℝ) : ρ r ≤ 1 := by unfold ρ; split_ifs <;> norm_num +private theorem τ_nonneg (r : ℝ) : 0 ≤ τ r := by unfold τ; split_ifs <;> norm_num +private theorem τ_le_one (r : ℝ) : τ r ≤ 1 := by unfold τ; split_ifs <;> norm_num + +private theorem ρ_eq_one (r : ℝ) (hr : r ≤ 1 / 2000) : ρ r = 1 := by + unfold ρ + split_ifs with h + · rfl + · exact absurd (by linarith) h + +private theorem τ_eq_one (r : ℝ) (hr : r ≤ 1 / 8) : τ r = 1 := by + unfold τ + split_ifs with h + · rfl + · exact absurd (by linarith) h + +private theorem τ_eq_zero (r : ℝ) (hr : 1 / 4 ≤ r) : τ r = 0 := by + unfold τ + split_ifs with h + · exact absurd hr (not_le.mpr h) + · rfl + +private theorem I_eq_zero (v r : ℝ) (hv : v ≤ 1 / 8) : I v r = 0 := by + simp only [I, ite_eq_left_iff] + exact fun h => absurd hv h + +private theorem Q_eq_zero (v : ℝ) (hv : v ≤ 1 / 4) : Q v = 0 := by + simp only [Q, ite_eq_left_iff] + exact fun h => absurd hv h + +private theorem I_eq_one (v r : ℝ) (hQ : Q v ≠ 0) (_ : ρ r ≠ 0) : I v r = 1 := by + unfold I + split_ifs with h + · exact absurd (Q_eq_zero v (by linarith)) hQ + · rfl + +/-! ### The normalization principle -/ + +-- A gate that is closed on one of three draws: dividing by its mean `2/3` removes the bias. +example (m : ℝ) : + 𝔼 s ∈ (univ : Finset (Fin 3)), m * ![1, 1, 0] s / max (1 / 2) (min 1 + (𝔼 s ∈ (univ : Finset (Fin 3)), (![1, 1, 0] : Fin 3 → ℝ) s)) = m := + expect_mul_div_clip_eq univ_nonempty (fun s _ => by fin_cases s <;> norm_num) + (fun s _ => by fin_cases s <;> norm_num) (by + have : (univ.filter fun s : Fin 3 => (![1, 1, 0] : Fin 3 → ℝ) s < 1) = {2} := by + ext s; fin_cases s <;> norm_num + rw [this]; norm_num) m + +/-! ### The incoming cap -/ + +/-- Every source has entry `1` in every column. -/ +private noncomputable def J : Matrix (Fin 3) (Fin 3) ℝ := fun _ _ => 1 + +-- All three retained sources score one at column `0`, so with `K_c = 2` the incoming gate is +-- closed. +example (T : Finset (Fin 3)) : incomingGate I τ 5 2 1 J univ T 0 = 0 := by + refine incomingGate_eq_zero (by norm_num) (by norm_num : (1 / 4 : ℝ) ≤ 1) τ_eq_zero ?_ + have : (univ.filter fun x : Fin 3 => (1 : ℝ) ≤ auxScore I 5 1 J T x 0) = univ := by + ext x + simp only [mem_filter, mem_univ, true_and, auxScore, J, div_one, I] + norm_num + rw [this] + decide + +-- Column and row support on every draw of any channels, with `K_c = 2` and `K = 3`. +example {ι κ : Type*} [Fintype ι] [Fintype κ] (X : ι → Fin 3 → Prop) (Y Yt : κ → Fin 3 → Prop) + [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Y t v)] [∀ t v, Decidable (Yt t v)] + (G : Matrix (Fin 3) (Fin 3) ℝ) (g₀ : Fin 3 → ℝ) (d : ι × κ) (x y : Fin 3) : + #{x ∈ ({w | X d.1 w} : Finset (Fin 3)) | + correctionAtom I τ 3 2 1 G X Y Yt Q (fun _ => 1) ρ g₀ d x y ≠ 0} < 2 ∧ + #{y ∈ ({w | Y d.2 w} : Finset (Fin 3)) | + correctionAtom I τ 3 2 1 G X Y Yt Q (fun _ => 1) ρ g₀ d x y ≠ 0} < 3 := by + refine ⟨card_filter_correctionAtom_col_ne_zero_lt (by norm_num) I_eq_one + (by norm_num : (1 / 4 : ℝ) ≤ 1) τ_eq_zero d y, + card_filter_correctionAtom_row_ne_zero_lt (by norm_num) (by norm_num : (0 : ℝ) ≤ 1 / 4) + Q_eq_zero (by norm_num : (1 / 1000 : ℝ) ≤ 1 / 4) + (fun r hr => ?_) d x⟩ + unfold ρ + split_ifs with h + · exact absurd hr (not_le.mpr h) + · rfl + +/-! ### The identity with all hypotheses discharged -/ + +/-- The `½`-walk `0 → 1 → 2` on three vertices. -/ +private noncomputable def W : Matrix (Fin 3) (Fin 3) ℝ := !![0, 1 / 2, 0; 0, 0, 1 / 2; 0, 0, 0] + +private theorem filter_W : (univ.filter fun w : Fin 3 => (1 / 8 : ℝ) < W w 1 / 1) = {0} := by + ext w; fin_cases w <;> norm_num [W] + +-- With channels that retain everything, `K = 4004` and `K_c = 8`, the correction atom at +-- `(0, 1)` with multiplier `3` has conditional mean `Q (1/2) · 3 = 3/2`. +example : 𝔼 d ∈ (univ.filter fun _ : Unit => True) ×ˢ (univ.filter fun _ : Unit => True), + correctionAtom I τ 4004 8 1 W (fun _ _ => True) (fun _ _ => True) (fun _ _ => True) Q + (fun _ => 1) ρ (fun _ => 3) d 0 1 = 3 / 2 := by + have h := expect_correctionAtom (I := I) (τ := τ) (K := 4004) (Kc := 8) (f := 1) (G := W) + (X := fun (_ : Unit) (_ : Fin 3) => True) (Y := fun (_ : Unit) (_ : Fin 3) => True) + (Yt := fun _ _ => True) (Q := Q) (h := fun _ => 1) (ρ := ρ) (g₀ := fun _ => 3) (x := 0) + (y := 1) ⟨(), by simp⟩ ⟨(), by simp⟩ (fun _ _ => rfl) ρ_nonneg ρ_le_one + (by norm_num : (0 : ℝ) < 1 / 2000) ρ_eq_one τ_nonneg τ_le_one + (by norm_num : (0 : ℝ) ≤ 1 / 8) τ_eq_one I_eq_zero one_pos + (fun w => by fin_cases w <;> norm_num [W]) (M := 1 / 2) (by simp [W, Fin.sum_univ_three]) + (c := 1) zero_le_one (by norm_num) (fun w _ => by simp) (p := 1) zero_le_one + (fun w _ => by simp) (B := 1) (fun _ => by rw [filter_W]; norm_num) (by norm_num) + rw [h] + norm_num [Q, W] + +/-- The pair bound of a retention channel, as a count over the draws retaining `y`. -/ +private theorem card_pair_le {κ V : Type*} [Fintype κ] {Y : κ → V → Prop} + [∀ t v, Decidable (Y t v)] {q : ℝ} {w y : V} + (h : (dens {t | Y t w ∧ Y t y} : ℝ) ≤ q * dens {t | Y t y}) : + (#{t | Y t y ∧ Y t w} : ℝ) ≤ q * #{t | Y t y} := by + have hcard : ∀ T : Finset κ, ((dens T : ℚ≥0) : ℝ) = #T / Fintype.card κ := fun T => by + rw [dens_eq_card_div_card]; push_cast; rfl + rw [hcard, hcard, ← mul_div_assoc] at h + have hset : ({t | Y t y ∧ Y t w} : Finset κ) = ({t | Y t w ∧ Y t y} : Finset κ) := by + ext t; simp only [mem_filter, mem_univ, true_and]; tauto + rw [hset] + rcases (Fintype.card κ).eq_zero_or_pos with h0 | h0 + · have : (univ : Finset κ) = ∅ := univ_eq_empty_iff.mpr (Fintype.card_eq_zero_iff.mp h0) + simp [this] + · exact (div_le_div_iff_of_pos_right (by exact_mod_cast h0)).mp h + +/-- The identity for one retention channel `C` used on both sides, at rate `f`, for every +nonnegative `G` with row mass at most one and at most `R / f` sources above `f / 8` in column +`y`, once `K ≥ 4 (1 + C_pair · 2000)` and `K_c ≥ 4 (1 + C_pair R)`. -/ +private theorem expect_correctionAtom_channel {V κ : Type*} [Fintype V] [Fintype κ] + {C : κ → V → Prop} [∀ t v, Decidable (C t v)] {f π Cπ Cpair Cvar : ℝ} + (hch : RetentionChannels C C f π 1 Cπ Cpair Cvar) (hf : 0 < f) (hCpair : 0 ≤ Cpair) + (G : Matrix V V ℝ) {x y : V} (hG0 : ∀ w, 0 ≤ G x w) (hG1 : ∑ w, G x w ≤ 1) {R : ℝ} + (hD : (#({w | 1 / 8 < G w y / f} : Finset V) : ℝ) * f ≤ R) {K Kc : ℕ} + (hK : 4 * (1 + Cpair * 2000) ≤ (K : ℝ)) (hKc : 4 * (1 + Cpair * R) ≤ (Kc : ℝ)) + (g₀ : V → ℝ) : + 𝔼 d ∈ ({s | C s x} : Finset κ) ×ˢ ({t | C t y} : Finset κ), + correctionAtom I τ K Kc f G C C C Q (fun _ => 1) ρ g₀ d x y = Q (G x y / f) * g₀ y := by + have hπ := (mul_pos one_pos hf).trans_le hch.lower + have hne : ∀ v, ({s | C s v} : Finset κ).Nonempty := fun v => by + by_contra hv + rw [not_nonempty_iff_eq_empty] at hv + have h := hch.dens_Y v + rw [hv, dens_empty, NNRat.cast_zero] at h + linarith + refine expect_correctionAtom (hne x) (hne y) (fun _ _ => rfl) ρ_nonneg ρ_le_one + (by norm_num : (0 : ℝ) < 1 / 2000) ρ_eq_one τ_nonneg τ_le_one + (by norm_num : (0 : ℝ) ≤ 1 / 8) τ_eq_one I_eq_zero hf hG0 hG1 (c := Cpair) hCpair + (by rw [show Cpair * 1 / (1 / 2000) = Cpair * 2000 by field_simp]; exact hK) + (fun w hwy => card_pair_le (hch.pair w y hwy)) (p := Cpair * f) (by positivity) + (fun w hwx => card_pair_le (hch.pair w x hwx)) (B := Cpair * R) (fun _ => ?_) hKc + calc Cpair * f * (#({w | 1 / 8 < G w y / f} : Finset V) : ℝ) + = Cpair * ((#({w | 1 / 8 < G w y / f} : Finset V) : ℝ) * f) := by ring + _ ≤ Cpair * R := by gcongr + +-- Affine retention channels over `𝔽_P` for both the start and the terminal side, at rate +-- `f = a ^ H` (`C_pair = 2 ^ H`). +example {V : Type*} [Fintype V] {P H : ℕ} [Fact P.Prime] {ident : V → ZMod P} + (hident : Function.Injective ident) {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) (ha0 : 0 < a) + (G : Matrix V V ℝ) {x y : V} (hG0 : ∀ w, 0 ≤ G x w) (hG1 : ∑ w, G x w ≤ 1) {R : ℝ} + (hD : (#({w | 1 / 8 < G w y / a ^ H} : Finset V) : ℝ) * a ^ H ≤ R) {K Kc : ℕ} + (hK : 4 * (1 + 2 ^ H * 2000) ≤ (K : ℝ)) (hKc : 4 * (1 + 2 ^ H * R) ≤ (Kc : ℝ)) + (g₀ : V → ℝ) : + 𝔼 d ∈ ({s | affineRetains P H ⌈P * a⌉₊ s (ident x)} : Finset _) ×ˢ + ({t | affineRetains P H ⌈P * a⌉₊ t (ident y)} : Finset _), + correctionAtom I τ K Kc (a ^ H) G (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) + (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) + (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) Q (fun _ => 1) ρ g₀ d x y = + Q (G x y / a ^ H) * g₀ y := + expect_correctionAtom_channel (retentionChannels_affineRetains hident hPa ha) (pow_pos ha0 H) + (by positivity) G hG0 hG1 hD hK hKc g₀ + +/-! ### Rank stability -/ + +-- Perturbing `3, 1, 2, 0` by at most `1/2` moves its second largest value `2` by at most `1/2`. +example : |kthLargest 2 univ (![3, 1, 2, 0] : Fin 4 → ℚ) - + kthLargest 2 univ (![5 / 2, 1, 5 / 2, 1 / 2] : Fin 4 → ℚ)| ≤ 1 / 2 := + abs_kthLargest_sub_kthLargest_le (by norm_num) (by norm_num) fun x _ => by + fin_cases x <;> norm_num + +end ComplexityTests.CorrectionAtom diff --git a/ComplexityTests/RootMetric.lean b/ComplexityTests/RootMetric.lean new file mode 100644 index 000000000..09d827078 --- /dev/null +++ b/ComplexityTests/RootMetric.lean @@ -0,0 +1,160 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexity.Foundations.Probability.AtomCutoffs +import Complexity.Foundations.Probability.CorrectionAtom +import Complexity.Foundations.Probability.RootMetric +import Complexity.Foundations.Analysis.RootError +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Tests for smooth switches, root errors and root metrics + +* The switch at its midpoint and the reflection of its complement. +* The correction atom identity and the incoming cap with the smooth cutoffs of (5.5) and (5.12), + every hypothesis discharged. +* Ordinary versus root error, and the homogeneous loss, on concrete values. +* The row norm and the uniform bound on a concrete table. +-/ + +namespace ComplexityTests.RootMetric + +open Finset Matrix Cslib Real +open scoped BigOperators + +/-! ### Smooth switches -/ + +-- The switch `χ_{0,1}` is `1/2` at the midpoint. +example : smoothSwitch 0 1 (1 / 2) = 1 / 2 := by + have hpos := expNegInvGlue.pos_of_pos (by norm_num : (0 : ℝ) < 1 / 2) + rw [smoothSwitch, smoothTransition] + norm_num + field_simp + ring + +-- The complement of `χ_{0,1}` at `1/4` is its value at `3/4`. +example : 1 - smoothSwitch 0 1 (1 / 4) = smoothSwitch 0 1 (3 / 4) := by + rw [smoothSwitch, smoothSwitch, smoothTransition.one_sub] + norm_num + +-- The fourth roots of the incoming cutoff are Lipschitz. +example : ∃ K, LipschitzWith K fun r => incomingCutoff r ^ (1 / 4 : ℝ) := + exists_lipschitzWith_incomingCutoff_rpow (by norm_num) + +/-! ### The correction atom with the smooth cutoffs -/ + +/-- Correction cutoff: zero through `ϑ = 1/4`. -/ +private noncomputable def Q : ℝ → ℝ := fun v => if v ≤ 1 / 4 then 0 else v + +private theorem le_of_Q_ne_zero {v : ℝ} (hQ : Q v ≠ 0) : 1 / 4 < v := by + unfold Q at hQ + split_ifs at hQ with h + · exact absurd rfl hQ + · exact not_le.1 h + +/-- The `½`-walk `0 → 1 → 2` on three vertices. -/ +private noncomputable def W : Matrix (Fin 3) (Fin 3) ℝ := !![0, 1 / 2, 0; 0, 0, 1 / 2; 0, 0, 0] + +private theorem filter_W : (univ.filter fun w : Fin 3 => (1 / 4 / 8 : ℝ) < W w 1 / 1) = {0} := by + ext w; fin_cases w <;> norm_num [W] + +-- With channels that retain everything, `ϑ = 1/4`, `K = 8004` and `K_c = 8`, the correction +-- atom at `(0, 1)` with multiplier `3` has conditional mean `Q (1/2) · 3 = 3/2`. +example : 𝔼 d ∈ (univ.filter fun _ : Unit => True) ×ˢ (univ.filter fun _ : Unit => True), + correctionAtom (auxCutoff (1 / 4)) incomingCutoff 8004 8 1 W (fun _ _ => True) + (fun _ _ => True) (fun _ _ => True) Q (prepCutoff (1 / 4)) (rowCutoff (1 / 4)) + (fun _ => 3) d 0 1 = 3 / 2 := by + have h := expect_correctionAtom (I := auxCutoff (1 / 4)) (τ := incomingCutoff) (K := 8004) + (Kc := 8) (f := 1) (G := W) (X := fun (_ : Unit) (_ : Fin 3) => True) + (Y := fun (_ : Unit) (_ : Fin 3) => True) (Yt := fun _ _ => True) (Q := Q) + (h := prepCutoff (1 / 4)) (ρ := rowCutoff (1 / 4)) (g₀ := fun _ => 3) (x := 0) (y := 1) + ⟨(), by simp⟩ ⟨(), by simp⟩ + (fun v hv => prepCutoff_eq_one (by norm_num) (by linarith [le_of_Q_ne_zero hv])) + (rowCutoff_nonneg _) (rowCutoff_le_one _) (by norm_num : (0 : ℝ) < 1 / 4 / 1000) + (fun r hr => rowCutoff_eq_one (by norm_num) hr) incomingCutoff_nonneg incomingCutoff_le_one + (by norm_num : (0 : ℝ) ≤ 1 / 4) (fun r hr => incomingCutoff_eq_one hr) + (fun v r hv => auxCutoff_eq_zero (by norm_num) hv) one_pos + (fun w => by fin_cases w <;> norm_num [W]) (M := 1 / 2) (by simp [W, Fin.sum_univ_three]) + (c := 1) zero_le_one (by norm_num) (fun w _ => by simp) (p := 1) zero_le_one + (fun w _ => by simp) (B := 1) (fun _ => by rw [filter_W]; norm_num) (by norm_num) + rw [h] + norm_num [Q, W] + +-- The incoming cap with the smooth cutoffs: on every draw of any channels, fewer than `K_c = 2` +-- retained sources have a nonzero correction atom in a column. +example {ι κ : Type*} [Fintype ι] [Fintype κ] (X : ι → Fin 3 → Prop) (Y Yt : κ → Fin 3 → Prop) + [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Y t v)] [∀ t v, Decidable (Yt t v)] + (G : Matrix (Fin 3) (Fin 3) ℝ) (g₀ : Fin 3 → ℝ) (d : ι × κ) (y : Fin 3) : + #{x ∈ ({w | X d.1 w} : Finset (Fin 3)) | + correctionAtom (auxCutoff (1 / 4)) incomingCutoff 3 2 1 G X Y Yt Q (prepCutoff (1 / 4)) + (rowCutoff (1 / 4)) g₀ d x y ≠ 0} < 2 := by + refine card_filter_correctionAtom_col_ne_zero_lt (by norm_num) ?_ (g := 1 / 2) (by norm_num) + (fun r hr => incomingCutoff_eq_zero hr) d y + intro v r hQ hρ + have hv := le_of_Q_ne_zero hQ + exact auxCutoff_eq_one_of_rowCutoff_ne_zero (by norm_num) (by linarith) hρ + +/-! ### Root error and the homogeneous loss -/ + +private theorem sixteen_rpow : (16 : ℝ) ^ ((4 : ℕ)⁻¹ : ℝ) = 2 := by + rw [show (16 : ℝ) = 2 ^ 4 by norm_num] + exact Real.pow_rpow_inv_natCast (by norm_num) (by norm_num) + +-- `|16 - 1| ≤ 4 · 16^{3/4} · |16^{1/4} - 1^{1/4}| = 4 · 8 · 1`. +example : |(16 : ℝ) - 1| ≤ 32 := by + have h := abs_sub_le_mul_abs_rpow_inv_sub (s := 4) (by norm_num) (z := 16) (w := 1) (C := 16) + (by norm_num) (by norm_num) le_rfl (by norm_num) + have h34 : (16 : ℝ) ^ ((((4 : ℕ) : ℝ) - 1) / ((4 : ℕ) : ℝ)) = 8 := by + rw [show (((4 : ℕ) : ℝ) - 1) / ((4 : ℕ) : ℝ) = ((4 : ℕ) : ℝ)⁻¹ * (3 : ℕ) by norm_num, + Real.rpow_mul (by norm_num), sixteen_rpow, Real.rpow_natCast] + norm_num + rw [h34, sixteen_rpow, Real.one_rpow] at h + norm_num at h ⊢ + +example : homogeneousLoss 2 3 1 = 1 := by norm_num [homogeneousLoss] + +-- The loss is not additive: `L(1, 1) = 0` lies below `L(1, 0) + L(0, 1) = 2`. +example : homogeneousLoss 2 (1 + 0) (0 + 1) ≤ homogeneousLoss 2 1 0 + homogeneousLoss 2 0 1 := by + have h := homogeneousLoss_sum_le (s := 2) (univ : Finset (Fin 2)) (by norm_num) + (w := fun _ => 1) (F := ![1, 0]) (F' := ![0, 1]) (fun _ _ => zero_le_one) + (fun i _ => by fin_cases i <;> norm_num) (fun i _ => by fin_cases i <;> norm_num) + simpa [Fin.sum_univ_two] using h + +-- The clipped relative error (7.7) for `H = 1 ≤ 1 · G` with `G = 1`, `H' = 3` and `a = 1`. +example : 1 * min 1 (|(1 : ℝ) - 3| / (1 + 1)) ^ 2 ≤ 2 * (3 * 1 + 3) ^ 1 * 1 := by + have h := mul_min_pow_le_homogeneousLoss (s := 2) (by norm_num) (C₀ := 1) (G := 1) (a := 1) + (H := 1) (H' := 3) zero_le_one zero_le_one one_pos zero_le_one (by norm_num) (by norm_num) + have hL : homogeneousLoss 2 1 3 = 1 := by norm_num [homogeneousLoss] + rwa [hL] at h + +/-! ### Row norms -/ + +/-- A table on `Fin 2` with a single nonzero entry `2` at `(0, 1)`. -/ +private def Z : Unit → Fin 2 → Fin 2 → ℝ := fun _ x y => if x = 0 ∧ y = 1 then 2 else 0 + +-- Its fourth-power norm with full channels, `N = 2` and `u = 1` is `2^4 / 2 = 8`. +example : rowNormPow 4 2 1 (fun (_ : Unit) (_ : Fin 2) => True) (fun _ _ => True) Z = 8 := by + simp [rowNormPow, Z, Fin.sum_univ_two] + norm_num + +-- The uniform bound: one nonzero entry of size `2` per row gives `‖Z‖^4 ≤ 1 · 2^4 · ‖1‖^4 = 16`. +example : rowNormPow 4 2 1 (fun (_ : Unit) (_ : Fin 2) => True) (fun _ _ => True) Z ≤ 16 := by + have h := rowNormPow_le_of_card_le (s := 4) (N := 2) (u := 1) (K := 1) (B := 2) + (X := fun (_ : Unit) (_ : Fin 2) => True) (Y := fun _ _ => True) (Z := Z) (by norm_num) + (by norm_num) (by norm_num) (fun _ x y => by unfold Z; split_ifs <;> norm_num) + (fun σ x _ => card_le_one.2 fun a ha b hb => by + simp only [Z, mem_filter, mem_univ, true_and, ne_eq, ite_eq_right_iff, not_forall] at ha hb + obtain ⟨⟨_, rfl⟩, _⟩ := ha + obtain ⟨⟨_, rfl⟩, _⟩ := hb + rfl) + have hv : vertexNormPow 4 2 1 (fun (_ : Unit) (_ : Fin 2) => True) (fun _ _ => (1 : ℝ)) = 1 := by + simp [vertexNormPow] + rw [hv] at h + norm_num at h + exact h + +end ComplexityTests.RootMetric