OAI/Probability/DilutedSpin/FullSelectedThermal.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.KernelTower.thermalDefect_bound line 13
2. def OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedThermal line 35
3. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_fullSelectedThermal line 50
4. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedThermal_nonneg line 77
5. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedThermal_bound line 82
6. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedThermal_integral_sq line 90
7. theorem OAI.DilutedSpinGlass.fullRoot_average_sq line 113

   Source documentation

   Jensen under the genuine entire disorder law, using its actual Poisson count.

   theorem fullRoot_average_sq
       (ξ : Fin M → Measure Y) [∀ j, IsProbabilityMeasure (ξ j)]
       (μ : Measure X) [IsProbabilityMeasure μ] (ν : Measure I) [IsProbabilityMeasure ν] (r s : ℝ≥0)
       {F : FullRootState Y X I M → ℝ} (hF : Measurable F) {K : ℝ}
       (hb : ∀ z, (F z)^2 ≤ K*(z.2.2.1:ℝ)) :
       (∫ z, F z ∂fullRootLaw ξ μ ν r s)^2 ≤ K*s := by
   …

   Mentions: OAI.DilutedSpinGlass.FullRootState, OAI.DilutedSpinGlass.fullRootLaw

8. lemma OAI.DilutedSpinGlass.SizeCoupling.measurable_integral_family line 146
9. lemma OAI.DilutedSpinGlass.SizeCoupling.measurable_spinMean_family line 151
10. lemma OAI.DilutedSpinGlass.SizeCoupling.measurable_countedMean_family line 174

    Source documentation

    Quenched averaging preserves measurability in the entire parameter vector, not merely in a single selected coordinate.

    lemma measurable_countedMean_family (μ : Measure X) [IsProbabilityMeasure μ]
        (ξ : Measure Y) [IsProbabilityMeasure ξ] (ν : Measure I) [IsProbabilityMeasure ν]
        {p r N : ℕ} [NeZero N] (theta : X → InteractionSample p) (field : Y → ℝ)
        (hθ : ∀ σ, Measurable (fun x => (theta x).1 σ)) (hh : Measurable field)
        (Q : (i : I) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
        (ψ : Z → (i : I) → Spin → FinitePath (A i) (r+1) → ℝ)
        (hψ : ∀ i σ a, Measurable (fun z => ψ z i σ a)) (k l : ℕ) :
        Measurable (fun z => countedMean (N := N) μ ξ ν theta field Q m (ψ z) k l) := by
    …

    Mentions: OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.SizeCoupling.countedMean

11. lemma OAI.DilutedSpinGlass.SizeCoupling.measurable_perturbedMean_family line 203
12. theorem OAI.DilutedSpinGlass.SizeCoupling.parameter_average_negligible line 222
13. lemma OAI.DilutedSpinGlass.PrescribedTree.constrainedHistory_singleton line 252