OAI/Geometry/RCD/Harmonic/RadialAverageTimeDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The L2 derivative of the actual averaged Sobolev family

The countable exceptional times disappear under integration. The derivative is represented by the exact endpoint difference of values.

  1. theorem OAI.RegularPointCoordinates.radial_average_L2_derivative line 19