OAI/Geometry/BallPacking/Necessity/C1Energy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TwoPointContinuation.approxBump line 40
  2. theorem OAI.TwoPointContinuation.approxBump_shrinks line 44
  3. def OAI.TwoPointContinuation.mollify line 48
  4. theorem OAI.TwoPointContinuation.mollify_tendsto line 51
  5. theorem OAI.TwoPointContinuation.mollify_smooth line 56
  6. theorem OAI.TwoPointContinuation.mollify_fderiv line 62
  7. theorem OAI.TwoPointContinuation.mollify_fderiv_tendsto line 71
  8. theorem OAI.TwoPointContinuation.mollify_norm_le line 77
  9. theorem OAI.TwoPointContinuation.mollify_jet_integral_tendsto line 102
  10. def OAI.HigherDimensionalBallPacking.Rigidity.c1Area line 156
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1Area_continuous line 159
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_standard_stokes_compact line 166
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_local_compact line 215
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_standard_stokes line 230
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.continuous_boundary_bounds line 264
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.continuous_boundary_limit line 300
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_pullback_continuous line 330
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_area_of_nonneg_of_angular_limit line 335