BallMaps.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The per-measure ball-map conclusion

The higher-codimension rectifiability theorem is restated with its conclusion expanded: one positive mass fraction and one Lipschitz bound work at every support point and admissible radius of the given measure. The lower bound is for the actual image of a map from a Euclidean ball, intersected with the ambient support ball. The hypotheses and admissible-radius condition are unchanged.

theorem OAI.RieszRectifiability.exact_unfolded_ball_map_conclusion line 23

Source documentation

The per-measure rectifiability theorem with its ball-map conclusion expanded.

theorem exact_unfolded_ball_map_conclusion (d n : ℕ) (hd : 4 ≤ d) (hn : 2 ≤ n) (hnd : n + 2 ≤ d)
    (μ : Measure (Ambient d)) (hreg : μ.Regular) (hAD : ADRegular n μ) (hRiesz : RieszL2Bounded n μ) :
    ∃ θ : ℝ, 0 < θ ∧ ∃ M : ℝ≥0,
      ∀ x ∈ μ.support, ∀ r : ℝ, AdmissibleRadius μ r →
        ∃ g : ball (0 : Ambient n) r → Ambient d,
          LipschitzWith M g ∧ ENNReal.ofReal (θ * r ^ n) ≤ μ (ball x r ∩ Set.range g) :=
…

Mentions: OAI.RieszRectifiability.Ambient, OAI.RieszRectifiability.ADRegular, OAI.RieszRectifiability.RieszL2Bounded, OAI.RieszRectifiability.AdmissibleRadius