OAI/Analysis/TriangularHilbert/HeatStar.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularHilbert.Heat.heatWeights line 16
  2. def OAI.TriangularHilbert.Heat.heatArray line 19
  3. def OAI.TriangularHilbert.Heat.heatEnergy line 22
  4. def OAI.TriangularHilbert.Heat.fixedBase line 25
  5. def OAI.TriangularHilbert.Heat.localGram line 28
  6. def OAI.TriangularHilbert.Heat.localFirst line 32
  7. def OAI.TriangularHilbert.Heat.localSecond line 36
  8. def OAI.TriangularHilbert.Heat.heatFirst line 40
  9. def OAI.TriangularHilbert.Heat.heatPure line 43
  10. def OAI.TriangularHilbert.Heat.heatVariance line 47
  11. lemma OAI.TriangularHilbert.Heat.heatEnergy_eq_localGram line 50
  12. lemma OAI.TriangularHilbert.Heat.fixedBase_update_center line 62
  13. lemma OAI.TriangularHilbert.Heat.fixedBase_update_variance line 76
  14. lemma OAI.TriangularHilbert.Heat.heatEnergy_hasDerivAt_center line 90
  15. lemma OAI.TriangularHilbert.Heat.heatFirst_hasDerivAt_center line 104
  16. lemma OAI.TriangularHilbert.Heat.heatEnergy_hasDerivAt_variance line 117