NSpinTensorHaar.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The Haar variance contribution for the actual tensor-enriched pressure.

theorem OAI.InvariantIsing.haar_tensorEnrichedPressure_variance line 18

Source documentation

Haar contributes the square of the normalized covariance rotation modulus divided by volume. The Gaussian and cascade randomness have been averaged in this observable, using the proved flat mean identity.

theorem haar_tensorEnrichedPressure_variance (hpub : HaarConcentrationInput) :
    ∃ C : ℝ, 0 < C ∧
    ∀ N : ℕ, 3 ≤ N →
    ∀ μ : Measure (SpecialOrthogonal N),
      IsProbabilityMeasure μ → μ.IsMulLeftInvariant →
    ∀ m k : ℕ, ∀ eig c : Fin N → ℝ,
    ∀ K : ℝ, 0 < K → (∀ i, |eig i| ≤ K) →
    ∀ I : Fin m → Finset (Fin N), ∀ degree : Fin k → Fin m → ℕ,
    ∀ amplitude : Fin k → ℝ, ∀ n : ℕ, ∀ b : ℕ → ℝ,
      CascadeExponents n b →
    ∀ site : ℕ → ℝ≥0, ∀ monomial : ℕ → Fin k → ℝ≥0,
      let v := fun i => tensorVarianceProfile I degree (site i) (monomial i)
…

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