PressureDifferenceConcentration.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Centering a logpartition difference using its two pressure variances.

theorem OAI.InvariantIsing.centered_scaled_difference_L1_bound line 15

Source documentation

The frozen CGF of one perturbation is a scaled difference of two pressures. Both variances suffice even though those pressures are dependent.

theorem centered_scaled_difference_L1_bound {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] {F G Z : Ω → ℝ} {a B : ℝ}
    (hF : MemLp F 2 P) (hG : MemLp G 2 P)
    (hvF : variance F P ≤ B) (hvG : variance G P ≤ B)
    (he : Z =ᵐ[P] fun ω => a * (F ω - G ω)) :
    MemLp Z 2 P ∧
      (∫ ω, |Z ω - ∫ ω', Z ω' ∂P| ∂P) ≤ 2 * |a| * Real.sqrt B := by
…