OAI/Geometry/RCD/Sobolev/PoissonPathDefectBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An absolute path-error bound from the actual Poisson mean estimate

  1. theorem OAI.RegularPointCoordinates.DistancePoissonMeanData.path_defect_bound line 22