OAI/Geometry/CAT0Fillings/Chord/Moments.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.Conformal.beta_dimension line 10
2. lemma OAI.CAT0Fillings.Conformal.beta_half_dimension line 12
3. lemma OAI.CAT0Fillings.Conformal.beta_inverse_half line 16
4. lemma OAI.CAT0Fillings.Conformal.beta_critical_ratio line 17
5. lemma OAI.CAT0Fillings.Conformal.beta_critical_product line 22
6. lemma OAI.CAT0Fillings.ChordMeasure.chord_measurable line 38
7. lemma OAI.CAT0Fillings.ChordMeasure.integral_power line 44
8. lemma OAI.CAT0Fillings.ChordMeasure.chord_second_moment line 49