OAI/Probability/DilutedSpin/PatternComparison.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.BooleanPolynomial.truth line 11
2. def OAI.DilutedSpinGlass.BooleanPolynomial.monomial line 12
3. def OAI.DilutedSpinGlass.BooleanPolynomial.coefficient line 13
4. lemma OAI.DilutedSpinGlass.BooleanPolynomial.interpolation line 17
5. lemma OAI.DilutedSpinGlass.BooleanPolynomial.product_expansion line 36
6. theorem OAI.DilutedSpinGlass.BooleanPolynomial.expansion line 53

   Source documentation

   Every predicate of a finite sharing profile is a finite real linear combination of positive sharing requirements. No endpoint mark is needed.

   theorem expansion (F : (R → Bool) → ℝ) (y : R → Bool) :
       F y = ∑ s : Finset R, coefficient F s * monomial s y := by
   …

   Mentions: OAI.DilutedSpinGlass.BooleanPolynomial.coefficient, OAI.DilutedSpinGlass.BooleanPolynomial.monomial

7. def OAI.DilutedSpinGlass.extractionProbe line 78

   Source documentation

   The exact probe sequence of pert:parameters, indexed from zero.

   noncomputable def extractionProbe (j : ℕ) : ℝ := 1 / ((j:ℝ)+4)

8. theorem OAI.DilutedSpinGlass.extractionProbe_pos line 80
9. theorem OAI.DilutedSpinGlass.extractionProbe_le_half line 84
10. theorem OAI.DilutedSpinGlass.extractionProbe_tendsto line 90
11. theorem OAI.DilutedSpinGlass.coefficients_tendsto_zero_of_uniform_remainders line 100

    Source documentation

    Real finite-remainder extraction. This avoids both a complex normal-family argument and a subsequence of limiting coefficients: all coefficients tend to zero directly. The same base function is tested at every probe, as required by the Poisson add-one identity.

    theorem coefficients_tendsto_zero_of_uniform_remainders
        (H : ℕ → ℝ → ℝ) (a : ℕ → ℕ → ℝ) (B : ℕ → ℝ) (C : ℝ)
        (_hB : ∀ k, 0 ≤ B k) (hC : 0 ≤ C)
        (hR : ∀ N k t, t ∈ Icc (0:ℝ) (1/2) →
          |H N t - ∑ i ∈ Finset.range (k+1), a N i * t^i| ≤ B k * t^(k+1))
        (err : ℕ → ℕ → ℝ) (herr : ∀ j, Tendsto (err j) atTop (𝓝 0))
        (hsmall : ∀ j N, |H N (extractionProbe j)| ≤
          C * extractionProbe j ^ (j+4) + err j N) :
        ∀ k, Tendsto (fun N => a N k) atTop (𝓝 0) := by
    …

    Mentions: OAI.DilutedSpinGlass.extractionProbe

12. theorem OAI.DilutedSpinGlass.integral_polynomial_remainder line 175

    Source documentation

    Uniform finite Taylor remainders survive an arbitrary probability-space average. This is a plain Bochner integral statement, not an analyticity axiom.

    theorem integral_polynomial_remainder {Z : Type*} [MeasurableSpace Z]
        (μ : Measure Z) [IsProbabilityMeasure μ] (F : Z → ℝ) (a : ℕ → Z → ℝ)
        (hF : Integrable F μ) (ha : ∀ j, Integrable (a j) μ) (k : ℕ) (t R : ℝ)
        (hR : ∀ z, |F z - ∑ j ∈ Finset.range (k+1), a j z*t^j| ≤ R) :
        |(∫ z, F z ∂μ) - ∑ j ∈ Finset.range (k+1), (∫ z, a j z ∂μ)*t^j| ≤ R := by
    …

13. theorem OAI.DilutedSpinGlass.integral_difference_bound line 191
14. lemma OAI.DilutedSpinGlass.limsup_sqrt_error_bound line 210
15. lemma OAI.DilutedSpinGlass.limsup_finite_linear_bound line 241
16. lemma OAI.DilutedSpinGlass.squeeze_triangle_grid_zero line 270

    Source documentation

    First take each fixed-grid limsup, then the grid limit, and only then let the arbitrary regularity cutoff tend to zero.

    lemma squeeze_triangle_grid_zero (a : ℕ → ℝ) (C : ℝ) (ha : ∀ n, 0 ≤ a n)
        (hC : 0 ≤ C) (b : ℝ → ℕ → ℝ)
        (hb : ∀ η, 0<η → Tendsto (b η) atTop (𝓝 (C*η)))
        (hbound : ∀ η, 0<η → ∀ n, a n ≤ b η n) :
        Tendsto a atTop (𝓝 0) := by
    …

17. def OAI.DilutedSpinGlass.Pattern.sign line 301

    Source documentation

    The manuscript's ±1 spin, represented by Bool.

    def sign (s : Bool) : ℝ := if s then 1 else -1

