PlaneRotation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Smooth coordinate-plane rotations for the finite Haar Ward calculation.

def OAI.InvariantIsing.planeGenerator line 14
Source documentation
Generator with xᵢ'=xⱼ and xⱼ'=-xᵢ.
```
def planeGenerator {N : ℕ} (i j : Fin N) : Matrix (Fin N) (Fin N) ℝ :=
…
```
lemma OAI.InvariantIsing.planeGenerator_skew line 17
def OAI.InvariantIsing.planeRotation line 23
Source documentation
The exponential of the plane generator is orthogonal.
```
def planeRotation {N : ℕ} (i j : Fin N) (t : ℝ) : Orthogonal N :=
…
```
Mentions: OAI.InvariantIsing.Orthogonal
lemma OAI.InvariantIsing.planeRotation_zero line 29
lemma OAI.InvariantIsing.planeGenerator_mulVec line 33
def OAI.InvariantIsing.matrixVectorCoordinate line 40
Source documentation
Coordinate evaluation of matrix-vector multiplication as a continuous linear functional, with the Frobenius norm used only for the exponential.
```
def matrixVectorCoordinate {N : ℕ} (k : Fin N) (v : Fin N → ℝ) :
    Matrix (Fin N) (Fin N) ℝ →L[ℝ] ℝ :=
…
```

lemma OAI.InvariantIsing.hasDerivAt_planeRotation_coordinate line 48

Source documentation

The coordinate derivative along a genuine Haar-preserving plane rotation.

lemma hasDerivAt_planeRotation_coordinate {N : ℕ} (i j k : Fin N)
    (U : Orthogonal N) (v : EuclideanSpace ℝ (Fin N)) (t : ℝ) :
    HasDerivAt (fun s => matrixRotation (planeRotation i j s * U) v k)
      ((if k = i then matrixRotation (planeRotation i j t * U) v j else 0) -
        (if k = j then matrixRotation (planeRotation i j t * U) v i else 0)) t := by
…

Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.matrixRotation, OAI.InvariantIsing.planeRotation

lemma OAI.InvariantIsing.hasDerivAt_planeRotation_energy line 66