OAI/Probability/DilutedSpin/FullSelectedRegularity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedLog line 17
2. def OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedScore line 25
3. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedLog_eq line 38
4. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedScore_eq line 49
5. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_fullSelectedLog line 58
6. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_fullSelectedScore line 66
7. def OAI.DilutedSpinGlass.clipReal line 93

   Source documentation

   A bounded representative, used only with a proof of AE equality. It does not impose a pointwise bound on all values of an unrestricted sample space.

   noncomputable def clipReal (C x : ℝ) : ℝ := max (-C) (min C x)

8. lemma OAI.DilutedSpinGlass.clipReal_bound line 95
9. lemma OAI.DilutedSpinGlass.clipReal_eq line 99
10. lemma OAI.DilutedSpinGlass.measurable_clipReal line 102
11. def OAI.DilutedSpinGlass.clipSample line 105
12. lemma OAI.DilutedSpinGlass.clipSample_bound line 108
13. lemma OAI.DilutedSpinGlass.clipSample_eq line 111
14. lemma OAI.DilutedSpinGlass.measurable_clipSample line 117
15. lemma OAI.DilutedSpinGlass.SizeCoupling.perturbedMean_congr line 128
16. theorem OAI.DilutedSpinGlass.SizeCoupling.actual_uniform_increment_ae line 141

    Source documentation

    The genuine bounded-model increment estimate, with AE (not vacuous global) bounds on the original physical law.

    theorem actual_uniform_increment_ae (ν : Measure I) [IsProbabilityMeasure ν]
        {p r N : ℕ} [NeZero N] (M : Model p)
        {C H : ℝ} (hC : 0 ≤ C) (hH : 0 ≤ H)
        (hθ : ∀ᵐ z ∂M.disorder.toMeasure, ∀ σ, |z.1 σ| ≤ C)
        (hh : ∀ᵐ h ∂M.field.toMeasure, |h| ≤ H)
        (Q : (i : I) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
        (hm : ∀ j, 0 < m j) (ψ : (i : I) → Spin → FinitePath (A i) (r+1) → ℝ)
        {D : ℝ} (hD : 0 ≤ D) (hψ : ∀ i σ a, |Real.log (ψ i σ a)| ≤ D) :
        |perturbedMean (N := N+1) M.disorder.toMeasure M.field.toMeasure ν id id Q m ψ
    …

    Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.SizeCoupling.perturbedMean