OAI/Geometry/IsometricImmersion/Energy/MixedDerivativeL2.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.HighEquation.word_no_x_eq_replicate line 12
  2. theorem OAI.SmoothLocal.HighEquation.orderedPartial_replicate_y line 22
  3. theorem OAI.SmoothLocal.HighEquation.orderedPartial_at_most_one_x_eLpNorm line 28
  4. theorem OAI.SmoothLocal.HighEquation.principal_mixed_abs_le_fullP_one line 58
  5. theorem OAI.SmoothLocal.HighEquation.principal_yy_abs_le_fullP_one line 69
  6. theorem OAI.SmoothLocal.HighEquation.ordered_mixed_eLpNorm_step line 80
  7. def OAI.SmoothLocal.HighEquation.mixedXBudget line 163
  8. theorem OAI.SmoothLocal.HighEquation.mixedXBudget_monotone line 167
  9. theorem OAI.SmoothLocal.HighEquation.mixedXBudget_base_le line 178
  10. theorem OAI.SmoothLocal.HighEquation.mixedXBudget_step line 182
  11. theorem OAI.SmoothLocal.HighEquation.mixedXBudget_lt_top line 194
  12. theorem OAI.SmoothLocal.HighEquation.all_orderN_mixed_eLpNorm_two line 202
  13. theorem OAI.SmoothLocal.HighEquation.all_orderN_mixed_memLp_two line 246