diff --git a/Complexity.lean b/Complexity.lean index 9a3bc3cde..9c528a2fc 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2724,6 +2724,7 @@ public import Complexity.Foundations.Order.Changes public import Complexity.Foundations.Order.UpperLower public import Complexity.Foundations.Probability.AtomCutoffs public import Complexity.Foundations.Probability.ColumnDetector +public import Complexity.Foundations.Probability.ConditionalProductMean public import Complexity.Foundations.Probability.CorrectionAtom public import Complexity.Foundations.Probability.DetectedHierarchy public import Complexity.Foundations.Probability.DetectedStage @@ -2731,9 +2732,12 @@ public import Complexity.Foundations.Probability.Gaussian.Multivariate public import Complexity.Foundations.Probability.Gaussian.Real public import Complexity.Foundations.Probability.Gaussian.Sheppard public import Complexity.Foundations.Probability.HierarchyParams +public import Complexity.Foundations.Probability.ProductError 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/ConditionalProductMean.lean b/Complexity/Foundations/Probability/ConditionalProductMean.lean new file mode 100644 index 000000000..3f25a9ce4 --- /dev/null +++ b/Complexity/Foundations/Probability/ConditionalProductMean.lean @@ -0,0 +1,240 @@ +/- +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.ProductError +public import Complexity.Foundations.Probability.TrueSampleMeans +public import Complexity.Foundations.Analysis.RootError +import Mathlib.Algebra.Order.BigOperators.Expect +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Conditional product means + +The conditioning event for a source `x` and endpoint `y` is the actual finite slice +`{σ | X σ x ∧ Y σ y}`. Its mean is `Cslib.conditionalTableMean`. The homogeneous loss +contracts through this finite expectation; multiplication by the slice's actual density +cancels the conditioning denominator before the source and endpoint sums are taken. +Empty slices have mean zero and need no nonemptiness hypothesis. + +The resulting root-metric comparison consumes the concrete coupled product estimate of +`Complexity.Foundations.Probability.ProductError`. For a coarse bin `b ≥ a`, the common +coefficient is `(b / a) * (f / πf)`: homogeneity contributes one factor `b / a`, and source +release contributes exactly `f / u` to the right error. The conservative comparison constant +is `(2 ^ (s - 1) * s ^ s) * (2 ^ (2 * (s - 1)) * s ^ s)`. + +The product-seed slice identity connects this finite operator to the actual true-atom +expectation in `Matrix.expect_correctionAtom_mul_denseAtom`. No estimator mean or error +contract is assumed. Fine-bin conditioning changes, domination of true signed contributions, +and the recursive estimator remain separate. + +## Main results + +* `Cslib.dens_mul_homogeneousLoss_expect_le`: finite conditional contraction with exact density. +* `Cslib.rootDistPow_conditionalTableMean_mul_le`: the integrated root-error comparison. +* `Cslib.rootDistPow_coarseProductMean_le`: the coarse-bin coefficient and source release. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Sections 7.2--7.3, Lemmas 7.1--7.3, September 23, 2026 revision `7ef5c0cc` + (preprint, not peer reviewed). +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Cslib + +/-- The homogeneous loss contracts through an actual finite mean, including the empty mean. -/ +theorem homogeneousLoss_expect_le {Ω : Type*} (S : Finset Ω) {s : ℕ} (hs : s ≠ 0) + {H H' : Ω → ℝ} (hH : ∀ σ ∈ S, 0 ≤ H σ) (hH' : ∀ σ ∈ S, 0 ≤ H' σ) : + homogeneousLoss s (𝔼 σ ∈ S, H σ) (𝔼 σ ∈ S, H' σ) ≤ + 𝔼 σ ∈ S, homogeneousLoss s (H σ) (H' σ) := by + simpa only [expect_eq_sum_div_card, div_eq_inv_mul, mul_sum] using + homogeneousLoss_sum_le S hs (w := fun _ => (#S : ℝ)⁻¹) + (fun _ _ => by positivity) hH hH' + +/-- Multiplying by the actual conditioning density cancels the conditional denominator. +All quantities may depend on the same draw, and the slice may be empty. -/ +theorem dens_mul_homogeneousLoss_expect_le {Ω : Type*} [Fintype Ω] [DecidableEq Ω] (S : Finset Ω) + {s : ℕ} (hs : s ≠ 0) {H H' : Ω → ℝ} + (hH : ∀ σ ∈ S, 0 ≤ H σ) (hH' : ∀ σ ∈ S, 0 ≤ H' σ) : + (dens S : ℝ) * homogeneousLoss s (𝔼 σ ∈ S, H σ) (𝔼 σ ∈ S, H' σ) ≤ + 𝔼 σ, if σ ∈ S then homogeneousLoss s (H σ) (H' σ) else 0 := by + classical + calc + _ ≤ (dens S : ℝ) * 𝔼 σ ∈ S, homogeneousLoss s (H σ) (H' σ) := + mul_le_mul_of_nonneg_left (homogeneousLoss_expect_le S hs hH hH') (by positivity) + _ = _ := by + rw [expect_eq_dens_mul_expect_of_eq_zero S _ (fun σ hσ => ite_eq_right hσ)] + congr 1 + exact expect_congr rfl fun σ hσ => (ite_eq_left hσ).symm + +private theorem dens_mul_root_expect_sub_pow_le {Ω : Type*} [Fintype Ω] [DecidableEq Ω] + (S : Finset Ω) {s : ℕ} (hs : s ≠ 0) {c : ℝ} (hc : 0 ≤ c) {H H' : Ω → ℝ} + (hH : ∀ σ ∈ S, 0 ≤ H σ) (hH' : ∀ σ ∈ S, 0 ≤ H' σ) : + (dens S : ℝ) * |(c * 𝔼 σ ∈ S, H σ) ^ (s⁻¹ : ℝ) - + (c * 𝔼 σ ∈ S, H' σ) ^ (s⁻¹ : ℝ)| ^ s ≤ + (2 ^ (s - 1) * (s : ℝ) ^ s) * c * + 𝔼 σ, if σ ∈ S then |H σ ^ (s⁻¹ : ℝ) - H' σ ^ (s⁻¹ : ℝ)| ^ s else 0 := by + classical + have hmean := rpow_inv_sub_pow_le_homogeneousLoss hs + (mul_nonneg hc (expect_nonneg hH)) (mul_nonneg hc (expect_nonneg hH')) + have hpoint : (𝔼 σ, if σ ∈ S then homogeneousLoss s (H σ) (H' σ) else 0) ≤ + (s : ℝ) ^ s * 𝔼 σ, if σ ∈ S then |H σ ^ (s⁻¹ : ℝ) - H' σ ^ (s⁻¹ : ℝ)| ^ s else 0 := by + rw [mul_expect] + refine expect_le_expect fun σ _ => ?_ + split_ifs with hσ + · exact homogeneousLoss_le_rpow_inv_sub_pow hs (hH σ hσ) (hH' σ hσ) + · simp + calc + _ ≤ (dens S : ℝ) * (2 ^ (s - 1) * homogeneousLoss s + (c * 𝔼 σ ∈ S, H σ) (c * 𝔼 σ ∈ S, H' σ)) := + mul_le_mul_of_nonneg_left hmean (by positivity) + _ = (2 ^ (s - 1) * c) * ((dens S : ℝ) * homogeneousLoss s + (𝔼 σ ∈ S, H σ) (𝔼 σ ∈ S, H' σ)) := by + rw [homogeneousLoss_mul hs hc] + ring + _ ≤ (2 ^ (s - 1) * c) * + 𝔼 σ, if σ ∈ S then homogeneousLoss s (H σ) (H' σ) else 0 := + mul_le_mul_of_nonneg_left (dens_mul_homogeneousLoss_expect_le S hs hH hH') (by positivity) + _ ≤ (2 ^ (s - 1) * c) * ((s : ℝ) ^ s * + 𝔼 σ, if σ ∈ S then |H σ ^ (s⁻¹ : ℝ) - H' σ ^ (s⁻¹ : ℝ)| ^ s else 0) := + mul_le_mul_of_nonneg_left hpoint (by positivity) + _ = _ := by ring + +variable {Ω V : Type*} [Fintype Ω] [Fintype V] + +/-- The actual finite conditional mean on the source/endpoint slice. It is zero when that +slice is empty. The output is a deterministic table, indexed by the source and endpoint. -/ +@[expose] noncomputable def conditionalTableMean (X Y : Ω → V → Prop) + [∀ σ x, Decidable (X σ x)] [∀ σ y, Decidable (Y σ y)] + (H : Ω → V → V → ℝ) (x y : V) : ℝ := + 𝔼 σ ∈ ({σ | X σ x ∧ Y σ y} : Finset Ω), H σ x y + +omit [Fintype V] in +/-- With separate source, intermediate and terminal seed coordinates, the actual slice is +exactly the product slice used by `Matrix.expect_correctionAtom_mul_denseAtom`. -/ +theorem conditionalTableMean_eq_expect_product {ι κ υ : Type*} + [Fintype ι] [Fintype κ] [Fintype υ] (X : ι → V → Prop) (Y : υ → V → Prop) + [∀ t x, Decidable (X t x)] [∀ t y, Decidable (Y t y)] + (H : ((ι × κ) × υ) → V → V → ℝ) (x y : V) : + conditionalTableMean (fun d v => X d.1.1 v) (fun d v => Y d.2 v) H x y = + 𝔼 d ∈ (({t | X t x} : Finset ι) ×ˢ (univ : Finset κ)) ×ˢ ({t | Y t y} : Finset υ), + H d x y := by + unfold conditionalTableMean + congr 1 + ext d + simp + +variable {s : ℕ} {N u : ℝ} {X Y : Ω → V → Prop} + [∀ σ x, Decidable (X σ x)] [∀ σ y, Decidable (Y σ y)] + +private theorem expect_filtered_sum_eq (H : Ω → V → V → ℝ) : + (𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), H σ x y) = + ∑ x, ∑ y, 𝔼 σ, if X σ x ∧ Y σ y then H σ x y else 0 := by + have hpoint : ∀ σ, + (∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), H σ x y) = + ∑ x, ∑ y, if X σ x ∧ Y σ y then H σ x y else 0 := by + intro σ + rw [sum_filter] + refine sum_congr rfl fun x _ => ?_ + by_cases hx : X σ x + · simp [hx, sum_filter] + · simp [hx] + simp_rw [hpoint] + rw [expect_sum_comm] + exact sum_congr rfl fun x _ => expect_sum_comm _ _ _ + +private theorem expect_mask_const [DecidableEq Ω] (S : Finset Ω) (c : ℝ) : + (𝔼 σ, if σ ∈ S then c else 0) = (dens S : ℝ) * c := by + classical + rcases S.eq_empty_or_nonempty with rfl | hS + · simp + · simpa only [NNRat.smul_def, expect_const hS] using Fintype.expect_ite_mem S (fun _ => c) + +/-- **Integrated conditional-mean comparison**. Multiplication by the same nonnegative scalar +costs one power of that scalar. The actual conditioning density cancels before summing over +source and endpoint coordinates. Neither nonempty slices nor independence are required. -/ +theorem rootDistPow_conditionalTableMean_mul_le (hs : s ≠ 0) (hN : 0 < N) (hu : 0 < u) + {c : ℝ} (hc : 0 ≤ c) {H H' : Ω → V → V → ℝ} + (hH : ∀ σ x y, 0 ≤ H σ x y) (hH' : ∀ σ x y, 0 ≤ H' σ x y) : + rootDistPow s N u X Y (fun _ x y => c * conditionalTableMean X Y H x y) + (fun _ x y => c * conditionalTableMean X Y H' x y) ≤ + (2 ^ (s - 1) * (s : ℝ) ^ s) * c * rootDistPow s N u X Y H H' := by + classical + rw [rootDistPow, rowNormPow, expect_filtered_sum_eq] + calc + _ ≤ (N * u)⁻¹ * ∑ x, ∑ y, (2 ^ (s - 1) * (s : ℝ) ^ s) * c * + 𝔼 σ, if X σ x ∧ Y σ y then |H σ x y ^ (s⁻¹ : ℝ) - H' σ x y ^ (s⁻¹ : ℝ)| ^ s else 0 := by + refine mul_le_mul_of_nonneg_left (sum_le_sum fun x _ => sum_le_sum fun y _ => ?_) + (by positivity) + have hmask := expect_mask_const ({σ | X σ x ∧ Y σ y} : Finset Ω) + (|(c * conditionalTableMean X Y H x y) ^ (s⁻¹ : ℝ) - + (c * conditionalTableMean X Y H' x y) ^ (s⁻¹ : ℝ)| ^ s) + simp only [mem_filter, mem_univ, true_and] at hmask + rw [hmask] + simpa only [conditionalTableMean, mem_filter, mem_univ, true_and] using + dens_mul_root_expect_sub_pow_le ({σ | X σ x ∧ Y σ y} : Finset Ω) hs hc + (fun σ _ => hH σ x y) (fun σ _ => hH' σ x y) + _ = _ := by + rw [rootDistPow, rowNormPow, expect_filtered_sum_eq] + simp only [← mul_sum] + ring + +/-- **Coarse-bin conditional product comparison**. The sample is the actual finite product +mean multiplied by `(b / a) * (f / πf)`, as in (7.2) after division by `a`, with `b ≥ a`. +The coefficient `f / πf` is left explicit; identifying `πf` with the intermediate channel's +uniform hit density is part of `Matrix.expect_correctionAtom_mul_denseAtom`. + +This estimate proves the single-power `b / a` cost and exact right-source factor `f / u`. +It concerns root error; clipped relative error additionally needs domination by the true raw +input, and the finer `b < a` bound requires changing terminal conditioning first. -/ +theorem rootDistPow_coarseProductMean_le {Z : Ω → V → Prop} + [∀ σ z, Decidable (Z σ z)] {a b f πf : ℝ} + (hs : s ≠ 0) (hN : 0 < N) (hu : 0 < u) (ha : 0 < a) (hab : a ≤ b) + (hf : 0 < f) (hπf : 0 < πf) {F F' B B' : Ω → V → V → ℝ} + (hF : ∀ σ x z, 0 ≤ F σ x z) (hF' : ∀ σ x z, 0 ≤ F' σ x z) + (hB : ∀ σ z y, 0 ≤ B σ z y) (hB' : ∀ σ z y, 0 ≤ B' σ z y) + {CF CB : ℝ} (hCF : 0 ≤ CF) (hCB : 0 ≤ CB) + (hFbound : ∀ σ x z, F' σ x z ≤ CF) (hBbound : ∀ σ z y, B σ z y ≤ CB) + {Kr Kc : ℕ} (hrow : ∀ σ z, Z σ z → #{y ∈ ({y | Y σ y} : Finset V) | B σ z y ≠ 0} ≤ Kr) + (hcol : ∀ σ z, Z σ z → #{x ∈ ({x | X σ x} : Finset V) | F' σ x z ≠ 0} ≤ Kc) : + let P := fun σ x y => ∑ z ∈ ({z | Z σ z} : Finset V), F σ x z * B σ z y + let P' := fun σ x y => ∑ z ∈ ({z | Z σ z} : Finset V), F' σ x z * B' σ z y + rootDistPow s N u X Y (fun _ x y => (b / a) * (f / πf) * conditionalTableMean X Y P x y) + (fun _ x y => (b / a) * (f / πf) * conditionalTableMean X Y P' x y) ≤ + ((2 ^ (s - 1) * (s : ℝ) ^ s) * (2 ^ (2 * (s - 1)) * (s : ℝ) ^ s)) * + ((b / a) * (f / πf)) * + (CB * Kr * rootDistPow s N u X Z F F' + + CF * Kc * (f / u) * rootDistPow s N f Z Y B B') := by + dsimp only + have hb : 0 ≤ b := ha.le.trans hab + have hc : 0 ≤ (b / a) * (f / πf) := by positivity + calc + _ ≤ (2 ^ (s - 1) * (s : ℝ) ^ s) * ((b / a) * (f / πf)) * + rootDistPow s N u X Y + (fun σ x y => ∑ z ∈ ({z | Z σ z} : Finset V), F σ x z * B σ z y) + (fun σ x y => ∑ z ∈ ({z | Z σ z} : Finset V), F' σ x z * B' σ z y) := + rootDistPow_conditionalTableMean_mul_le hs hN hu hc + (fun σ x y => sum_nonneg fun z _ => mul_nonneg (hF σ x z) (hB σ z y)) + (fun σ x y => sum_nonneg fun z _ => mul_nonneg (hF' σ x z) (hB' σ z y)) + _ ≤ (2 ^ (s - 1) * (s : ℝ) ^ s) * ((b / a) * (f / πf)) * + ((2 ^ (2 * (s - 1)) * (s : ℝ) ^ s) * + (CB * Kr * rootDistPow s N u X Z F F' + + CF * Kc * (f / u) * rootDistPow s N f Z Y B B')) := + mul_le_mul_of_nonneg_left + (rootDistPow_mul_le hs hN hu hf hF hF' hB hB' hCF hCB hFbound hBbound hrow hcol) + (by positivity) + _ = _ := by ring + +end Cslib diff --git a/Complexity/Foundations/Probability/ProductError.lean b/Complexity/Foundations/Probability/ProductError.lean new file mode 100644 index 000000000..d9c849a31 --- /dev/null +++ b/Complexity/Foundations/Probability/ProductError.lean @@ -0,0 +1,327 @@ +/- +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.SourceRelease +import Complexity.Foundations.Analysis.RootError +import Mathlib.Algebra.Order.BigOperators.Expect +import Mathlib.Algebra.Order.Ring.Basic +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Coupled product errors and source release + +For four nonnegative tables on one environment, compare the concrete products +`P σ x y = ∑ z ∈ Z σ, F σ x z * B σ z y` and `P'` built from `F'`, `B'`. +Splitting each product through `F' * B` charges the left error against the row support of `B` +and the right error against the incoming support of `F'`. The latter changes source rate from +`u` to `f` and has the exact normalization cost `f / u`. + +The root-metric estimate uses the homogeneous-loss mixture inequality and scalar product-root +comparison. Its explicit conservative constant is `2 ^ (2 * (s - 1)) * s ^ s`, or `16384` at +`s = 4`. All four tables may depend on the same environment. The right error is a common table +at `(z, y)`, with no additional old-source argument. + +This is the product and source-domain part of the proof of [OpenAI2026LogSpace, Lemma 7.3]. +The coarse/fine terminal scale comparisons and conditional-mean estimates remain separate. +No final-estimator or machine-space contract is assumed. + +## Main results + +* `Cslib.rootDistPow_mul_le`: a coupled product-table estimate with row and incoming caps. +* `Matrix.correctionAtom_denseAtom_rootDistPow_le`: the actual atom specialization, deriving + both support caps from the incoming and row gates. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + proof of Lemma 7.3, September 23, 2026 revision `7ef5c0cc` (preprint, not peer reviewed). +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Cslib + +private theorem root_mul_sub_pow_le {s : ℕ} (hs : s ≠ 0) {a a' b b' : ℝ} + (ha : 0 ≤ a) (ha' : 0 ≤ a') (hb : 0 ≤ b) (hb' : 0 ≤ b') : + |(a * b) ^ (s⁻¹ : ℝ) - (a' * b') ^ (s⁻¹ : ℝ)| ^ s ≤ + 2 ^ (s - 1) * (b * |a ^ (s⁻¹ : ℝ) - a' ^ (s⁻¹ : ℝ)| ^ s + + a' * |b ^ (s⁻¹ : ℝ) - b' ^ (s⁻¹ : ℝ)| ^ s) := by + have heq : (a * b) ^ (s⁻¹ : ℝ) - (a' * b') ^ (s⁻¹ : ℝ) = + (a ^ (s⁻¹ : ℝ) - a' ^ (s⁻¹ : ℝ)) * b ^ (s⁻¹ : ℝ) + + a' ^ (s⁻¹ : ℝ) * (b ^ (s⁻¹ : ℝ) - b' ^ (s⁻¹ : ℝ)) := by + rw [Real.mul_rpow ha hb, Real.mul_rpow ha' hb'] + ring + have habs : |(a * b) ^ (s⁻¹ : ℝ) - (a' * b') ^ (s⁻¹ : ℝ)| ≤ + |a ^ (s⁻¹ : ℝ) - a' ^ (s⁻¹ : ℝ)| * b ^ (s⁻¹ : ℝ) + + a' ^ (s⁻¹ : ℝ) * |b ^ (s⁻¹ : ℝ) - b' ^ (s⁻¹ : ℝ)| := by + rw [heq] + refine (abs_add_le _ _).trans_eq ?_ + rw [abs_mul, abs_mul, abs_of_nonneg (Real.rpow_nonneg hb _), + abs_of_nonneg (Real.rpow_nonneg ha' _)] + refine (pow_le_pow_left₀ (abs_nonneg _) habs s).trans ?_ + refine (add_pow_le (by positivity) (by positivity) s).trans_eq ?_ + rw [mul_pow, mul_pow, Real.rpow_inv_natCast_pow hb hs, Real.rpow_inv_natCast_pow ha' hs] + ring + +private theorem root_sum_mul_sub_pow_le {α : Type*} (T : Finset α) {s : ℕ} (hs : s ≠ 0) + {a a' b b' : α → ℝ} (ha : ∀ z ∈ T, 0 ≤ a z) (ha' : ∀ z ∈ T, 0 ≤ a' z) + (hb : ∀ z ∈ T, 0 ≤ b z) (hb' : ∀ z ∈ T, 0 ≤ b' z) : + |(∑ z ∈ T, a z * b z) ^ (s⁻¹ : ℝ) - (∑ z ∈ T, a' z * b' z) ^ (s⁻¹ : ℝ)| ^ s ≤ + (2 ^ (2 * (s - 1)) * (s : ℝ) ^ s) * + ∑ z ∈ T, (b z * |a z ^ (s⁻¹ : ℝ) - a' z ^ (s⁻¹ : ℝ)| ^ s + + a' z * |b z ^ (s⁻¹ : ℝ) - b' z ^ (s⁻¹ : ℝ)| ^ s) := by + have hsum := homogeneousLoss_sum_le T hs (w := fun _ => 1) + (F := fun z => a z * b z) (F' := fun z => a' z * b' z) (fun _ _ => zero_le_one) + (fun z hz => mul_nonneg (ha z hz) (hb z hz)) + (fun z hz => mul_nonneg (ha' z hz) (hb' z hz)) + simp only [one_mul] at hsum + calc + _ ≤ 2 ^ (s - 1) * homogeneousLoss s (∑ z ∈ T, a z * b z) (∑ z ∈ T, a' z * b' z) := + rpow_inv_sub_pow_le_homogeneousLoss hs + (sum_nonneg fun z hz => mul_nonneg (ha z hz) (hb z hz)) + (sum_nonneg fun z hz => mul_nonneg (ha' z hz) (hb' z hz)) + _ ≤ 2 ^ (s - 1) * ∑ z ∈ T, homogeneousLoss s (a z * b z) (a' z * b' z) := + mul_le_mul_of_nonneg_left hsum (by positivity) + _ ≤ 2 ^ (s - 1) * ∑ z ∈ T, (s : ℝ) ^ s * + (2 ^ (s - 1) * (b z * |a z ^ (s⁻¹ : ℝ) - a' z ^ (s⁻¹ : ℝ)| ^ s + + a' z * |b z ^ (s⁻¹ : ℝ) - b' z ^ (s⁻¹ : ℝ)| ^ s)) := by + refine mul_le_mul_of_nonneg_left (sum_le_sum fun z hz => ?_) (by positivity) + exact (homogeneousLoss_le_rpow_inv_sub_pow hs (mul_nonneg (ha z hz) (hb z hz)) + (mul_nonneg (ha' z hz) (hb' z hz))).trans + (mul_le_mul_of_nonneg_left (root_mul_sub_pow_le hs (ha z hz) (ha' z hz) + (hb z hz) (hb' z hz)) (by positivity)) + _ = _ := by + simp only [← mul_sum] + rw [show 2 * (s - 1) = (s - 1) + (s - 1) by omega, pow_add] + ring + +private theorem sum_le_mul_of_card_support_le {α : Type*} (T : Finset α) {v : α → ℝ} + {C : ℝ} (hC : 0 ≤ C) (hv : ∀ z, v z ≤ C) {K : ℕ} (hK : #{z ∈ T | v z ≠ 0} ≤ K) : + ∑ z ∈ T, v z ≤ K * C := by + classical + have hsum : ∑ z ∈ T, v z = ∑ z ∈ T with v z ≠ 0, v z := by + rw [sum_filter] + refine sum_congr rfl fun z _ => ?_ + split_ifs with hz + · rfl + · exact not_ne_iff.mp hz + rw [hsum] + calc + _ ≤ ∑ z ∈ T with v z ≠ 0, C := sum_le_sum fun z _ => hv z + _ = (#{z ∈ T | v z ≠ 0} : ℝ) * C := by rw [sum_const, nsmul_eq_mul] + _ ≤ K * C := mul_le_mul_of_nonneg_right (by exact_mod_cast hK) hC + +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)] + +/-- **Coupled product errors with source release**. The true or estimated tables may share +all their randomness. Only `B` needs the row cap and bound `CB`, and only `F'` needs the incoming +cap and bound `CF`, because the scalar comparison splits through `F' * B`. +The source normalization in the right error is exactly `f / u`. -/ +theorem rootDistPow_mul_le (hs : s ≠ 0) (hN : 0 < N) (hu : 0 < u) (hf : 0 < f) + {F F' B B' : Ω → V → V → ℝ} + (hF : ∀ σ x z, 0 ≤ F σ x z) (hF' : ∀ σ x z, 0 ≤ F' σ x z) + (hB : ∀ σ z y, 0 ≤ B σ z y) (hB' : ∀ σ z y, 0 ≤ B' σ z y) + {CF CB : ℝ} (hCF : 0 ≤ CF) (hCB : 0 ≤ CB) + (hFbound : ∀ σ x z, F' σ x z ≤ CF) (hBbound : ∀ σ z y, B σ z y ≤ CB) + {Kr Kc : ℕ} (hrow : ∀ σ z, Z σ z → #{y ∈ ({y | Y σ y} : Finset V) | B σ z y ≠ 0} ≤ Kr) + (hcol : ∀ σ z, Z σ z → #{x ∈ ({x | X σ x} : Finset V) | F' σ x z ≠ 0} ≤ Kc) : + rootDistPow s N u X Y (fun σ x y => ∑ z ∈ ({z | Z σ z} : Finset V), F σ x z * B σ z y) + (fun σ x y => ∑ z ∈ ({z | Z σ z} : Finset V), F' σ x z * B' σ z y) ≤ + (2 ^ (2 * (s - 1)) * (s : ℝ) ^ s) * + (CB * Kr * rootDistPow s N u X Z F F' + + CF * Kc * (f / u) * rootDistPow s N f Z Y B B') := by + classical + let eF : Ω → V → V → ℝ := fun σ x z => |F σ x z ^ (s⁻¹ : ℝ) - F' σ x z ^ (s⁻¹ : ℝ)| ^ s + let eB : Ω → V → V → ℝ := fun σ z y => |B σ z y ^ (s⁻¹ : ℝ) - B' σ z y ^ (s⁻¹ : ℝ)| ^ s + have heF : ∀ σ x z, 0 ≤ eF σ x z := fun _ _ _ => by dsimp [eF]; positivity + have heB : ∀ σ z y, 0 ≤ eB σ z y := fun _ _ _ => by dsimp [eB]; positivity + have hleft : (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + ∑ z ∈ ({z | Z σ z} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), B σ z y * eF σ x z ≤ + CB * Kr * rootDistPow s N u X Z F F' := by + calc + _ ≤ (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + ∑ z ∈ ({z | Z σ z} : Finset V), ((Kr : ℝ) * CB) * eF σ x z := by + refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (by positivity) + refine sum_le_sum fun x _ => sum_le_sum fun z hz => ?_ + rw [← sum_mul] + exact mul_le_mul_of_nonneg_right + (sum_le_mul_of_card_support_le _ hCB (hBbound σ z) (hrow σ z (by simpa using hz))) + (heF σ x z) + _ = _ := by + simp only [rootDistPow, rowNormPow, eF, ← mul_sum, ← mul_expect] + ring + have hright : (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + ∑ z ∈ ({z | Z σ z} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), F' σ x z * eB σ z y ≤ + CF * Kc * (f / u) * rootDistPow s N f Z Y B B' := by + have hpoint : ∀ σ x, + ∑ z ∈ ({z | Z σ z} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), F' σ x z * eB σ z y ≤ + CF * ∑ z ∈ ({z | Z σ z} : Finset V) with F' σ x z ≠ 0, + ∑ y ∈ ({y | Y σ y} : Finset V), eB σ z y := by + intro σ x + conv_rhs => rw [mul_sum, sum_filter] + refine sum_le_sum fun z _ => ?_ + by_cases hz : F' σ x z = 0 + · simp [hz] + · simp only [hz, ne_eq, not_false_eq_true, ↓reduceIte] + rw [← mul_sum] + exact mul_le_mul_of_nonneg_right (hFbound σ x z) (sum_nonneg fun y _ => heB σ z y) + have hrelease : (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + ∑ z ∈ ({z | Z σ z} : Finset V) with F' σ x z ≠ 0, + ∑ y ∈ ({y | Y σ y} : Finset V), eB σ z y ≤ + Kc * (f / u) * rootDistPow s N f Z Y B B' := by + exact sourceRelease_le_rowNormPow hN hu hf (fun σ x z => F' σ x z ≠ 0) hcol + (fun σ z y => B σ z y ^ (s⁻¹ : ℝ) - B' σ z y ^ (s⁻¹ : ℝ)) + calc + _ ≤ (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + CF * ∑ z ∈ ({z | Z σ z} : Finset V) with F' σ x z ≠ 0, + ∑ y ∈ ({y | Y σ y} : Finset V), eB σ z y := by + exact mul_le_mul_of_nonneg_left + (expect_le_expect fun σ _ => sum_le_sum fun x _ => hpoint σ x) (by positivity) + _ = CF * ((N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + ∑ z ∈ ({z | Z σ z} : Finset V) with F' σ x z ≠ 0, + ∑ y ∈ ({y | Y σ y} : Finset V), eB σ z y) := by + simp only [← mul_sum, ← mul_expect] + ring + _ ≤ CF * (Kc * (f / u) * rootDistPow s N f Z Y B B') := + mul_le_mul_of_nonneg_left hrelease hCF + _ = _ := by ring + have hswap : ∀ σ x, + ∑ y ∈ ({y | Y σ y} : Finset V), ∑ z ∈ ({z | Z σ z} : Finset V), + (B σ z y * eF σ x z + F' σ x z * eB σ z y) = + (∑ z ∈ ({z | Z σ z} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), B σ z y * eF σ x z) + + ∑ z ∈ ({z | Z σ z} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), F' σ x z * eB σ z y := by + intro σ x + rw [sum_comm] + simp only [sum_add_distrib] + rw [rootDistPow, rowNormPow] + calc + _ ≤ (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), + (2 ^ (2 * (s - 1)) * (s : ℝ) ^ s) * + ∑ z ∈ ({z | Z σ z} : Finset V), (B σ z y * eF σ x z + F' σ x z * eB σ z y) := by + refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (by positivity) + refine sum_le_sum fun x _ => sum_le_sum fun y _ => ?_ + exact root_sum_mul_sub_pow_le _ hs (fun z _ => hF σ x z) (fun z _ => hF' σ x z) + (fun z _ => hB σ z y) (fun z _ => hB' σ z y) + _ = (2 ^ (2 * (s - 1)) * (s : ℝ) ^ s) * + (((N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ z ∈ ({z | Z σ z} : Finset V), + ∑ y ∈ ({y | Y σ y} : Finset V), B σ z y * eF σ x z) + + ((N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ z ∈ ({z | Z σ z} : Finset V), + ∑ y ∈ ({y | Y σ y} : Finset V), F' σ x z * eB σ z y)) := by + simp only [← mul_sum, ← mul_expect] + simp_rw [hswap] + simp only [sum_add_distrib, expect_add_distrib, ← mul_sum] + ring + _ ≤ _ := mul_le_mul_of_nonneg_left (add_le_add hleft hright) (by positivity) + +end Cslib + +namespace Matrix + +variable {Ω V ι κ υ : Type*} [Fintype Ω] [Fintype V] [Fintype ι] [Fintype κ] [Fintype υ] + {s KF Kc KB : ℕ} {N u f b : ℝ} {I : ℝ → ℝ → ℝ} {τ Q hF ρF k hB ρB : ℝ → ℝ} + {X : ι → V → Prop} {Z Zt : κ → V → Prop} {Y Yt : υ → V → Prop} + [∀ t x, Decidable (X t x)] [∀ t z, Decidable (Z t z)] [∀ t z, Decidable (Zt t z)] + [∀ t y, Decidable (Y t y)] [∀ t y, Decidable (Yt t y)] + +private theorem nonneg_correctionAtom {G : Matrix V V ℝ} {g₀ : V → ℝ} + (hQ0 : ∀ v, 0 ≤ Q v) (hρ0 : ∀ r, 0 ≤ ρF r) (hτ0 : ∀ r, 0 ≤ τ r) + (hg₀ : ∀ z, 0 ≤ g₀ z) (d : ι × κ) (x z : V) : + 0 ≤ correctionAtom I τ KF Kc f G X Z Zt Q hF ρF g₀ d x z := by + rw [correctionAtom] + split_ifs + · refine mul_nonneg (div_nonneg (mul_nonneg (hQ0 _) (mul_nonneg (hρ0 _) (hτ0 _))) ?_) + (hg₀ z) + exact le_trans (by norm_num : (0 : ℝ) ≤ 1 / 2) (le_max_left _ _) + · exact le_rfl + +private theorem nonneg_denseAtom {H : Matrix V V ℝ} + (hk0 : ∀ v, 0 ≤ k v) (hρ0 : ∀ r, 0 ≤ ρB r) (t : υ) (z y : V) : + 0 ≤ denseAtom Y Yt k hB ρB KB b H t z y := by + rw [denseAtom] + split_ifs + · refine div_nonneg (mul_nonneg (hk0 _) (hρ0 _)) ?_ + exact le_trans (by norm_num : (0 : ℝ) ≤ 1 / 2) (le_max_left _ _) + · exact le_rfl + +/-- **Product errors for actual correction and dense atoms**. The matrices, multipliers, and +both seed maps may depend on one shared environment. The bounded cutoffs give `CF = 2 * AF` +and `CB = 2 * AB`; the actual incoming and row gates give caps `Kc` and `KB`. + +The intermediate source normalization changes from `u` to the correction scale `f`, with exact +factor `f / u`. This theorem does not change the terminal scale `b` or take conditional means. -/ +theorem correctionAtom_denseAtom_rootDistPow_le + (drawF : Ω → ι × κ) (drawB : Ω → υ) + (G G' H H' : Ω → Matrix V V ℝ) (g g' : Ω → V → ℝ) + (hs : s ≠ 0) (hN : 0 < N) (hu : 0 < u) (hf : 0 < f) + (hQ0 : ∀ v, 0 ≤ Q v) (hk0 : ∀ v, 0 ≤ k v) + (hρF0 : ∀ r, 0 ≤ ρF r) (hρF1 : ∀ r, ρF r ≤ 1) + (hτ0 : ∀ r, 0 ≤ τ r) (hτ1 : ∀ r, τ r ≤ 1) + (hρB0 : ∀ r, 0 ≤ ρB r) (hρB1 : ∀ r, ρB r ≤ 1) + (hg0 : ∀ σ z, 0 ≤ g σ z) (hg'0 : ∀ σ z, 0 ≤ g' σ z) (hg'1 : ∀ σ z, g' σ z ≤ 1) + {AF AB : ℝ} (hAF : 0 ≤ AF) (hAB : 0 ≤ AB) + (hQbound : ∀ σ x z, Q (G' σ x z / f) ≤ AF) + (hkbound : ∀ σ z y, k (H σ z y / b) ≤ AB) + (hKc : 0 < Kc) (hIQ : ∀ v r, Q v ≠ 0 → ρF r ≠ 0 → I v r = 1) + {gF : ℝ} (hgF : gF ≤ 1) (hτclose : ∀ r, gF ≤ r → τ r = 0) + (hYt : ∀ t y, Yt t y → Y t y) (hKB : 0 < KB) + {eB gB : ℝ} (heB : 0 ≤ eB) (hkzero : ∀ v, v ≤ eB → k v = 0) + (hgB : gB ≤ eB) (hρBclose : ∀ r, gB ≤ r → ρB r = 0) : + let F := fun σ => correctionAtom I τ KF Kc f (G σ) X Z Zt Q hF ρF (g σ) (drawF σ) + let F' := fun σ => correctionAtom I τ KF Kc f (G' σ) X Z Zt Q hF ρF (g' σ) (drawF σ) + let B := fun σ => denseAtom Y Yt k hB ρB KB b (H σ) (drawB σ) + let B' := fun σ => denseAtom Y Yt k hB ρB KB b (H' σ) (drawB σ) + Cslib.rootDistPow s N u (fun σ x => X (drawF σ).1 x) (fun σ y => Yt (drawB σ) y) + (fun σ x y => ∑ z ∈ ({z | Zt (drawF σ).2 z} : Finset V), F σ x z * B σ z y) + (fun σ x y => ∑ z ∈ ({z | Zt (drawF σ).2 z} : Finset V), F' σ x z * B' σ z y) ≤ + (2 ^ (2 * (s - 1)) * (s : ℝ) ^ s) * + ((2 * AB) * KB * Cslib.rootDistPow s N u (fun σ x => X (drawF σ).1 x) + (fun σ z => Zt (drawF σ).2 z) F F' + + (2 * AF) * Kc * (f / u) * Cslib.rootDistPow s N f (fun σ z => Zt (drawF σ).2 z) + (fun σ y => Yt (drawB σ) y) B B') := by + classical + dsimp only + refine Cslib.rootDistPow_mul_le hs hN hu hf + (fun σ => nonneg_correctionAtom hQ0 hρF0 hτ0 (hg0 σ) (drawF σ)) + (fun σ => nonneg_correctionAtom hQ0 hρF0 hτ0 (hg'0 σ) (drawF σ)) + (fun σ => nonneg_denseAtom hk0 hρB0 (drawB σ)) + (fun σ => nonneg_denseAtom hk0 hρB0 (drawB σ)) + (by positivity) (by positivity) ?_ ?_ ?_ ?_ + · intro σ x z + calc + _ ≤ |correctionAtom I τ KF Kc f (G' σ) X Z Zt Q hF ρF (g' σ) (drawF σ) x z| := + le_abs_self _ + _ ≤ 2 * |Q (G' σ x z / f)| * |g' σ z| := abs_correctionAtom_le hρF0 hρF1 hτ0 hτ1 _ _ _ + _ = 2 * Q (G' σ x z / f) * g' σ z := by + rw [abs_of_nonneg (hQ0 _), abs_of_nonneg (hg'0 _ _)] + _ ≤ (2 * AF) * 1 := mul_le_mul + (mul_le_mul_of_nonneg_left (hQbound σ x z) (by norm_num)) (hg'1 σ z) (hg'0 σ z) + (by positivity) + _ = _ := mul_one _ + · intro σ z y + calc + _ ≤ |denseAtom Y Yt k hB ρB KB b (H σ) (drawB σ) z y| := le_abs_self _ + _ ≤ 2 * |k (H σ z y / b)| := abs_denseAtom_le hρB0 hρB1 _ _ _ + _ = 2 * k (H σ z y / b) := by rw [abs_of_nonneg (hk0 _)] + _ ≤ _ := mul_le_mul_of_nonneg_left (hkbound σ z y) (by norm_num) + · intro σ z _ + refine (card_le_card ?_).trans + (card_filter_denseAtom_ne_zero_lt (h := hB) (a := b) (G := H σ) + hYt hKB heB hkzero hgB hρBclose (drawB σ) z).le + intro y hy + exact mem_filter.mpr ⟨mem_univ _, (mem_filter.mp hy).2⟩ + · intro σ z _ + exact (card_filter_correctionAtom_col_ne_zero_lt hKc hIQ hgF hτclose (drawF σ) z).le + +end Matrix diff --git a/Complexity/Foundations/Probability/RootMetric.lean b/Complexity/Foundations/Probability/RootMetric.lean index 419b8cccd..5b98e8774 100644 --- a/Complexity/Foundations/Probability/RootMetric.lean +++ b/Complexity/Foundations/Probability/RootMetric.lean @@ -71,17 +71,17 @@ 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 [OpenAI2026LogSpace, (5.19)]. -/ -noncomputable def rootDistPow (H H' : Ω → V → V → ℝ) : ℝ := +@[expose] noncomputable def rootDistPow (H H' : Ω → V → V → ℝ) : ℝ := rowNormPow s N u X Y fun σ x y => H σ x y ^ (s⁻¹ : ℝ) - H' σ x y ^ (s⁻¹ : ℝ) /-- The `s`-th power `‖v‖^s_{u;s}` of the integrated norm of a random vertex array [OpenAI2026LogSpace, (5.20)]. -/ -noncomputable def vertexNormPow (v : Ω → V → ℝ) : ℝ := +@[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 000000000..0df6d50d1 --- /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 000000000..90e504c52 --- /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/ConditionalProductMean.lean b/ComplexityTests/ConditionalProductMean.lean new file mode 100644 index 000000000..b637997ec --- /dev/null +++ b/ComplexityTests/ConditionalProductMean.lean @@ -0,0 +1,186 @@ +/- +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.ConditionalProductMean +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Tests for conditional product means + +The source and endpoint use the same two-of-three mask. Estimated factors on a path +`0 → 1 → 2` are coupled: their products are `0` and `32` on the two conditioning draws. +The actual conditional means are `1` and `16`. Source and endpoint densities are `2/3`, +the intermediate density is one, and the coarse coefficient is `b/a = 3/2`. +The resulting integrated fourth-root error is exactly `1/2`. + +Further examples identify the true mean of concrete correction and dense atoms through +`TrueSampleMeans`, and check empty slices and an empty environment. +-/ + +namespace ComplexityTests.ConditionalProductMean + +open Finset Matrix Cslib +open scoped BigOperators + +private abbrev kept (σ : Fin 3) (_ : Fin 3) : Prop := σ ≠ 2 +private abbrev middle (_ _ : Fin 3) : Prop := True + +private def F (_ : Fin 3) (x z : Fin 3) : ℝ := if x = 0 ∧ z = 1 then 1 else 0 +private def F' (σ x z : Fin 3) : ℝ := if σ = 1 ∧ x = 0 ∧ z = 1 then 8 else 0 +private def B (σ z y : Fin 3) : ℝ := if kept σ y ∧ z = 1 ∧ y = 2 then 1 else 0 +private def B' (σ z y : Fin 3) : ℝ := if σ = 1 ∧ z = 1 ∧ y = 2 then 4 else 0 + +private noncomputable def product (A D : Fin 3 → Fin 3 → Fin 3 → ℝ) + (σ x y : Fin 3) : ℝ := ∑ z, A σ x z * D σ z y + +private theorem slice (x y : Fin 3) : + ({σ | kept σ x ∧ kept σ y} : Finset (Fin 3)) = {0, 1} := by + change ({σ : Fin 3 | σ ≠ 2 ∧ σ ≠ 2} : Finset (Fin 3)) = {0, 1} + decide + +-- The masks are correlated, so the joint density is `2/3`, not the product `4/9`. +example (x y : Fin 3) : (dens {σ | kept σ x ∧ kept σ y} : ℝ) = 2 / 3 := by + rw [slice, dens_eq_card_div_card] + norm_num + +private theorem true_mean (x y : Fin 3) : + conditionalTableMean kept kept (product F B) x y = if x = 0 ∧ y = 2 then 1 else 0 := by + rw [conditionalTableMean, slice] + fin_cases x <;> fin_cases y <;> + norm_num [expect_eq_sum_div_card, product, F, B, kept, Fin.sum_univ_three] + +private theorem estimated_mean (x y : Fin 3) : + conditionalTableMean kept kept (product F' B') x y = if x = 0 ∧ y = 2 then 16 else 0 := by + rw [conditionalTableMean, slice] + fin_cases x <;> fin_cases y <;> + norm_num [expect_eq_sum_div_card, product, F', B', Fin.sum_univ_three] + +example : product F' B' 0 0 2 = 0 ∧ product F' B' 1 0 2 = 32 := by + norm_num [product, F', B', Fin.sum_univ_three] + +private theorem root_sixteen : (16 : ℝ) ^ (4⁻¹ : ℝ) = 2 := by + rw [show (16 : ℝ) = 2 ^ 4 by norm_num] + exact Real.pow_rpow_inv_natCast (by norm_num) (by norm_num) + +private theorem scaled_gap : |(3 / 2 : ℝ) ^ (4⁻¹ : ℝ) - 24 ^ (4⁻¹ : ℝ)| ^ 4 = 3 / 2 := by + rw [show (24 : ℝ) = (3 / 2) * 16 by norm_num, + Real.mul_rpow (by norm_num : (0 : ℝ) ≤ 3 / 2) (by norm_num : (0 : ℝ) ≤ 16), root_sixteen] + rw [show (3 / 2 : ℝ) ^ (4⁻¹ : ℝ) - (3 / 2 : ℝ) ^ (4⁻¹ : ℝ) * 2 = + -((3 / 2 : ℝ) ^ (4⁻¹ : ℝ)) by ring] + rw [abs_neg, abs_of_nonneg (Real.rpow_nonneg (by norm_num : (0 : ℝ) ≤ 3 / 2) _)] + exact Real.rpow_inv_natCast_pow (by norm_num) (by norm_num) + +private theorem mean_error : + rootDistPow 4 3 (2 / 3) kept kept + (fun _ x y => (3 / 2) * conditionalTableMean kept kept (product F B) x y) + (fun _ x y => (3 / 2) * conditionalTableMean kept kept (product F' B') x y) = 1 / 2 := by + norm_num [rootDistPow, rowNormPow, true_mean, estimated_mean, kept, sum_filter, + expect_eq_sum_div_card, Fin.sum_univ_three] + rw [show (1 / 4 : ℝ) = 4⁻¹ by rw [one_div], scaled_gap] + norm_num + +private theorem coarse_bound : + rootDistPow 4 3 (2 / 3) kept kept + (fun _ x y => (3 / 2) * conditionalTableMean kept kept (product F B) x y) + (fun _ x y => (3 / 2) * conditionalTableMean kept kept (product F' B') x y) ≤ + 50331648 * (rootDistPow 4 3 (2 / 3) kept middle F F' + + 12 * rootDistPow 4 3 1 middle kept B B') := by + have hrow : ∀ σ z, middle σ z → #{y ∈ ({y | kept σ y} : Finset (Fin 3)) | B σ z y ≠ 0} ≤ 1 := by + intro σ z _ + refine card_le_one.2 fun y hy y' hy' => ?_ + have hy2 : y = 2 := by + by_contra h + simp [B, h] at hy + have hy'2 : y' = 2 := by + by_contra h + simp [B, h] at hy' + exact hy2.trans hy'2.symm + have hcol : ∀ σ z, middle σ z → #{x ∈ ({x | kept σ x} : Finset (Fin 3)) | F' σ x z ≠ 0} ≤ 1 := by + intro σ z _ + refine card_le_one.2 fun x hx x' hx' => ?_ + have hx0 : x = 0 := by + by_contra h + simp [F', h] at hx + have hx'0 : x' = 0 := by + by_contra h + simp [F', h] at hx' + exact hx0.trans hx'0.symm + have h := rootDistPow_coarseProductMean_le (s := 4) (N := 3) (u := 2 / 3) + (X := kept) (Y := kept) (Z := middle) (a := 2 / 3) (b := 1) (f := 1) (πf := 1) + (F := F) (F' := F') (B := B) (B' := B') (by decide) (by norm_num) (by norm_num) + (by norm_num) (by norm_num) (by norm_num) (by norm_num) + (fun _ _ _ => by unfold F; split_ifs <;> norm_num) + (fun _ _ _ => by unfold F'; split_ifs <;> norm_num) + (fun _ _ _ => by unfold B; split_ifs <;> norm_num) + (fun _ _ _ => by unfold B'; split_ifs <;> norm_num) + (CF := 8) (CB := 1) (by norm_num) (by norm_num) + (fun _ _ _ => by unfold F'; split_ifs <;> norm_num) + (fun _ _ _ => by unfold B; split_ifs <;> norm_num) hrow hcol + norm_num [middle] at h + exact h + +-- The theorem applies to this positive error with actual, dependent conditioning masks. +example : (1 / 2 : ℝ) ≤ 50331648 * (rootDistPow 4 3 (2 / 3) kept middle F F' + + 12 * rootDistPow 4 3 1 middle kept B B') := by + have h := coarse_bound + rwa [mean_error] at h + +/-! ### The actual true-atom mean -/ + +private abbrev full {α : Type*} (_ : α) (_ : Fin 2) : Prop := True +private abbrev used (σ : Bool) (_ : Fin 2) : Prop := σ = true +private def G (x z : Fin 2) : ℝ := if x = 0 ∧ z = 1 then 1 else 0 +private def H (z y : Fin 2) : ℝ := if z = 1 ∧ y = 0 then 1 else 0 + +private noncomputable def trueAtomProduct (d : (Unit × Unit) × Bool) (x y : Fin 2) : ℝ := + ∑ z, correctionAtom (fun _ _ => 0) (fun _ => 1) 8 8 1 G full full full id (fun _ => 1) + (fun _ => 1) (fun _ => 1) d.1 x z * + denseAtom full used id (fun _ => 1) (fun _ => 1) 4 1 H d.2 z y + +example : conditionalTableMean (fun (_ : (Unit × Unit) × Bool) => full ()) + (fun d => used d.2) trueAtomProduct 0 0 = 1 := by + rw [conditionalTableMean_eq_expect_product (κ := Unit) (X := fun (_ : Unit) => full ()) + (Y := used) (H := trueAtomProduct)] + 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) (G := G) (H := H) (g₀ := fun _ => 1) + (X := fun (_ : Unit) => full ()) (Z := fun (_ : Unit) => full ()) (Zt := fun _ => full ()) + (Y := fun (_ : Bool) => full ()) (Ya := used) (Yt := used) (x := 0) (y := 0) + (hSx := ⟨(), by simp⟩) (hZπ := fun _ => by simp [full]) (hπf := by norm_num) + (hYt := fun _ h => h) (hSy := ⟨true, 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 [G]) + (MF := 1) (hGM := by norm_num [G, Fin.sum_univ_two]) (cF := 1) (hcF := zero_le_one) + (hKF := by norm_num) (hpairZ := fun _ _ _ => by simp [full]) + (p := 1) (hp := zero_le_one) (hpairX := fun _ _ => by simp [full]) + (R := 1) (hR := fun z _ => by + fin_cases z <;> norm_num [G, univ_fin2, filter_insert, filter_singleton]) + (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 [H]) + (MB := 1) (hHM := fun z => by fin_cases z <;> norm_num [H, Fin.sum_univ_two]) + (cB := 1) (hcB := zero_le_one) (hKB := by norm_num) + (hpairY := fun _ _ => by simp [used, full]) + norm_num [used, filter_eq', dens_eq_card_div_card, G, H, Fin.sum_univ_two] at h + norm_num [trueAtomProduct, used, filter_eq', Fin.sum_univ_two] + exact h + +/-! ### Empty slices remain defined -/ + +example (T : Fin 3 → Fin 3 → Fin 3 → ℝ) (x y : Fin 3) : + conditionalTableMean (fun _ _ => False) kept T x y = 0 := by + simp [conditionalTableMean] + +example (T : Empty → Fin 3 → Fin 3 → ℝ) (x y : Fin 3) : + conditionalTableMean (fun _ _ => True) (fun _ _ => True) T x y = 0 := by + simp [conditionalTableMean] + +end ComplexityTests.ConditionalProductMean diff --git a/ComplexityTests/ProductError.lean b/ComplexityTests/ProductError.lean new file mode 100644 index 000000000..e5d591fb7 --- /dev/null +++ b/ComplexityTests/ProductError.lean @@ -0,0 +1,175 @@ +/- +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.ProductError +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Tests for coupled product errors + +An actual correction edge `0 → 1` and dense edge `1 → 2` have weights `1` in the first +version and `16` in the second. Their usage channels use the same Boolean seed, so their +masks are perfectly correlated. The product-root error has positive fourth power `81 / 2`, +while the source normalizations `u = 1/3`, `f = 1` make the release factor three. +-/ + +namespace ComplexityTests.ProductError + +open Finset Matrix Cslib +open scoped BigOperators + +private abbrev full {α : Type*} (_ : α) (_ : Fin 3) : Prop := True +private abbrev mask (σ : Bool) (_ : Fin 3) : Prop := σ = true + +private noncomputable def left (w : ℝ) (x z : Fin 3) : ℝ := + if x = 0 ∧ z = 1 then w else 0 + +private noncomputable def right (w : ℝ) (z y : Fin 3) : ℝ := + if z = 1 ∧ y = 2 then w + 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 noncomputable def Q (v : ℝ) : ℝ := max v 0 +private noncomputable def k (v : ℝ) : ℝ := max (v - 1) 0 + +private theorem gate_nonneg (r : ℝ) : 0 ≤ gate r := by + unfold gate + split_ifs <;> norm_num + +private theorem gate_le_one (r : ℝ) : gate r ≤ 1 := by + unfold gate + split_ifs <;> norm_num + +private theorem gate_zero (r : ℝ) (hr : 1 ≤ r) : gate r = 0 := ite_eq_right (not_lt.mpr hr) + +private theorem score_one (v r : ℝ) (hv : Q v ≠ 0) (_ : (1 : ℝ) ≠ 0) : score v r = 1 := by + have hv0 : v ≠ 0 := fun h => hv (by simp [Q, h]) + exact ite_eq_right hv0 + +private theorem incoming_one (w : ℝ) (z : Fin 3) : + incomingGate score gate 3 2 1 (left w) univ univ z = 1 := by + have hcard : #{x : Fin 3 | 1 ≤ auxScore score 3 1 (left w) univ x z} ≤ 1 := by + refine card_le_one.2 fun x hx x' hx' => ?_ + have hx0 : x = 0 := by + by_contra h + norm_num [auxScore, score, left, h] at hx + have hx'0 : x' = 0 := by + by_contra h + norm_num [auxScore, score, left, h] at hx' + exact hx0.trans hx'0.symm + have hlt : kthLargest 2 univ (fun x => auxScore score 3 1 (left w) univ x z) < 1 := by + exact lt_of_not_ge fun h => by + have := (le_kthLargest_iff (by decide) zero_lt_one).mp h + omega + exact ite_eq_left hlt + +private theorem row_one (w : ℝ) (z : Fin 3) : rowGate gate 2 1 (right w) univ z = 1 := by + have hcard : #{y : Fin 3 | 1 ≤ right w z y / 1} ≤ 1 := by + refine card_le_one.2 fun y hy y' hy' => ?_ + have hy2 : y = 2 := by + by_contra h + norm_num [right, h] at hy + have hy'2 : y' = 2 := by + by_contra h + norm_num [right, h] at hy' + exact hy2.trans hy'2.symm + have hlt : kthLargest 2 univ (fun y => right w z y / 1) < 1 := by + exact lt_of_not_ge fun h => by + have := (le_kthLargest_iff (by decide) zero_lt_one).mp h + omega + exact ite_eq_left hlt + +private noncomputable def correction (w : ℝ) (σ : Bool) (x z : Fin 3) : ℝ := + correctionAtom score gate 3 2 1 (left w) full full mask Q (fun _ => 1) + (fun _ => 1) (fun _ => 1) ((), σ) x z + +private noncomputable def dense (w : ℝ) (σ : Bool) (z y : Fin 3) : ℝ := + denseAtom full mask k (fun _ => 1) gate 2 1 (right w) σ z y + +private theorem correction_eq (w : ℝ) (σ : Bool) (x z : Fin 3) : + correction w σ x z = if σ = true then Q (left w x z) else 0 := by + have hn : correctionNormalizer (ι := Unit) score gate 3 2 1 (left w) full full mask (fun _ => 1) + (fun _ => 1) x z = 1 := by + simp [correctionNormalizer, correctionPrep, rowGate, full, mask, incoming_one, filter_eq'] + norm_num [correction, correctionAtom, rowGate, full, mask, incoming_one, hn] + +private theorem dense_eq (w : ℝ) (σ : Bool) (z y : Fin 3) : + dense w σ z y = if σ = true then k (right w z y) else 0 := by + have hn : atomNormalizer full mask (fun _ => 1) gate 2 1 (right w) z y = 1 := by + simp [atomNormalizer, atomPrep, full, mask, row_one, filter_eq'] + norm_num [dense, denseAtom, full, mask, row_one, hn] + +private noncomputable def sample (w : ℝ) (σ : Bool) (x y : Fin 3) : ℝ := + ∑ z ∈ ({z | mask σ z} : Finset (Fin 3)), correction w σ x z * dense w σ z y + +private theorem sample_eq (w : ℝ) (σ : Bool) (x y : Fin 3) : + sample w σ x y = if σ = true ∧ x = 0 ∧ y = 2 then (max w 0) ^ 2 else 0 := by + fin_cases σ <;> fin_cases x <;> fin_cases y <;> + norm_num [sample, mask, correction_eq, dense_eq, Q, k, left, right, Fin.sum_univ_three, + pow_two] + +example : sample 1 true 0 2 = 1 ∧ sample 16 true 0 2 = 256 ∧ sample 16 false 0 2 = 0 := by + norm_num [sample_eq] + +private theorem root_sixteen : (16 : ℝ) ^ (4⁻¹ : ℝ) = 2 := by + rw [show (16 : ℝ) = 2 ^ 4 by norm_num] + exact Real.pow_rpow_inv_natCast (by norm_num) (by norm_num) + +private theorem root_two_fifty_six : (256 : ℝ) ^ (4⁻¹ : ℝ) = 4 := by + rw [show (256 : ℝ) = 4 ^ 4 by norm_num] + exact Real.pow_rpow_inv_natCast (by norm_num) (by norm_num) + +private theorem product_error : rootDistPow 4 3 (1 / 3) (fun (_ : Bool) => full ()) mask + (sample 1) (sample 16) = 81 / 2 := by + norm_num [rootDistPow, rowNormPow, full, mask, sample_eq, expect_eq_sum_div_card, + sum_filter, Fin.sum_univ_three, Fintype.sum_bool, root_two_fifty_six] + +private theorem left_error : rootDistPow 4 3 (1 / 3) (fun (_ : Bool) => full ()) mask + (correction 1) (correction 16) = 1 / 2 := by + norm_num [rootDistPow, rowNormPow, full, mask, correction_eq, Q, left, + expect_eq_sum_div_card, sum_filter, Fin.sum_univ_three, Fintype.sum_bool, root_sixteen] + +private theorem right_error : rootDistPow 4 3 1 mask mask (dense 1) (dense 16) = 1 / 6 := by + norm_num [rootDistPow, rowNormPow, mask, dense_eq, k, right, expect_eq_sum_div_card, + sum_filter, Fin.sum_univ_three, Fintype.sum_bool, root_sixteen] + +-- Both caps are discharged from the actual atom gates. The two seed maps are correlated. +private theorem actual_atom_bound : + rootDistPow 4 3 (1 / 3) (fun (_ : Bool) => full ()) mask (sample 1) (sample 16) ≤ + 16384 * (4 * rootDistPow 4 3 (1 / 3) (fun (_ : Bool) => full ()) mask + (correction 1) (correction 16) + + 192 * rootDistPow 4 3 1 mask mask (dense 1) (dense 16)) := by + have h := correctionAtom_denseAtom_rootDistPow_le + (X := fun (_ : Unit) => full ()) (Z := fun (_ : Bool) => full ()) (Zt := mask) + (Y := fun (_ : Bool) => full ()) (Yt := mask) + (I := score) (τ := gate) (Q := Q) (hF := fun _ => 1) (ρF := fun _ => 1) + (k := k) (hB := fun _ => 1) (ρB := gate) (KF := 3) (Kc := 2) (KB := 2) + (s := 4) (N := 3) (u := 1 / 3) (f := 1) (b := 1) + (fun σ : Bool => ((), σ)) id (fun _ => left 1) (fun _ => left 16) + (fun _ => right 1) (fun _ => right 16) (fun _ _ => 1) (fun _ _ => 1) + (by decide) (by norm_num) (by norm_num) (by norm_num) + (fun v => le_max_right v 0) (fun v => le_max_right (v - 1) 0) + (fun _ => zero_le_one) (fun _ => le_rfl) gate_nonneg gate_le_one gate_nonneg gate_le_one + (fun _ _ => zero_le_one) (fun _ _ => zero_le_one) (fun _ _ => le_rfl) + (AF := 16) (AB := 1) (by norm_num) (by norm_num) + (fun _ x z => by fin_cases x <;> fin_cases z <;> norm_num [Q, left]) + (fun _ z y => by fin_cases z <;> fin_cases y <;> norm_num [k, right]) + (by decide) score_one (gF := 1) le_rfl gate_zero (fun _ _ _ => True.intro) + (by decide) (eB := 1) (gB := 1) zero_le_one + (fun v hv => max_eq_right (sub_nonpos.mpr hv)) le_rfl gate_zero + norm_num only [Nat.reduceSub, Nat.reduceMul, pow_succ, pow_zero, one_mul, mul_one, + one_div_div, div_one, id_eq, Prod.fst, Prod.snd] at h + exact h + +-- The positive left side and unequal source normalizations are evaluated independently. +example : (81 / 2 : ℝ) ≤ 557056 := by + have h := actual_atom_bound + rw [product_error, left_error, right_error] at h + convert h using 1 + norm_num + +end ComplexityTests.ProductError diff --git a/ComplexityTests/SourceRelease.lean b/ComplexityTests/SourceRelease.lean new file mode 100644 index 000000000..466bb1d79 --- /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 000000000..d1b237e82 --- /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