PressureMean.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Almost-sure concentration of the actual pressure about its expectation.

def OAI.InvariantIsing.noninteractingPressure line 15
Source documentation
Deterministic reference obtained by removing the quadratic interaction.
```
def noninteractingPressure {N : ℕ} (c : Fin N → ℝ) : ℝ :=
…
```
lemma OAI.InvariantIsing.rotatedPressure_zero line 18
lemma OAI.InvariantIsing.abs_pressure_sub_noninteracting_le line 22

theorem OAI.InvariantIsing.ae_pressure_sub_mean_tendsto_zero line 30

Source documentation

Uniformly bounded spectra give almost-sure concentration about the mean, for arbitrary deterministic fields and arbitrary dependence across dimensions.

theorem ae_pressure_sub_mean_tendsto_zero (hpub : HaarConcentrationInput)
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (U : (n : ℕ) → Ω → SpecialOrthogonal (n + 3))
    (hU : ∀ n, Measurable (U n))
    (hHaar : ∀ n, (P.map (U n)).IsMulLeftInvariant)
    (eig c : (n : ℕ) → Fin (n + 3) → ℝ)
    (K : ℝ) (hK : 0 < K) (heig : ∀ n i, |eig n i| ≤ K) :
    ∀ᵐ ω ∂P, Tendsto (fun n =>
      rotatedPressure (eig n) (specialRotation (U n ω)) (c n) -
        ∫ η, rotatedPressure (eig n) (specialRotation (U n η)) (c n) ∂P)
      atTop (𝓝 0) := by
…

Mentions: OAI.InvariantIsing.HaarConcentrationInput, OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.specialRotation