OAI/Geometry/RCD/Transport/CompactFactorMidpoint.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A normalized midpoint datum for each actual compact heat factor

The amplitude is the supremum of the earlier heat factor. Kernel comparison controls this same supremum at every observation point.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_factor_midpoint line 22