OAI/Geometry/IsometricImmersion/Caps/CapL2Basics.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Analytic.integral_sq_eq_eLpNorm_toReal_sq line 15
  2. theorem OAI.SmoothLocal.Analytic.integral_sq_le_of_eLpNorm_two_le line 30
  3. theorem OAI.SmoothLocal.Analytic.eLpNorm_two_le_of_integral_sq_le line 38
  4. def OAI.SmoothLocal.HighEquation.CoordinateL2Bound line 51
  5. theorem OAI.SmoothLocal.HighEquation.CoordinateL2Bound.mono line 55
  6. theorem OAI.SmoothLocal.HighEquation.CoordinateL2Bound.restrict line 61
  7. theorem OAI.SmoothLocal.HighEquation.CoordinateL2Bound.eLpNorm_le line 67
  8. theorem OAI.SmoothLocal.HighEquation.CoordinateL2Bound.memLp line 74
  9. theorem OAI.SmoothLocal.HighEquation.CoordinateL2Bound.integral_sq line 82
  10. theorem OAI.SmoothLocal.HighEquation.heightStateFactor_eq_ordered line 89
  11. theorem OAI.SmoothLocal.HighEquation.CoordinateL2Bound.heightFactors line 95
  12. theorem OAI.SmoothLocal.HighEquation.CoordinateL2Bound.heightFactors_of_aestronglyMeasurable line 103
  13. theorem OAI.SmoothLocal.HighEquation.coordinateBound_heightFactors line 112
  14. theorem OAI.SmoothLocal.Flow.closedRectangle_subset_capChartDomain line 126
  15. theorem OAI.SmoothLocal.Flow.coordinateL2Bound_to_nested_flow_coordinateBound line 133