HaarVariance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Haar variance for the Frobenius moduli used by the perturbed model.

lemma OAI.InvariantIsing.haar_frobeniusLipschitz_memLp_two line 13

theorem OAI.InvariantIsing.haar_frobeniusLipschitz_variance line 32

Source documentation

The published concentration input bounds every measurable Frobenius Lipschitz observable, with constants independent of dimension.

theorem haar_frobeniusLipschitz_variance (hpub : HaarConcentrationInput) :
    ∃ C : ℝ, 0 < C ∧
    ∀ N : ℕ, 3 ≤ N →
    ∀ μ : Measure (SpecialOrthogonal N),
      IsProbabilityMeasure μ → μ.IsMulLeftInvariant →
    ∀ f : SpecialOrthogonal N → ℝ, Measurable f →
    ∀ L : ℝ, 0 < L →
      (∀ U V, |f U - f V| ≤ L * frobeniusDistance U V) →
      variance f μ ≤ C * L ^ 2 / N := by
…

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