OAI/Geometry/IsometricImmersion/Caps/CapInductionData.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SmoothLocal.Flow.CapInductionHeight line 16
  2. def OAI.SmoothLocal.Flow.lowerCapConstant line 26
  3. theorem OAI.SmoothLocal.Flow.lowerCapConstant_pos line 29
  4. structure OAI.SmoothLocal.Flow.CapInductionFlow line 33
  5. theorem OAI.SmoothLocal.Flow.exists_capInductionFlow line 53
  6. theorem OAI.SmoothLocal.Flow.CapInductionFlow.image_properties line 73
  7. theorem OAI.SmoothLocal.Flow.CapInductionFlow.image_subset_square line 80
  8. theorem OAI.SmoothLocal.Flow.CapInductionFlow.pointwise_from_larger_L2 line 85
  9. def OAI.SmoothLocal.Flow.originalC8L2Budget line 98
  10. theorem OAI.SmoothLocal.Flow.originalC8L2Budget_coe line 101
  11. theorem OAI.SmoothLocal.Flow.CapInductionHeight.original_L2 line 107
  12. theorem OAI.SmoothLocal.Flow.compact_continuous_memLp_two line 120
  13. theorem OAI.SmoothLocal.Flow.integral_each_sq_le_sum line 125