OAI/Probability/InvariantIsing/Haar/HaarPolynomialHeat.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InvariantIsing.HaarPolynomialCoordinates line 11
2. def OAI.InvariantIsing.haarPolynomialCoordinates line 14
3. def OAI.InvariantIsing.haarPolynomialRestrictedLaplacian line 18
4. def OAI.InvariantIsing.haarPolynomialCoordinateLaplacian line 22
5. def OAI.InvariantIsing.haarPolynomialHeat line 28
6. lemma OAI.InvariantIsing.haarPolynomialHeat_zero line 34
7. lemma OAI.InvariantIsing.haarPolynomialCoordinates_heat line 38
8. lemma OAI.InvariantIsing.haarPolynomialCoordinateLaplacian_apply line 46
9. def OAI.InvariantIsing.haarPolynomialCoordinateEval line 55
10. lemma OAI.InvariantIsing.haarPolynomialCoordinateEval_apply line 61
11. theorem OAI.InvariantIsing.haarPolynomialHeat_hasDerivAt line 68

    Source documentation

    The finite matrix exponential satisfies the actual heat equation under evaluation.

    theorem haarPolynomialHeat_hasDerivAt {N d : ℕ}
        (p : haarPolynomialSpace N d) (M : Matrix (Fin N) (Fin N) ℝ) (t : ℝ) :
        HasDerivAt (fun s => matrixPolynomialEval M
            ((haarPolynomialHeat N d s p : haarPolynomialSpace N d) : MatrixPolynomial N))
          (matrixPolynomialEval M (haarPolynomialLaplacian N
            ((haarPolynomialHeat N d t p : haarPolynomialSpace N d) : MatrixPolynomial N))) t := by
    …

    Mentions: OAI.InvariantIsing.haarPolynomialSpace, OAI.InvariantIsing.matrixPolynomialEval, OAI.InvariantIsing.haarPolynomialHeat, OAI.InvariantIsing.MatrixPolynomial, OAI.InvariantIsing.haarPolynomialLaplacian