OAI/Geometry/Varifold/NullComparison.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Five-ball Hausdorff comparison for integral varifolds

Integral varifolds are modeled by rectifiable weighted measures and tangent projections. Smooth graphs provide the regular-locus model. The supporting results establish local finiteness, Hausdorff domination, first-variation integrability, and smooth graph embeddings.

A five-ball covering gives quantitative Hausdorff comparison from local lower ball-mass bounds, and localization gives the corresponding null-set comparison for integral varifolds. The lower bounds and weight-nullness are hypotheses: stationary monotonicity, weighted almost-everywhere regularity, and the geometric-measure bridge are not proved here. Thus neither stationary integral-varifold almost-everywhere regularity nor its round-sphere corollary is established.

  1. abbrev OAI.StationaryVarifolds.Euclidean line 28
  2. abbrev OAI.StationaryVarifolds.PlaneEnd line 31
  3. instance OAI.StationaryVarifolds.planeEndMeasurableSpace line 33
  4. instance OAI.StationaryVarifolds.planeEndBorelSpace line 34
  5. def OAI.StationaryVarifolds.CountablyRectifiable line 37
  6. def OAI.StationaryVarifolds.IsApproximateTangentPlane line 45
  7. def OAI.StationaryVarifolds.rectifiableWeight line 58
  8. structure OAI.StationaryVarifolds.IntegralVarifold line 64
  9. def OAI.StationaryVarifolds.tangentialDivergence line 81
  10. def OAI.StationaryVarifolds.StationaryWeight line 87
  11. def OAI.StationaryVarifolds.liftedMeasure line 95
  12. def OAI.StationaryVarifolds.IntegralVarifold.weight line 103
  13. def OAI.StationaryVarifolds.IntegralVarifold.measure line 106
  14. def OAI.StationaryVarifolds.IntegralVarifold.Stationary line 109
  15. structure OAI.StationaryVarifolds.SmoothGraph line 116
  16. def OAI.StationaryVarifolds.SmoothGraph.parametrization line 129
  17. def OAI.StationaryVarifolds.SmoothGraph.carrier line 132
  18. def OAI.StationaryVarifolds.SmoothGraph.parameter line 136
  19. def OAI.StationaryVarifolds.SmoothGraph.plane line 140
  20. def OAI.StationaryVarifolds.SmoothGraph.weight line 143
  21. def OAI.StationaryVarifolds.SmoothGraph.measure line 146
  22. def OAI.StationaryVarifolds.SmoothGraph.MinimalIn line 151
  23. def OAI.StationaryVarifolds.IntegralVarifold.RegularAt line 162
  24. def OAI.StationaryVarifolds.IntegralVarifold.singularSet line 169
  25. theorem OAI.StationaryVarifolds.IntegralVarifold.exists_finite_open_nhds line 175
  26. theorem OAI.StationaryVarifolds.IntegralVarifold.weight_apply line 186
  27. theorem OAI.StationaryVarifolds.IntegralVarifold.map_fst_measure line 193
  28. theorem OAI.StationaryVarifolds.IntegralVarifold.hausdorff_restrict_le line 202
  29. theorem OAI.StationaryVarifolds.IntegralVarifold.hausdorff_inter_carrier_zero line 213
  30. theorem OAI.StationaryVarifolds.IntegralVarifold.ae_norm_plane_le_one line 221
  31. theorem OAI.StationaryVarifolds.IntegralVarifold.integrable_tangentialDivergence line 232
  32. theorem OAI.StationaryVarifolds.SmoothGraph.parameter_parametrization line 269
  33. theorem OAI.StationaryVarifolds.SmoothGraph.parametrization_smooth line 285
  34. theorem OAI.StationaryVarifolds.SmoothGraph.parameter_continuous line 289
  35. theorem OAI.StationaryVarifolds.SmoothGraph.parametrization_isEmbedding line 293
  36. theorem OAI.StationaryVarifolds.SmoothGraph.parametrization_rank line 304
  37. theorem OAI.StationaryVarifolds.ball_bound_on_support_of_ae line 337
  38. theorem OAI.StationaryVarifolds.hausdorffMeasure_le_open_of_ball_bound line 374
  39. theorem OAI.StationaryVarifolds.hausdorffMeasure_le_mul_of_ball_bound line 445
  40. theorem OAI.StationaryVarifolds.hausdorffMeasure_zero_of_ball_bound line 464
  41. theorem OAI.StationaryVarifolds.hausdorffMeasure_zero_of_locally_finite_ball_bound line 475
  42. theorem OAI.StationaryVarifolds.IntegralVarifold.hausdorff_zero_of_weight_zero_of_ball_bound line 512