Concentration.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Haar concentration for Ising pressure

Frobenius Lipschitz continuity and measurability give concentration of the Ising pressure about a median.

lemma OAI.InvariantIsing.measurable_specialRotation_eval line 19
lemma OAI.InvariantIsing.measurable_rotatedPressure line 29

theorem OAI.InvariantIsing.haar_pressure_median_tail line 43

Source documentation

Uniform concentration about a median for the actual spectral-orbit pressure, conditional only on the cited concentration theorem. No pressure limit is an assumption or a conclusion of this finite-volume estimate.

theorem haar_pressure_median_tail (hpub : HaarConcentrationInput) :
    ∃ C c₀ : ℝ, 0 < C ∧ 0 < c₀ ∧
    ∀ N : ℕ, 3 ≤ N →
    ∀ μ : Measure (SpecialOrthogonal N),
      IsProbabilityMeasure μ → μ.IsMulLeftInvariant →
    ∀ eig c : Fin N → ℝ, ∀ K : ℝ, 0 < K → (∀ i, |eig i| ≤ K) →
    ∃ m : ℝ,
      (1 / 2 : ℝ) ≤ μ.real {U | rotatedPressure eig (specialRotation U) c ≤ m} ∧
      (1 / 2 : ℝ) ≤ μ.real {U | m ≤ rotatedPressure eig (specialRotation U) c} ∧
      ∀ r : ℝ, 0 < r →
        μ.real {U | r ≤ |rotatedPressure eig (specialRotation U) c - m|} ≤
          C * Real.exp (-c₀ * (N : ℝ) * r ^ 2 / K ^ 2) := by
…

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