OAI/Geometry/IsometricImmersion/Pulses/PulseDensitySlab.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Pulse.curvatureDensity line 13
2. def OAI.SmoothLocal.Pulse.curvatureDensityJetError line 16
3. theorem OAI.SmoothLocal.Pulse.curvatureDensityJetError_eq line 25
4. theorem OAI.SmoothLocal.Pulse.curvatureDensityJetError_le line 34
5. def OAI.SmoothLocal.Pulse.testDensityErrorCoefficient line 62
6. theorem OAI.SmoothLocal.Pulse.exists_test_density_slab_bound line 65
7. theorem OAI.SmoothLocal.Pulse.perturbed_density_slab_with_comparison line 105