OAI/Geometry/IsometricImmersion/Darboux/QMomentAbsorption.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Pulse.qMomentErrorCoefficient line 13
2. theorem OAI.SmoothLocal.Pulse.qMomentErrorCoefficient_nonneg line 17
3. theorem OAI.SmoothLocal.Pulse.qForcingRemainderBudget_le_first_scale line 27
4. theorem OAI.SmoothLocal.Pulse.qMoment_budget_absorption_threshold line 42