SpecialPlaneRotation.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Genuine coordinate-plane rotations and infinitesimal Haar invariance on SO(N), the rotation group used by the actual enriched model.

def OAI.InvariantIsing.specialToOrthogonal line 17
Source documentation
Forget only the determinant-one condition.
```
def specialToOrthogonal {N : ℕ} : SpecialOrthogonal N →* Orthogonal N where
…
```
Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Orthogonal
lemma OAI.InvariantIsing.matrixRotation_specialToOrthogonal line 22
lemma OAI.InvariantIsing.measurable_specialToOrthogonal line 25
lemma OAI.InvariantIsing.orthogonal_det_eq_one_or_neg_one line 30
Source documentation
Orthogonal determinants have only two possible real values.
```
lemma orthogonal_det_eq_one_or_neg_one {N : ℕ} (U : Orthogonal N) :
    (U : Matrix (Fin N) (Fin N) ℝ).det = 1 ∨
      (U : Matrix (Fin N) (Fin N) ℝ).det = -1 := by
…
```
Mentions: OAI.InvariantIsing.Orthogonal
lemma OAI.InvariantIsing.planeRotation_det line 39
Source documentation
A continuous plane-rotation path starts at determinant one and cannot switch between the two orthogonal determinant values.
```
lemma planeRotation_det {N : ℕ} (i j : Fin N) (t : ℝ) :
    (planeRotation i j t : Matrix (Fin N) (Fin N) ℝ).det = 1 := by
…
```
Mentions: OAI.InvariantIsing.planeRotation
def OAI.InvariantIsing.specialPlaneRotation line 56
Source documentation
The same matrix exponential, now as an element of the special orthogonal group.
```
def specialPlaneRotation {N : ℕ} (i j : Fin N) (t : ℝ) : SpecialOrthogonal N :=
…
```
Mentions: OAI.InvariantIsing.SpecialOrthogonal
lemma OAI.InvariantIsing.specialPlaneRotation_zero line 60
lemma OAI.InvariantIsing.specialToOrthogonal_planeRotation line 66

lemma OAI.InvariantIsing.integral_special_rotation_derivative_eq_zero line 70

Source documentation

A dominated infinitesimal left rotation has Haar mean zero.

lemma integral_special_rotation_derivative_eq_zero {N : ℕ} (μ : Measure (SpecialOrthogonal N))
    [μ.IsMulLeftInvariant] (R : ℝ → SpecialOrthogonal N) (hR : R 0 = 1)
    (f : SpecialOrthogonal N → ℝ) (hf : Measurable f) (hfi : Integrable f μ)
    (f' : ℝ → SpecialOrthogonal N → ℝ) (hf' : AEStronglyMeasurable (f' 0) μ)
    (B : SpecialOrthogonal 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.SpecialOrthogonal

theorem OAI.InvariantIsing.integral_special_gibbs_rotation_identity line 110

Source documentation

Exact finite-volume Haar Ward identity. All regularity assumptions concern finite-dimensional derivatives; none assumes a limiting overlap identity.

theorem integral_special_gibbs_rotation_identity {N : ℕ}
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
    (R : ℝ → SpecialOrthogonal N) (hR : R 0 = 1)
    {w : S → ℝ} (hw : GibbsReference w)
    (H A : SpecialOrthogonal N → S → ℝ)
    (hHm : ∀ σ, Measurable (fun U => H U σ))
    (hAm : ∀ σ, Measurable (fun U => A U σ))
    (dH dA : ℝ → SpecialOrthogonal N → S → ℝ)
    (hdHm : ∀ σ, Measurable (fun U => dH 0 U σ))
    (hdAm : ∀ σ, Measurable (fun U => dA 0 U σ))
    (hHd : ∀ U t, t ∈ Set.Ioo (-1 : ℝ) 1 → ∀ σ,
      HasDerivAt (fun s => H (R s * U) σ) (dH t U σ) t)
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal