OAI/Probability/InvariantIsing/Haar/HaarPolynomialValue.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded continuous polynomial observables on the physical rotation group.

  1. def OAI.InvariantIsing.haarPolynomialValue line 12
  2. lemma OAI.InvariantIsing.continuous_haarPolynomialValue line 15
  3. lemma OAI.InvariantIsing.haarPolynomialValue_bound line 23
  4. lemma OAI.InvariantIsing.haarPolynomialValue_integrable line 29
  5. theorem OAI.InvariantIsing.integral_haarPolynomialDerivation line 37

    Source documentation

    Infinitesimal Haar invariance, with the domination supplied by compactness.

    theorem integral_haarPolynomialDerivation {N : ℕ}
    (μ : Measure (SpecialOrthogonal N)) [IsFiniteMeasure μ] [μ.IsMulLeftInvariant]
    (p : MatrixPolynomial N) (i j : Fin N) :
    (∫ U, haarPolynomialValue (matrixPolynomialDerivation (planeGenerator i j) p) U ∂μ) = 0 := by
…

    Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.MatrixPolynomial, OAI.InvariantIsing.haarPolynomialValue, OAI.InvariantIsing.matrixPolynomialDerivation, OAI.InvariantIsing.planeGenerator