OAI/Geometry/BallPacking/Necessity/AffineBubble.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.planeUnitCutoff line 37
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeUnitCutoff_smooth line 39
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeUnitCutoff_compact line 42
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeUnitCutoff_bounds line 45
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeUnitCutoff_one line 48
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeUnitCutoff_deriv_zero line 51
  7. def OAI.HigherDimensionalBallPacking.Rigidity.planeDilatedCutoff line 60
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeDilatedCutoff_smooth line 63
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeDilatedCutoff_compact line 69
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeDilatedCutoff_bounds line 73
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeDilatedCutoff_fderiv line 77
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeDilatedCutoff_tendsto_smul line 87
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeDilatedCutoff_eventually_one line 93
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeDilatedCutoff_eventually_deriv_zero line 100
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.compact_smooth_derivative_sq_integrable line 107
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeDilatedCutoff_grad_integral line 115
  17. def OAI.HigherDimensionalBallPacking.Rigidity.cutoffDerivativeTail line 128
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffDerivativeTail_bounds line 133
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffDerivativeTail_integrable line 139
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffDerivativeTail_integral_tendsto line 153
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffWedge_norm_le line 168
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffWedge_young line 186
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.integral_cutoffCurl_tendsto line 199
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.integral_planarCurl_zero_of_sq_integrable line 220
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialForm_self_smul line 256
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialForm_on_graph_continuous line 263
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialForm_compact_coercive line 288
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarCR_opNorm_bound line 331
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.curvePrimitive_sq_integrable_of_compact_image line 349
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.compact_image_finite_energy_constant line 397