OAI/Geometry/CAT0Fillings/Density/RadialEstimate.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.cutoffVariationWeight line 14
2. lemma OAI.CAT0Fillings.cutoffVariationWeight_bounds line 17
3. lemma OAI.CAT0Fillings.cutoff_pointwise_estimate line 30
4. lemma OAI.CAT0Fillings.ChartGeometry.ae_density_zero_or_not_mem line 65
5. lemma OAI.CAT0Fillings.ChartGeometry.cutoff_weight_integrable line 99
6. lemma OAI.CAT0Fillings.ChartGeometry.radialVariationChart_cutoff line 126