OAI/Probability/InvariantIsing/Haar/HaarHeatContinuity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Joint continuity of the finite polynomial heat flow.

  1. def OAI.InvariantIsing.haarPolynomialBasis line 11
  2. lemma OAI.InvariantIsing.haarPolynomialEval_eq_coordinates line 15
  3. lemma OAI.InvariantIsing.continuous_haarPolynomialHeat_coordinates line 29
  4. lemma OAI.InvariantIsing.continuous_haarPolynomialHeat_value line 37