OAI/Geometry/IsometricImmersion/Energy/LocalQResidualL2.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.HighEquation.HorizontalMetricTwoJetBound.mono_order line 13
2. theorem OAI.SmoothLocal.HighEquation.exists_same_slice_actual_Q_source_bound line 21
3. theorem OAI.SmoothLocal.HighEquation.exists_same_slice_actual_Q_source_norm_bound line 57