OAI/Geometry/CAT0Fillings/Euler/Moments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ChordMeasure.total_congr line 12
2. lemma OAI.CAT0Fillings.ChordMeasure.probability_congr line 13
3. lemma OAI.CAT0Fillings.ChordMeasure.ae_of_ae line 18
4. lemma OAI.CAT0Fillings.ChartGeometry.inner_power_inclusion line 32
5. lemma OAI.CAT0Fillings.ChartGeometry.power_pair_integral line 47
6. lemma OAI.CAT0Fillings.ChartGeometry.inner_power_gradient line 59
7. lemma OAI.CAT0Fillings.ChartGeometry.euler_weighted_moment line 71