OAI/Geometry/RCD/Harmonic/DyadicRootDirectionConvergence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sharp estimates for the full sequence of root-normalized directions

  1. theorem OAI.RegularPointCoordinates.dyadic_root_unit_direction_convergence line 14