OAI/Geometry/CAT0Fillings/Chord/RadialIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ChartGeometry.radial_completed_pointwise line 15
2. lemma OAI.CAT0Fillings.ChartGeometry.memLp_radialCompletedA line 24
3. lemma OAI.CAT0Fillings.ChartGeometry.completed_radial line 48
4. lemma OAI.CAT0Fillings.ChartGeometry.scalar_added_cancel line 83
5. def OAI.CAT0Fillings.ChartGeometry.completedExpression line 93
6. lemma OAI.CAT0Fillings.ChartGeometry.integrable_completedExpression line 97
7. lemma OAI.CAT0Fillings.ChartGeometry.added_energy_integral line 108