18. theorem OAI.DilutedSpinGlass.Pattern.abs_sign line 303
19. theorem OAI.DilutedSpinGlass.Pattern.sign_sq line 304
20. theorem OAI.DilutedSpinGlass.Pattern.sign_indicator line 306
21. def OAI.DilutedSpinGlass.Pattern.character line 309
22. theorem OAI.DilutedSpinGlass.Pattern.abs_character line 311
23. theorem OAI.DilutedSpinGlass.Pattern.character_empty line 314
24. theorem OAI.DilutedSpinGlass.Pattern.character_kernel line 318

    Source documentation

    Fourier inversion kernel on replica-spin patterns.

    theorem character_kernel {ι : Type*} [Fintype ι] [DecidableEq ι] (e f : ι → Bool) :
        (∑ S : Finset ι, character S e * character S f) =
          if e=f then (2 : ℝ) ^ Fintype.card ι else 0 := by
    …

    Mentions: OAI.DilutedSpinGlass.Pattern.character

25. def OAI.DilutedSpinGlass.Pattern.moment line 341

    Source documentation

    Moments include all replica subsets, not only pair overlaps.

    noncomputable def moment {ι : Type*} [Fintype ι] [DecidableEq ι] (P : (ι → Bool) → ℝ) (S : Finset ι) : ℝ :=
    …

26. theorem OAI.DilutedSpinGlass.Pattern.inversion line 345

    Source documentation

    Exact Walsh inversion for an arbitrary signed pattern mass.

    theorem inversion {ι : Type*} [Fintype ι] [DecidableEq ι] (P : (ι → Bool) → ℝ) (e : ι → Bool) :
        P e = (∑ S : Finset ι, moment P S * character S e) / (2 : ℝ)^Fintype.card ι := by
    …

    Mentions: OAI.DilutedSpinGlass.Pattern.moment, OAI.DilutedSpinGlass.Pattern.character

27. theorem OAI.DilutedSpinGlass.Pattern.variation_le_moments line 360

    Source documentation

    The total variation discrepancy costs one per nonempty multioverlap. Both masses have the same total, so the empty Fourier coefficient cancels.

    theorem variation_le_moments {ι : Type*} [Fintype ι] [DecidableEq ι]
        (P Q : (ι → Bool) → ℝ) (htotal : ∑ e, P e = ∑ e, Q e) :
        (∑ e, |P e-Q e|) ≤
          ∑ S ∈ (Finset.univ : Finset (Finset ι)).erase ∅, |moment P S-moment Q S| := by
    …

    Mentions: OAI.DilutedSpinGlass.Pattern.moment

28. theorem OAI.DilutedSpinGlass.Pattern.product_variation_step line 390

    Source documentation

    Exact coordinatewise product telescoping, in a form usable for different probability laws at different message labels.

    theorem product_variation_step {α β : Type*} [Fintype α] [Fintype β]
        (P Q : α → ℝ) (U V : β → ℝ)
        (hP : ∀ x, 0 ≤ P x) (hV : ∀ y, 0 ≤ V y)
        (hPt : ∑ x, P x = 1) (hVt : ∑ y, V y = 1) :
        (∑ x, ∑ y, |P x*U y-Q x*V y|) ≤
          (∑ x, |P x-Q x|) + ∑ y, |U y-V y| := by
    …

29. theorem OAI.DilutedSpinGlass.Pattern.observable_variation line 411

    Source documentation

    Testing a spin pattern by a bounded observable costs twice the total variation.

    theorem observable_variation {α : Type*} [Fintype α] (P Q f : α → ℝ)
        (hf : ∀ x, |f x| ≤ 1) :
        |(∑ x, P x*f x)-(∑ x, Q x*f x)| ≤ ∑ x, |P x-Q x| := by
    …

30. theorem OAI.DilutedSpinGlass.Pattern.product_variation line 425

    Source documentation

    Tensorization with the sharp linear number of independent labels.

    theorem product_variation {α : Type*} [Fintype α]
        (P Q : α → ℝ) (hP : ∀ x, 0 ≤ P x) (hQ : ∀ x, 0 ≤ Q x)
        (hPt : ∑ x, P x = 1) (hQt : ∑ x, Q x = 1) (a : ℕ) :
        (∑ x : Fin a → α, |(∏ i, P (x i))-(∏ i, Q (x i))|) ≤
          (a : ℝ) * ∑ x, |P x-Q x| := by
    …

31. theorem OAI.DilutedSpinGlass.Pattern.pattern_replacement line 451

    Source documentation

    The deterministic empirical-pattern comparison in comp:patterns. The hypotheses are probability masses, and the conclusion involves ALL nonempty replica-subset moments, with no assumption of decorrelation.

    theorem pattern_replacement {ι : Type*} [Fintype ι] [DecidableEq ι]
        (P Q : (ι → Bool) → ℝ) (hP : ∀ x, 0 ≤ P x) (hQ : ∀ x, 0 ≤ Q x)
        (hPt : ∑ x, P x = 1) (hQt : ∑ x, Q x = 1) (a : ℕ)
        (f : (Fin a → (ι → Bool)) → ℝ) (hf : ∀ x, |f x| ≤ 1) :
        |(∑ x, (∏ i, P (x i))*f x)-(∑ x, (∏ i, Q (x i))*f x)| ≤
          (a : ℝ) * ∑ S ∈ (Finset.univ : Finset (Finset ι)).erase ∅, |moment P S-moment Q S| := by
    …

    Mentions: OAI.DilutedSpinGlass.Pattern.moment

