diff --git a/Complexity.lean b/Complexity.lean index 7f870ea21..79eaa9772 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2558,6 +2558,7 @@ public import Complexity.Foundations.Data.Fin.Tuple public import Complexity.Foundations.Data.Finset.Average public import Complexity.Foundations.Data.Finset.Expect public import Complexity.Foundations.Data.Finset.Finpartition +public import Complexity.Foundations.Data.Finset.KthLargest public import Complexity.Foundations.Data.Finset.Markov public import Complexity.Foundations.Data.Finset.OrderGlue public import Complexity.Foundations.Data.Finset.OrderedFilter @@ -2689,6 +2690,7 @@ public import Complexity.Foundations.LinearAlgebra.Matrix.Kronecker public import Complexity.Foundations.LinearAlgebra.Matrix.Lindsey public import Complexity.Foundations.LinearAlgebra.Matrix.ListProd public import Complexity.Foundations.LinearAlgebra.Matrix.Moore +public import Complexity.Foundations.LinearAlgebra.Matrix.PilotCorrection public import Complexity.Foundations.LinearAlgebra.Matrix.Rank public import Complexity.Foundations.LinearAlgebra.Matrix.RectPermanent public import Complexity.Foundations.LinearAlgebra.Matrix.SchurComplement @@ -2711,6 +2713,8 @@ 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.ColumnDetector +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 @@ -2978,6 +2982,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.DetectorChannels public import Complexity.Probability.PairwiseIndependentHash.Retention public import Complexity.Probability.PairwiseIndependentHash.RetentionChannel public import Complexity.Probability.PairwiseIndependentHash.Shift diff --git a/Complexity/Foundations/Data/Finset/KthLargest.lean b/Complexity/Foundations/Data/Finset/KthLargest.lean new file mode 100644 index 000000000..b1198aef3 --- /dev/null +++ b/Complexity/Foundations/Data/Finset/KthLargest.lean @@ -0,0 +1,116 @@ +/- +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.Data.Finset.Max + +/-! +# The `k`-th largest value, padded with zeros + +`Finset.kthLargest k s h` is the `k`-th largest member of the multiset of values `h x`, `x ∈ s`, +padded with infinitely many zeros. It is the largest value `h x` that is reached or exceeded by at +least `k` of the values, or `0` if that is larger. So it is nonnegative, and it is `0` when fewer +than `k` of the values are positive. This is the order statistic `rank_k` of the detectors in the +OpenAI preprint [OpenAI2026LogSpace, Section 4.2]. + +It is characterized by threshold counts: for `0 < k` and `0 ≤ t`, the `k`-th largest value exceeds +`t` exactly when at least `k` values exceed `t` (`Finset.lt_kthLargest_iff`), and for `0 < t` it +is at least `t` exactly when at least `k` values are at least `t` (`Finset.le_kthLargest_iff`). + +## Main definitions + +* `Finset.kthLargest`: the `k`-th largest value, padded with zeros. + +## Main results + +* `Finset.kthLargest_nonneg`, `Finset.kthLargest_le`: bounds. +* `Finset.lt_kthLargest_iff`, `Finset.le_kthLargest_iff`: the threshold characterizations. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 4.2 (preprint, not peer reviewed) +-/ + +public section + +namespace Finset + +variable {α R : Type*} [LinearOrder R] [Zero R] + +/-- The **`k`-th largest value** of `h` on `s`, padded with zeros: the largest value `h x`, +`x ∈ s`, that at least `k` values `h w`, `w ∈ s`, reach or exceed, or `0` if that is larger. -/ +@[expose] def kthLargest (k : ℕ) (s : Finset α) (h : α → R) : R := + (insert 0 ((s.filter fun x => k ≤ #{w ∈ s | h x ≤ h w}).image h)).max' (insert_nonempty _ _) + +variable {k : ℕ} {s : Finset α} {h : α → R} {t : R} + +theorem kthLargest_nonneg : 0 ≤ kthLargest k s h := + le_max' _ _ (mem_insert_self _ _) + +/-- The `k`-th largest value is at most any nonnegative upper bound of the values. -/ +theorem kthLargest_le (ht : 0 ≤ t) (hh : ∀ x ∈ s, h x ≤ t) : kthLargest k s h ≤ t := by + refine max'_le _ _ _ fun a ha => ?_ + rcases mem_insert.mp ha with rfl | ha + · exact ht + · obtain ⟨x, hx, rfl⟩ := mem_image.mp ha + exact hh x (mem_filter.mp hx).1 + +/-- A value of `s` reached or exceeded by at least `k` values is at most the `k`-th largest. -/ +private theorem le_kthLargest_of_le_card {x : α} (hx : x ∈ s) + (hk : k ≤ #{w ∈ s | h x ≤ h w}) : h x ≤ kthLargest k s h := + le_max' _ _ (mem_insert_of_mem (mem_image_of_mem h (mem_filter.mpr ⟨hx, hk⟩))) + +omit [Zero R] in +/-- If at least `k > 0` values satisfy a threshold condition, so does the smallest of them, which +is reached or exceeded by all of them. -/ +private theorem exists_le_card (hk : 0 < k) (p : R → Prop) [DecidablePred p] + (hp : k ≤ #{x ∈ s | p (h x)}) : + ∃ x ∈ s, p (h x) ∧ k ≤ #{w ∈ s | h x ≤ h w} := by + have hne : ({x ∈ s | p (h x)} : Finset α).Nonempty := card_pos.mp (hk.trans_le hp) + obtain ⟨x, hx, hmin⟩ := exists_min_image _ h hne + obtain ⟨hxs, hpx⟩ := mem_filter.mp hx + refine ⟨x, hxs, hpx, hp.trans (card_le_card fun w hw => ?_)⟩ + exact mem_filter.mpr ⟨(mem_filter.mp hw).1, hmin w hw⟩ + +/-- **The `k`-th largest value exceeds `t ≥ 0`** exactly when at least `k > 0` values do. -/ +theorem lt_kthLargest_iff (hk : 0 < k) (ht : 0 ≤ t) : + t < kthLargest k s h ↔ k ≤ #{x ∈ s | t < h x} := by + constructor + · intro hlt + obtain ⟨a, ha, hta⟩ : ∃ a ∈ _, t < a := ⟨_, max'_mem _ _, hlt⟩ + rcases mem_insert.mp ha with rfl | ha + · exact absurd ht (not_le.mpr hta) + obtain ⟨x, hx, rfl⟩ := mem_image.mp ha + obtain ⟨-, hkx⟩ := mem_filter.mp hx + exact hkx.trans (card_le_card fun w hw => by + obtain ⟨hws, hxw⟩ := mem_filter.mp hw + exact mem_filter.mpr ⟨hws, hta.trans_le hxw⟩) + · intro hcard + obtain ⟨x, hxs, htx, hkx⟩ := exists_le_card hk (t < ·) hcard + exact htx.trans_le (le_kthLargest_of_le_card hxs hkx) + +/-- **The `k`-th largest value is at least `t > 0`** exactly when at least `k > 0` values are. -/ +theorem le_kthLargest_iff (hk : 0 < k) (ht : 0 < t) : + t ≤ kthLargest k s h ↔ k ≤ #{x ∈ s | t ≤ h x} := by + constructor + · intro hle + obtain ⟨a, ha, hta⟩ : ∃ a ∈ _, t ≤ a := ⟨_, max'_mem _ _, hle⟩ + rcases mem_insert.mp ha with rfl | ha + · exact absurd ht (not_lt.mpr hta) + obtain ⟨x, hx, rfl⟩ := mem_image.mp ha + obtain ⟨-, hkx⟩ := mem_filter.mp hx + exact hkx.trans (card_le_card fun w hw => by + obtain ⟨hws, hxw⟩ := mem_filter.mp hw + exact mem_filter.mpr ⟨hws, hta.trans hxw⟩) + · intro hcard + obtain ⟨x, hxs, htx, hkx⟩ := exists_le_card hk (t ≤ ·) hcard + exact htx.trans (le_kthLargest_of_le_card hxs hkx) + +end Finset diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/CopyStage.lean b/Complexity/Foundations/LinearAlgebra/Matrix/CopyStage.lean index d9a33084e..9ee05d128 100644 --- a/Complexity/Foundations/LinearAlgebra/Matrix/CopyStage.lean +++ b/Complexity/Foundations/LinearAlgebra/Matrix/CopyStage.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Foundations.LinearAlgebra.Matrix.FactorialTruncation +import Complexity.Foundations.LinearAlgebra.Matrix.PilotCorrection import Mathlib.Algebra.BigOperators.Fin /-! @@ -95,65 +96,24 @@ variable {V : Type*} [Fintype V] {φ : V → ℝ → ℝ} {C : Matrix V V ℝ} { variable (hC0 : ∀ x y, 0 ≤ C x y) (hφ0 : ∀ y t, 0 ≤ φ y t) (hφθ : ∀ y t, φ y t ≤ max (t - θ * f) 0) (hθf : 0 ≤ θ * f) -omit [Fintype V] in -include hφθ hθf in -private theorem cutoff_le_self' (y : V) {t : ℝ} (ht : 0 ≤ t) : φ y t ≤ t := - (hφθ y t).trans (max_le (by linarith) ht) - omit [Fintype V] in include hφ0 hφθ hθf in private theorem cutoff_zero (y : V) : φ y 0 = 0 := le_antisymm ((hφθ y 0).trans (max_le (by linarith) le_rfl)) (hφ0 y 0) -include hC0 hφ0 hφθ hθf in -private theorem iter_succ_le_input (k : ℕ) (x y : V) : - cutoffCorrectionIter φ C (k + 1) x y ≤ (C + cutoffCorrectionIter φ C k * C) x y := by - rw [cutoffCorrectionIter_succ] - exact cutoff_le_self' hφθ hθf y <| add_nonneg (hC0 x y) <| Finset.sum_nonneg fun z _ => - mul_nonneg (cutoffCorrectionIter_nonneg hφ0 k x z) (hC0 z y) - include hC0 hφ0 hφθ hθf in /-- **Row sums of the iterates**: the `k`-th iterate of a cutoff correction of a substochastic `C` has row sums at most `k` [OpenAI2026LogSpace, Lemma 4.2]. -/ theorem cutoffCorrectionIter_sum_le (hC1 : C *ᵥ 1 ≤ 1) (k : ℕ) (x : V) : - ∑ y, cutoffCorrectionIter φ C k x y ≤ k := by - have hrow : ∀ z, ∑ y, C z y ≤ 1 := fun z => by simpa [mulVec, dotProduct] using hC1 z - induction k with - | zero => simp [cutoffCorrectionIter] - | succ k ih => - set F := cutoffCorrectionIter φ C k - calc ∑ y, cutoffCorrectionIter φ C (k + 1) x y ≤ ∑ y, (C + F * C) x y := - Finset.sum_le_sum fun y _ => iter_succ_le_input hC0 hφ0 hφθ hθf k x y - _ = ∑ y, C x y + ∑ z, F x z * ∑ y, C z y := by - simp only [Matrix.add_apply, Matrix.mul_apply, Finset.sum_add_distrib, Finset.mul_sum] - rw [Finset.sum_comm] - _ ≤ 1 + ∑ z, F x z * 1 := add_le_add (hrow x) (Finset.sum_le_sum fun z _ => - mul_le_mul_of_nonneg_left (hrow z) (cutoffCorrectionIter_nonneg hφ0 k x z)) - _ ≤ (k + 1 : ℕ) := by simp only [mul_one]; push_cast; linarith - -include hC0 hφ0 hφθ hθf in -/-- The input `(C + E_k C) x y` of the `(k + 1)`-th step is at most `(k + 1) f`. -/ -private theorem input_le (hCf : ∀ x y, C x y ≤ f) (hf : 0 ≤ f) (hC1 : C *ᵥ 1 ≤ 1) (k : ℕ) - (x y : V) : (C + cutoffCorrectionIter φ C k * C) x y ≤ (k + 1) * f := by - have hsum := cutoffCorrectionIter_sum_le hC0 hφ0 hφθ hθf hC1 k x - calc (C + cutoffCorrectionIter φ C k * C) x y - = C x y + ∑ z, cutoffCorrectionIter φ C k x z * C z y := rfl - _ ≤ f + ∑ z, cutoffCorrectionIter φ C k x z * f := add_le_add (hCf x y) - (Finset.sum_le_sum fun z _ => - mul_le_mul_of_nonneg_left (hCf z y) (cutoffCorrectionIter_nonneg hφ0 k x z)) - _ ≤ (k + 1) * f := by rw [← Finset.sum_mul]; nlinarith + ∑ y, cutoffCorrectionIter φ C k x y ≤ k := + (isCorrectionSeq_cutoffCorrectionIter hC0 hφ0 hφθ hθf).sum_le hC1 k x include hC0 hφ0 hφθ hθf in /-- **Entries of the iterates**: the `k`-th iterate has entries at most `k f` [OpenAI2026LogSpace, Lemma 4.2]. -/ theorem cutoffCorrectionIter_le_mul (hCf : ∀ x y, C x y ≤ f) (hf : 0 ≤ f) (hC1 : C *ᵥ 1 ≤ 1) - (k : ℕ) (x y : V) : cutoffCorrectionIter φ C k x y ≤ k * f := by - cases k with - | zero => simp [cutoffCorrectionIter] - | succ k => - push_cast - exact (iter_succ_le_input hC0 hφ0 hφθ hθf k x y).trans - (input_le hC0 hφ0 hφθ hθf hCf hf hC1 k x y) + (k : ℕ) (x y : V) : cutoffCorrectionIter φ C k x y ≤ k * f := + (isCorrectionSeq_cutoffCorrectionIter hC0 hφ0 hφθ hθf).le_mul hCf hf hC1 k x y include hC0 hφ0 hφθ hθf in /-- **The residual entry bound**: `C - E_k + E_k C` has entries at most `(k + 1) f` @@ -161,7 +121,8 @@ include hC0 hφ0 hφθ hθf in theorem cutoffCorrection_residual_le_mul (hCf : ∀ x y, C x y ≤ f) (hf : 0 ≤ f) (hC1 : C *ᵥ 1 ≤ 1) (k : ℕ) (x y : V) : (C - cutoffCorrectionIter φ C k + cutoffCorrectionIter φ C k * C) x y ≤ (k + 1) * f := by - have h := input_le hC0 hφ0 hφθ hθf hCf hf hC1 k x y + have h := (isCorrectionSeq_cutoffCorrectionIter hC0 hφ0 hφθ hθf).input_le_mul hCf hf hC1 k + x y have h0 := cutoffCorrectionIter_nonneg (C := C) hφ0 k x y simp only [Matrix.add_apply, Matrix.sub_apply] at h ⊢ linarith @@ -180,12 +141,13 @@ theorem cutoffCorrection_residual_dominates (hCf : ∀ x y, C x y ≤ f) (hf : 0 have ha0 : 0 ≤ (C + cutoffCorrectionIter φ C k * C) x y := add_nonneg (hC0 x y) (Finset.sum_nonneg fun z _ => mul_nonneg (cutoffCorrectionIter_nonneg hφ0 k x z) (hC0 z y)) - have ha := input_le hC0 hφ0 hφθ hθf hCf hf hC1 k x y + have ha := (isCorrectionSeq_cutoffCorrectionIter hC0 hφ0 hφθ hθf).input_le_mul hCf hf hC1 k + x y have hEa : cutoffCorrectionIter φ C (k + 1) x y = φ y ((C + cutoffCorrectionIter φ C k * C) x y) := by rw [cutoffCorrectionIter_succ]; rfl have he0 := cutoffCorrectionIter_nonneg (C := C) hφ0 (k + 1) x y - have hea := iter_succ_le_input hC0 hφ0 hφθ hθf k x y + have hea := (isCorrectionSeq_cutoffCorrectionIter hC0 hφ0 hφθ hθf).le_input k x y have hFE : (cutoffCorrectionIter φ C k * C) x y ≤ (cutoffCorrectionIter φ C (k + 1) * C) x y := Finset.sum_le_sum fun z _ => mul_le_mul_of_nonneg_right (cutoffCorrectionIter_le_succ hC0 hφ0 hφm k x z) (hC0 z y) diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/PilotCorrection.lean b/Complexity/Foundations/LinearAlgebra/Matrix/PilotCorrection.lean new file mode 100644 index 000000000..d9373a6d8 --- /dev/null +++ b/Complexity/Foundations/LinearAlgebra/Matrix/PilotCorrection.lean @@ -0,0 +1,331 @@ +/- +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.LinearAlgebra.Matrix.FactorialTruncation + +/-! +# The pilot correction with step-dependent multipliers + +In the correction-and-copy hierarchy of the OpenAI preprint (2026-09-23), Section 4.2, idea 3 in +issue #474 [OpenAI2026LogSpace], the column multiplier of the cutoff correction is chosen by a +*pilot*: a run of the correction recursion in which the multiplier may decrease from step to +step. At step `i + 1` the pilot forms its input `G = C + Ê_i C`, evaluates a column number +`U G y` on it (in the preprint a detector, see `Complexity.Foundations.Probability.ColumnDetector`), +takes the running maximum `M_(i+1) = M_i ⊔ U G`, and sets +`Ê_(i+1) x y = c (G x y) * γ (M_(i+1) y)` for a base cutoff `c` and a nonincreasing `γ` +(`Matrix.pilotCorrection`, `Matrix.pilotMax`, `Matrix.pilotInput`). The actual correction then +runs the fixed-multiplier recursion `Matrix.cutoffCorrectionIter` with the final multiplier +`γ (M_k y)`. + +All bounds of [OpenAI2026LogSpace, Lemma 4.2] hold for any sequence of corrections that starts at +zero and stays between zero and its input, `0 ≤ F (i + 1) ≤ C + F i C` +(`Matrix.IsCorrectionSeq`). Both the pilot (`Matrix.isCorrectionSeq_pilotCorrection`) and the +fixed-multiplier recursion (`Matrix.isCorrectionSeq_cutoffCorrectionIter`) are of this form. For +a substochastic `C` with entries at most `f`, the `i`-th correction and the input of step `i + 1` +have row sums at most `i` and `i + 1` and entries at most `i f` and `(i + 1) f`; they are +supported within any cover of the support of `C`, and strictly upper triangular when `C` is. +Since the running maximum only grows and `γ` is nonincreasing, the actual correction and its inputs +are bounded by those of the pilot (`Matrix.cutoffCorrectionIter_le_pilotCorrection`). + +## Main definitions + +* `Matrix.IsCorrectionSeq`: corrections starting at zero and dominated by their inputs. +* `Matrix.pilotCorrection`, `Matrix.pilotMax`, `Matrix.pilotInput`: the pilot. + +## Main results + +* `Matrix.IsCorrectionSeq.sum_le`, `Matrix.IsCorrectionSeq.sum_input_le`, + `Matrix.IsCorrectionSeq.le_mul`, `Matrix.IsCorrectionSeq.input_le_mul`: row-sum and entry + bounds. +* `Matrix.IsCorrectionSeq.mem`, `Matrix.IsCorrectionSeq.input_mem`: supports. +* `Matrix.IsCorrectionSeq.isStrictUpperTriangular`, + `Matrix.IsCorrectionSeq.input_isStrictUpperTriangular`: strict forwardness. +* `Matrix.isCorrectionSeq_cutoffCorrectionIter`, `Matrix.isCorrectionSeq_pilotCorrection`: the + actual correction and the pilot are correction sequences. +* `Matrix.cutoffCorrectionIter_le_of_isCorrectionSeq`: comparison with a dominating sequence. +* `Matrix.pilotMax_mono`, `Matrix.exists_lt_pilotInput_of_lt_pilotMax`: the running maximum. +* `Matrix.cutoffCorrectionIter_le_pilotCorrection`: the actual correction is at most the pilot. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 4.2 and Lemma 4.2 (preprint, not peer reviewed) +-/ + +public section + +open Finset + +namespace Matrix + +variable {V : Type*} [Fintype V] {F : ℕ → Matrix V V ℝ} {f : ℝ} + +/-- `F` is a **correction sequence** for `C`: it starts at zero, and each correction lies between +zero and its input, `0 ≤ F (i + 1) ≤ C + F i * C` entrywise. The pilot of the preprint, with +step-dependent multipliers, and the actual correction, with a fixed multiplier, are both of this +form [OpenAI2026LogSpace, Lemma 4.2]. -/ +structure IsCorrectionSeq (C : Matrix V V ℝ) (F : ℕ → Matrix V V ℝ) : Prop where + zero : F 0 = 0 + nonneg_succ : ∀ i x y, 0 ≤ F (i + 1) x y + le_input : ∀ i x y, F (i + 1) x y ≤ (C + F i * C) x y + +section Sequence + +variable {C : Matrix V V ℝ} + +namespace IsCorrectionSeq + +variable (hF : IsCorrectionSeq C F) +include hF + +theorem nonneg (i : ℕ) (x y : V) : 0 ≤ F i x y := by + cases i with + | zero => simp [hF.zero] + | succ i => exact hF.nonneg_succ i x y + +theorem input_nonneg (hC0 : ∀ x y, 0 ≤ C x y) (i : ℕ) (x y : V) : 0 ≤ (C + F i * C) x y := + add_nonneg (hC0 x y) (sum_nonneg fun z _ => mul_nonneg (hF.nonneg i x z) (hC0 z y)) + +/-- **Row sums of the corrections**: the `i`-th correction of a substochastic `C` has row sums at +most `i`, and the input of step `i + 1` at most `i + 1` [OpenAI2026LogSpace, Lemma 4.2]. -/ +theorem sum_input_le (hC1 : C *ᵥ 1 ≤ 1) : + ∀ i x, ∑ y, (C + F i * C) x y ≤ i + 1 ∧ ∑ y, F i x y ≤ i := by + have hrow : ∀ z, ∑ y, C z y ≤ 1 := fun z => by simpa [mulVec, dotProduct] using hC1 z + have hinput : ∀ i x, ∑ y, F i x y ≤ i → ∑ y, (C + F i * C) x y ≤ i + 1 := fun i x hi => by + calc ∑ y, (C + F i * C) x y = ∑ y, C x y + ∑ z, F i x z * ∑ y, C z y := by + simp only [Matrix.add_apply, Matrix.mul_apply, sum_add_distrib, mul_sum] + rw [sum_comm] + _ ≤ 1 + ∑ z, F i x z * 1 := add_le_add (hrow x) (sum_le_sum fun z _ => + mul_le_mul_of_nonneg_left (hrow z) (hF.nonneg i x z)) + _ ≤ i + 1 := by simp only [mul_one]; linarith + intro i + induction i with + | zero => intro x; simpa [hF.zero] using hinput 0 x (by simp [hF.zero]) + | succ i ih => + intro x + have hsum : ∑ y, F (i + 1) x y ≤ (i + 1 : ℕ) := by + push_cast + exact (sum_le_sum fun y _ => hF.le_input i x y).trans (ih x).1 + exact ⟨hinput _ x hsum, hsum⟩ + +theorem sum_le (hC1 : C *ᵥ 1 ≤ 1) (i : ℕ) (x : V) : ∑ y, F i x y ≤ i := + (hF.sum_input_le hC1 i x).2 + +/-- **Entries of the inputs**: the input of step `i + 1` has entries at most `(i + 1) f` +[OpenAI2026LogSpace, Lemma 4.2]. -/ +theorem input_le_mul (hCf : ∀ x y, C x y ≤ f) (hf : 0 ≤ f) (hC1 : C *ᵥ 1 ≤ 1) (i : ℕ) + (x y : V) : (C + F i * C) x y ≤ (i + 1) * f := by + have hsum := hF.sum_le hC1 i x + calc (C + F i * C) x y = C x y + ∑ z, F i x z * C z y := rfl + _ ≤ f + ∑ z, F i x z * f := add_le_add (hCf x y) + (sum_le_sum fun z _ => mul_le_mul_of_nonneg_left (hCf z y) (hF.nonneg i x z)) + _ ≤ (i + 1) * f := by rw [← sum_mul]; nlinarith + +/-- **Entries of the corrections**: the `i`-th correction has entries at most `i f` +[OpenAI2026LogSpace, Lemma 4.2]. -/ +theorem le_mul (hCf : ∀ x y, C x y ≤ f) (hf : 0 ≤ f) (hC1 : C *ᵥ 1 ≤ 1) (i : ℕ) (x y : V) : + F i x y ≤ i * f := by + cases i with + | zero => simp [hF.zero] + | succ i => + push_cast + exact (hF.le_input i x y).trans (hF.input_le_mul hCf hf hC1 i x y) + +variable {A : Finset V} + +/-- The corrections and the inputs are supported within any set `A` covering the support of `C` +[OpenAI2026LogSpace, Lemma 4.2]. -/ +theorem input_mem_and_mem (hA : ∀ x y, C x y ≠ 0 → x ∈ A ∧ y ∈ A) : + ∀ i x y, ((C + F i * C) x y ≠ 0 → x ∈ A ∧ y ∈ A) ∧ (F i x y ≠ 0 → x ∈ A ∧ y ∈ A) := by + have hinput : ∀ i, (∀ x y, F i x y ≠ 0 → x ∈ A ∧ y ∈ A) → + ∀ x y, (C + F i * C) x y ≠ 0 → x ∈ A ∧ y ∈ A := fun i hi x y h => by + by_contra hxy + apply h + have hCxy : C x y = 0 := by by_contra h'; exact hxy (hA x y h') + simp only [Matrix.add_apply, Matrix.mul_apply, hCxy, zero_add] + refine sum_eq_zero fun z _ => ?_ + by_cases hE : F i x z = 0 + · rw [hE, zero_mul] + by_cases hCz : C z y = 0 + · rw [hCz, mul_zero] + exact absurd ⟨(hi x z hE).1, (hA z y hCz).2⟩ hxy + intro i + induction i with + | zero => + have h0 : ∀ x y, F 0 x y ≠ 0 → x ∈ A ∧ y ∈ A := fun x y h => by simp [hF.zero] at h + exact fun x y => ⟨hinput 0 h0 x y, h0 x y⟩ + | succ i ih => + have hi : ∀ x y, F (i + 1) x y ≠ 0 → x ∈ A ∧ y ∈ A := fun x y h => + (ih x y).1 fun h' => h (le_antisymm (h' ▸ hF.le_input i x y) (hF.nonneg_succ i x y)) + exact fun x y => ⟨hinput _ hi x y, hi x y⟩ + +theorem mem (hA : ∀ x y, C x y ≠ 0 → x ∈ A ∧ y ∈ A) (i : ℕ) (x y : V) (h : F i x y ≠ 0) : + x ∈ A ∧ y ∈ A := + (hF.input_mem_and_mem hA i x y).2 h + +theorem input_mem (hA : ∀ x y, C x y ≠ 0 → x ∈ A ∧ y ∈ A) (i : ℕ) (x y : V) + (h : (C + F i * C) x y ≠ 0) : x ∈ A ∧ y ∈ A := + (hF.input_mem_and_mem hA i x y).1 h + +/-- The corrections of a strictly upper triangular `C` are strictly upper triangular +[OpenAI2026LogSpace, Lemma 4.2]. -/ +theorem isStrictUpperTriangular [Preorder V] (hC : C.IsStrictUpperTriangular) (i : ℕ) : + (F i).IsStrictUpperTriangular := by + induction i with + | zero => intro x y _; simp [hF.zero] + | succ i ih => + intro x y hxy + have h := hF.le_input i x y + rw [(hC.add (ih.mul hC)) hxy] at h + exact le_antisymm h (hF.nonneg_succ i x y) + +theorem input_isStrictUpperTriangular [Preorder V] (hC : C.IsStrictUpperTriangular) (i : ℕ) : + (C + F i * C).IsStrictUpperTriangular := + hC.add ((hF.isStrictUpperTriangular hC i).mul hC) + +end IsCorrectionSeq + +/-- The fixed-multiplier recursion `Matrix.cutoffCorrectionIter` is a correction sequence when +the cutoffs satisfy `0 ≤ φ y t ≤ max (t - θ f) 0` with `0 ≤ θ f`. -/ +theorem isCorrectionSeq_cutoffCorrectionIter {φ : V → ℝ → ℝ} {θ : ℝ} (hC0 : ∀ x y, 0 ≤ C x y) + (hφ0 : ∀ y t, 0 ≤ φ y t) (hφθ : ∀ y t, φ y t ≤ max (t - θ * f) 0) (hθf : 0 ≤ θ * f) : + IsCorrectionSeq C (cutoffCorrectionIter φ C) where + zero := rfl + nonneg_succ i x y := cutoffCorrectionIter_nonneg hφ0 (i + 1) x y + le_input i x y := by + rw [cutoffCorrectionIter_succ] + refine (hφθ y _).trans (max_le (by linarith) ?_) + exact add_nonneg (hC0 x y) (sum_nonneg fun z _ => + mul_nonneg (cutoffCorrectionIter_nonneg hφ0 i x z) (hC0 z y)) + +/-- **Comparison with a dominating sequence**: if the cutoffs `φ y` are monotone and the first +`k` steps of `F` dominate the cutoffs of their own inputs, then the first `k` iterates of the +fixed-multiplier recursion, and their inputs, are at most those of `F` +[OpenAI2026LogSpace, Lemma 4.2]. -/ +theorem cutoffCorrectionIter_le_of_isCorrectionSeq {φ : V → ℝ → ℝ} (hC0 : ∀ x y, 0 ≤ C x y) + (hφm : ∀ y, Monotone (φ y)) {k : ℕ} + (hφF : ∀ i < k, ∀ x y, φ y ((C + F i * C) x y) ≤ F (i + 1) x y) (hF : IsCorrectionSeq C F) : + ∀ i ≤ k, ∀ x y, cutoffCorrectionIter φ C i x y ≤ F i x y ∧ + (C + cutoffCorrectionIter φ C i * C) x y ≤ (C + F i * C) x y := by + have hinput : ∀ i, (∀ x y, cutoffCorrectionIter φ C i x y ≤ F i x y) → + ∀ x y, (C + cutoffCorrectionIter φ C i * C) x y ≤ (C + F i * C) x y := + fun i hi x y => add_le_add_right (sum_le_sum fun z _ => + mul_le_mul_of_nonneg_right (hi x z) (hC0 z y)) _ + intro i + induction i with + | zero => + have h0 : ∀ x y, cutoffCorrectionIter φ C 0 x y ≤ F 0 x y := fun x y => by + simp [cutoffCorrectionIter, hF.zero] + exact fun _ x y => ⟨h0 x y, hinput 0 h0 x y⟩ + | succ i ih => + intro hik + have hi : ∀ x y, cutoffCorrectionIter φ C (i + 1) x y ≤ F (i + 1) x y := fun x y => by + rw [cutoffCorrectionIter_succ] + exact (hφm y ((ih (by omega) x y).2)).trans (hφF i (by omega) x y) + exact fun x y => ⟨hi x y, hinput _ hi x y⟩ + +end Sequence + +/-! ### The pilot -/ + +section Pilot + +variable (c γ : ℝ → ℝ) (U : Matrix V V ℝ → V → ℝ) (C : Matrix V V ℝ) + +/-- The **pilot** as a pair of the current correction and the running maximum of the column +numbers. Step `i + 1` forms the input `G = C + Ê_i C`, updates the running maximum to +`M_(i+1) = M_i ⊔ U G`, and sets `Ê_(i+1) x y = c (G x y) * γ (M_(i+1) y)` +[OpenAI2026LogSpace, (4.10)–(4.13)]. -/ +noncomputable def pilot : ℕ → Matrix V V ℝ × (V → ℝ) + | 0 => (0, 0) + | i + 1 => + let G := C + (pilot i).1 * C + let M := (pilot i).2 ⊔ U G + (of fun x y => c (G x y) * γ (M y), M) + +/-- The `i`-th pilot correction `Ê_i`. -/ +noncomputable def pilotCorrection (i : ℕ) : Matrix V V ℝ := (pilot c γ U C i).1 + +/-- The input `G = C + Ê_i C` of pilot step `i + 1`; the preprint's `G_(i+1)`. -/ +@[expose] noncomputable def pilotInput (i : ℕ) : Matrix V V ℝ := C + pilotCorrection c γ U C i * C + +/-- The running maximum `M_i = max (0, U G_1, …, U G_i)` of the column numbers after `i` pilot +steps. The pilot multiplier of step `i` is `γ (M_i y)`. -/ +noncomputable def pilotMax (i : ℕ) : V → ℝ := (pilot c γ U C i).2 + +variable {c γ U C} + +@[simp] theorem pilotCorrection_zero : pilotCorrection c γ U C 0 = 0 := by rfl + +@[simp] theorem pilotMax_zero : pilotMax c γ U C 0 = 0 := by rfl + +theorem pilotMax_succ (i : ℕ) : + pilotMax c γ U C (i + 1) = pilotMax c γ U C i ⊔ U (pilotInput c γ U C i) := by rfl + +theorem pilotCorrection_succ_apply (i : ℕ) (x y : V) : + pilotCorrection c γ U C (i + 1) x y = + c (pilotInput c γ U C i x y) * γ (pilotMax c γ U C (i + 1) y) := by rfl + +/-- The running maximum grows. -/ +theorem pilotMax_mono {i j : ℕ} (hij : i ≤ j) (y : V) : + pilotMax c γ U C i y ≤ pilotMax c γ U C j y := by + induction hij with + | refl => exact le_rfl + | step _ ih => exact ih.trans (by rw [pilotMax_succ]; exact le_sup_left) + +/-- If the running maximum after `k` steps exceeds `a ≥ 0`, some column number `U G_(i+1)`, +`i < k`, does. -/ +theorem exists_lt_pilotInput_of_lt_pilotMax {a : ℝ} (ha : 0 ≤ a) {k : ℕ} {y : V} + (h : a < pilotMax c γ U C k y) : ∃ i < k, a < U (pilotInput c γ U C i) y := by + induction k with + | zero => exact absurd h (not_lt.mpr ha) + | succ k ih => + rw [pilotMax_succ, Pi.sup_apply, lt_sup_iff] at h + rcases h with h | h + · obtain ⟨i, hi, hU⟩ := ih h + exact ⟨i, by omega, hU⟩ + · exact ⟨k, by omega, h⟩ + +/-- **The pilot is a correction sequence** when the base cutoff satisfies `0 ≤ c t ≤ t` for +`t ≥ 0` and the multipliers lie in `[0, 1]` [OpenAI2026LogSpace, Lemma 4.2]. -/ +theorem isCorrectionSeq_pilotCorrection (hC0 : ∀ x y, 0 ≤ C x y) (hc0 : ∀ t, 0 ≤ c t) + (hct : ∀ t, 0 ≤ t → c t ≤ t) (hγ0 : ∀ t, 0 ≤ γ t) (hγ1 : ∀ t, γ t ≤ 1) : + IsCorrectionSeq C (pilotCorrection c γ U C) := by + have hnonneg : ∀ i x y, 0 ≤ pilotCorrection c γ U C (i + 1) x y := fun i x y => by + rw [pilotCorrection_succ_apply]; exact mul_nonneg (hc0 _) (hγ0 _) + have hall : ∀ i x y, 0 ≤ pilotCorrection c γ U C i x y := fun i x y => by + cases i with + | zero => simp + | succ i => exact hnonneg i x y + refine ⟨rfl, hnonneg, fun i x y => ?_⟩ + rw [pilotCorrection_succ_apply] + have hG : 0 ≤ pilotInput c γ U C i x y := + add_nonneg (hC0 x y) (sum_nonneg fun z _ => mul_nonneg (hall i x z) (hC0 z y)) + exact (mul_le_of_le_one_right (hc0 _) (hγ1 _)).trans (hct _ hG) + +/-- **The actual correction is at most the pilot.** Run the fixed-multiplier recursion with the +cutoffs `φ y t = c t * γ (M_k y)`, the final pilot multiplier. For a monotone nonnegative `c` and +a nonincreasing `γ`, its first `k` iterates and their inputs are at most the pilot corrections and +pilot inputs [OpenAI2026LogSpace, Lemma 4.2]. -/ +theorem cutoffCorrectionIter_le_pilotCorrection (hC0 : ∀ x y, 0 ≤ C x y) (hc0 : ∀ t, 0 ≤ c t) + (hct : ∀ t, 0 ≤ t → c t ≤ t) (hcm : Monotone c) (hγ0 : ∀ t, 0 ≤ γ t) (hγ1 : ∀ t, γ t ≤ 1) + (hγm : Antitone γ) {k i : ℕ} (hik : i ≤ k) (x y : V) : + cutoffCorrectionIter (fun y t => c t * γ (pilotMax c γ U C k y)) C i x y ≤ + pilotCorrection c γ U C i x y ∧ + (C + cutoffCorrectionIter (fun y t => c t * γ (pilotMax c γ U C k y)) C i * C) x y ≤ + pilotInput c γ U C i x y := by + refine cutoffCorrectionIter_le_of_isCorrectionSeq hC0 + (fun y => hcm.mul_const (hγ0 _)) (fun j hj x y => ?_) + (isCorrectionSeq_pilotCorrection hC0 hc0 hct hγ0 hγ1) i hik x y + rw [pilotCorrection_succ_apply] + exact mul_le_mul_of_nonneg_left (hγm (pilotMax_mono (by omega) y)) (hc0 _) + +end Pilot + +end Matrix diff --git a/Complexity/Foundations/Probability/ColumnDetector.lean b/Complexity/Foundations/Probability/ColumnDetector.lean new file mode 100644 index 000000000..5756f4530 --- /dev/null +++ b/Complexity/Foundations/Probability/ColumnDetector.lean @@ -0,0 +1,469 @@ +/- +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.Data.Finset.KthLargest +public import Mathlib.Algebra.BigOperators.Expect +public import Mathlib.Data.Finset.Density +public import Mathlib.LinearAlgebra.Matrix.Defs +public import Mathlib.Basic.Real.Basic +import Complexity.Foundations.Data.Finset.Markov +import Mathlib.Algebra.Order.BigOperators.Expect +import Mathlib.Algebra.BigOperators.Field +import Mathlib.Algebra.BigOperators.Ring.Finset +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# Column detectors from retention channels + +A *column detector* decides, with true expectations over random retained sets, whether a column +of a nonnegative matrix `G` has many substantial entries. It is the detector of the OpenAI preprint +(2026-09-23), Section 4.2, idea 3 in issue #474 [OpenAI2026LogSpace], which chooses the column +multipliers of the correction-and-copy hierarchy. + +**Channels.** Two *retention channels* `X : ι → V → Prop` and `Y : κ → V → Prop` select random +sets of vertices from independent uniform seeds `s : ι` and `t : κ`; independence is built in, +since the seed space is the product `ι × κ`. `Cslib.Probability.RetentionChannels` records the +properties that the detector uses, at rate `f` [OpenAI2026LogSpace, (4.8), (4.9)]: + +* every vertex is retained with the same probability `π`, with `c_π f ≤ π ≤ C_π f`; +* for `w ≠ y`, `Pr[Y(w) ∧ Y(y)] ≤ C_pair f Pr[Y(y)]`; +* a nonempty set `A` retains fewer than `|A| π / 2` members of `X` with probability at most + `C_var / (|A| π)`. + +**The detector.** For a draw `T` of the terminal channel `Y`, the *row gate* of row `x` is +`ρ (rank_K {G x w / f : w ∈ T})` (`Matrix.rowGate`); it is one unless `K` retained entries of the +row exceed `η f`. For a draw `S` of the start channel `X`, the *trial* at column `y` is +`rank_J {ϕ (G x y / f) * gate x : x ∈ S}` (`Matrix.detectorTrial`), where `rank_j` is the `j`-th +largest value padded with zeros (`Finset.kthLargest`). The *detector number* `U y` is the +expectation of the trial over both channels, conditioned on `Y(y)` (`Matrix.columnDetector`). + +**The detector lemma** [OpenAI2026LogSpace, Lemma 4.3]. Let `ϕ` be zero through `δ₀` and one from +`δ₁`, and `ρ` one through `η > 0`, both with values in `[0, 1]`. + +1. If the rows of `G ≥ 0` sum to at most `k`, the gate rank satisfies `K ≥ 160 (1 + C_pair k / η)`, + and `R` satisfies `c_π R ≥ max (4 J, 40 C_var)`, then a column with more than `R / f` entries + at least `δ₁ f` has `U y ≥ 19 / 20` (`Matrix.le_columnDetector`). +2. If `U y > 1 / 4`, the column has more than `J / (4 C_π f)` entries above `δ₀ f` + (`Matrix.lt_card_of_lt_columnDetector`). + +Each statement uses only the hypotheses it needs; for instance the second needs neither the +row-sum bound nor the row gates' threshold. + +The first statement uses no independence between the row gates of different rows; it combines +Markov's inequality for the gate failures with the lower tail of the start channel. + +## Main definitions + +* `Cslib.Probability.RetentionChannels`: the channel properties used by the detector. +* `Matrix.rowGate`, `Matrix.detectorTrial`, `Matrix.columnDetector`: the detector. + +## Main results + +* `Matrix.columnDetector_nonneg`, `Matrix.columnDetector_le_one`: detector numbers lie in `[0, 1]`. +* `Matrix.le_columnDetector`: columns with many large entries are detected. +* `Matrix.lt_card_of_lt_columnDetector`: detected columns have many substantial entries. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 4.2 and Lemma 4.3 (preprint, not peer reviewed) +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Cslib.Probability + +/-- **Retention channels** `X` and `Y` at rate `f`, with independent uniform seeds `s : ι` and +`t : κ`: every vertex is retained by either channel with the same probability `π`, +`c_π f ≤ π ≤ C_π f`; two distinct vertices `w ≠ y` are both retained by `Y` with probability at +most `C_pair f` times that of `y`; and a nonempty set `A` retains fewer than `|A| π / 2` members +of `X` with probability at most `C_var / (|A| π)`. These are the properties +[OpenAI2026LogSpace, (4.8), (4.9)] that the detectors use. -/ +structure RetentionChannels {V ι κ : Type*} [Fintype ι] [Fintype κ] (X : ι → V → Prop) + (Y : κ → V → Prop) [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Y t v)] + (f π cπ Cπ Cpair Cvar : ℝ) : Prop where + dens_X : ∀ v, (dens {s | X s v} : ℝ) = π + dens_Y : ∀ v, (dens {t | Y t v} : ℝ) = π + lower : cπ * f ≤ π + upper : π ≤ Cπ * f + pair : ∀ w y, w ≠ y → (dens {t | Y t w ∧ Y t y} : ℝ) ≤ Cpair * f * dens {t | Y t y} + tail : ∀ A : Finset V, A.Nonempty → + (dens {s | 2 * (#{x ∈ A | X s x} : ℝ) < #A * π} : ℝ) ≤ Cvar / (#A * π) + +end Cslib.Probability + +namespace Matrix + +open Cslib.Probability + +variable {V ι κ : Type*} [Fintype V] [Fintype ι] [Fintype κ] + +section Definitions + +/-- The **row gate** of row `x` for a draw `T` of the terminal channel: +`ρ (rank_K {G x w / f : w ∈ T})` [OpenAI2026LogSpace, (4.11)]. -/ +@[expose] noncomputable def rowGate (ρ : ℝ → ℝ) (K : ℕ) (f : ℝ) (G : Matrix V V ℝ) + (T : Finset V) (x : V) : ℝ := + ρ (kthLargest K T fun w => G x w / f) + +/-- A **detector trial** at column `y`, for draws `S` of the start channel and `T` of the terminal +channel: `rank_J {ϕ (G x y / f) * rowGate x : x ∈ S}` [OpenAI2026LogSpace, (4.12)]. -/ +@[expose] noncomputable def detectorTrial (ϕ ρ : ℝ → ℝ) (J K : ℕ) (f : ℝ) (G : Matrix V V ℝ) + (S T : Finset V) (y : V) : ℝ := + kthLargest J S fun x => ϕ (G x y / f) * rowGate ρ K f G T x + +/-- The **detector number** of column `y`: the expectation of the detector trial over the seeds of +both channels, conditioned on `Y(y)` [OpenAI2026LogSpace, (4.12)]. -/ +@[expose] noncomputable def columnDetector (X : ι → V → Prop) (Y : κ → V → Prop) + [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Y t v)] (ϕ ρ : ℝ → ℝ) (J K : ℕ) (f : ℝ) + (G : Matrix V V ℝ) (y : V) : ℝ := + 𝔼 s, 𝔼 t ∈ {t | Y t y}, detectorTrial ϕ ρ J K f G {x | X s x} {w | Y t w} y + +end Definitions + +variable {X : ι → V → Prop} {Y : κ → V → Prop} [∀ s v, Decidable (X s v)] + [∀ t v, Decidable (Y t v)] {ϕ ρ : ℝ → ℝ} {J K : ℕ} {f : ℝ} {G : Matrix V V ℝ} {y : V} + +private theorem dens_cast {α : Type*} [Fintype α] (s : Finset α) : + ((dens s : ℚ≥0) : ℝ) = #s / Fintype.card α := by + rw [dens_eq_card_div_card]; push_cast; rfl + +private theorem columnDetector_eq_sum : + columnDetector X Y ϕ ρ J K f G y = + (∑ s, ∑ t ∈ {t | Y t y}, detectorTrial ϕ ρ J K f G {x | X s x} {w | Y t w} y) / + (Fintype.card ι * #({t | Y t y} : Finset κ)) := by + rw [columnDetector, Fintype.expect_eq_sum_div_card] + simp only [expect_eq_sum_div_card] + rw [← Finset.sum_div, div_div, mul_comm (#({t | Y t y} : Finset κ) : ℝ)] + +omit [Fintype V] in +theorem detectorTrial_nonneg {S T : Finset V} : 0 ≤ detectorTrial ϕ ρ J K f G S T y := + kthLargest_nonneg + +omit [Fintype V] in +theorem detectorTrial_le_one (hϕ0 : ∀ t, 0 ≤ ϕ t) (hϕ1 : ∀ t, ϕ t ≤ 1) + (hρ1 : ∀ t, ρ t ≤ 1) {S T : Finset V} : detectorTrial ϕ ρ J K f G S T y ≤ 1 := + kthLargest_le zero_le_one fun _ _ => + (mul_le_mul_of_nonneg_left (hρ1 _) (hϕ0 _)).trans (by rw [mul_one]; exact hϕ1 _) + +theorem columnDetector_nonneg : 0 ≤ columnDetector X Y ϕ ρ J K f G y := by + rw [columnDetector] + exact expect_nonneg fun _ _ => expect_nonneg fun _ _ => detectorTrial_nonneg + +theorem columnDetector_le_one (hϕ0 : ∀ t, 0 ≤ ϕ t) (hϕ1 : ∀ t, ϕ t ≤ 1) + (hρ1 : ∀ t, ρ t ≤ 1) : columnDetector X Y ϕ ρ J K f G y ≤ 1 := by + rw [columnDetector_eq_sum] + refine div_le_one_of_le₀ ?_ (by positivity) + calc ∑ s, ∑ t ∈ {t | Y t y}, detectorTrial ϕ ρ J K f G {x | X s x} {w | Y t w} y + ≤ ∑ _s : ι, ∑ _t ∈ ({t | Y t y} : Finset κ), (1 : ℝ) := + sum_le_sum fun _ _ => sum_le_sum fun _ _ => detectorTrial_le_one hϕ0 hϕ1 hρ1 + _ = Fintype.card ι * #({t | Y t y} : Finset κ) := by + simp only [sum_const, card_univ, nsmul_eq_mul, mul_one] + +variable {π cπ Cπ Cpair Cvar : ℝ} + +omit [Fintype V] in +private theorem card_X (hch : RetentionChannels X Y f π cπ Cπ Cpair Cvar) (v : V) : + (#({s | X s v} : Finset ι) : ℝ) = π * Fintype.card ι := by + have h := hch.dens_X v + rw [dens_cast] at h + rcases (Fintype.card ι).eq_zero_or_pos with h0 | h0 + · have : (#({s | X s v} : Finset ι)) = 0 := Nat.eq_zero_of_le_zero + (h0 ▸ card_le_univ _) + simp [this, h0] + · rw [← h]; field_simp + +/-- **Detected columns have many substantial entries** [OpenAI2026LogSpace, Lemma 4.3 (2)]: if +`ϕ` vanishes through `δ₀` and the detector number of column `y` exceeds `1 / 4`, more than +`J / (4 C_π f)` entries of the column exceed `δ₀ f`. -/ +theorem lt_card_of_lt_columnDetector (hch : RetentionChannels X Y f π cπ Cπ Cpair Cvar) + (hf : 0 < f) (hϕ0 : ∀ t, 0 ≤ ϕ t) (hϕ1 : ∀ t, ϕ t ≤ 1) {δ₀ : ℝ} + (hϕδ : ∀ t, t ≤ δ₀ → ϕ t = 0) (hρ1 : ∀ t, ρ t ≤ 1) (hJ : 0 < J) + (hU : 1 / 4 < columnDetector X Y ϕ ρ J K f G y) : + J / (4 * Cπ * f) < #({x | δ₀ * f < G x y} : Finset V) := by + set A0 : Finset V := {x | δ₀ * f < G x y} + set T : Finset κ := {t | Y t y} + have hJr : (0 : ℝ) < J := by exact_mod_cast hJ + -- a trial is at most the number of retained substantial entries over `J` + have htrial : ∀ s t, detectorTrial ϕ ρ J K f G {x | X s x} {w | Y t w} y ≤ + (#{x ∈ A0 | X s x} : ℝ) / J := by + intro s t + rcases le_or_gt (detectorTrial ϕ ρ J K f G {x | X s x} {w | Y t w} y) 0 with h | h + · exact h.trans (by positivity) + have hcard := (lt_kthLargest_iff hJ le_rfl).mp h + have hsub : ({x ∈ ({x | X s x} : Finset V) | + 0 < ϕ (G x y / f) * rowGate ρ K f G {w | Y t w} x}) ⊆ {x ∈ A0 | X s x} := by + intro x hx + simp only [mem_filter, mem_univ, true_and, A0] at hx ⊢ + refine ⟨?_, hx.1⟩ + by_contra hle + have : G x y / f ≤ δ₀ := by rw [div_le_iff₀ hf]; linarith + rw [hϕδ _ this, zero_mul] at hx + exact lt_irrefl _ hx.2 + have hJle : (J : ℝ) ≤ #{x ∈ A0 | X s x} := by exact_mod_cast hcard.trans (card_le_card hsub) + rw [le_div_iff₀ hJr] + calc detectorTrial ϕ ρ J K f G {x | X s x} {w | Y t w} y * J ≤ 1 * J := + mul_le_mul_of_nonneg_right (detectorTrial_le_one hϕ0 hϕ1 hρ1) hJr.le + _ ≤ _ := by rw [one_mul]; exact hJle + -- summing over the start seeds counts each substantial entry with its retention probability + have hsumX : ∑ s, (#{x ∈ A0 | X s x} : ℝ) = #A0 * (π * Fintype.card ι) := by + simp only [natCast_card_filter] + rw [sum_comm] + simp only [← natCast_card_filter, card_X hch, sum_const, nsmul_eq_mul] + have hT : 0 < #T := by + rw [card_pos] + by_contra hT + rw [not_nonempty_iff_eq_empty] at hT + have : columnDetector X Y ϕ ρ J K f G y = 0 := by + rw [columnDetector_eq_sum]; simp [T, hT] + linarith + have hι : 0 < Fintype.card ι := by + rw [Fintype.card_pos_iff] + by_contra hι + rw [not_nonempty_iff] at hι + have : columnDetector X Y ϕ ρ J K f G y = 0 := by + rw [columnDetector_eq_sum]; simp + linarith + have hTr : (0 : ℝ) < #T := by exact_mod_cast hT + have hιr : (0 : ℝ) < Fintype.card ι := by exact_mod_cast hι + have hUle : columnDetector X Y ϕ ρ J K f G y ≤ #A0 * π / J := by + rw [columnDetector_eq_sum, div_le_div_iff₀ (by positivity) hJr] + calc (∑ s, ∑ t ∈ T, detectorTrial ϕ ρ J K f G {x | X s x} {w | Y t w} y) * J + ≤ (∑ s, ∑ _t ∈ T, (#{x ∈ A0 | X s x} : ℝ) / J) * J := + mul_le_mul_of_nonneg_right + (sum_le_sum fun s _ => sum_le_sum fun t _ => htrial s t) hJr.le + _ = #T * ∑ s, (#{x ∈ A0 | X s x} : ℝ) := by + simp only [sum_const, nsmul_eq_mul, Finset.mul_sum, Finset.sum_mul] + exact sum_congr rfl fun s _ => by field_simp + _ = #A0 * π * (Fintype.card ι * #T) := by rw [hsumX]; ring + have hπ : 0 < π := by + by_contra hπ + have : #A0 * π / J ≤ 0 := + div_nonpos_of_nonpos_of_nonneg (mul_nonpos_of_nonneg_of_nonpos (by positivity) + (not_lt.mp hπ)) hJr.le + linarith + have hCπ : 0 < Cπ * f := hπ.trans_le hch.upper + have h1 : J / 4 < #A0 * π := by + have := hU.trans_le hUle + rw [lt_div_iff₀ hJr] at this + linarith + rw [div_lt_iff₀ (by nlinarith)] + calc (J : ℝ) = J / 4 * 4 := by ring + _ < #A0 * π * 4 := by linarith + _ ≤ #A0 * (Cπ * f) * 4 := by gcongr; exact hch.upper + _ = #A0 * (4 * Cπ * f) := by ring + +omit [Fintype V] in +private theorem card_pos_of_dens {α : Type*} [Fintype α] {s : Finset α} {π : ℝ} (hπ : 0 < π) + (h : (dens s : ℝ) = π) : 0 < Fintype.card α ∧ 0 < #s := by + rw [dens_cast] at h + rcases (Fintype.card α).eq_zero_or_pos with h0 | h0 + · simp [h0] at h; linarith + refine ⟨h0, Nat.pos_of_ne_zero fun hs => ?_⟩ + simp [hs] at h; linarith + +/-- **Columns with many large entries are detected** [OpenAI2026LogSpace, Lemma 4.3 (1)]. Let the +rows of `G ≥ 0` sum to at most `k`, let `ϕ` be one from `δ₁`, let `ρ ≤ 1` be one through `η > 0`, +let the gate rank satisfy `K ≥ 160 (1 + C_pair k / η)`, and let `c_π R ≥ 4 J` and +`c_π R ≥ 40 C_var`. If more than `R / f` entries of column `y` are at least `δ₁ f`, its detector +number is at least `19 / 20`. -/ +theorem le_columnDetector (hch : RetentionChannels X Y f π cπ Cπ Cpair Cvar) (hf : 0 < f) + (hcπ : 0 < cπ) (hCpair : 0 ≤ Cpair) {δ₁ : ℝ} (hϕδ : ∀ t, δ₁ ≤ t → ϕ t = 1) + (hρ1 : ∀ t, ρ t ≤ 1) {η : ℝ} (hη : 0 < η) + (hρη : ∀ t, t ≤ η → ρ t = 1) (hG0 : ∀ x w, 0 ≤ G x w) {k : ℝ} + (hGk : ∀ x, ∑ w, G x w ≤ k) (hK : 160 * (1 + Cpair * k / η) ≤ K) (hJ : 0 < J) {R : ℝ} + (hRJ : 4 * J ≤ cπ * R) (hRvar : 40 * Cvar ≤ cπ * R) + (hy : R / f < #({x | δ₁ * f ≤ G x y} : Finset V)) : + 19 / 20 ≤ columnDetector X Y ϕ ρ J K f G y := by + classical + set A : Finset V := {x | δ₁ * f ≤ G x y} + set T : Finset κ := {t | Y t y} + set D : ℝ := 1 + Cpair * k / η + set gate : κ → V → ℝ := fun t x => rowGate ρ K f G {w | Y t w} x + have hπ : 0 < π := (mul_pos hcπ hf).trans_le hch.lower + have hJr : (0 : ℝ) < J := by exact_mod_cast hJ + have hnπ : cπ * R < #A * π := by + have h1 : R < #A * f := by rwa [div_lt_iff₀ hf] at hy + calc cπ * R < cπ * (#A * f) := mul_lt_mul_of_pos_left h1 hcπ + _ = #A * (cπ * f) := by ring + _ ≤ #A * π := mul_le_mul_of_nonneg_left hch.lower (by positivity) + have hnπ0 : 0 < (#A : ℝ) * π := by linarith + have hA : A.Nonempty := by + rw [← card_pos, ← Nat.cast_pos (α := ℝ)] + exact pos_of_mul_pos_left hnπ0 hπ.le + obtain ⟨hι, -⟩ := card_pos_of_dens hπ (hch.dens_X y) + obtain ⟨hκ, hT⟩ := card_pos_of_dens hπ (hch.dens_Y y) + have hκr : (0 : ℝ) < Fintype.card κ := by exact_mod_cast hκ + have hιr : (0 : ℝ) < Fintype.card ι := by exact_mod_cast hι + have hTr : (0 : ℝ) < #T := by exact_mod_cast hT + have hD : 1 ≤ D := by + have : 0 ≤ Cpair * k / η := by + have hk : 0 ≤ k := (sum_nonneg fun w _ => hG0 y w).trans (hGk y) + positivity + linarith + have hKpos : 0 < K := by + have : (0 : ℝ) < K := by linarith + exact_mod_cast this + -- Markov's inequality for the row gates: each row fails its gate on few terminal draws + have hgate : ∀ x, (#{t ∈ T | gate t x < 1} : ℝ) * K ≤ #T * D := by + intro x + set W : Finset V := {w | η * f < G x w} + have hW : (#W : ℝ) * (η * f) ≤ k := + (card_filter_mul_le_sum univ _ (fun w => G x w) (fun w _ => hG0 x w) + fun _ _ hw => hw.le).trans (hGk x) + have hbadK : ∀ t ∈ T, gate t x < 1 → (K : ℝ) ≤ #{w ∈ W | Y t w} := by + intro t _ ht + have hlt : η < kthLargest K {w | Y t w} (fun w => G x w / f) := by + by_contra hle + have h1 := hρη _ (not_lt.mp hle) + simp only [gate, rowGate] at ht + rw [h1] at ht + exact lt_irrefl _ ht + have hcard := (lt_kthLargest_iff hKpos hη.le).mp hlt + have hsub : ({w ∈ ({w | Y t w} : Finset V) | η < G x w / f} : Finset V) ⊆ + {w ∈ W | Y t w} := fun w hw => by + simp only [mem_filter, mem_univ, true_and, W] at hw ⊢ + exact ⟨by rw [lt_div_iff₀ hf] at hw; exact hw.2, hw.1⟩ + exact_mod_cast hcard.trans (card_le_card hsub) + have hMarkov : (#{t ∈ T | gate t x < 1} : ℝ) * K ≤ ∑ t ∈ T, (#{w ∈ W | Y t w} : ℝ) := + card_filter_mul_le_sum T _ _ (fun _ _ => by positivity) hbadK + have hswap : ∑ t ∈ T, (#{w ∈ W | Y t w} : ℝ) = ∑ w ∈ W, (#{t ∈ T | Y t w} : ℝ) := by + simp only [natCast_card_filter] + exact sum_comm + have hterm : ∀ w ∈ W, (#{t ∈ T | Y t w} : ℝ) ≤ (if y = w then (#T : ℝ) else 0) + + Cpair * f * #T := by + intro w _ + have hle : (#{t ∈ T | Y t w} : ℝ) ≤ #T := by exact_mod_cast card_filter_le _ _ + by_cases hwy : y = w + · simp only [hwy, ↓reduceIte] + have : 0 ≤ Cpair * f * #T := by positivity + linarith + · simp only [hwy, ↓reduceIte, zero_add] + have hp := hch.pair w y (Ne.symm hwy) + rw [dens_cast, dens_cast, ← mul_div_assoc, div_le_div_iff_of_pos_right hκr] at hp + have hset : ({t ∈ T | Y t w} : Finset κ) = ({t | Y t w ∧ Y t y} : Finset κ) := by + ext t; simp only [T, mem_filter, mem_univ, true_and]; tauto + rw [hset] + exact hp + have hWf : (#W : ℝ) * f ≤ k / η := by + rw [le_div_iff₀ hη]; linarith + calc (#{t ∈ T | gate t x < 1} : ℝ) * K + ≤ ∑ w ∈ W, ((if y = w then (#T : ℝ) else 0) + Cpair * f * #T) := + hMarkov.trans (hswap ▸ sum_le_sum hterm) + _ = (if y ∈ W then (#T : ℝ) else 0) + #W * (Cpair * f * #T) := by + rw [sum_add_distrib, sum_ite_eq, sum_const, nsmul_eq_mul] + _ ≤ #T + #T * Cpair * (#W * f) := by + have : (if y ∈ W then (#T : ℝ) else 0) ≤ #T := by split_ifs <;> [exact le_rfl; positivity] + nlinarith + _ ≤ #T + #T * Cpair * (k / η) := by gcongr + _ = #T * D := by simp only [D]; ring + -- the expected number of retained large rows that fail their gate + set N : ι → ℝ := fun s => #{x ∈ A | X s x} + set L : ι → κ → ℝ := fun s t => #{x ∈ A | X s x ∧ gate t x < 1} + have hL0 : ∀ s t, 0 ≤ L s t := fun _ _ => by positivity + have hsumL : ∑ s, ∑ t ∈ T, L s t ≤ #A * π * Fintype.card ι * (#T * D / K) := by + have heq : ∑ s, ∑ t ∈ T, L s t = + ∑ x ∈ A, (#{s | X s x} : ℝ) * #{t ∈ T | gate t x < 1} := by + have h1 : ∀ s t, L s t = ∑ x ∈ A, + (if X s x then (1 : ℝ) else 0) * (if gate t x < 1 then 1 else 0) := fun s t => by + simp only [L, natCast_card_filter, ite_zero_mul_ite_zero, mul_one] + simp only [h1, natCast_card_filter, sum_mul_sum] + exact (sum_congr rfl fun s _ => sum_comm).trans sum_comm + rw [heq] + have hKr : (0 : ℝ) < K := by exact_mod_cast hKpos + calc ∑ x ∈ A, (#{s | X s x} : ℝ) * #{t ∈ T | gate t x < 1} + ≤ ∑ _x ∈ A, π * Fintype.card ι * (#T * D / K) := by + refine sum_le_sum fun x _ => ?_ + rw [card_X hch] + exact mul_le_mul_of_nonneg_left (by rw [le_div_iff₀ hKr]; exact hgate x) + (by positivity) + _ = #A * π * Fintype.card ι * (#T * D / K) := by + rw [sum_const, nsmul_eq_mul]; ring + -- outside two bad events, at least `J` retained large rows pass their gates + have hgood : ∀ s t, ¬ 2 * N s < #A * π → ¬ #A * π < 4 * L s t → + 1 ≤ detectorTrial ϕ ρ J K f G {x | X s x} {w | Y t w} y := by + intro s t h1 h2 + push Not at h1 h2 + have hsplit : N s = L s t + #{x ∈ A | X s x ∧ ¬ gate t x < 1} := by + simp only [N, L, natCast_card_filter, ← sum_add_distrib] + refine sum_congr rfl fun x _ => ?_ + by_cases hX : X s x <;> by_cases hg : gate t x < 1 <;> simp [hX, hg] + have hJle : (J : ℝ) ≤ #{x ∈ A | X s x ∧ ¬ gate t x < 1} := by + have : 4 * (J : ℝ) < #A * π := hRJ.trans_lt hnπ + linarith + refine (le_kthLargest_iff hJ one_pos).mpr ?_ + refine Nat.cast_le.mp (hJle.trans ?_) + refine Nat.cast_le.mpr (card_le_card fun x hx => ?_) + simp only [mem_filter, mem_univ, true_and, A] at hx ⊢ + refine ⟨hx.2.1, ?_⟩ + have hϕx : ϕ (G x y / f) = 1 := hϕδ _ (by rw [le_div_iff₀ hf]; exact hx.1) + have hgx : gate t x = 1 := le_antisymm (hρ1 _) (not_lt.mp hx.2.2) + simp only [gate] at hgx + rw [hϕx, hgx, one_mul] + -- sum the pointwise bound `trial ≥ 1 - [bad start draw] - [many gate failures]` + set b1 : ι → ℝ := fun s => if 2 * N s < #A * π then 1 else 0 + set b2 : ι → κ → ℝ := fun s t => if #A * π < 4 * L s t then 1 else 0 + have hpoint : ∀ s t, 1 - b1 s - b2 s t ≤ + detectorTrial ϕ ρ J K f G {x | X s x} {w | Y t w} y := by + intro s t + have h0 : 0 ≤ detectorTrial ϕ ρ J K f G {x | X s x} {w | Y t w} y := detectorTrial_nonneg + by_cases h1 : 2 * N s < #A * π + · have : 0 ≤ b2 s t := by simp only [b2]; split_ifs <;> norm_num + simp only [b1, h1, ↓reduceIte] + linarith + by_cases h2 : #A * π < 4 * L s t + · simp only [b1, b2, h1, h2, ↓reduceIte] + linarith + · simp only [b1, b2, h1, h2, ↓reduceIte, sub_zero] + exact hgood s t h1 h2 + have hb1 : ∑ s, b1 s ≤ Cvar / (#A * π) * Fintype.card ι := by + have ht := hch.tail A hA + rw [dens_cast, div_le_iff₀ hιr] at ht + simp only [b1, N] + rw [sum_boole] + exact ht + have hb2 : ∑ s, ∑ t ∈ T, b2 s t ≤ 4 / (#A * π) * ∑ s, ∑ t ∈ T, L s t := by + rw [mul_sum] + refine sum_le_sum fun s _ => ?_ + rw [mul_sum] + refine sum_le_sum fun t _ => ?_ + simp only [b2] + split_ifs with h + · rw [div_mul_eq_mul_div, le_div_iff₀ hnπ0]; linarith + · have := hL0 s t; positivity + have hvar : Cvar / (#A * π) ≤ 1 / 40 := by + rw [div_le_div_iff₀ hnπ0 (by norm_num)]; linarith + have hgatebound : 4 / (#A * π) * (#A * π * Fintype.card ι * (#T * D / K)) ≤ + Fintype.card ι * #T / 40 := by + have hKr : (0 : ℝ) < K := by exact_mod_cast hKpos + have : 4 / (#A * π) * (#A * π * Fintype.card ι * (#T * D / K)) = + 4 * D / K * (Fintype.card ι * #T) := by + field_simp + rw [this, div_eq_mul_one_div (Fintype.card ι * (#T : ℝ)) 40, mul_comm _ (1 / 40 : ℝ)] + refine mul_le_mul_of_nonneg_right ?_ (by positivity) + rw [div_le_iff₀ hKr]; linarith + rw [columnDetector_eq_sum, le_div_iff₀ (by positivity)] + have h4 : 0 ≤ 4 / (#A * π) := by positivity + calc 19 / 20 * (Fintype.card ι * #T : ℝ) + ≤ Fintype.card ι * #T - #T * (Cvar / (#A * π) * Fintype.card ι) - + 4 / (#A * π) * (#A * π * Fintype.card ι * (#T * D / K)) := by + nlinarith [mul_le_mul_of_nonneg_left hvar (by positivity : (0 : ℝ) ≤ #T * Fintype.card ι)] + _ ≤ Fintype.card ι * #T - #T * ∑ s, b1 s - ∑ s, ∑ t ∈ T, b2 s t := by + nlinarith [mul_le_mul_of_nonneg_left hb1 hTr.le, mul_le_mul_of_nonneg_left hsumL h4] + _ = ∑ s, ∑ t ∈ T, (1 - b1 s - b2 s t) := by + simp only [sum_sub_distrib, sum_const, nsmul_eq_mul, card_univ, mul_one] + rw [← mul_sum] + _ ≤ _ := sum_le_sum fun s _ => sum_le_sum fun t _ => hpoint s t + +end Matrix diff --git a/Complexity/Foundations/Probability/DetectedStage.lean b/Complexity/Foundations/Probability/DetectedStage.lean new file mode 100644 index 000000000..ab425a36c --- /dev/null +++ b/Complexity/Foundations/Probability/DetectedStage.lean @@ -0,0 +1,295 @@ +/- +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.LinearAlgebra.Matrix.CopyStage +public import Complexity.Foundations.LinearAlgebra.Matrix.PilotCorrection +public import Complexity.Foundations.Probability.ColumnDetector +import Mathlib.Algebra.BigOperators.Fin +import Mathlib.Algebra.Order.Floor.Semiring + +/-! +# One stage of the hierarchy with detector-chosen multipliers + +This file closes the detector interface of `Matrix.copyStage_rates` +[OpenAI2026LogSpace, Section 4.2, Proposition 4.5]. One stage of the correction-and-copy hierarchy +runs the pilot (`Matrix.pilotMax`) with the column detector +`Matrix.columnDetector X Y ϕ ρ J K f` as its column number, for retention channels `X`, `Y` +satisfying `Cslib.Probability.RetentionChannels`. Let `M = M_k` be the final running maximum of the +detector numbers. Then + +* the column multiplier of the actual correction is `γ (M y)`, so the cutoffs are + `φ y t = c t * γ (M y)` for the base cutoff `c t = f Q (t / f)`; +* the copy weights are `r 0 x = 1` and `r j x = κ (M x)` for `j ≠ 0` + (`Matrix.detectorWeight`) [OpenAI2026LogSpace, (4.22)]; +* the overloaded vertices are `O = {x | 1 / 4 < M x}` (`Matrix.overloaded`). + +Since `γ` is one through `1 / 2` and `κ` is zero through `1 / 4` and one from `1 / 2`, every +column is either fully corrected or overloaded with all copies active, and only overloaded vertices +have active extra copies. The detector lemma (`Matrix.lt_card_of_lt_columnDetector`) gives each +overloaded column more than `J / (4 C_π f)` entries above `δ₀ f` in some pilot input, and +incidence counting over the pilot inputs, whose rows sum to at most `1, …, k`, gives +`m |O| ≤ |A|` once `2 C_π m k (k + 1) ≤ δ₀ J` [OpenAI2026LogSpace, (4.24)]. So the stage has the +density, intertwining and active-count conclusions of `Matrix.copyStage_rates` +(`Matrix.detectedStage_rates`), with only the channel properties and deterministic constant +conditions as hypotheses. + +The pilot also bounds the column counts of the corrected columns +[OpenAI2026LogSpace, Lemma 4.3 (3)]: if the pilot multiplier of a column is positive, its pilot +inputs have at most `R / f` entries at least `δ₁ f` (`Matrix.card_le_of_pilot_pos`), and so do +the inputs of the actual correction when the final multiplier is positive +(`Matrix.card_le_of_multiplier_pos`). + +## Main definitions + +* `Matrix.detectorWeight`: the copy weights `r` from the running maximum. +* `Matrix.overloaded`: the overloaded vertices. + +## Main results + +* `Matrix.card_overloaded_le`: the incidence bound `m |O| ≤ |A|`. +* `Matrix.detectedStage_rates`: one stage with detector-chosen multipliers and copies. +* `Matrix.card_le_of_pilot_pos`, `Matrix.card_le_of_multiplier_pos`: column counts of corrected + columns. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 4.2, Lemma 4.3 and Proposition 4.5 (preprint, not peer reviewed) +-/ + +public section + +open Finset Cslib.Probability + +namespace Matrix + +section Definitions + +variable {V : Type*} + +/-- The **copy weights** from the running maximum `M` of the detector numbers: the primary copy +has weight one, every other copy of `x` weight `κ (M x)` [OpenAI2026LogSpace, (4.22)]. -/ +@[expose] noncomputable def detectorWeight {m : ℕ} (κ : ℝ → ℝ) (M : V → ℝ) (j : Fin (m + 1)) + (x : V) : ℝ := + if j = 0 then 1 else κ (M x) + +/-- The **overloaded** vertices: those whose running maximum of detector numbers exceeds `1 / 4` +[OpenAI2026LogSpace, Proposition 4.5]. -/ +@[expose] noncomputable def overloaded [Fintype V] (M : V → ℝ) : Finset V := + {x | 1 / 4 < M x} + +end Definitions + +variable {V ι ι' : Type*} [Fintype V] [Fintype ι] [Fintype ι'] {X : ι → V → Prop} + {Y : ι' → V → Prop} [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Y t v)] {ϕ ρ : ℝ → ℝ} + {J K : ℕ} {f π cπ Cπ Cpair Cvar : ℝ} {c γ : ℝ → ℝ} {C : Matrix V V ℝ} + +private theorem sum_fin_succ_cast (k : ℕ) : ∑ i : Fin k, ((i : ℝ) + 1) = k * (k + 1) / 2 := by + rw [Fin.sum_univ_eq_sum_range (fun i => (i : ℝ) + 1)] + induction k with + | zero => simp + | succ k ih => rw [sum_range_succ, ih]; push_cast; ring + +/-- **Few overloaded vertices** [OpenAI2026LogSpace, Proposition 4.5]: after `k` pilot steps with +the column detector, if `A` covers the support of `C` and `2 C_π m k (k + 1) ≤ δ₀ J`, then +`m |O| ≤ |A|`. Each overloaded column has more than `J / (4 C_π f)` entries above `δ₀ f` in some +pilot input, and the pilot inputs have row sums at most `1, …, k`. -/ +theorem card_overloaded_le (hch : RetentionChannels X Y f π cπ Cπ Cpair Cvar) (hf : 0 < f) + (hCπ : 0 < Cπ) (hϕ0 : ∀ t, 0 ≤ ϕ t) (hϕ1 : ∀ t, ϕ t ≤ 1) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) + (hϕδ : ∀ t, t ≤ δ₀ → ϕ t = 0) (hρ1 : ∀ t, ρ t ≤ 1) (hJ : 0 < J) (hC0 : ∀ x y, 0 ≤ C x y) + (hC1 : C *ᵥ 1 ≤ 1) {A : Finset V} (hA : ∀ x y, C x y ≠ 0 → x ∈ A ∧ y ∈ A) + (hc0 : ∀ t, 0 ≤ c t) (hct : ∀ t, 0 ≤ t → c t ≤ t) (hγ0 : ∀ t, 0 ≤ γ t) + (hγ1 : ∀ t, γ t ≤ 1) {k m : ℕ} (hJm : 2 * Cπ * m * k * (k + 1) ≤ δ₀ * J) : + m * #(overloaded (pilotMax c γ (columnDetector X Y ϕ ρ J K f) C k)) ≤ #A := by + set U := columnDetector X Y ϕ ρ J K f + set O := overloaded (pilotMax c γ U C k) + have hseq := isCorrectionSeq_pilotCorrection (U := U) hC0 hc0 hct hγ0 hγ1 + -- every overloaded column has many substantial entries in some pilot input + have hinc : ∀ y ∈ O, ∃ i : Fin k, J / (4 * Cπ * f) < + #({x | δ₀ * f < pilotInput c γ U C i x y} : Finset V) := by + intro y hy + simp only [O, overloaded, mem_filter, mem_univ, true_and] at hy + obtain ⟨i, hi, hU⟩ := exists_lt_pilotInput_of_lt_pilotMax (by norm_num) hy + exact ⟨⟨i, hi⟩, lt_card_of_lt_columnDetector hch hf hϕ0 hϕ1 hϕδ hρ1 hJ hU⟩ + rcases O.eq_empty_or_nonempty with hO | hO + · rw [hO, card_empty, mul_zero]; exact Nat.zero_le _ + have hk : 0 < k := by + obtain ⟨y, hy⟩ := hO + obtain ⟨⟨i, hi⟩, -⟩ := hinc y hy + omega + set N := ⌊J / (4 * Cπ * f)⌋₊ + 1 + have hN : ∀ y ∈ O, ∃ i : Fin k, N ≤ #({x | δ₀ * f < pilotInput c γ U C i x y} : Finset V) := by + intro y hy + obtain ⟨i, hi⟩ := hinc y hy + exact ⟨i, Nat.succ_le_of_lt ((Nat.floor_lt (by positivity)).mpr hi)⟩ + have hcount := card_mul_le_of_incidences (fun i : Fin k => pilotInput c γ U C i) + (fun i x y => hseq.input_nonneg hC0 i x y) (fun i => (i : ℝ) + 1) + (fun i x => (hseq.sum_input_le hC1 i x).1) A + (fun i x y h => (hseq.input_mem hA i x y h).1) (mul_pos hδ₀ hf) O hN + rw [sum_fin_succ_cast] at hcount + have hNJ : J / (4 * Cπ * f) < N := by + simp only [N]; push_cast; exact Nat.lt_floor_add_one _ + have hJN : (J : ℝ) * δ₀ < 4 * Cπ * N * δ₀ * f := by + rw [div_lt_iff₀ (by positivity)] at hNJ + nlinarith + have hkpos : (0 : ℝ) < k * (k + 1) := by + have : (0 : ℝ) < k := by exact_mod_cast hk + positivity + -- `#O N δ₀ f ≤ #A k (k + 1) / 2` and `2 C_π m k (k + 1) ≤ δ₀ J < 4 C_π N δ₀ f` + have key : (m : ℝ) * #O * (2 * Cπ * k * (k + 1)) ≤ #A * (2 * Cπ * k * (k + 1)) := by + have h1 : (m : ℝ) * #O * (2 * Cπ * k * (k + 1)) ≤ #O * (δ₀ * J) := by + have := mul_le_mul_of_nonneg_left hJm (Nat.cast_nonneg (α := ℝ) #O) + nlinarith + have h2 : (#O : ℝ) * (δ₀ * J) ≤ #O * (4 * Cπ * N * δ₀ * f) := + mul_le_mul_of_nonneg_left (by nlinarith) (Nat.cast_nonneg _) + have h3 : (#O : ℝ) * (4 * Cπ * N * δ₀ * f) ≤ #A * (2 * Cπ * k * (k + 1)) := by + have := mul_le_mul_of_nonneg_left hcount (by positivity : (0 : ℝ) ≤ 4 * Cπ) + nlinarith + linarith + have : (m : ℝ) * #O ≤ #A := le_of_mul_le_mul_right key (by positivity) + exact_mod_cast this + +/-- **Corrected pilot columns have few large entries** [OpenAI2026LogSpace, Lemma 4.3 (3)]. Under +the hypotheses of `Matrix.le_columnDetector` with row-sum bound `k`, if `γ` vanishes from `4 / 5` +on and the pilot multiplier `γ (M_(i+1) y)` of step `i + 1 ≤ k` is positive, then the pilot input +of that step has at most `R / f` entries at least `δ₁ f` in column `y`. -/ +theorem card_le_of_pilot_pos (hch : RetentionChannels X Y f π cπ Cπ Cpair Cvar) (hf : 0 < f) + (hcπ : 0 < cπ) (hCpair : 0 ≤ Cpair) {δ₁ : ℝ} (hϕδ : ∀ t, δ₁ ≤ t → ϕ t = 1) + (hρ1 : ∀ t, ρ t ≤ 1) {η : ℝ} (hη : 0 < η) (hρη : ∀ t, t ≤ η → ρ t = 1) + (hC0 : ∀ x y, 0 ≤ C x y) (hC1 : C *ᵥ 1 ≤ 1) (hc0 : ∀ t, 0 ≤ c t) + (hct : ∀ t, 0 ≤ t → c t ≤ t) (hγ0 : ∀ t, 0 ≤ γ t) (hγ1 : ∀ t, γ t ≤ 1) + (hγ45 : ∀ t, 4 / 5 ≤ t → γ t = 0) {k : ℕ} (hK : 160 * (1 + Cpair * k / η) ≤ K) + (hJ : 0 < J) {R : ℝ} (hRJ : 4 * J ≤ cπ * R) (hRvar : 40 * Cvar ≤ cπ * R) {i : ℕ} + (hi : i < k) {y : V} + (hpos : 0 < γ (pilotMax c γ (columnDetector X Y ϕ ρ J K f) C (i + 1) y)) : + (#({x | δ₁ * f ≤ pilotInput c γ (columnDetector X Y ϕ ρ J K f) C i x y} : Finset V) : ℝ) ≤ + R / f := by + set U := columnDetector X Y ϕ ρ J K f + have hseq := isCorrectionSeq_pilotCorrection (U := U) hC0 hc0 hct hγ0 hγ1 + by_contra hlt + have hrow : ∀ x, ∑ w, pilotInput c γ U C i x w ≤ (k : ℝ) := fun x => by + have := (hseq.sum_input_le hC1 i x).1 + have hik : (i : ℝ) + 1 ≤ k := by exact_mod_cast hi + exact this.trans hik + have hU : 19 / 20 ≤ U (pilotInput c γ U C i) y := + le_columnDetector hch hf hcπ hCpair hϕδ hρ1 hη hρη (hseq.input_nonneg hC0 i) hrow hK hJ hRJ + hRvar (not_le.mp hlt) + have hM : 4 / 5 ≤ pilotMax c γ U C (i + 1) y := by + rw [pilotMax_succ, Pi.sup_apply] + exact le_sup_of_le_right (by linarith) + rw [hγ45 _ hM] at hpos + exact lt_irrefl _ hpos + +/-- **Corrected columns have few large entries** [OpenAI2026LogSpace, Lemma 4.3 (3)]: if the +final multiplier `γ (M_k y)` is positive, then for every `i < k` the input of step `i + 1` of the +actual correction, with cutoffs `c t * γ (M_k y)`, has at most `R / f` entries at least `δ₁ f` in +column `y`. -/ +theorem card_le_of_multiplier_pos (hch : RetentionChannels X Y f π cπ Cπ Cpair Cvar) + (hf : 0 < f) (hcπ : 0 < cπ) (hCpair : 0 ≤ Cpair) {δ₁ : ℝ} (hϕδ : ∀ t, δ₁ ≤ t → ϕ t = 1) + (hρ1 : ∀ t, ρ t ≤ 1) {η : ℝ} (hη : 0 < η) (hρη : ∀ t, t ≤ η → ρ t = 1) + (hC0 : ∀ x y, 0 ≤ C x y) (hC1 : C *ᵥ 1 ≤ 1) (hc0 : ∀ t, 0 ≤ c t) + (hct : ∀ t, 0 ≤ t → c t ≤ t) (hcm : Monotone c) (hγ0 : ∀ t, 0 ≤ γ t) (hγ1 : ∀ t, γ t ≤ 1) + (hγm : Antitone γ) (hγ45 : ∀ t, 4 / 5 ≤ t → γ t = 0) {k : ℕ} + (hK : 160 * (1 + Cpair * k / η) ≤ K) (hJ : 0 < J) {R : ℝ} (hRJ : 4 * J ≤ cπ * R) + (hRvar : 40 * Cvar ≤ cπ * R) {y : V} + (hpos : 0 < γ (pilotMax c γ (columnDetector X Y ϕ ρ J K f) C k y)) {i : ℕ} (hi : i < k) : + let M := pilotMax c γ (columnDetector X Y ϕ ρ J K f) C k + (#({x | δ₁ * f ≤ (C + cutoffCorrectionIter (fun y t => c t * γ (M y)) C i * C) x y} : + Finset V) : ℝ) ≤ R / f := by + intro M + set U := columnDetector X Y ϕ ρ J K f + have hstep : 0 < γ (pilotMax c γ U C (i + 1) y) := + hpos.trans_le (hγm (pilotMax_mono (by omega) y)) + refine le_trans ?_ (card_le_of_pilot_pos hch hf hcπ hCpair hϕδ hρ1 hη hρη hC0 hC1 hc0 hct + hγ0 hγ1 hγ45 hK hJ hRJ hRvar hi hstep) + refine Nat.cast_le.mpr (card_le_card fun x hx => ?_) + simp only [mem_filter, mem_univ, true_and] at hx ⊢ + exact hx.trans (cutoffCorrectionIter_le_pilotCorrection hC0 hc0 hct hcm hγ0 hγ1 hγm + hi.le x y).2 + +variable [DecidableEq V] [LinearOrder V] {θ L θ₂ : ℝ} {κ χ : ℝ → ℝ} {τ₀ τ₁ q : ℝ} + +/-- **One stage with detector-chosen multipliers and copies** +[OpenAI2026LogSpace, Proposition 4.5]. Run `k` pilot steps with the column detector, let `M` be +the final running maximum, correct `C` by `k` steps of the cutoffs `φ y t = c t * γ (M y)`, and +split the residual `D` with the copy weights `Matrix.detectorWeight κ M` and the overloaded set +`Matrix.overloaded M`. If the base cutoff satisfies the hypotheses of the factorial truncation +together with `t - θ₂ f ≤ c t`, `γ` is nonincreasing and one through `1 / 2`, `κ` is zero through +`1 / 4` and one from `1 / 2`, `2 C_π m k (k + 1) ≤ δ₀ J`, and the copy constants are chosen as in +`Matrix.copyStage_rates`, then the copy step has entries at most `f / q`, intertwines with its +projection, and is supported in at most `2 |A|` copies. -/ +theorem detectedStage_rates (hch : RetentionChannels X Y f π cπ Cπ Cpair Cvar) + (hC : C.IsStrictUpperTriangular) (hC0 : ∀ x y, 0 ≤ C x y) (hCf : ∀ x y, C x y ≤ f) + (hC1 : C *ᵥ 1 ≤ 1) {A : Finset V} (hA : ∀ x y, C x y ≠ 0 → x ∈ A ∧ y ∈ A) (hf : 0 < f) + (hc0 : ∀ t, 0 ≤ c t) (hcθ : ∀ t, c t ≤ max (t - θ * f) 0) (hcm : Monotone c) + (hcL : ∀ s t, s ≤ t → c t - c s ≤ L * (t - s)) (hcθ₂ : ∀ t, t - θ₂ * f ≤ c t) (hθ : 0 < θ) + (hL : 0 ≤ L) (hγ0 : ∀ t, 0 ≤ γ t) (hγ1 : ∀ t, γ t ≤ 1) (hγhalf : ∀ t, t ≤ 1 / 2 → γ t = 1) + (hκ0 : ∀ t, 0 ≤ κ t) (hκ1 : ∀ t, κ t ≤ 1) (hκq : ∀ t, t ≤ 1 / 4 → κ t = 0) + (hκhalf : ∀ t, 1 / 2 < t → κ t = 1) (hCπ : 0 < Cπ) (hϕ0 : ∀ t, 0 ≤ ϕ t) + (hϕ1 : ∀ t, ϕ t ≤ 1) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (hϕδ : ∀ t, t ≤ δ₀ → ϕ t = 0) + (hρ1 : ∀ t, ρ t ≤ 1) (hJ : 0 < J) {k m : ℕ} (hJm : 2 * Cπ * m * k * (k + 1) ≤ δ₀ * J) + (hτ₀ : θ₂ * f + f * Real.exp (1 / θ) * (L / θ) ^ k / k.factorial ≤ τ₀) + (hχ0 : ∀ t, 0 ≤ χ t) (hχ1 : ∀ t, χ t ≤ 1) (hχ₀ : ∀ t, t ≤ τ₀ → χ t = 0) + (hχ₁ : ∀ t, τ₁ ≤ t → χ t = 1) (hτ₁ : τ₁ ≤ f / q) (hcopies : (k + 1) * f / (m + 1) ≤ f / q) : + let M := pilotMax c γ (columnDetector X Y ϕ ρ J K f) C k + let E := cutoffCorrectionIter (fun y t => c t * γ (M y)) C k + let D := C - E + E * C + (∀ a b, copyStage χ m (detectorWeight κ M) D a b ≤ f / q) ∧ + copyStage χ m (detectorWeight κ M) D * copyWeight (detectorWeight κ M) = + copyWeight (detectorWeight κ M) * D ∧ + (∀ a b, copyStage χ m (detectorWeight κ M) D a b ≠ 0 → + a ∈ copyCover A (overloaded M) ∧ b ∈ copyCover A (overloaded M)) ∧ + #(copyCover (m := m) A (overloaded M)) ≤ 2 * #A := by + intro M E D + have hct : ∀ t, 0 ≤ t → c t ≤ t := fun t ht => + (hcθ t).trans (max_le (by nlinarith [mul_pos hθ hf]) ht) + have hO := card_overloaded_le (K := K) (k := k) (m := m) hch hf hCπ hϕ0 hϕ1 hδ₀ hϕδ hρ1 hJ hC0 + hC1 hA hc0 hct hγ0 hγ1 hJm + refine copyStage_rates (φ := fun y t => c t * γ (M y)) (θ := θ) (L := L) (m := m) (χ := χ) + (τ₀ := τ₀) (τ₁ := τ₁) (r := detectorWeight κ M) (A := A) (O := overloaded M) (θ₂ := θ₂) + (q := q) hC hC0 hCf hC1 + (fun y t => mul_nonneg (hc0 t) (hγ0 _)) + (fun y t => (mul_le_of_le_one_right (hc0 t) (hγ1 _)).trans (hcθ t)) + (fun y => hcm.mul_const (hγ0 _)) + (fun y s t hst => ?_) hf hθ hL k hA (fun x => by simp [detectorWeight]) + (fun j x => ?_) (fun j x hj hr => ?_) (fun y => ?_) hτ₀ hχ0 hχ1 hχ₀ hχ₁ hτ₁ hcopies hO + · -- the cutoffs are `L`-Lipschitz + have hmono : 0 ≤ c t - c s := sub_nonneg.mpr (hcm hst) + calc c t * γ (M y) - c s * γ (M y) = γ (M y) * (c t - c s) := by ring + _ ≤ 1 * (c t - c s) := mul_le_mul_of_nonneg_right (hγ1 _) hmono + _ ≤ L * (t - s) := by rw [one_mul]; exact hcL s t hst + · -- the weights lie in `[0, 1]` + unfold detectorWeight + split_ifs + · exact ⟨zero_le_one, le_rfl⟩ + · exact ⟨hκ0 _, hκ1 _⟩ + · -- only overloaded vertices have active extra copies + simp only [detectorWeight, hj, ↓reduceIte] at hr + simp only [overloaded, mem_filter, mem_univ, true_and] + by_contra hle + exact hr (hκq _ (not_lt.mp hle)) + · -- every column is fully corrected or overloaded with all copies active + by_cases hg : γ (M y) = 1 + · left + intro t + simp only [hg, mul_one] + exact hcθ₂ t + · right + have hhalf : 1 / 2 < M y := by + by_contra hle + exact hg (hγhalf _ (not_lt.mp hle)) + refine ⟨fun j => ?_, ?_⟩ + · unfold detectorWeight + split_ifs + · rfl + · exact hκhalf _ hhalf + · simp only [overloaded, mem_filter, mem_univ, true_and] + linarith + +end Matrix diff --git a/Complexity/Probability/PairwiseIndependentHash/DetectorChannels.lean b/Complexity/Probability/PairwiseIndependentHash/DetectorChannels.lean new file mode 100644 index 000000000..ec1343a5e --- /dev/null +++ b/Complexity/Probability/PairwiseIndependentHash/DetectorChannels.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 +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Probability.ColumnDetector +public import Complexity.Probability.PairwiseIndependentHash.RetentionChannel + +/-! +# Affine retention channels satisfy the detector interface + +The affine retention channels over `𝔽_P` (`Cslib.Probability.affineRetains`) satisfy the channel +interface `Cslib.Probability.RetentionChannels` of the column detectors, with the constants +`c_π = 1`, `C_π = C_pair = 2 ^ H` and `C_var = 4`. Vertices are identified with field elements +through an injective identifier map `ident : V → ZMod P`, and both channels use the affine seed +space; their independence comes from the product of the two seed spaces. So the detector lemma +(`Matrix.le_columnDetector`, `Matrix.lt_card_of_lt_columnDetector`) and the detected stage +(`Matrix.detectedStage_rates`) hold for these channels at rate `f = a ^ H`, where +`1 ≤ P a` and `a ≤ 1` [OpenAI2026LogSpace, (4.8), (4.9)]. + +## Main results + +* `Cslib.Probability.retentionChannels_affineRetains`: the affine channels at rate `a ^ H`. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 4.2 (preprint, not peer reviewed) +-/ + +public section + +open Finset + +namespace Cslib.Probability + +variable {V : Type*} {P H : ℕ} [Fact P.Prime] + +/-- **Affine retention channels satisfy the detector interface.** Let `ident : V → ZMod P` be +injective, `1 ≤ P a` and `a ≤ 1`, and `L = ⌈P a⌉`. Retaining `v` when the affine seed retains +`ident v`, for each of two channels, gives retention channels at rate `f = a ^ H` with retention +probability `π = (L / P) ^ H` and constants `c_π = 1`, `C_π = C_pair = 2 ^ H`, `C_var = 4`. -/ +theorem retentionChannels_affineRetains {ident : V → ZMod P} (hident : Function.Injective ident) + {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) : + RetentionChannels (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) + (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) (a ^ H) + ((((⌈P * a⌉₊ : ℕ) : ℝ) / P) ^ H) 1 (2 ^ H) (2 ^ H) 4 := by + obtain ⟨hL, hlow, hup, hpair, htail⟩ := affineRetains_rates (H := H) hPa ha + have hdens : ∀ v, (dens {s | affineRetains P H ⌈P * a⌉₊ s (ident v)} : ℝ) = + (((⌈P * a⌉₊ : ℕ) : ℝ) / P) ^ H := fun v => by + rw [dens_affineRetains hL]; push_cast; rfl + refine ⟨hdens, hdens, by rw [one_mul]; exact hlow, hup, fun w y hwy => ?_, fun A hA => ?_⟩ + · exact hpair _ _ (hident.ne hwy) + · have hcard : #(A.image ident) = #A := card_image_of_injective A hident + have hfilter : ∀ s, #{x ∈ A | affineRetains P H ⌈P * a⌉₊ s (ident x)} = + #{y ∈ A.image ident | affineRetains P H ⌈P * a⌉₊ s y} := fun s => by + rw [filter_image, card_image_of_injective _ hident] + have := htail (A.image ident) (hA.image ident) + simp only [hcard, ← hfilter] at this + exact this + +end Cslib.Probability diff --git a/ComplexityTests/DetectorChannels.lean b/ComplexityTests/DetectorChannels.lean new file mode 100644 index 000000000..a00f4d873 --- /dev/null +++ b/ComplexityTests/DetectorChannels.lean @@ -0,0 +1,43 @@ +/- +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.DetectorChannels +import Mathlib.Tactic.NormNum.Prime + +/-! +# Tests for affine channels in the column detector +-/ + +namespace ComplexityTests.DetectorChannels + +open Finset Matrix Cslib.Probability + +private instance : Fact (Nat.Prime 5) := ⟨by norm_num⟩ + +/-- The affine channels on `𝔽₅` with `H = 2` and `a = 1 / 2`: rate `f = 1 / 4`, side +`L = ⌈5 / 2⌉ = 3`, retention probability `(3 / 5) ^ 2`. -/ +private theorem channels : + RetentionChannels (fun s (v : ZMod 5) => affineRetains 5 2 ⌈(5 : ℕ) * (1 / 2 : ℝ)⌉₊ s (id v)) + (fun s (v : ZMod 5) => affineRetains 5 2 ⌈(5 : ℕ) * (1 / 2 : ℝ)⌉₊ s (id v)) ((1 / 2) ^ 2) + ((((⌈(5 : ℕ) * (1 / 2 : ℝ)⌉₊ : ℕ) : ℝ) / (5 : ℕ)) ^ 2) 1 (2 ^ 2) (2 ^ 2) 4 := + retentionChannels_affineRetains Function.injective_id (by norm_num) (by norm_num) + +-- With detector rank `J = 20`, the threshold `J / (4 C_π f) = 20 / (4 · 4 · (1 / 4)) = 5` is the +-- whole vertex set, so on `𝔽₅` no column is ever flagged, whatever the matrix. +example (G : Matrix (ZMod 5) (ZMod 5) ℝ) (y : ZMod 5) : + columnDetector (fun s (v : ZMod 5) => affineRetains 5 2 ⌈(5 : ℕ) * (1 / 2 : ℝ)⌉₊ s (id v)) + (fun s (v : ZMod 5) => affineRetains 5 2 ⌈(5 : ℕ) * (1 / 2 : ℝ)⌉₊ s (id v)) + (fun t => min (max t 0) 1) (fun _ => 1) 20 1 ((1 / 2) ^ 2) G y ≤ 1 / 4 := by + refine not_lt.mp fun h => ?_ + have := lt_card_of_lt_columnDetector channels (by norm_num) + (fun t => le_min (le_max_right _ _) zero_le_one) (fun t => min_le_right _ _) (δ₀ := 0) + (fun t ht => by rw [max_eq_right ht, min_eq_left zero_le_one]) (fun _ => le_rfl) + (by norm_num) h + have hcard : (#({x | 0 * (1 / 2) ^ 2 < G x y} : Finset (ZMod 5)) : ℝ) ≤ 5 := by + exact_mod_cast (card_le_univ _).trans (by simp) + norm_num at this hcard + linarith + +end ComplexityTests.DetectorChannels diff --git a/ComplexityTests/Detectors.lean b/ComplexityTests/Detectors.lean new file mode 100644 index 000000000..fc8731cde --- /dev/null +++ b/ComplexityTests/Detectors.lean @@ -0,0 +1,215 @@ +/- +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.DetectedStage +import Mathlib.Analysis.SpecialFunctions.Exponential +import Mathlib.Analysis.Complex.ExponentialBounds +import Mathlib.Tactic.FinCases + +/-! +# Tests for the pilot, the column detectors and a detected stage +-/ + +namespace ComplexityTests.Detectors + +open Finset Matrix Cslib.Probability + +/-! ### Channels that retain every vertex -/ + +/-- A channel with one seed that retains every vertex. -/ +private abbrev all {V : Type*} : Unit → V → Prop := fun _ _ => True + +/-- Channels that retain everything satisfy the channel interface at every rate `f ∈ (0, 1]`, with +`c_π = 1`, `C_π = C_pair = 1 / f` and `C_var = 0`. -/ +private theorem retentionChannels_all {V : Type*} {f : ℝ} (hf : 0 < f) (hf1 : f ≤ 1) : + RetentionChannels (all (V := V)) all f 1 1 (1 / f) (1 / f) 0 where + dens_X _ := by simp [all] + dens_Y _ := by simp [all] + lower := by simpa using hf1 + upper := by rw [one_div_mul_cancel hf.ne'] + pair _ _ _ := by simp [all, hf.ne'] + tail A _ := by + have : ({s | 2 * (#{x ∈ A | all s x} : ℝ) < #A * 1} : Finset Unit) = ∅ := by + ext s + simp only [all, filter_true, mul_one, mem_filter, mem_univ, true_and, notMem_empty, + iff_false, not_lt] + linarith [(Nat.cast_nonneg (α := ℝ) #A)] + rw [this] + simp + +/-! ### Step cutoffs -/ + +/-- The step `0` through `a`, `1` above. -/ +private noncomputable def up (a t : ℝ) : ℝ := if t ≤ a then 0 else 1 + +/-- The step `1` through `a`, `0` above. -/ +private noncomputable def down (a t : ℝ) : ℝ := if t ≤ a then 1 else 0 + +private theorem up_nonneg (a t : ℝ) : 0 ≤ up a t := by unfold up; split_ifs <;> norm_num +private theorem up_le_one (a t : ℝ) : up a t ≤ 1 := by unfold up; split_ifs <;> norm_num +private theorem up_of_le {a t : ℝ} (h : t ≤ a) : up a t = 0 := by simp only [up, h, ↓reduceIte] +private theorem up_of_lt {a t : ℝ} (h : a < t) : up a t = 1 := by + simp only [up, not_le.mpr h, ↓reduceIte] +private theorem down_nonneg (a t : ℝ) : 0 ≤ down a t := by unfold down; split_ifs <;> norm_num +private theorem down_le_one (a t : ℝ) : down a t ≤ 1 := by unfold down; split_ifs <;> norm_num +private theorem down_of_le {a t : ℝ} (h : t ≤ a) : down a t = 1 := by + simp only [down, h, ↓reduceIte] +private theorem down_antitone (a : ℝ) : Antitone (down a) := fun s t hst => by + unfold down; split_ifs with h1 h2 <;> first | exact absurd (hst.trans h1) h2 | norm_num + +/-! ### The detector lemma on a concrete column -/ + +/-- Rows `0, …, 4` each have one entry `1 / 5`, in column `5`. -/ +private noncomputable def G : Matrix (Fin 6) (Fin 6) ℝ := + of fun x y => if y = 5 ∧ x ≠ 5 then 1 / 5 else 0 + +private theorem G0 : ∀ x w, 0 ≤ G x w := by + intro x w; simp only [G, of_apply]; split_ifs <;> norm_num + +private theorem G_row : ∀ x, ∑ w, G x w ≤ (1 : ℝ) := by + intro x; fin_cases x <;> simp [G] <;> norm_num + +-- Column `5` has five entries `1 / 5 ≥ δ₁ f` with `f = 1` and `δ₁ = 1 / 6`, more than +-- `R / f = 4`, so its detector number is at least `19 / 20`. The score is the step at `1 / 10`, +-- the gate the step at `η = 1 / 2`, and the gate rank `K = 480 ≥ 160 (1 + 1 / (1 / 2))`. +example : 19 / 20 ≤ columnDetector all all (up (1 / 10)) (down (1 / 2)) 1 480 1 G 5 := by + have hcount : (4 : ℝ) / 1 < #(univ.filter fun x => 1 / 6 * 1 ≤ G x 5) := by + have hsub : (univ.erase 5 : Finset (Fin 6)) ⊆ univ.filter fun x => 1 / 6 * 1 ≤ G x 5 := + fun x hx => by + have hx5 : x ≠ 5 := ne_of_mem_erase hx + simp only [mem_filter, mem_univ, true_and, G, of_apply, hx5, ne_eq, not_false_eq_true, + ↓reduceIte] + norm_num + have := card_le_card hsub + rw [card_erase_of_mem (mem_univ _), card_univ, Fintype.card_fin] at this + have : (5 : ℝ) ≤ #(univ.filter fun x => 1 / 6 * 1 ≤ G x 5) := by exact_mod_cast this + linarith + exact le_columnDetector (J := 1) (K := 480) (G := G) (R := 4) + (retentionChannels_all (V := Fin 6) one_pos le_rfl) one_pos one_pos (by norm_num) + (δ₁ := 1 / 6) (fun t ht => up_of_lt (by linarith)) (down_le_one _) + (by norm_num : (0 : ℝ) < 1 / 2) (fun t ht => down_of_le ht) G0 G_row (by norm_num) + one_pos (by norm_num) (by norm_num) hcount + +-- An empty column has no substantial entries, so its detector number is at most `1 / 4`. +example : columnDetector all all (up (1 / 10)) (down (1 / 2)) 1 480 1 G 0 ≤ 1 / 4 := by + refine not_lt.mp fun h => ?_ + have := lt_card_of_lt_columnDetector (J := 1) (K := 480) (G := G) + (retentionChannels_all (V := Fin 6) one_pos le_rfl) one_pos (up_nonneg _) (up_le_one _) + (fun t ht => up_of_le ht) (down_le_one _) one_pos h + have hempty : (univ.filter fun x => 1 / 10 * 1 < G x 0) = ∅ := by + ext x; simp only [G, of_apply, Fin.reduceEq, false_and, ↓reduceIte, mem_filter, mem_univ, + true_and, notMem_empty, iff_false, not_lt]; norm_num + rw [hempty, card_empty, Nat.cast_zero] at this + norm_num at this + +/-! ### A stage of the hierarchy with detector-chosen multipliers -/ + +/-- A walk on three time layers: from `0` to `1` and from `1` to `2`, each with probability +`f = 1 / 2`. -/ +private noncomputable def C : Matrix (Fin 3) (Fin 3) ℝ := !![0, 1 / 2, 0; 0, 0, 1 / 2; 0, 0, 0] + +private theorem hC : C.IsStrictUpperTriangular := by + intro i j h; fin_cases i <;> fin_cases j <;> simp_all [C] + +private theorem hC0 : ∀ x y, 0 ≤ C x y := by + intro x y; fin_cases x <;> fin_cases y <;> norm_num [C] + +private theorem hCf : ∀ x y, C x y ≤ 1 / 2 := by + intro x y; fin_cases x <;> fin_cases y <;> norm_num [C] + +private theorem hC1 : C *ᵥ 1 ≤ 1 := by + intro x; fin_cases x <;> norm_num [C, mulVec, dotProduct, Fin.sum_univ_three] + +/-- The hard base cutoff `t ↦ max (t - θ f) 0` with `θ = 1 / 4`, `f = 1 / 2`. -/ +private noncomputable def c (t : ℝ) : ℝ := max (t - 1 / 8) 0 + +private theorem hcL : ∀ s t, s ≤ t → c t - c s ≤ 1 * (t - s) := fun s t _ => by + simp only [c, one_mul] + have := le_max_left (s - 1 / 8) 0 + have := le_max_right (s - 1 / 8) 0 + have : max (t - 1 / 8) 0 ≤ max (s - 1 / 8) 0 + (t - s) := max_le (by linarith) (by linarith) + linarith + +private theorem c_nonneg (t : ℝ) : 0 ≤ c t := le_max_right _ _ +private theorem c_le (t : ℝ) (ht : 0 ≤ t) : c t ≤ t := max_le (by linarith) ht +private theorem c_mono : Monotone c := fun _ _ h => max_le_max (by linarith) le_rfl + +/-! ### The pilot -/ + +/-- A column number that flags column `2`, whatever the input. -/ +private noncomputable def flag2 : Matrix (Fin 3) (Fin 3) ℝ → Fin 3 → ℝ := + fun _ y => if y = 2 then 1 else 0 + +-- After one pilot step the running maximum flags column `2`, which loses its multiplier. +example : pilotMax c (down (1 / 2)) flag2 C 1 2 = 1 := by + rw [pilotMax_succ]; norm_num [flag2] + +-- Column `1` is corrected, `Ê₁ (0, 1) = c (1 / 2) = 3 / 8`; column `2` is not. +example : pilotCorrection c (down (1 / 2)) flag2 C 1 0 1 = 3 / 8 := by + rw [pilotCorrection_succ_apply, pilotMax_succ] + norm_num [pilotInput, flag2, c, C, down] + +example : pilotCorrection c (down (1 / 2)) flag2 C 1 1 2 = 0 := by + rw [pilotCorrection_succ_apply, pilotMax_succ] + norm_num [flag2, down] + +-- The pilot corrections have row sums at most the step count. +example (x : Fin 3) : ∑ y, pilotCorrection c (down (1 / 2)) flag2 C 2 x y ≤ 2 := by + exact_mod_cast (isCorrectionSeq_pilotCorrection hC0 c_nonneg c_le (down_nonneg _) + (down_le_one _)).sum_le hC1 2 x + +-- The actual correction with the final multiplier stays below the pilot. +example (x y : Fin 3) : + cutoffCorrectionIter (fun y t => c t * down (1 / 2) (pilotMax c (down (1 / 2)) flag2 C 2 y)) + C 1 x y ≤ pilotCorrection c (down (1 / 2)) flag2 C 1 x y := + (cutoffCorrectionIter_le_pilotCorrection hC0 c_nonneg c_le c_mono (down_nonneg _) + (down_le_one _) (down_antitone _) (by norm_num : 1 ≤ 2) x y).1 + +/-! ### One stage -/ + +/-- `e ^ 4 · 4 ^ 15 / 15! ≤ 1 / 8`: fifteen iterations make the truncation error small. -/ +private theorem factorial_bound : + (1 / 2 : ℝ) * Real.exp (1 / (1 / 4)) * (1 / (1 / 4)) ^ 15 / (Nat.factorial 15) ≤ 1 / 16 := by + have he : Real.exp 4 ≤ 55 := by + have h1 : Real.exp 4 = Real.exp 1 ^ 4 := by rw [← Real.exp_nat_mul]; norm_num + rw [h1] + calc Real.exp 1 ^ 4 ≤ 2.7182818286 ^ 4 := + pow_le_pow_left₀ (Real.exp_pos 1).le Real.exp_one_lt_d9.le 4 + _ ≤ 55 := by norm_num + norm_num [Nat.factorial] + nlinarith + +-- One stage with `k = 15` pilot and correction steps, `m + 1 = 32` copies, the full-retention +-- channels at rate `f = 1 / 2`, the detector score `up (1 / 10)` with `δ₀ = 1 / 10` and rank +-- `J = 297600 ≥ 2 C_π m k (k + 1) / δ₀`: the copies have entries at most `f / q = 1 / 4`, +-- intertwine with their projection, and at most `2 · 3` of them are active. +example : + let M := pilotMax c (down (1 / 2)) (columnDetector all all (up (1 / 10)) (down (1 / 2)) 297600 + 1 (1 / 2)) C 15 + let E := cutoffCorrectionIter (fun y t => c t * down (1 / 2) (M y)) C 15 + let D := C - E + E * C + (∀ a b, copyStage (up (3 / 16)) 31 (detectorWeight (up (1 / 4)) M) D a b ≤ 1 / 2 / 2) ∧ + copyStage (up (3 / 16)) 31 (detectorWeight (up (1 / 4)) M) D * + copyWeight (detectorWeight (up (1 / 4)) M) = + copyWeight (detectorWeight (up (1 / 4)) M) * D ∧ + (∀ a b, copyStage (up (3 / 16)) 31 (detectorWeight (up (1 / 4)) M) D a b ≠ 0 → + a ∈ copyCover univ (overloaded M) ∧ b ∈ copyCover univ (overloaded M)) ∧ + #(copyCover (m := 31) (univ : Finset (Fin 3)) (overloaded M)) ≤ + 2 * #(univ : Finset (Fin 3)) := + detectedStage_rates (X := all) (Y := all) (ϕ := up (1 / 10)) (ρ := down (1 / 2)) (J := 297600) + (K := 1) (f := 1 / 2) (c := c) (γ := down (1 / 2)) (C := C) (A := univ) (κ := up (1 / 4)) + (χ := up (3 / 16)) (q := 2) (k := 15) (m := 31) (θ := 1 / 4) (L := 1) (θ₂ := 1 / 4) + (τ₀ := 3 / 16) (τ₁ := 1 / 4) (δ₀ := 1 / 10) + (retentionChannels_all (V := Fin 3) (by norm_num) (by norm_num)) hC hC0 hCf hC1 + (fun _ _ _ => ⟨mem_univ _, mem_univ _⟩) (by norm_num) c_nonneg + (fun t => le_of_eq (by norm_num [c])) c_mono hcL + (fun t => by norm_num [c]) (by norm_num) zero_le_one (down_nonneg _) (down_le_one _) + (fun t ht => down_of_le ht) (up_nonneg _) (up_le_one _) (fun t ht => up_of_le ht) + (fun t ht => up_of_lt (by linarith)) (by norm_num) (up_nonneg _) (up_le_one _) (by norm_num) + (fun t ht => up_of_le ht) (down_le_one _) (by norm_num) (by norm_num) + (by linarith [factorial_bound]) (up_nonneg _) (up_le_one _) (fun t ht => up_of_le ht) + (fun t ht => up_of_lt (by linarith)) (by norm_num) (by norm_num) + +end ComplexityTests.Detectors diff --git a/ComplexityTests/KthLargest.lean b/ComplexityTests/KthLargest.lean new file mode 100644 index 000000000..7dac815a7 --- /dev/null +++ b/ComplexityTests/KthLargest.lean @@ -0,0 +1,53 @@ +/- +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.Data.Finset.KthLargest +import Mathlib.Algebra.Order.Ring.Rat +import Mathlib.Data.Fin.VecNotation +import Mathlib.Data.Fintype.Basic +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Tests for the `k`-th largest value +-/ + +namespace ComplexityTests.KthLargest + +open Finset + +/-- The values `3, 1, 2, 0`. -/ +private def h : Fin 4 → ℚ := ![3, 1, 2, 0] + +private theorem filter_two_lt : (univ.filter fun x => (2 : ℚ) < h x) = {0} := by + decide + +private theorem filter_two_le : (univ.filter fun x => (2 : ℚ) ≤ h x) = {0, 2} := by + decide + +private theorem filter_zero_lt : (univ.filter fun x => (0 : ℚ) < h x) = {0, 1, 2} := by + decide + +-- The second largest of `3, 1, 2, 0` is `2`: two values are at least `2`, one exceeds it. +example : kthLargest 2 univ h = 2 := by + refine le_antisymm (not_lt.mp fun hlt => ?_) ?_ + · have := (lt_kthLargest_iff (by norm_num) (by norm_num)).mp hlt + rw [filter_two_lt, card_singleton] at this + omega + · rw [le_kthLargest_iff (by norm_num) (by norm_num), filter_two_le] + rfl + +-- Only three values are positive, so the padded fourth largest is `0`. +example : kthLargest 4 univ h = 0 := by + refine le_antisymm (not_lt.mp fun hlt => ?_) kthLargest_nonneg + have := (lt_kthLargest_iff (by norm_num) le_rfl).mp hlt + rw [filter_zero_lt] at this + exact absurd this (by decide) + +-- Values above a nonnegative bound bound the order statistic. +example (k : ℕ) : kthLargest k univ h ≤ 3 := + kthLargest_le (by norm_num) fun x _ => by fin_cases x <;> norm_num [h] + +end ComplexityTests.KthLargest