OAI/Probability/InvariantIsing/Arrays/TensorHaarWard.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.finiteGibbsVariation line 18
2. lemma OAI.InvariantIsing.measurable_finiteGibbsVariation line 22
3. lemma OAI.InvariantIsing.finiteGibbsVariation_add_H line 34
4. lemma OAI.InvariantIsing.integrable_gaussian_finiteGibbsVariation line 42
5. lemma OAI.InvariantIsing.integral_gaussian_finiteGibbsVariation line 53

   Source documentation

   Pointwise averaging of the normalized Gibbs rotation derivative over finite Gaussian marks leaves precisely its explicit covariance correction.

   lemma integral_gaussian_finiteGibbsVariation {d : ℕ} {w : S → ℝ}
       (hw : GibbsReference w) (H O A dO : S → ℝ) (D C : S → Fin (d + 1) → ℝ) :
       (∫ g, finiteGibbsVariation w (fun x => H x + linearGaussian C g x) O
         (fun x => A x + linearGaussian D g x) dO
         ∂Measure.pi (fun _ : Fin (d + 1) => gaussianReal 0 1)) =
         (∫ g, finiteGibbsVariation w (fun x => H x + linearGaussian C g x) O A dO
           ∂Measure.pi (fun _ : Fin (d + 1) => gaussianReal 0 1)) +
         ∫ g, gaussianWardCorrection w (fun x => H x + linearGaussian C g x) O (gaussianCross D C)
           ∂Measure.pi (fun _ : Fin (d + 1) => gaussianReal 0 1) := by
   …

   Mentions: OAI.InvariantIsing.finiteGibbsVariation, OAI.InvariantIsing.gaussianWardCorrection

6. lemma OAI.InvariantIsing.abs_linearGaussian_le line 70
7. theorem OAI.InvariantIsing.integral_special_gaussian_gibbs_rotation_identity line 82

   Source documentation

   A finite-prior Haar Ward identity with Gaussian coefficient tensors. The assumptions are elementary measurability, derivatives and finite bounds; the covariance correction is derived, not postulated.

   theorem integral_special_gaussian_gibbs_rotation_identity {N d : ℕ}
       (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
       (R : ℝ → SpecialOrthogonal N) (hR : R 0 = 1)
       {w : S → ℝ} (hw : GibbsReference w)
       (H O : SpecialOrthogonal N → S → ℝ) (C : SpecialOrthogonal N → S → Fin (d + 1) → ℝ)
       (hHm : ∀ x, Measurable (fun U => H U x))
       (hOm : ∀ x, Measurable (fun U => O U x))
       (hCm : ∀ x a, Measurable (fun U => C U x a))
       (dH dO : ℝ → SpecialOrthogonal N → S → ℝ)
       (dC : ℝ → SpecialOrthogonal N → S → Fin (d + 1) → ℝ)
       (hdHm : ∀ x, Measurable (fun U => dH 0 U x))
       (hdOm : ∀ x, Measurable (fun U => dO 0 U x))
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal