OAI/Geometry/RCD/Heat/LocalSmoothLogarithmC3.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Three bounded logarithm derivatives on a positive interval

The third derivative gives a Lipschitz bound for the second derivative. Only these finite jets are used for Sobolev regularity of the log source.

  1. theorem OAI.RegularPointCoordinates.exists_local_smooth_log_C3 line 18