OAI/Probability/DilutedSpin/FunctionalStability.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integral_independentInsertion_trialLog line 24
2. lemma OAI.DilutedSpinGlass.fieldAverage_map_stability line 57
3. lemma OAI.DilutedSpinGlass.disorderAverage_map_eq line 78
4. lemma OAI.DilutedSpinGlass.disorderAverage_map_stability line 88
5. lemma OAI.DilutedSpinGlass.pressure_map_stability line 115

   Source documentation

   Uniform first-moment stability of the exact pinned physical pressure.

   lemma pressure_map_stability {p N : ℕ} (M : Model p) (hN : 0<N)
       (hθ : Integrable (fun z : InteractionSample p => ‖z.1‖) M.disorder.toMeasure)
       (hh : Integrable (fun h : ℝ => |h|) M.field.toMeasure)
       (T : InteractionSample p → InteractionSample p) (g : ℝ → ℝ)
       (hT : Measurable T) (hg : Measurable g)
       (hD : Integrable (fun z => ‖(T z).1-z.1‖) M.disorder.toMeasure)
       (hd : Integrable (fun h => |g h-h|) M.field.toMeasure) :
       |pressure (mapModel M T g hT hg) N-pressure M N|≤
         (M.alpha:ℝ)*(∫ z,‖(T z).1-z.1‖ ∂M.disorder.toMeasure)+(∫ h,|g h-h| ∂M.field.toMeasure) := by
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.pressure, OAI.DilutedSpinGlass.mapModel

6. lemma OAI.DilutedSpinGlass.trialSiteField_map_eq line 154
7. lemma OAI.DilutedSpinGlass.trialSiteField_map_stability line 163
8. lemma OAI.DilutedSpinGlass.trialSiteDisorder_map_eq line 180
9. lemma OAI.DilutedSpinGlass.trialSiteDisorder_map_stability line 190
10. lemma OAI.DilutedSpinGlass.functional_map_stability line 216
11. def OAI.DilutedSpinGlass.trialDisorderAt line 282
12. lemma OAI.DilutedSpinGlass.trialDisorderAt_measurable line 288
13. lemma OAI.DilutedSpinGlass.trialDisorderAt_bound line 292
14. lemma OAI.DilutedSpinGlass.trialSite_integrable_prod line 302
15. lemma OAI.DilutedSpinGlass.trialDisorderAt_integral line 312
16. lemma OAI.DilutedSpinGlass.trialDisorderAt_joint_integrable line 318
17. lemma OAI.DilutedSpinGlass.trialPoisson_field_order line 327