OAI/Geometry/IsometricImmersion/Darboux/QEnergyApplication.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.HighEquation.qHighBTheta_contDiffOn line 13
2. theorem OAI.SmoothLocal.HighEquation.qHighBXi_contDiffOn line 21
3. theorem OAI.SmoothLocal.HighEquation.actualQHighRemainder_contDiffOn line 29
4. theorem OAI.SmoothLocal.HighEquation.spatialProductL2Budget_mono_width line 57
5. theorem OAI.SmoothLocal.HighEquation.qRemainderSliceBudget_mono_width line 68
6. theorem OAI.SmoothLocal.HighEquation.actualQ_source_norm_le line 85
7. theorem OAI.SmoothLocal.HighEquation.actual_Q_moving_slab_energy line 109
8. theorem OAI.SmoothLocal.HighEquation.actual_Q_moving_slab_energy_with_source_budget line 145