OAI/Geometry/CAT0Fillings/Rearrangement/Gradient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.Rearrangement.map_norm_absolutelyContinuous line 17
2. lemma OAI.CAT0Fillings.Rearrangement.ae_norm_of_ae line 33
3. lemma OAI.CAT0Fillings.Rearrangement.ae_norm_fderiv_radial line 36
4. lemma OAI.CAT0Fillings.Rearrangement.radial_energy_identity line 46
5. lemma OAI.CAT0Fillings.Rearrangement.radialInverse_deriv_zero_outside line 69
6. lemma OAI.CAT0Fillings.Rearrangement.radialInverse_energy_support line 78
7. theorem OAI.CAT0Fillings.Rearrangement.euclidean_rearrangement_energy_bound line 99