OAI/Geometry/RCD/Heat/BoundedHeatMixedGramBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded mixed heat Grams and compact positive ranges

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_heat_mixed_gram_bound line 19
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_heat_positive_range line 41