OAI/Geometry/BallPacking/Compactness/MarkedCurves.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.anchoredEnergyFamily line 16
  2. lemma OAI.HigherDimensionalBallPacking.Rigidity.anchoredEnergyFamily_equicontinuous line 20
  3. lemma OAI.HigherDimensionalBallPacking.Rigidity.anchoredEnergyFamily_pointwise line 31
  4. lemma OAI.HigherDimensionalBallPacking.Rigidity.anchoredEnergyFamily_compactClosure line 42
  5. lemma OAI.HigherDimensionalBallPacking.Rigidity.energy_family_czero_subsequence line 57
  6. lemma OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_line_uniform_energy line 74
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_line_czero_compactness line 92
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_line_gradient_bound line 111
  9. def OAI.HigherDimensionalBallPacking.Rigidity.markedLocalCurve line 143
  10. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedLocalCurve_smooth line 146
  11. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedLocalCurve_bound line 149
  12. lemma OAI.HigherDimensionalBallPacking.Rigidity.bilinear_cauchy line 156
  13. lemma OAI.HigherDimensionalBallPacking.Rigidity.cauchy_mapJet line 167
  14. lemma OAI.HigherDimensionalBallPacking.Rigidity.undo_frozen_cutoff line 172
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_local_jet_cauchy line 183
  16. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compact_local_holder_cauchy line 284
  17. lemma OAI.HigherDimensionalBallPacking.Rigidity.dilatedCurve_reconstruction line 364
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_line_source_escape line 372
  19. lemma OAI.HigherDimensionalBallPacking.Rigidity.norm_le_of_capacity_le line 401
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_line_uniform_defect_support line 409
  21. def OAI.HigherDimensionalBallPacking.Rigidity.localResidual line 434
  22. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCurveJet_local_fderiv line 437
  23. lemma OAI.HigherDimensionalBallPacking.Rigidity.localResidual_value line 448
  24. lemma OAI.HigherDimensionalBallPacking.Rigidity.localResidual_at_original line 458
  25. lemma OAI.HigherDimensionalBallPacking.Rigidity.localResidual_cauchy line 467