FullPerturbationVariance.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform variance for both terms of the actual finite perturbation.

theorem OAI.InvariantIsing.fullPerturbationPressure_variance line 19

Source documentation

The explicit complete monomial enumeration removes the degree-cap assumption. The diagonal perturbation is the exact eigenvalue shift proved in rotatedEnergy_diagonalPerturbation.

theorem fullPerturbationPressure_variance (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), ∀ u : Fin N → ℝ, (∀ j, |u j| ≤ 2) →
    ∀ v : Fin m → ℝ, (∀ a, |v a| ≤ 2) → ∀ t : ℝ, |t| ≤ 1 →
    ∀ n : ℕ, ∀ b : ℕ → ℝ, CascadeExponents n b →
    ∀ h : ℕ → ℝ, Monotone h → 0 ≤ h 0 → ∀ H : ℝ, h n ≤ H →
      let degree := fun j : Fin N => enumeratedSpectralDegree m j
…

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