OAI/Geometry/RCD/Harmonic/AverageQuadraticError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Passing an additive transport error from averages to continuous values

  1. theorem OAI.RegularPointCoordinates.quadratic_comparison_of_average_bound_add line 14

    Also declared: OAI/Analysis/RCDHeat/VariableHeatODE.lean:273 (same declaration text).