OAI/Analysis/TriangularHilbert/PlaneDom.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TriangularHilbert.Heat.abs_le_one_add_sq line 13
  2. lemma OAI.TriangularHilbert.Heat.planePoly_ge_first line 16
  3. lemma OAI.TriangularHilbert.Heat.planePoly_ge_second line 21
  4. lemma OAI.TriangularHilbert.Heat.chart_abs_bound line 26
  5. lemma OAI.TriangularHilbert.Heat.endpoint_gaussian_bound line 39
  6. def OAI.TriangularHilbert.Heat.rootCoefficient line 55
  7. lemma OAI.TriangularHilbert.Heat.exists_heatArray_gaussian_bound line 59
  8. lemma OAI.TriangularHilbert.Heat.triangleBlocks_entry_bound line 97
  9. lemma OAI.TriangularHilbert.Heat.norm_rowStar_le_bound line 103
  10. lemma OAI.TriangularHilbert.Heat.exists_heatCarrier_gaussian_bound line 113
  11. lemma OAI.TriangularHilbert.Heat.norm_heatMask_le line 128
  12. lemma OAI.TriangularHilbert.Heat.exists_score_polynomial_bound line 139