OAI/Probability/InvariantIsing/Haar/HaarFunctionalCurvature.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The sum of squared Lie brackets, with the precise dimension factor.

  1. def OAI.InvariantIsing.planeFunctionalMatrix line 11
  2. lemma OAI.InvariantIsing.planeFunctionalMatrix_skew line 15
  3. lemma OAI.InvariantIsing.sum_plane_functional_bracket_sq line 22
  4. theorem OAI.InvariantIsing.sum_plane_functional_double_bracket_sq line 49

    Source documentation

    The ordered-plane convention has curvature factor N - 2. The factor four here becomes one after the antisymmetric Hessian estimate.

    theorem sum_plane_functional_double_bracket_sq {N : ℕ}
    (ell : Matrix (Fin N) (Fin N) ℝ →ₗ[ℝ] ℝ) :
    (∑ i, ∑ j, ∑ k, ∑ l,
      (ell (planeGenerator i j*planeGenerator k l-
        planeGenerator k l*planeGenerator i j))^2) =
      (4*((N : ℝ)-2))*(∑ i, ∑ j, (ell (planeGenerator i j))^2) := by
…

    Mentions: OAI.InvariantIsing.planeGenerator