OAI/Geometry/IsometricImmersion/Energy/MovingSlabEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Hyperbolic.movingEnergy_hasDerivAt_of_sliceEquation line 14
2. theorem OAI.SmoothLocal.Hyperbolic.moving_source_integral_bound_of_slicePositivity line 83
3. theorem OAI.SmoothLocal.Hyperbolic.movingEnergyRate_le_of_sliceBounds line 131
4. def OAI.SmoothLocal.Hyperbolic.shrinkingSlab line 191
5. theorem OAI.SmoothLocal.Hyperbolic.point_mem_shrinkingSlab line 195
6. theorem OAI.SmoothLocal.Hyperbolic.shrinkingSlab_subset_rectangle line 201
7. theorem OAI.SmoothLocal.Hyperbolic.moving_slab_energy_propagation line 212