OAI/Geometry/CAT0Fillings/Chord/DoubleAverage.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.integral_density_nonnegative line 14
2. lemma OAI.CAT0Fillings.density_real_univ line 24
3. lemma OAI.CAT0Fillings.density_finite line 31
4. lemma OAI.CAT0Fillings.weighted_double_distance_lower line 40
5. lemma OAI.CAT0Fillings.ChordMeasure.chord_weight_identity line 64
6. lemma OAI.CAT0Fillings.ChordMeasure.chord_moment_identity line 71
7. lemma OAI.CAT0Fillings.ChordMeasure.chord_double_identity line 82
8. lemma OAI.CAT0Fillings.ChordMeasure.opposite_average line 101