SelectedRestartAreaLoss.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Surface-area loss in selected restart charts

At a good restart root, the mass left outside a selected surface piece is bounded by its discarded Hausdorff area. Applying this estimate at each selected root turns an area-loss hypothesis into the uniform deficit required by the recursive chart assembly; bad roots contribute an empty remainder.

theorem OAI.RieszRectifiability.selected_restart_remainder_mass_le_surface_loss line 23

Source documentation

A good restart root converts discarded model area into a bound for the remaining mass.

theorem selected_restart_remainder_mass_le_surface_loss {n d : ℕ}
    (μ : Measure (Ambient d)) (G : ℝ) (hG : 0 < G) (hg : GlobalUpperGrowth n G μ)
    (R : ℝ) (hR : 0 < R) (k : ℕ) (z : (supportLatticeNets μ R hR k).points)
    (Bad : SupportCellDescendant μ R hR k z → Prop)
    (q : SupportCellDescendant μ R hR k z) (hq : ¬ Bad q) (E : Set (Ambient d))
    (ε : ℝ) (hε : 0 < ε) (hεfine : ε ≤ 1 / 281474976710656)
    (hsmall : activeProjectionError d ε ≤ 1 / 128) (N : ℕ) (P : ℝ≥0)
    (a : SelectedRestartSurfaceData n Bad q E ε N P) :
    μ (selectedRestartRemainder Bad q E) ≤
      (ENNReal.ofReal G + activeRegionStopMassAreaConstant n G) *
        (μH[(n : ℝ)] : Measure (Ambient d))
          ((Set.range a.model ∩ closedBall q.center (3 * q.radius)) \ E) := by
…

Mentions: OAI.RieszRectifiability.Ambient, OAI.RieszRectifiability.GlobalUpperGrowth, OAI.RieszRectifiability.supportLatticeNets, OAI.RieszRectifiability.SupportCellDescendant, OAI.RieszRectifiability.activeProjectionError, OAI.RieszRectifiability.SelectedRestartSurfaceData, OAI.RieszRectifiability.selectedRestartRemainder, OAI.RieszRectifiability.activeRegionStopMassAreaConstant

theorem OAI.RieszRectifiability.original_AD_Riesz_recursive_chart_from_surface_pieces line 44

Source documentation

Uniformly small area losses yield a recursive Lipschitz chart with prescribed mass deficit. The deficit threshold and restart budget are chosen before the surface-piece parameters.

theorem original_AD_Riesz_recursive_chart_from_surface_pieces {p d : ℕ} (hnd : p + 1 ≤ d)
    (μ : Measure (Ambient d)) [μ.Regular] (hAD : ADRegular (p + 1) μ)
    (hRiesz : RieszL2Bounded (p + 1) μ) (G : ℝ) (hG : 0 < G)
    (hg : GlobalUpperGrowth (p + 1) G μ) (H ε : ℝ) (hH : 1 ≤ H) (hε : 0 < ε)
    (hεfine : ε ≤ 1 / 281474976710656) (hsmall : activeProjectionError d ε ≤ 1 / 128)
    (ζ : ℝ) (hζ : 0 < ζ) :
    ∃ δ : ℝ, 0 < δ ∧ ∃ b : ℕ, 0 < b ∧ ∀ (N : ℕ) (P : ℝ≥0)
      (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.Ambient, OAI.RieszRectifiability.ADRegular, OAI.RieszRectifiability.RieszL2Bounded, OAI.RieszRectifiability.GlobalUpperGrowth, OAI.RieszRectifiability.activeProjectionError, OAI.RieszRectifiability.supportLatticeNets, OAI.RieszRectifiability.AdmissibleRadius, OAI.RieszRectifiability.latticeRadius, OAI.RieszRectifiability.SupportCellDescendant