diff --git a/Complexity.lean b/Complexity.lean index 9a3bc3cdea..23713eb444 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2733,7 +2733,9 @@ 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.SourceRelease public import Complexity.Foundations.Probability.StochasticAtom +public import Complexity.Foundations.Probability.TrueSampleMeans public import Complexity.Foundations.Quantum.Measurement public import Complexity.Foundations.Relation.InductiveCounting public import Complexity.Foundations.Relation.RelatesWithinSteps diff --git a/Complexity/Foundations/Probability/RootMetric.lean b/Complexity/Foundations/Probability/RootMetric.lean index 419b8cccd2..651f7bbf26 100644 --- a/Complexity/Foundations/Probability/RootMetric.lean +++ b/Complexity/Foundations/Probability/RootMetric.lean @@ -71,7 +71,7 @@ variable (s : ℕ) (N u : ℝ) (X Y : Ω → V → Prop) [∀ σ v, Decidable (X /-- 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 → ℝ) : ℝ := +@[expose] 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 @@ -81,7 +81,7 @@ noncomputable def rootDistPow (H H' : Ω → V → V → ℝ) : ℝ := /-- 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 → ℝ) : ℝ := +@[expose] noncomputable def vertexNormPow (v : Ω → V → ℝ) : ℝ := (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), |v σ x| ^ s end Definitions diff --git a/Complexity/Foundations/Probability/SourceRelease.lean b/Complexity/Foundations/Probability/SourceRelease.lean new file mode 100644 index 0000000000..0df6d50d10 --- /dev/null +++ b/Complexity/Foundations/Probability/SourceRelease.lean @@ -0,0 +1,163 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Probability.RootMetric +public import Complexity.Foundations.Probability.CorrectionAtom +import Mathlib.Algebra.Order.BigOperators.Expect +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Positivity + +/-! +# Source release through a bounded incoming relation + +In a product of stochastic tables, the right factor is queried at an intermediate vertex `z`. +Its error is a common table `e σ z y`: it does not take the old source `x` as an extra argument. +If the left support relation has at most `K` retained sources at each `z`, double counting +eliminates the old source at cost `K`. Changing the source normalization from `1 / u` to +`1 / f` then contributes exactly `f / u`. + +This is the explicit source-release inequality in the proof of [OpenAI2026LogSpace, Lemma 7.3], +in the September 23, 2026 source version at `openai/math` commit `7ef5c0cc`. Here the indicators +`X_u`, `Z_f`, and `Y_b` are finite-set restrictions `X`, `Z`, and `Y`; the left normalization +is written `(N * u)⁻¹`. The exponent is any natural number, including the paper's `s = 8`. +The theorem proves the source-domain comparison, not the remaining scale comparisons or the +recursive estimator of that lemma. No independence hypothesis is imposed: the support relation, +channels, and error may all depend on the same environment `σ`. + +The correction-atom corollaries discharge the incoming-degree hypothesis using +`Matrix.card_filter_correctionAtom_col_ne_zero_lt`. An arbitrary map from the full environment +to the atom's two seeds allows additional shared coordinates in the right error. + +## Main results + +* `Finset.sum_sum_filter_le_mul_sum_of_card_le`: the finite double-counting inequality. +* `Cslib.sourceRelease_le_rowNormPow`, `Cslib.sourceRelease_le_vertexNormPow`: the exact + `K * (f / u)` cost for a common right table or vector. +* `Matrix.correctionAtom_sourceRelease_le_rowNormPow`, + `Matrix.correctionAtom_sourceRelease_le_vertexNormPow`: source release for correction atoms. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + proof of Lemma 7.3 (preprint, not peer reviewed). +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Finset + +/-- A nonnegative weight at a target is counted at most `K` times if that target has at most +`K` incoming sources. The weight is common to all sources. -/ +theorem sum_sum_filter_le_mul_sum_of_card_le {α β : Type*} (S : Finset α) (T : Finset β) + (P : α → β → Prop) [∀ x z, Decidable (P x z)] {w : β → ℝ} {K : ℕ} + (hw : ∀ z ∈ T, 0 ≤ w z) (hK : ∀ z ∈ T, #{x ∈ S | P x z} ≤ K) : + ∑ x ∈ S, ∑ z ∈ T with P x z, w z ≤ K * ∑ z ∈ T, w z := by + calc + ∑ x ∈ S, ∑ z ∈ T with P x z, w z = + ∑ z ∈ T, (#{x ∈ S | P x z} : ℝ) * w z := by + simp only [sum_filter] + rw [sum_comm] + refine sum_congr rfl fun z _ => ?_ + rw [← sum_filter, sum_const, nsmul_eq_mul] + _ ≤ ∑ z ∈ T, (K : ℝ) * w z := by + refine sum_le_sum fun z hz => mul_le_mul_of_nonneg_right ?_ (hw z hz) + exact_mod_cast hK z hz + _ = K * ∑ z ∈ T, w z := (mul_sum ..).symm + +end Finset + +namespace Cslib + +variable {Ω V : Type*} [Fintype Ω] [Fintype V] + {s : ℕ} {N u f : ℝ} {X Z Y : Ω → V → Prop} + [∀ σ x, Decidable (X σ x)] [∀ σ z, Decidable (Z σ z)] [∀ σ y, Decidable (Y σ y)] + +/-- **Source release for a common right table**, the explicit double-counting estimate in the +proof of [OpenAI2026LogSpace, Lemma 7.3]. A pointwise incoming cap costs `K * (f / u)` in norm +power. The error and the relation may depend on the same environment. -/ +theorem sourceRelease_le_rowNormPow (hN : 0 < N) (hu : 0 < u) (hf : 0 < f) + (P : Ω → V → V → Prop) [∀ σ x z, Decidable (P σ x z)] {K : ℕ} + (hK : ∀ σ z, Z σ z → #{x ∈ ({x | X σ x} : Finset V) | P σ x z} ≤ K) + (e : Ω → V → V → ℝ) : + (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + ∑ z ∈ ({z | Z σ z} : Finset V) with P σ x z, + ∑ y ∈ ({y | Y σ y} : Finset V), |e σ z y| ^ s ≤ + K * (f / u) * rowNormPow s N f Z Y e := by + calc + _ ≤ (N * u)⁻¹ * 𝔼 σ, (K : ℝ) * + ∑ z ∈ ({z | Z σ z} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), + |e σ z y| ^ s := by + refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (by positivity) + refine sum_sum_filter_le_mul_sum_of_card_le _ _ (P σ) (fun _ _ => by positivity) ?_ + intro z hz + exact hK σ z (by simpa using hz) + _ = _ := by + rw [← mul_expect, rowNormPow] + field_simp + +/-- The vector version of source release, used for the right error in a reward update. -/ +theorem sourceRelease_le_vertexNormPow (hN : 0 < N) (hu : 0 < u) (hf : 0 < f) + (P : Ω → V → V → Prop) [∀ σ x z, Decidable (P σ x z)] {K : ℕ} + (hK : ∀ σ z, Z σ z → #{x ∈ ({x | X σ x} : Finset V) | P σ x z} ≤ K) + (v : Ω → V → ℝ) : + (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + ∑ z ∈ ({z | Z σ z} : Finset V) with P σ x z, |v σ z| ^ s ≤ + K * (f / u) * vertexNormPow s N f Z v := by + calc + _ ≤ (N * u)⁻¹ * 𝔼 σ, (K : ℝ) * ∑ z ∈ ({z | Z σ z} : Finset V), |v σ z| ^ s := by + refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (by positivity) + refine sum_sum_filter_le_mul_sum_of_card_le _ _ (P σ) (fun _ _ => by positivity) ?_ + intro z hz + exact hK σ z (by simpa using hz) + _ = _ := by + rw [← mul_expect, vertexNormPow] + field_simp + +end Cslib + +namespace Matrix + +variable {Ω V ι κ : Type*} [Fintype Ω] [Fintype V] [Fintype ι] [Fintype κ] + {s K Kc : ℕ} {N u f : ℝ} {I : ℝ → ℝ → ℝ} {τ Q h ρ : ℝ → ℝ} + {G : Matrix V V ℝ} {g₀ : V → ℝ} {X : ι → V → Prop} {Y Yt : κ → V → Prop} + [∀ t x, Decidable (X t x)] [∀ t z, Decidable (Y t z)] [∀ t z, Decidable (Yt t z)] + +/-- Source release for an actual correction atom. Its incoming gate supplies the degree bound; +no separate sparsity or independence assumption is needed. `draw` selects the atom's seeds +from the full shared environment. -/ +theorem correctionAtom_sourceRelease_le_rowNormPow (draw : Ω → ι × κ) + (Yb : Ω → V → Prop) [∀ σ y, Decidable (Yb σ y)] (hN : 0 < N) (hu : 0 < u) (hf : 0 < f) + (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) (e : Ω → V → V → ℝ) : + (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X (draw σ).1 x} : Finset V), + ∑ z ∈ ({z | Yt (draw σ).2 z} : Finset V) + with correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ (draw σ) x z ≠ 0, + ∑ y ∈ ({y | Yb σ y} : Finset V), |e σ z y| ^ s ≤ + Kc * (f / u) * Cslib.rowNormPow s N f (fun σ z => Yt (draw σ).2 z) Yb e := by + refine Cslib.sourceRelease_le_rowNormPow hN hu hf _ (fun σ z _ => ?_) e + exact (card_filter_correctionAtom_col_ne_zero_lt hKc hIQ hg hτ (draw σ) z).le + +/-- Source release for a common right vector through a correction atom, with its incoming +degree bound supplied by the incoming gate. -/ +theorem correctionAtom_sourceRelease_le_vertexNormPow (draw : Ω → ι × κ) + (hN : 0 < N) (hu : 0 < u) (hf : 0 < f) (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) (v : Ω → V → ℝ) : + (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X (draw σ).1 x} : Finset V), + ∑ z ∈ ({z | Yt (draw σ).2 z} : Finset V) + with correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ (draw σ) x z ≠ 0, + |v σ z| ^ s ≤ + Kc * (f / u) * Cslib.vertexNormPow s N f (fun σ z => Yt (draw σ).2 z) v := by + refine Cslib.sourceRelease_le_vertexNormPow hN hu hf _ (fun σ z _ => ?_) v + exact (card_filter_correctionAtom_col_ne_zero_lt hKc hIQ hg hτ (draw σ) z).le + +end Matrix diff --git a/Complexity/Foundations/Probability/TrueSampleMeans.lean b/Complexity/Foundations/Probability/TrueSampleMeans.lean new file mode 100644 index 0000000000..90e504c526 --- /dev/null +++ b/Complexity/Foundations/Probability/TrueSampleMeans.lean @@ -0,0 +1,233 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Probability.CorrectionAtom +import Mathlib.Algebra.BigOperators.Field +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# True means of sampled atom products + +The direct and correction--dense sample terms of [OpenAI2026LogSpace, Lemma 7.1] use a broad +terminal conditioning slice and a possibly narrower usage slice. Their exact retention-density +ratio changes the conditioning. In a product, a second ratio cancels the sampling of the +intermediate vertex. + +These results use the concrete `Matrix.denseAtom` and `Matrix.correctionAtom` definitions. +The true dense atom is a function of the terminal seed alone, while the correction atom uses +the source and intermediate seeds. Thus the required factorization follows from finite product +averages. No independence of estimated factors, estimator correctness, or machine certificate +is assumed. + +The formulas are the raw direct and product terms before division by the parent first-channel +scale. Copy projections, detector and reward assembly, and the conditional-walk schedule remain +separate parts of the estimator construction. + +## Main results + +* `Finset.expect_mul_dens_div_of_subset`: change a finite conditioning slice by its exact + density ratio, for a function supported on the smaller slice. +* `Matrix.expect_denseAtom_change_usage`: the importance-weighted dense-atom mean. +* `Matrix.expect_correctionAtom_unconditioned`: the correction-atom mean when the intermediate + seed is unconditioned. +* `Matrix.expect_correctionAtom_mul_denseAtom`: the exact correction--dense product mean on + the source/terminal conditioning slice, with the intermediate seed averaged over all draws. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 7.2, Lemma 7.1, September 23, 2026 revision `7ef5c0cc` (preprint, not peer reviewed). +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Finset + +/-- A function supported on `T ⊆ S` has the same mean after restricting to `T` and multiplying +its mean on `S` by the exact ratio of the two uniform densities. -/ +theorem expect_mul_dens_div_of_subset {Ω : Type*} [Fintype Ω] {S T : Finset Ω} + (hTS : T ⊆ S) (hT : T.Nonempty) (v : Ω → ℝ) + (hv : ∀ σ ∈ S, σ ∉ T → v σ = 0) : + 𝔼 σ ∈ S, ((dens S : ℝ) / dens T) * v σ = 𝔼 σ ∈ T, v σ := by + have hS : S.Nonempty := hT.mono hTS + have hScard : (#S : ℝ) ≠ 0 := by exact_mod_cast hS.card_ne_zero + have hTcard : (#T : ℝ) ≠ 0 := by exact_mod_cast hT.card_ne_zero + have hΩcard : (Fintype.card Ω : ℝ) ≠ 0 := by + have hpos : 0 < Fintype.card Ω := hT.card_pos.trans_le (card_le_univ T) + exact_mod_cast hpos.ne' + have hsum : ∑ σ ∈ S, v σ = ∑ σ ∈ T, v σ := (sum_subset hTS hv).symm + rw [← mul_expect, expect_eq_sum_div_card, expect_eq_sum_div_card, hsum, + dens_eq_card_div_card, dens_eq_card_div_card] + push_cast + field_simp + +/-- Averaging a supported function over the full seed space multiplies its conditional mean +by the exact retention density. -/ +theorem expect_eq_dens_mul_expect_of_eq_zero {Ω : Type*} [Fintype Ω] (S : Finset Ω) + (v : Ω → ℝ) (hv : ∀ σ ∉ S, v σ = 0) : + 𝔼 σ, v σ = (dens S : ℝ) * 𝔼 σ ∈ S, v σ := by + classical + have hmask : ∀ σ, v σ = if σ ∈ S then v σ else 0 := by + intro σ + split_ifs with hσ + · rfl + · exact hv σ hσ + calc + 𝔼 σ, v σ = 𝔼 σ, if σ ∈ S then v σ else 0 := + expect_congr rfl fun σ _ => hmask σ + _ = _ := by simpa only [NNRat.smul_def] using Fintype.expect_ite_mem S v + +end Finset + +namespace Matrix + +variable {V κ : Type*} [Fintype V] [Fintype κ] + +/-- The actual dense atom, averaged on a broader terminal slice, has the correct mean after +the exact density-ratio importance correction [OpenAI2026LogSpace, Lemma 7.1]. The sufficient +gate hypotheses are those of `Matrix.expect_denseAtom`. -/ +theorem expect_denseAtom_change_usage {Y Ya Yt : κ → V → Prop} + [∀ t v, Decidable (Y t v)] [∀ t v, Decidable (Ya t v)] [∀ t v, Decidable (Yt t v)] + {k h ρ : ℝ → ℝ} {K : ℕ} {b : ℝ} {G : Matrix V V ℝ} {x y : V} + (hYt : ∀ t, Yt t y → Ya t y) (hS : ({t | Yt t y} : Finset κ).Nonempty) + (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) (hb : 0 < b) (hG0 : ∀ w, 0 ≤ G x w) + {M : ℝ} (hGM : ∑ w, G x w ≤ M) {c : ℝ} (hc : 0 ≤ c) (hK : 2 * (1 + c * M / η) ≤ K) + (hpair : ∀ w, w ≠ y → (#{t | Yt t y ∧ Y t w} : ℝ) ≤ c * b * #{t | Yt t y}) : + 𝔼 t ∈ ({t | Ya t y} : Finset κ), + b * ((dens {t | Ya t y} : ℝ) / dens {t | Yt t y}) * denseAtom Y Yt k h ρ K b G t x y = + b * k (G x y / b) := by + have hsub : ({t | Yt t y} : Finset κ) ⊆ ({t | Ya t y} : Finset κ) := by + intro t ht + exact mem_filter.mpr ⟨mem_univ _, hYt t (by simpa using ht)⟩ + have hchange := expect_mul_dens_div_of_subset hsub hS (fun t => denseAtom Y Yt k h ρ K b G t x y) + (fun t _ ht => by + have hnot : ¬ Yt t y := by simpa using ht + simp [denseAtom, hnot]) + simp only [mul_assoc] + rw [← mul_expect, hchange, + expect_denseAtom hS hkh hρ0 hρ1 hη hρη hb hG0 hGM hc hK hpair] + +variable {ι : Type*} [Fintype ι] + +/-- The intermediate seed may be left unconditioned: the actual correction atom then has +mean `π_f * Q (G x z / f) * g₀ z`, where `π_f` is the exact density of its usage slice. +Its built-in mask supplies the support condition. -/ +theorem expect_correctionAtom_unconditioned {I : ℝ → ℝ → ℝ} {τ Q h ρ : ℝ → ℝ} + {K Kc : ℕ} {f : ℝ} {G : Matrix V V ℝ} {g₀ : V → ℝ} + {X : ι → V → Prop} {Z Zt : κ → V → Prop} + [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Z t v)] [∀ t v, Decidable (Zt t v)] + {x z : V} (hSx : ({s | X s x} : Finset ι).Nonempty) + (hSz : ({t | Zt t z} : 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) + (hpairZ : ∀ w, w ≠ z → (#{t | Zt t z ∧ Z t w} : ℝ) ≤ c * f * #{t | Zt t z}) + {p : ℝ} (hp : 0 ≤ p) + (hpairX : ∀ w, w ≠ x → (#{s | X s x ∧ X s w} : ℝ) ≤ p * #{s | X s x}) + {B : ℝ} (hB : g₀ z ≠ 0 → p * #({w | e < G w z / f} : Finset V) ≤ B) + (hKc : 4 * (1 + B) ≤ Kc) : + 𝔼 d ∈ ({s | X s x} : Finset ι) ×ˢ (univ : Finset κ), + correctionAtom I τ K Kc f G X Z Zt Q h ρ g₀ d x z = + (dens {t | Zt t z} : ℝ) * (Q (G x z / f) * g₀ z) := by + have hmean := expect_correctionAtom hSx hSz hQh hρ0 hρ1 hη hρη hτ0 hτ1 hτ₀ hττ hI + hf hG0 hGM hc hK hpairZ hp hpairX hB hKc + have hsupport : ∀ s, (𝔼 t, correctionAtom I τ K Kc f G X Z Zt Q h ρ g₀ (s, t) x z) = + (dens {t | Zt t z} : ℝ) * 𝔼 t ∈ ({t | Zt t z} : Finset κ), + correctionAtom I τ K Kc f G X Z Zt Q h ρ g₀ (s, t) x z := by + intro s + refine expect_eq_dens_mul_expect_of_eq_zero _ _ fun t ht => ?_ + have hnot : ¬ Zt t z := by simpa using ht + simp [correctionAtom, hnot] + rw [expect_product] + simp_rw [hsupport] + rw [← mul_expect, ← expect_product', hmean] + +/-- **The true correction--dense product mean** [OpenAI2026LogSpace, Lemma 7.1]. Average the +actual sample over the source slice, all intermediate seeds, and the broad terminal slice. +The terminal density ratio changes to the usage slice; `f / πf` cancels intermediate sampling. +The result is the product of the two deterministic entries in their original matrix units. + +The uniform intermediate hit probability is stated as the actual density equality `hZπ`. +All atom normalizations follow from their gate and pair-count hypotheses; none are postulated +as mean identities. The true right atom only uses the third seed coordinate. -/ +theorem expect_correctionAtom_mul_denseAtom {υ : Type*} [Fintype υ] + {I : ℝ → ℝ → ℝ} {τ Q hF ρF k hB ρB : ℝ → ℝ} {KF Kc KB : ℕ} + {f b πf : ℝ} {G H : Matrix V V ℝ} {g₀ : V → ℝ} + {X : ι → V → Prop} {Z Zt : κ → V → Prop} {Y Ya Yt : υ → V → Prop} + [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Z t v)] [∀ t v, Decidable (Zt t v)] + [∀ t v, Decidable (Y t v)] [∀ t v, Decidable (Ya t v)] [∀ t v, Decidable (Yt t v)] + {x y : V} (hSx : ({s | X s x} : Finset ι).Nonempty) + (hZπ : ∀ z, (dens {t | Zt t z} : ℝ) = πf) (hπf : 0 < πf) + (hYt : ∀ t, Yt t y → Ya t y) (hSy : ({t | Yt t y} : Finset υ).Nonempty) + (hQh : ∀ v, Q v ≠ 0 → hF v = 1) (hρF0 : ∀ r, 0 ≤ ρF r) (hρF1 : ∀ r, ρF r ≤ 1) + {ηF : ℝ} (hηF : 0 < ηF) (hρFη : ∀ r, r ≤ ηF → ρF 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) {MF : ℝ} (hGM : ∑ w, G x w ≤ MF) + {cF : ℝ} (hcF : 0 ≤ cF) (hKF : 4 * (1 + cF * MF / ηF) ≤ KF) + (hpairZ : ∀ z w, w ≠ z → (#{t | Zt t z ∧ Z t w} : ℝ) ≤ cF * f * #{t | Zt t z}) + {p : ℝ} (hp : 0 ≤ p) + (hpairX : ∀ w, w ≠ x → (#{s | X s x ∧ X s w} : ℝ) ≤ p * #{s | X s x}) + {R : ℝ} (hR : ∀ z, g₀ z ≠ 0 → p * #({w | e < G w z / f} : Finset V) ≤ R) + (hKc : 4 * (1 + R) ≤ Kc) + (hkh : ∀ v, k v ≠ 0 → hB v = 1) (hρB0 : ∀ r, 0 ≤ ρB r) (hρB1 : ∀ r, ρB r ≤ 1) + {ηB : ℝ} (hηB : 0 < ηB) (hρBη : ∀ r, r ≤ ηB → ρB r = 1) (hb : 0 < b) + (hH0 : ∀ z w, 0 ≤ H z w) {MB : ℝ} (hHM : ∀ z, ∑ w, H z w ≤ MB) + {cB : ℝ} (hcB : 0 ≤ cB) (hKB : 2 * (1 + cB * MB / ηB) ≤ KB) + (hpairY : ∀ w, w ≠ y → (#{t | Yt t y ∧ Y t w} : ℝ) ≤ cB * b * #{t | Yt t y}) : + 𝔼 d ∈ (({s | X s x} : Finset ι) ×ˢ (univ : Finset κ)) ×ˢ ({t | Ya t y} : Finset υ), + b * ((dens {t | Ya t y} : ℝ) / dens {t | Yt t y}) * (f / πf) * + ∑ z, correctionAtom I τ KF Kc f G X Z Zt Q hF ρF g₀ d.1 x z * + denseAtom Y Yt k hB ρB KB b H d.2 z y = + ∑ z, (f * Q (G x z / f) * g₀ z) * (b * k (H z y / b)) := by + have hSz : ∀ z, ({t | Zt t z} : Finset κ).Nonempty := by + intro z + have hpos : (0 : ℝ) < dens {t | Zt t z} := by rw [hZπ]; exact hπf + refine dens_ne_zero.mp ?_ + intro hz + rw [hz] at hpos + norm_num at hpos + have hleft : ∀ z, (𝔼 d ∈ ({s | X s x} : Finset ι) ×ˢ (univ : Finset κ), + correctionAtom I τ KF Kc f G X Z Zt Q hF ρF g₀ d x z) = + πf * (Q (G x z / f) * g₀ z) := by + intro z + rw [expect_correctionAtom_unconditioned hSx (hSz z) hQh hρF0 hρF1 hηF hρFη hτ0 hτ1 + hτ₀ hττ hI hf hG0 hGM hcF hKF (hpairZ z) hp hpairX (hR z) hKc, hZπ] + have hright : ∀ z, (𝔼 t ∈ ({t | Ya t y} : Finset υ), + b * ((dens {t | Ya t y} : ℝ) / dens {t | Yt t y}) * + denseAtom Y Yt k hB ρB KB b H t z y) = b * k (H z y / b) := by + intro z + exact expect_denseAtom_change_usage hYt hSy hkh hρB0 hρB1 hηB hρBη hb (hH0 z) + (hHM z) hcB hKB hpairY + simp_rw [mul_sum] + rw [expect_sum_comm] + refine sum_congr rfl fun z _ => ?_ + rw [expect_product] + calc + _ = 𝔼 l ∈ ({s | X s x} : Finset ι) ×ˢ (univ : Finset κ), + 𝔼 t ∈ ({t | Ya t y} : Finset υ), + ((f / πf) * correctionAtom I τ KF Kc f G X Z Zt Q hF ρF g₀ l x z) * + (b * ((dens {t | Ya t y} : ℝ) / dens {t | Yt t y}) * + denseAtom Y Yt k hB ρB KB b H t z y) := by + refine expect_congr rfl fun l _ => expect_congr rfl fun t _ => ?_ + ring + _ = _ := by + rw [← expect_mul_expect, ← mul_expect, hleft z, hright z] + field_simp + +end Matrix diff --git a/ComplexityTests/SourceRelease.lean b/ComplexityTests/SourceRelease.lean new file mode 100644 index 0000000000..466bb1d79c --- /dev/null +++ b/ComplexityTests/SourceRelease.lean @@ -0,0 +1,138 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ +import Complexity.Foundations.Probability.SourceRelease +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Tests for source release + +The examples check the double-counting bound, a sharp `f / u = 2` cost with an environment- +dependent relation and error, and source release through a nonzero concrete correction atom. +-/ + +namespace ComplexityTests.SourceRelease + +open Finset Matrix Cslib +open scoped BigOperators + +-- Exactly two of three sources contribute to both targets, whose weights are `3` and `7`. +example : ∑ x : Fin 3, ∑ z ∈ (univ : Finset (Fin 2)) with x ≠ 2, (![3, 7] : Fin 2 → ℝ) z ≤ + 2 * ∑ z : Fin 2, (![3, 7] : Fin 2 → ℝ) z := by + refine sum_sum_filter_le_mul_sum_of_card_le univ univ (fun x _ => x ≠ 2) ?_ ?_ + · intro z _ + fin_cases z <;> norm_num + · intro z _ + decide + +/-- Both the support relation and the error depend on this same two-point environment. -/ +private def error (σ : Fin 2) (_ _ : Fin 2) : ℝ := if σ = 0 then 2 else 3 + +private noncomputable def releasedTableError : ℝ := + (2 * (1 / 2))⁻¹ * 𝔼 σ : Fin 2, ∑ x : Fin 2, + ∑ z ∈ ({z | z = σ} : Finset (Fin 2)) with x = σ, + ∑ y ∈ ({y | y = 0} : Finset (Fin 2)), |error σ z y| ^ 4 + +-- The degree bound is one, while the rate change doubles the child's norm power. +example : releasedTableError ≤ 2 * rowNormPow 4 2 1 (fun σ z : Fin 2 => z = σ) + (fun (_ : Fin 2) (y : Fin 2) => y = 0) error := by + have h := sourceRelease_le_rowNormPow (s := 4) (N := 2) (u := 1 / 2) (f := 1) + (X := fun (_ : Fin 2) (_ : Fin 2) => True) (Z := fun σ z => z = σ) + (Y := fun _ y => y = 0) (by norm_num) (by norm_num) (by norm_num) + (fun σ x _ => x = σ) (K := 1) (fun σ z _ => by simp [filter_eq']) error + simpa [releasedTableError] using h + +example : releasedTableError = 97 / 2 := by + norm_num [releasedTableError, error, expect_eq_sum_div_card, sum_filter, Fin.sum_univ_two, + filter_eq'] + +example : rowNormPow 4 2 1 (fun σ z : Fin 2 => z = σ) + (fun (_ : Fin 2) (y : Fin 2) => y = 0) error = 97 / 4 := by + norm_num [rowNormPow, error, expect_eq_sum_div_card, sum_filter, Fin.sum_univ_two, filter_eq'] + +-- The vector API uses the same common environment, with no independence assumptions. +example : (2 * (1 / 2) : ℝ)⁻¹ * 𝔼 σ : Fin 2, ∑ x : Fin 2, + ∑ z ∈ ({z | z = σ} : Finset (Fin 2)) with x = σ, |error σ z 0| ^ 4 ≤ + 2 * vertexNormPow 4 2 1 (fun σ z : Fin 2 => z = σ) (fun σ z => error σ z 0) := by + have h := sourceRelease_le_vertexNormPow (s := 4) (N := 2) (u := 1 / 2) (f := 1) + (X := fun (_ : Fin 2) (_ : Fin 2) => True) (Z := fun σ z => z = σ) + (by norm_num) (by norm_num) (by norm_num) (fun σ x _ => x = σ) (K := 1) + (fun σ z _ => by simp [filter_eq']) (fun σ z => error σ z 0) + simpa using h + +/-! ### A concrete correction atom -/ + +/-- A single nonzero entry, from vertex `0` to vertex `1`. -/ +private def G (x z : Fin 2) : ℝ := if x = 0 ∧ z = 1 then 1 else 0 + +private noncomputable def score (v _ : ℝ) : ℝ := if v = 0 then 0 else 1 + +private noncomputable def gate (r : ℝ) : ℝ := if r < 1 then 1 else 0 + +private abbrev full (_ : Unit) (_ : Fin 2) : Prop := True + +private noncomputable def atom (d : Unit × Unit) (x z : Fin 2) : ℝ := + correctionAtom score gate 3 2 1 G full full full id (fun _ => 1) (fun _ => 1) (fun _ => 1) d x z + +private theorem score_one (v r : ℝ) (hv : id v ≠ 0) (_ : (1 : ℝ) ≠ 0) : score v r = 1 := by + simpa only [id_eq, score, ite_eq_right_iff, zero_ne_one, imp_false] using hv + +private theorem gate_zero (r : ℝ) (hr : 1 ≤ r) : gate r = 0 := by + exact ite_eq_right (not_lt.mpr hr) + +private theorem incoming_one (z : Fin 2) : + incomingGate score gate 3 2 1 G univ univ z = 1 := by + have hcard : #{x : Fin 2 | 1 ≤ auxScore score 3 1 G univ x z} < 2 := by + fin_cases z <;> norm_num [auxScore, score, G, univ_fin2, filter_insert, filter_singleton] + have hlt : kthLargest 2 univ (fun x => auxScore score 3 1 G univ x z) < 1 := by + exact lt_of_not_ge fun h => hcard.not_ge ((le_kthLargest_iff (by decide) zero_lt_one).mp h) + exact ite_eq_left hlt + +-- The test is nonzero: the atom keeps the unique edge and its normalizer is one. +private theorem atom_eq (d : Unit × Unit) (x z : Fin 2) : atom d x z = G x z := by + have hnorm : correctionNormalizer score gate 3 2 1 G full full full (fun _ => 1) + (fun _ => 1) x z = 1 := by + simp [correctionNormalizer, correctionPrep, rowGate, full, incoming_one] + norm_num [atom, correctionAtom, rowGate, full, incoming_one, hnorm] + +example : atom ((), ()) 0 1 = 1 := by rw [atom_eq]; norm_num [G] + +-- An additional environment coordinate can govern the right error without changing atom seeds. +-- The incoming cap is discharged by the correction-atom theorem, not supplied as an assumption. +example : (2 * (1 / 2) : ℝ)⁻¹ * 𝔼 σ : Fin 2, ∑ x : Fin 2, + ∑ z ∈ (univ : Finset (Fin 2)) with atom ((), ()) x z ≠ 0, + ∑ y : Fin 2, |error σ z y| ^ 4 ≤ + 4 * rowNormPow 4 2 1 (fun (_ : Fin 2) (_ : Fin 2) => True) + (fun _ _ => True) error := by + have h := correctionAtom_sourceRelease_le_rowNormPow (K := 3) (Kc := 2) (s := 4) + (N := 2) (u := 1 / 2) (f := 1) (I := score) (τ := gate) (Q := id) + (h := fun _ => 1) (ρ := fun _ => 1) (G := G) (g₀ := fun _ => 1) + (X := full) (Y := full) (Yt := full) (fun _ : Fin 2 => ((), ())) (fun _ _ => True) + (by norm_num) (by norm_num) (by norm_num) (by decide) score_one (g := 1) le_rfl gate_zero error + norm_num [full, atom] at h ⊢ + exact h + +example : (2 * (1 / 2) : ℝ)⁻¹ * 𝔼 σ : Fin 2, ∑ x : Fin 2, + ∑ z ∈ (univ : Finset (Fin 2)) with atom ((), ()) x z ≠ 0, |error σ z 0| ^ 4 ≤ + 4 * vertexNormPow 4 2 1 (fun (_ : Fin 2) (_ : Fin 2) => True) + (fun σ z => error σ z 0) := by + have h := correctionAtom_sourceRelease_le_vertexNormPow (K := 3) (Kc := 2) (s := 4) + (N := 2) (u := 1 / 2) (f := 1) (I := score) (τ := gate) (Q := id) + (h := fun _ => 1) (ρ := fun _ => 1) (G := G) (g₀ := fun _ => 1) + (X := full) (Y := full) (Yt := full) (fun _ : Fin 2 => ((), ())) + (by norm_num) (by norm_num) (by norm_num) (by decide) score_one (g := 1) le_rfl gate_zero + (fun σ z => error σ z 0) + norm_num [full, atom] at h ⊢ + exact h + +-- The analogous vector error has positive mass, equal to `E[2^4, 3^4] = 97/2`. +example : (2 * (1 / 2) : ℝ)⁻¹ * 𝔼 σ : Fin 2, ∑ x : Fin 2, + ∑ z ∈ (univ : Finset (Fin 2)) with atom ((), ()) x z ≠ 0, |error σ z 0| ^ 4 = 97 / 2 := by + simp only [atom_eq] + norm_num [error, G, expect_eq_sum_div_card, sum_filter, Fin.sum_univ_two, filter_eq'] + +end ComplexityTests.SourceRelease diff --git a/ComplexityTests/TrueSampleMeans.lean b/ComplexityTests/TrueSampleMeans.lean new file mode 100644 index 0000000000..d1b237e827 --- /dev/null +++ b/ComplexityTests/TrueSampleMeans.lean @@ -0,0 +1,158 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ +import Complexity.Foundations.Probability.TrueSampleMeans +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Tests for the true sampled means + +The source and intermediate channels each retain on one of two seeds. The broad terminal slice +has two of four seeds; its usage slice has only one. Both correction factors are therefore two. +The correction edge `0 → 1` has weight `1/2`, and the dense edge `1 → 0` has weight `1/3`. +The product sample is `2/3` on one of its four conditioning draws and zero on the others, giving +the prescribed positive product `1/6`. +-/ + +namespace ComplexityTests.TrueSampleMeans + +open Finset Matrix +open scoped BigOperators + +private abbrev X (s : Bool) (_ : Fin 2) : Prop := s = true +private abbrev Z (t : Bool) (_ : Fin 2) : Prop := t = true +private abbrev Y (_ : Fin 4) (_ : Fin 2) : Prop := True +private abbrev Ya (t : Fin 4) (_ : Fin 2) : Prop := t.val < 2 +private abbrev Yt (t : Fin 4) (_ : Fin 2) : Prop := t = 0 + +private noncomputable def left (x z : Fin 2) : ℝ := if x = 0 ∧ z = 1 then 1 / 2 else 0 +private noncomputable def right (z y : Fin 2) : ℝ := if z = 1 ∧ y = 0 then 1 / 3 else 0 + +private theorem source_slice (x : Fin 2) : ({s | X s x} : Finset Bool) = {true} := by + change ({s | s = true} : Finset Bool) = {true} + decide + +private theorem middle_slice (z : Fin 2) : ({t | Z t z} : Finset Bool) = {true} := by + change ({t | t = true} : Finset Bool) = {true} + decide + +private theorem broad_slice (y : Fin 2) : ({t | Ya t y} : Finset (Fin 4)) = {0, 1} := by + change ({t : Fin 4 | t.val < 2} : Finset (Fin 4)) = {0, 1} + decide + +private theorem usage_slice (y : Fin 2) : ({t | Yt t y} : Finset (Fin 4)) = {0} := by + change ({t | t = 0} : Finset (Fin 4)) = {0} + decide + +private theorem middle_density (z : Fin 2) : (dens {t | Z t z} : ℝ) = 1 / 2 := by + rw [middle_slice, dens_eq_card_div_card] + norm_num + +private theorem broad_density (y : Fin 2) : (dens {t | Ya t y} : ℝ) = 1 / 2 := by + rw [broad_slice, dens_eq_card_div_card] + norm_num + +private theorem usage_density (y : Fin 2) : (dens {t | Yt t y} : ℝ) = 1 / 4 := by + rw [usage_slice, dens_eq_card_div_card] + norm_num + +private theorem usage_subset (y : Fin 2) (t : Fin 4) (ht : Yt t y) : Ya t y := by + rcases ht with rfl + norm_num [Ya] + +private theorem column_support (z : Fin 2) : #{w : Fin 2 | 0 < left w z} ≤ 1 := by + refine card_le_one.2 fun u hu v hv => ?_ + have hu0 : u = 0 := by + by_contra h + simp [left, h] at hu + have hv0 : v = 0 := by + by_contra h + simp [left, h] at hv + exact hu0.trans hv0.symm + +private noncomputable def correction (d : Bool × Bool) (x z : Fin 2) : ℝ := + correctionAtom (fun _ _ => 0) (fun _ => 1) 8 8 1 left X Z Z id (fun _ => 1) + (fun _ => 1) (fun _ => 1) d x z + +private noncomputable def dense (t : Fin 4) (z y : Fin 2) : ℝ := + denseAtom Y Yt id (fun _ => 1) (fun _ => 1) 4 1 right t z y + +private theorem correction_eq (d : Bool × Bool) (x z : Fin 2) : + correction d x z = if d.2 = true then left x z else 0 := by + have hn : correctionNormalizer (fun _ _ => 0) (fun _ => 1) 8 8 1 left X Z Z + (fun _ => 1) (fun _ => 1) x z = 1 := by + simp [correctionNormalizer, correctionPrep, rowGate, incomingGate, X, Z, filter_eq'] + norm_num [correction, correctionAtom, rowGate, incomingGate, Z, hn] + +private theorem dense_eq (t : Fin 4) (z y : Fin 2) : + dense t z y = if t = 0 then right z y else 0 := by + norm_num [dense, denseAtom, atomNormalizer, atomPrep, rowGate, Yt, filter_eq'] + +private noncomputable def sample (d : (Bool × Bool) × Fin 4) : ℝ := + 4 * ∑ z, correction d.1 0 z * dense d.2 z 0 + +-- Both scalar corrections are nontrivial, and the integrand is genuinely nonzero. +example : (dens {t | Ya t 0} : ℝ) / dens {t | Yt t 0} = 2 ∧ + (1 : ℝ) / dens {t | Z t 0} = 2 := by + rw [broad_density, usage_density, middle_density] + norm_num + +example : sample ((true, true), 0) = 2 / 3 := by + norm_num [sample, correction_eq, dense_eq, left, right, Fin.sum_univ_two] + +example : sample ((true, false), 0) = 0 ∧ sample ((true, true), 1) = 0 := by + norm_num [sample, correction_eq, dense_eq, left, right, Fin.sum_univ_two] + +-- The direct term changes from the two-draw broad slice to the singleton usage slice. +private theorem direct_mean : + 𝔼 t ∈ ({t | Ya t 0} : Finset (Fin 4)), 2 * dense t 1 0 = 1 / 3 := by + have h := expect_denseAtom_change_usage (Y := Y) (Ya := Ya) (Yt := Yt) (k := id) + (h := fun _ => 1) (ρ := fun _ => 1) (K := 4) (b := 1) (G := right) (x := 1) (y := 0) + (usage_subset 0) ⟨0, by decide⟩ (fun _ _ => rfl) (fun _ => zero_le_one) (fun _ => le_rfl) + (η := 1) one_pos (fun _ _ => rfl) one_pos + (fun w => by fin_cases w <;> norm_num [right]) (M := 1) (by norm_num [right, Fin.sum_univ_two]) + (c := 1) zero_le_one (by norm_num) (fun w _ => by simp [Y, Yt]) + rw [broad_density, usage_density] at h + norm_num [dense, right] at h ⊢ + exact h + +-- Adding the independent source conditioning leaves the direct mean unchanged. +example : 𝔼 d ∈ ({s | X s 1} : Finset Bool) ×ˢ ({t | Ya t 0} : Finset (Fin 4)), + 2 * dense d.2 1 0 = 1 / 3 := by + rw [expect_product] + simp only [direct_mean, source_slice, expect_singleton] + +-- The product theorem is applied with every gate, pair-count and density hypothesis discharged. +-- In particular the coefficient `f / πf = 2` is justified by the actual middle-channel density. +example : 𝔼 d ∈ (({s | X s 0} : Finset Bool) ×ˢ (univ : Finset Bool)) ×ˢ + ({t | Ya t 0} : Finset (Fin 4)), sample d = 1 / 6 := by + have h := expect_correctionAtom_mul_denseAtom + (I := fun _ _ => 0) (τ := fun _ => 1) (Q := id) (hF := fun _ => 1) (ρF := fun _ => 1) + (k := id) (hB := fun _ => 1) (ρB := fun _ => 1) (KF := 8) (Kc := 8) (KB := 4) + (f := 1) (b := 1) (πf := 1 / 2) (G := left) (H := right) (g₀ := fun _ => 1) + (X := X) (Z := Z) (Zt := Z) (Y := Y) (Ya := Ya) (Yt := Yt) (x := 0) (y := 0) + (hSx := ⟨true, by decide⟩) (hZπ := middle_density) (hπf := by norm_num) + (hYt := usage_subset 0) (hSy := ⟨0, by decide⟩) + (hQh := fun _ _ => rfl) (hρF0 := fun _ => zero_le_one) (hρF1 := fun _ => le_rfl) + (ηF := 1) (hηF := one_pos) (hρFη := fun _ _ => rfl) + (hτ0 := fun _ => zero_le_one) (hτ1 := fun _ => le_rfl) (τ₀ := 0) (hτ₀ := le_rfl) + (hττ := fun _ _ => rfl) (e := 0) (hI := fun _ _ _ => rfl) + (hf := one_pos) (hG0 := fun w => by fin_cases w <;> norm_num [left]) + (MF := 1) (hGM := by norm_num [left, Fin.sum_univ_two]) (cF := 1) (hcF := zero_le_one) + (hKF := by norm_num) (hpairZ := fun z w _ => by simp [Z]) + (p := 1) (hp := zero_le_one) (hpairX := fun w _ => by simp [X]) + (R := 1) (hR := fun z _ => by simpa using column_support z) + (hKc := by norm_num) (hkh := fun _ _ => rfl) (hρB0 := fun _ => zero_le_one) + (hρB1 := fun _ => le_rfl) (ηB := 1) (hηB := one_pos) (hρBη := fun _ _ => rfl) + (hb := one_pos) (hH0 := fun z w => by fin_cases z <;> fin_cases w <;> norm_num [right]) + (MB := 1) (hHM := fun z => by fin_cases z <;> norm_num [right, Fin.sum_univ_two]) + (cB := 1) (hcB := zero_le_one) (hKB := by norm_num) (hpairY := fun w _ => by simp [Y, Yt]) + rw [broad_density, usage_density] at h + norm_num [sample, correction, dense, left, right, Fin.sum_univ_two] at h ⊢ + exact h + +end ComplexityTests.TrueSampleMeans