OAI/Geometry/RCD/Transport/DistancePoissonOptimalMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual Poisson mean estimate on every compressed optimal plan

  1. theorem OAI.RegularPointCoordinates.DistancePoissonMeanData.optimal_mean_estimate line 23