OAI/Geometry/IsometricImmersion/Comparison/ComparisonSourceBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Pulse.pulseLeadingBound line 13
2. theorem OAI.SmoothLocal.Pulse.pulseLeadingBound_nonneg line 16
3. theorem OAI.SmoothLocal.Pulse.pulsePrincipalLeading_abs_bound line 20
4. def OAI.SmoothLocal.Pulse.comparisonSourceBudget line 43
5. theorem OAI.SmoothLocal.Pulse.comparisonSourceBudget_nonneg line 48
6. theorem OAI.SmoothLocal.Pulse.exists_actual_comparison_source_pointwise_bound line 58