OAI/Geometry/RCD/Transport/HarmonicOptimalPlanMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original harmonic-coordinate means on every compressed optimal plan

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_harmonic_mean_on_optimal_plan line 20