OAI/Geometry/IsometricImmersion/Pulses/PulseMomentError.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Pulse.pulseTest_abs_le line 12
2. theorem OAI.SmoothLocal.Pulse.axisBump_Icc_integral line 17
3. theorem OAI.SmoothLocal.Pulse.pulse_spatial_mass_integral line 25
4. theorem OAI.SmoothLocal.Pulse.pulseWeightedMoment_bound line 38
5. theorem OAI.SmoothLocal.Pulse.pulseWeightedMoment_integrable line 58
6. theorem OAI.SmoothLocal.Pulse.pulseWeightedMoment_sub line 66
7. theorem OAI.SmoothLocal.Pulse.pulseWeightedMoment_lower_of_remainder line 74
8. theorem OAI.SmoothLocal.Pulse.pulseWeightedMoment_lower_order_error line 91