OAI/Analysis/TriangularHilbert/PlaneIntegral.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TriangularHilbert.Heat.measurable_chart line 13
  2. lemma OAI.TriangularHilbert.Heat.hasDerivAt_chart_of_center line 16
  3. def OAI.TriangularHilbert.Heat.planeIntegral line 29
  4. lemma OAI.TriangularHilbert.Heat.planeIntegral_eq line 32
  5. lemma OAI.TriangularHilbert.Heat.hasDerivAt_planeIntegral line 35
  6. lemma OAI.TriangularHilbert.Heat.finite_variance_bounds line 54
  7. lemma OAI.TriangularHilbert.Heat.abs_le_add_one_of_mem_Ioo line 68
  8. structure OAI.TriangularHilbert.Heat.HeatPlaneIntegrable line 75
  9. lemma OAI.TriangularHilbert.Heat.heatPlane_integrable line 84
  10. lemma OAI.TriangularHilbert.Heat.planeEnergy_hasDerivAt line 107
  11. lemma OAI.TriangularHilbert.Heat.planeFirst_hasDerivAt line 119
  12. lemma OAI.TriangularHilbert.Heat.planeFirst_hasDerivAt_other line 131
  13. lemma OAI.TriangularHilbert.Heat.planePure_eq_mixed line 144