OAI/Geometry/RCD/Sobolev/ShiftedDyadicSubsolutionLevels.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Shifted middle levels for the potential term

  1. theorem OAI.RegularPointCoordinates.shifted_dyadic_middle_level_bounds line 9