TensorPerturbationVariance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The full O(1/N) pressure variance for the manuscript's finite perturbation.

lemma OAI.InvariantIsing.monomialVarianceIncrement_zero_le_one line 15

theorem OAI.InvariantIsing.tensorPerturbationPressure_variance line 25

Source documentation

With bounded field heights and linearly enumerated monomial degrees, the actual finite perturbation has a uniform pressure variance of order inverse volume. The only conditional inputs are the named Haar and Gaussian concentration consequences.

theorem tensorPerturbationPressure_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), ∀ degree : Fin N → Fin m → ℕ,
    ∀ u : Fin N → ℝ, (∀ j, |u j| ≤ 2) →
    ∀ D : ℝ, 0 ≤ D → (∀ j, (∑ a, (degree j a : ℝ)) ≤ D * ((j : ℝ) + 1)) →
    ∀ n : ℕ, ∀ treeDegree : Fin N → ℕ, ∀ b : ℕ → ℝ, CascadeExponents n b →
    ∀ h : ℕ → ℝ, Monotone h → 0 ≤ h 0 → ∀ H : ℝ, h n ≤ H →
      let v := tensorPathProfile I degree n treeDegree h
…

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