OAI/Probability/InvariantIsing/Core/BoundedObservableMinimum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.bounded_nonnegative_cgf_bounds line 16
2. lemma OAI.InvariantIsing.integrable_bounded_random_cgf line 38
3. theorem OAI.InvariantIsing.boundedObservable_energy_at_minimum line 60

   Source documentation

   Unlike the Gaussian perturbation, a diagonal coordinate is a bounded observable of the random rotation. Its exact tilted fluctuation still follows from convexity, the deterministic minimum, and three pointwise concentration bounds.

   theorem boundedObservable_energy_at_minimum {Ω X : Type*}
       [MeasurableSpace Ω] [MeasurableSpace X]
       (P : Measure Ω) [IsProbabilityMeasure P] (ν : Ω → Measure X) (hν : Measurable ν)
       [∀ ω, IsProbabilityMeasure (ν ω)] (Y : Ω × X → ℝ) (hY : Measurable Y)
       (B : ℝ) (hB : ∀ ω x, |Y (ω, x)| ≤ B)
       {v c a s δ K : ℝ} (hs : 0 < s) (hK : 0 < K)
       (hmin : ∀ t ∈ Set.Icc (v - s) (v + s),
         -(∫ ω, cgf (fun x => Y (ω, x)) (ν ω) v ∂P) + c * (v - a) ^ 2 ≤
         -(∫ ω, cgf (fun x => Y (ω, x)) (ν ω) t ∂P) + c * (t - a) ^ 2)
       (hconc : ∀ t ∈ ({v - s, v, v + s} : Set ℝ),
         (∫ ω, |cgf (fun x => Y (ω, x)) (ν ω) t -
           (∫ ω', cgf (fun x => Y (ω', x)) (ν ω') t ∂P)| ∂P) ≤ δ) :
   …