TensorPerturbationCGF.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual finite perturbation has the CGF concentration needed at minima.

theorem OAI.InvariantIsing.tensorPerturbationCGF_statistics line 17

Source documentation

The selected field's mean is an actual pressure difference, and its centered fluctuation is uniformly of order square root volume.

theorem tensorPerturbationCGF_statistics (hhaar : HaarConcentrationInput)
    (hgauss : GaussianLipschitzVarianceInput) :
    ∃ C : ℝ, 0 < C ∧
    ∀ N : ℕ, 3 ≤ N →
    ∀ μ : Measure (SpecialOrthogonal N), IsProbabilityMeasure μ → μ.IsMulLeftInvariant →
    ∀ m : ℕ, ∀ eig c : Fin N → ℝ, ∀ K : ℝ, 0 < K → (∀ i, |eig i| ≤ K) →
    ∀ I : Fin m → Finset (Fin N), ∀ degree : Fin N → Fin m → ℕ,
    ∀ u : Fin N → ℝ, (∀ j, |u j| ≤ 2) →
    ∀ D : ℝ, 0 ≤ D → (∀ j, (∑ a, (degree j a : ℝ)) ≤ D * ((j : ℝ) + 1)) →
    ∀ n : ℕ, ∀ r : Fin N → ℕ, ∀ b : ℕ → ℝ, CascadeExponents n b →
    ∀ h : ℕ → ℝ, Monotone h → 0 ≤ h 0 → ∀ H : ℝ, h n ≤ H →
    ∀ j : Fin N, ∀ w : ℝ, |w| ≤ 2 →
…

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