OAI/Geometry/RCD/Harmonic/QuadraticRateOptimization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Optimizing the positive spatial scale in the quadratic rate

  1. theorem OAI.RegularPointCoordinates.square_le_of_young_bounds line 9