OAI/Geometry/RCD/Sobolev/DyadicSubsolutionLevels.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A middle level for the potential term in the dyadic iteration

  1. theorem OAI.RegularPointCoordinates.dyadic_middle_level_bounds line 9