32. def OAI.DilutedSpinGlass.Pattern.empirical line 462

    Source documentation

    Empirical law of the replica pattern at a uniformly sampled site.

    noncomputable def empirical {ι : Type*} [Fintype ι] {N : ℕ}
        (σ : Fin N → ι → Bool) (e : ι → Bool) : ℝ := by
    …

33. theorem OAI.DilutedSpinGlass.Pattern.empirical_nonneg line 467
34. theorem OAI.DilutedSpinGlass.Pattern.empirical_total line 471

    Source documentation

    The normalization uses N>=1, as required for reservoir sizes.

    theorem empirical_total {ι : Type*} [Fintype ι] [DecidableEq ι] {N : ℕ} (hN : 0 < N)
        (σ : Fin N → ι → Bool) : (∑ e, empirical σ e) = 1 := by
    …

    Mentions: OAI.DilutedSpinGlass.Pattern.empirical

35. theorem OAI.DilutedSpinGlass.Pattern.empirical_moment line 482
36. theorem OAI.DilutedSpinGlass.Pattern.mass_le_one line 503
37. theorem OAI.DilutedSpinGlass.Pattern.mass_abs_average line 509
38. theorem OAI.DilutedSpinGlass.Pattern.bounded_integrable line 518
39. def OAI.DilutedSpinGlass.Pattern.meanMass line 524

    Source documentation

    The unconditional spin-pattern distribution, not a conditional law.

    noncomputable def meanMass (P : Ω → α → ℝ) (x : α) : ℝ := ∫ ω, P ω x ∂μ
    …

40. theorem OAI.DilutedSpinGlass.Pattern.meanMass_nonneg line 527
41. theorem OAI.DilutedSpinGlass.Pattern.meanMass_total line 530
42. theorem OAI.DilutedSpinGlass.Pattern.meanMass_moment line 543

    Source documentation

    Averaging the empirical law reproduces the expected multioverlaps.

    theorem meanMass_moment {ι : Type*} [Fintype ι] [DecidableEq ι]
        (P : Ω → (ι → Bool) → ℝ) (hm : ∀ x, Measurable (fun ω => P ω x))
        (hP : ∀ ω x, 0 ≤ P ω x) (hPt : ∀ ω, ∑ x, P ω x = 1) (S : Finset ι) :
        moment (meanMass (μ := μ) P) S = ∫ ω, moment (P ω) S ∂μ := by
    …

    Mentions: OAI.DilutedSpinGlass.Pattern.moment, OAI.DilutedSpinGlass.Pattern.meanMass

43. theorem OAI.DilutedSpinGlass.Pattern.expected_pattern_replacement line 557

    Source documentation

    The integrated empirical-pattern comparison, valid for arbitrary reservoir root laws. This is comp:pattern-error; conditioning on independent new insertion disorder can subsequently be performed without changing the bound.

    theorem expected_pattern_replacement {ι : Type*} [Fintype ι] [DecidableEq ι]
        (P : Ω → (ι → Bool) → ℝ) (hm : ∀ x, Measurable (fun ω => P ω x))
        (hP : ∀ ω x, 0 ≤ P ω x) (hPt : ∀ ω, ∑ x, P ω x = 1)
        (a : ℕ) (f : (Fin a → (ι → Bool)) → ℝ) (hf : ∀ x, |f x| ≤ 1) :
        |(∫ ω, ∑ x, (∏ i, P ω (x i))*f x ∂μ) -
          (∑ x, (∏ i, meanMass (μ := μ) P (x i))*f x)| ≤
    …

    Mentions: OAI.DilutedSpinGlass.Pattern.meanMass

44. lemma OAI.DilutedSpinGlass.limsup_finite_bound line 612
45. lemma OAI.DilutedSpinGlass.series_double_limit line 638

    Source documentation

    Uniform summable remainders commute with the ordered limsup/grid limits. No diagonal exchange of the two limits is used.

    lemma series_double_limit (a : ℕ → ℕ → ℝ) (f : ℕ → ℕ → ℕ → ℝ)
        (c tail : ℕ → ℝ) (ha : ∀ L n, 0≤a L n)
        (hab : ∀ L, IsBoundedUnder (·≤·) atTop (a L))
        (hc : ∀ k, 0≤c k) (hf : ∀ k L, IsBoundedUnder (·≤·) atTop (f k L))
        (hflim : ∀ k, Tendsto (fun L => limsup (f k L) atTop) atTop (𝓝 0))
        (htail : Tendsto tail atTop (𝓝 0))
        (h : ∀ K L n, a L n≤tail K+∑ k∈Finset.range K, c k*f k L n) :
        Tendsto (fun L => limsup (a L) atTop) atTop (𝓝 0) := by
    …