OAI/Probability/InvariantIsing/Haar/HaarPolynomialRotation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial differentiation along the actual special-orthogonal rotations.

  1. def OAI.InvariantIsing.haarMatrixCoordinate line 12

    Source documentation

    Coordinate evaluation in the Frobenius matrix space.

    def haarMatrixCoordinate {N : ℕ} (i j : Fin N) :
    Matrix (Fin N) (Fin N) ℝ →L[ℝ] ℝ :=
…
  2. lemma OAI.InvariantIsing.hasDerivAt_specialPlaneRotation_entry line 19
  3. theorem OAI.InvariantIsing.hasDerivAt_specialPlaneRotation_polynomial line 35