HaarDerivative.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Differentiating Haar rotation invariance

Infinitesimal Haar invariance gives the integral identity for spectral Ward identities under explicit domination assumptions.

abbrev OAI.InvariantIsing.Orthogonal line 19
Also declared: ComparatorChallenges/InvariantIsing.lean:27 (same declaration text).

lemma OAI.InvariantIsing.integral_rotation_derivative_eq_zero line 22

Source documentation

A dominated infinitesimal left rotation has Haar mean zero.

lemma integral_rotation_derivative_eq_zero {N : ℕ} (μ : Measure (Orthogonal N))
    [μ.IsMulLeftInvariant] (R : ℝ → Orthogonal N) (hR : R 0 = 1)
    (f : Orthogonal N → ℝ) (hf : Measurable f) (hfi : Integrable f μ)
    (f' : ℝ → Orthogonal N → ℝ) (hf' : AEStronglyMeasurable (f' 0) μ)
    (B : Orthogonal N → ℝ) (hB : Integrable B μ)
    (hbound : ∀ᵐ U ∂μ, ∀ t ∈ Set.Ioo (-1 : ℝ) 1, ‖f' t U‖ ≤ B U)
    (hderiv : ∀ᵐ U ∂μ, ∀ t ∈ Set.Ioo (-1 : ℝ) 1,
      HasDerivAt (fun s => f (R s * U)) (f' t U) t) :
    ∫ U, f' 0 U ∂μ = 0 := by
…

Mentions: OAI.InvariantIsing.Orthogonal