OAI/Geometry/RCD/Heat/BoundedHeatMixedGram.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Mixed Sobolev Gram entries for two actual positive-time heat factors

A common earlier heat time and polarization handle distinct times. Only the two original bounded-amplitude hypotheses are used.

  1. theorem OAI.RegularPointCoordinates.heatSobolev_split line 19
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_heat_mixed_gram line 34