SurfacePieces.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Class-uniform surface pieces for restart charts

Uniform upper and lower area estimates give native surface measures with common growth and projection bounds. A geometric loss estimate then chooses a finite chart depth for any positive deficit. The precision, Lipschitz bounds, and restart piece parameters are selected from the fixed dimensions and regularity constants before the original measure or its support cell is introduced.

theorem OAI.RieszRectifiability.quantitative_uniform_precision_area_models line 29

Source documentation

Area comparison constants are uniform over the measure class and the allowed precision.

theorem quantitative_uniform_precision_area_models {n d : ℕ} (hn : 0 < n) (hnd : n ≤ d)
    (C G : ℝ) (hC : 1 ≤ C) (hG : 0 < G) :
    ∃ Ktop : ℝ≥0∞, Ktop < ⊤ ∧ ∃ Kupper : ℝ≥0∞, Kupper < ⊤ ∧
      ∃ Klower : ℝ≥0∞, 0 < Klower ∧ Klower < ⊤ ∧
      ∀ (μ : Measure (Ambient d)) [μ.Regular], ADRegularWithConstant n C μ →
      GlobalUpperGrowth n G μ → ∀ ε : ℝ, 0 < ε → ε ≤ 1 / 281474976710656 → activeProjectionError d ε ≤ 1 / 128 →
      ∀ (R : ℝ) (hR : 0 < R) (k : ℕ) (z : (supportLatticeNets μ R hR k).points),
        AdmissibleRadius μ (latticeRadius R k / 8) →
        let Good := fun q : SupportCellDescendant μ R hR k z =>
…

Mentions: OAI.RieszRectifiability.Ambient, OAI.RieszRectifiability.ADRegularWithConstant, OAI.RieszRectifiability.GlobalUpperGrowth, OAI.RieszRectifiability.activeProjectionError, OAI.RieszRectifiability.supportLatticeNets, OAI.RieszRectifiability.AdmissibleRadius, OAI.RieszRectifiability.latticeRadius, OAI.RieszRectifiability.SupportCellDescendant

theorem OAI.RieszRectifiability.quantitative_matched_surface_models line 83

Source documentation

The model surfaces carry regular, unbounded AD measures with common projection geometry.

theorem quantitative_matched_surface_models {n d : ℕ} (hn : 0 < n) (hnd : n ≤ d)
    (C₀ G : ℝ) (hC₀ : 1 ≤ C₀) (hG : 0 < G) :
    ∃ Ktop : ℝ≥0∞, Ktop < ⊤ ∧ ∃ K : ℝ, 1 ≤ K ∧
      ∀ (μ : Measure (Ambient d)) [μ.Regular], ADRegularWithConstant n C₀ μ →
      GlobalUpperGrowth n G μ → ∀ ε : ℝ, 0 < ε → ε ≤ 1 / 72057594037927936 → activeProjectionError d ε ≤ 1 / 4096 →
      ∀ (R : ℝ) (hR : 0 < R) (k : ℕ) (z : (supportLatticeNets μ R hR k).points),
        AdmissibleRadius μ (latticeRadius R k / 8) →
        let Good := fun q : SupportCellDescendant μ R hR k z =>
…

theorem OAI.RieszRectifiability.quantitative_uniform_surface_ball_charts line 133
Source documentation
A measure-independent precision admits ball charts with any prescribed positive area deficit. The Lipschitz constant may depend on that deficit, but is chosen before the measure.
```
theorem quantitative_uniform_surface_ball_charts {n d : ℕ} (hn : 0 < n) (hnd : n ≤ d)
    (C G : ℝ) (hC : 1 ≤ C) (hG : 0 < G) :
    ∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 / 281474976710656 ∧ activeProjectionError d ε ≤ 1 / 128 ∧
      ∀ δ : ℝ, 0 < δ → ∃ M : ℝ≥0,
      ∀ (μ : Measure (Ambient d)) [μ.Regular], ADRegularWithConstant n C μ →
      GlobalUpperGrowth n G μ → ∀ (R : ℝ) (hR : 0 < R) (k : ℕ) (z : (supportLatticeNets μ R hR k).points),
        AdmissibleRadius μ (latticeRadius R k / 8) →
        let Good := fun q : SupportCellDescendant μ R hR k z =>
…
```
Mentions: OAI.RieszRectifiability.activeProjectionError, OAI.RieszRectifiability.Ambient, OAI.RieszRectifiability.ADRegularWithConstant, OAI.RieszRectifiability.GlobalUpperGrowth, OAI.RieszRectifiability.supportLatticeNets, OAI.RieszRectifiability.AdmissibleRadius, OAI.RieszRectifiability.latticeRadius, OAI.RieszRectifiability.SupportCellDescendant

theorem OAI.RieszRectifiability.quantitative_uniform_restart_surface_pieces line 202

Source documentation

Choose common piece-count and Lipschitz parameters before assembling all selected restarts.

theorem quantitative_uniform_restart_surface_pieces {n d : ℕ} (hn : 0 < n) (hnd : n ≤ d)
    (C G : ℝ) (hC : 1 ≤ C) (hG : 0 < G) :
    ∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 / 281474976710656 ∧ activeProjectionError d ε ≤ 1 / 128 ∧
      ∀ δ : ℝ, 0 < δ → ∃ (N : ℕ) (P : ℝ≥0),
    ∀ (μ : Measure (Ambient d)) [μ.Regular], ADRegularWithConstant n C μ →
    GlobalUpperGrowth n G μ → ∀ (R : ℝ) (hR : 0 < R) (k : ℕ) (z : (supportLatticeNets μ R hR k).points),
      AdmissibleRadius μ (latticeRadius R k / 8) →
      let Bad := fun i : SupportCellDescendant μ R hR k z =>
…

Mentions: OAI.RieszRectifiability.activeProjectionError, OAI.RieszRectifiability.Ambient, OAI.RieszRectifiability.ADRegularWithConstant, OAI.RieszRectifiability.GlobalUpperGrowth, OAI.RieszRectifiability.supportLatticeNets, OAI.RieszRectifiability.AdmissibleRadius, OAI.RieszRectifiability.latticeRadius, OAI.RieszRectifiability.SupportCellDescendant