OAI/Geometry/RCD/Sobolev/ComposedGammaContinuity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Continuity of a weighted nonlinear gradient square

The weight only needs L² continuity, including at the initial heat time.

  1. theorem OAI.RegularPointCoordinates.composed_gamma_pairing_continuousAt line 17