OAI/Geometry/RCD/Heat/HeatRelativeTangent.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Pointwise relative bounds for the strong heat tangent

  1. theorem OAI.RegularPointCoordinates.lp_relative_order line 13
  2. theorem OAI.RegularPointCoordinates.heat_exponential_tangent_bound line 28
  3. theorem OAI.RegularPointCoordinates.heat_exponential_remainder_bound line 56
  4. theorem OAI.RegularPointCoordinates.heat_exponential_nonneg line 74
  5. theorem OAI.RegularPointCoordinates.heat_exponential_power_integrable line 83