OAI/Geometry/RCD/Metric/CoarseEvolutionBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A short-time sufficient form of the dimensional evolution bound

Bounding the exponential integral by its endpoint retains the sharp coefficient at time zero, as required for the integrated Bochner limit.

  1. theorem OAI.RegularPointCoordinates.gronwallBound_one_le line 13