OAI/Probability/DilutedSpin/NormalizedCutoff.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.centerSample line 11
2. lemma OAI.DilutedSpinGlass.measurable_centerSample line 13
3. def OAI.DilutedSpinGlass.centeredModel line 16
4. def OAI.DilutedSpinGlass.clippedModel line 19
5. lemma OAI.DilutedSpinGlass.clipReal_abs_le line 22
6. lemma OAI.DilutedSpinGlass.clipSample_norm_le line 28
7. lemma OAI.DilutedSpinGlass.clipSample_difference_bound line 34
8. lemma OAI.DilutedSpinGlass.clipSample_eventually_eq line 40
9. lemma OAI.DilutedSpinGlass.clipReal_eventually_eq line 49
10. lemma OAI.DilutedSpinGlass.clipping_interaction_error_tendsto line 54
11. lemma OAI.DilutedSpinGlass.clipping_field_error_tendsto line 65
12. lemma OAI.DilutedSpinGlass.centeredModel_symmetric line 79
13. lemma OAI.DilutedSpinGlass.convex_pow_tangent line 101
14. lemma OAI.DilutedSpinGlass.even_cavity_remainder_nonneg line 117
15. lemma OAI.DilutedSpinGlass.admissible_upper_coefficient_nonpos line 125

    Source documentation

    Coefficients of all three regularized insertions share this sign.

    lemma admissible_upper_coefficient_nonpos {p : ℕ} (M : Model p) (hM : Admissible M)
        (n : ℕ) (hn : 1≤n) (t P B : ℝ) (ht : 0≤t) :
        -(t^n/(n:ℝ))*(∫ z : InteractionSample p,(-z.2.2.1)^n ∂M.disorder.toMeasure)*
          (P^p-(p:ℝ)*P*B^(p-1)+((p-1:ℕ):ℝ)*B^p) ≤ 0 := by
    …

    Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.Admissible, OAI.DilutedSpinGlass.InteractionSample

16. lemma OAI.DilutedSpinGlass.regularized_ratio_pos line 134
17. lemma OAI.DilutedSpinGlass.regularized_ratio_bounds line 143
18. lemma OAI.DilutedSpinGlass.regularized_normalized_log_bound line 163

    Source documentation

    Normalized regularization never requires integrability of log a.

    lemma regularized_normalized_log_bound {d d₀ t C : ℝ} (hC : 0≤C)
        (hd : |d|<1) (hd₀ : |d₀|<1) (ht0 : 0≤t) (ht1 : t≤1)
        (hlo : Real.exp (-C)≤(1+d)/(1+d₀)) (hhi : (1+d)/(1+d₀)≤Real.exp C) :
        |Real.log (1+t*d)-Real.log (1+t*d₀)|≤C := by
    …