OAI/Probability/DilutedSpin/MeasureHierarchy.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.MeasureMean.logMean line 14

   Source documentation

   Logarithmic conditional power mean, for an arbitrary Borel probability law.

   noncomputable def logMean (m : ℝ) (f : Ω → ℝ) : ℝ :=
   …

2. theorem OAI.DilutedSpinGlass.MeasureMean.bounded_integrable line 17
3. theorem OAI.DilutedSpinGlass.MeasureMean.exp_integrable line 22
4. theorem OAI.DilutedSpinGlass.MeasureMean.exp_integral_pos line 32
5. theorem OAI.DilutedSpinGlass.MeasureMean.logMean_const line 36
6. theorem OAI.DilutedSpinGlass.MeasureMean.logMean_mono line 40
7. theorem OAI.DilutedSpinGlass.MeasureMean.logMean_add_const line 49
8. theorem OAI.DilutedSpinGlass.MeasureMean.logMean_stability line 58
9. theorem OAI.DilutedSpinGlass.MeasureMean.logMean_bound line 72
10. theorem OAI.DilutedSpinGlass.MeasureMean.insertion line 80

    Source documentation

    The exact one-level insertion identity, not restricted to finite priors. The tilted law is Mathlib's normalized exponential tilted measure.

    theorem insertion {m : ℝ} (_hm : m ≠ 0) {f a : Ω → ℝ} {B C : ℝ}
        (hf : Measurable f) (ha : Measurable a) (hfb : ∀ x, |f x| ≤ B)
        (hab : ∀ x, |a x| ≤ C) :
        logMean μ m (fun x => f x+a x) - logMean μ m f =
          logMean (μ.tilted (fun x => m*f x)) m a := by
    …

    Mentions: OAI.DilutedSpinGlass.MeasureMean.logMean

11. theorem OAI.DilutedSpinGlass.MeasureMean.tilt_insertion line 97

    Source documentation

    The updated probability kernel is the same whether insertions are made successively or together.

    theorem tilt_insertion {m : ℝ} {f a : Ω → ℝ} {B : ℝ}
        (hf : Measurable f) (hfb : ∀ x, |f x| ≤ B) :
        (μ.tilted (fun x => m*f x)).tilted (fun x => m*a x) =
          μ.tilted (fun x => m*(f x+a x)) := by
    …

12. theorem OAI.DilutedSpinGlass.logMean_continuous_bound line 113
13. theorem OAI.DilutedSpinGlass.trialLog_continuous_bound line 137
14. theorem OAI.DilutedSpinGlass.logMean_stability line 160
15. theorem OAI.DilutedSpinGlass.trialLog_stability line 173
16. theorem OAI.DilutedSpinGlass.continuous_q line 190
17. theorem OAI.DilutedSpinGlass.continuous_edge line 197
18. theorem OAI.DilutedSpinGlass.continuous_log_edge line 204
19. theorem OAI.DilutedSpinGlass.continuous_message line 208
20. theorem OAI.DilutedSpinGlass.continuous_siteLog line 223
21. theorem OAI.DilutedSpinGlass.weighted_exp_pos line 244
22. theorem OAI.DilutedSpinGlass.weighted_log_exp_stability line 252

    Source documentation

    Stability before any disorder averaging; no lower bound on the positive message probabilities or moment condition on the messages occurs.

    theorem weighted_log_exp_stability {ι : Type*} [Fintype ι] (w f g : ι → ℝ)
        (hw : ∀ i, 0 ≤ w i) (hs : ∑ i, w i = 1) {D : ℝ}
        (hD : ∀ i, |f i-g i| ≤ D) :
        |Real.log (∑ i, w i * Real.exp (f i)) -
          Real.log (∑ i, w i * Real.exp (g i))| ≤ D := by
    …

23. theorem OAI.DilutedSpinGlass.log_edge_stability line 273
24. theorem OAI.DilutedSpinGlass.message_stability line 280
25. theorem OAI.DilutedSpinGlass.siteLog_stability line 289
26. theorem OAI.DilutedSpinGlass.trial_edge_stability line 318
27. theorem OAI.DilutedSpinGlass.trial_site_stability line 325