OAI/Probability/DilutedSpin/Polarization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.Polarization.sign line 11
2. lemma OAI.DilutedSpinGlass.Polarization.sign_not line 12
3. lemma OAI.DilutedSpinGlass.Polarization.sign_sq line 13
4. def OAI.DilutedSpinGlass.Polarization.flip line 17
5. lemma OAI.DilutedSpinGlass.Polarization.flip_involutive line 18
6. lemma OAI.DilutedSpinGlass.Polarization.prod_sign_flip line 25
7. lemma OAI.DilutedSpinGlass.Polarization.signed_cube_sum line 37

   Source documentation

   The signed cube average annihilates every non-surjective assignment of k slots to k colors. Thus only permutations survive polarization.

   lemma signed_cube_sum (f : ι → ι) :
       (∑ ε : ι → Bool, (∏ i, sign (ε i)) * ∏ i, sign (ε (f i))) =
         if Function.Bijective f then (2 : ℝ) ^ Fintype.card ι else 0 := by
   …

   Mentions: OAI.DilutedSpinGlass.Polarization.sign

8. lemma OAI.DilutedSpinGlass.Polarization.signed_polarization line 69

   Source documentation

   Unnormalized real polarization, with exactly the ordered-permutation multiplicity. This does not assume a vanishing diagonal.

   lemma signed_polarization (M : MultilinearMap ℝ (fun _ : ι => E) ℝ)
       (hsym : ∀ (v : ι → E) (π : Equiv.Perm ι), M (v ∘ π) = M v) (v : ι → E) :
       (∑ ε : ι → Bool, (∏ j, sign (ε j)) *
           M (fun _ => ∑ j, sign (ε j) • v j)) =
         (2 : ℝ) ^ Fintype.card ι * (Fintype.card ι).factorial * M v := by
   …

   Mentions: OAI.DilutedSpinGlass.Polarization.sign

9. def OAI.DilutedSpinGlass.Polarization.averageDirection line 103
10. lemma OAI.DilutedSpinGlass.Polarization.normalized_polarization line 106
11. lemma OAI.DilutedSpinGlass.Polarization.averageDirection_bound line 137
12. lemma OAI.DilutedSpinGlass.abs_integral_le_one line 164
13. lemma OAI.DilutedSpinGlass.centered_scalar_div_bound line 174
14. theorem OAI.DilutedSpinGlass.root_matrix_error_bound line 191

    Source documentation

    Root averaging MUST precede the absolute value of the covariance. This lemma retains that quantifier order, while integrating genuine single-copy projection errors. There is no root-wise concentration hypothesis.

    theorem root_matrix_error_bound {Z : Type*} [MeasurableSpace Z] (μ : Measure Z)
        [IsProbabilityMeasure μ] (E H H1 F A Et Eo : Z → ℝ) (J δ c B M : ℝ)
        (hJ : J ≠ 0) (hδ : 0 ≤ δ)
        (hF : ∀ z, |F z| ≤ 1) (hA : ∀ z, |A z| ≤ 1)
        (h1 : ∀ z, H1 z/J = -δ*A z)
        (hE : Integrable E μ) (hH : Integrable H μ) (_hAint : Integrable A μ)
        (hEt : Integrable Et μ) (hEo : Integrable Eo μ)
        (hpoint : ∀ z, c*E z ≤ δ+H z/J+Et z*B/|J|+M*Eo z) :
        c*(∫ z, E z ∂μ) ≤ 2*δ+
          |(∫ z, H z ∂μ)-(∫ z, F z ∂μ)*(∫ z, H1 z ∂μ)|/|J|+
          (∫ z, Et z ∂μ)*B/|J|+M*(∫ z, Eo z ∂μ) := by
    …

15. theorem OAI.DilutedSpinGlass.select_parameters line 232
16. theorem OAI.DilutedSpinGlass.countable_parameter_selection line 270

    Source documentation

    All score errors are made small on one deterministic low-increment sequence. The parameter may range over an arbitrary probability space; this is the noncompact-parameter step in pert:selection.

    theorem countable_parameter_selection
        {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
        (Δ : ℕ → Ω → ℝ) (e : ℕ → ℕ → Ω → ℝ)
        (hΔ : ∀ N, Integrable (Δ N) μ) (he : ∀ ν N, Integrable (e ν N) μ)
        (hne : ∀ ν N x, 0 ≤ e ν N x)
        {C v u : ℝ} (hC : 0 ≤ C) (hvu : v < u)
        (hlower : ∀ N x, -C ≤ Δ N x)
        (hlow : ∀ n, ∃ N, n ≤ N ∧ ∫ x, Δ N x ∂μ ≤ v)
        (hlim : ∀ ν, Tendsto (fun N => ∫ x, e ν N x ∂μ) atTop (𝓝 0)) :
        ∃ (Ns : ℕ → ℕ) (xs : ℕ → Ω), StrictMono Ns ∧
          (∀ j, Δ (Ns j) (xs j) ≤ u) ∧
          (∀ ν, Tendsto (fun j => e ν (Ns j) (xs j)) atTop (𝓝 0)) := by
    …