OAI/Geometry/CAT0Fillings/Chord/Barycenter.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.TangentDensity.moment_lt_two line 13
2. def OAI.CAT0Fillings.squaredPotential line 64
3. lemma OAI.CAT0Fillings.integrable_dist_sq line 66
4. lemma OAI.CAT0Fillings.continuous_squaredPotential line 72
5. theorem OAI.CAT0Fillings.exists_barycenter_variance line 81
6. theorem OAI.CAT0Fillings.double_distance_lower_bound line 115