OAI/Geometry/IsometricImmersion/Energy/DirectedCutoffBalance.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Weighted.multiplierCutoffError line 13
2. theorem OAI.SmoothLocal.Weighted.multiplier_divergence_quadratic line 17
3. theorem OAI.SmoothLocal.Weighted.multiplierQuadratic_cutoff_split line 28
4. theorem OAI.SmoothLocal.Weighted.multiplierCutoffError_contDiffOn line 61
5. theorem OAI.SmoothLocal.Weighted.multiplierCutoffError_zero line 69
6. theorem OAI.SmoothLocal.Weighted.directed_source_young_scalar line 73