OAI/Analysis/TriangularHilbert/HeatCost.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularHilbert.Heat.heatCost line 15
  2. def OAI.TriangularHilbert.Heat.heatMixed line 19
  3. def OAI.TriangularHilbert.Heat.heatScores line 24
  4. lemma OAI.TriangularHilbert.Heat.fixedBase_update_other line 27
  5. lemma OAI.TriangularHilbert.Heat.heatFirst_hasDerivAt_other line 36
  6. lemma OAI.TriangularHilbert.Heat.two_heatMixed_le line 52
  7. lemma OAI.TriangularHilbert.Heat.localGram_center line 59
  8. lemma OAI.TriangularHilbert.Heat.localGram_other line 65
  9. lemma OAI.TriangularHilbert.Heat.groupFirst_eq_insert line 75
  10. lemma OAI.TriangularHilbert.Heat.localFirst_center line 85
  11. lemma OAI.TriangularHilbert.Heat.localFirst_other line 96
  12. lemma OAI.TriangularHilbert.Heat.heatCost_center line 114
  13. lemma OAI.TriangularHilbert.Heat.heatCost_other line 120
  14. lemma OAI.TriangularHilbert.Heat.heatCost_nonneg line 129
  15. lemma OAI.TriangularHilbert.Heat.heatCost_neighbors line 140