SelectedRestartAssembly.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Surface data for selected restart assembly

Finite Lipschitz surface pieces and an active-region limit model supply the parent chart at a good restart. At a bad restart the selected stop is the root, so immediate-child assembly suffices. Both cases share a bound given by two restart-chart steps.

structure OAI.RieszRectifiability.SelectedRestartSurfaceData line 26
Source documentation
Plane fits, a limit model, and bounded surface pieces covering the restart set.
```
structure SelectedRestartSurfaceData (n : ℕ)
    (Bad : SupportCellDescendant μ R hR k z → Prop)
    (q : SupportCellDescendant μ R hR k z) (E : Set (Ambient d))
    (ε : ℝ) (N : ℕ) (P : ℝ≥0) where
…
```
Mentions: OAI.RieszRectifiability.SupportCellDescendant, OAI.RieszRectifiability.Ambient
def OAI.RieszRectifiability.selectedRestartChildNode line 46
Source documentation
Embed an immediate child of a relative selected stop into the next restart nodes.
```
def selectedRestartChildNode (Bad : SupportCellDescendant μ R hR k z → Prop)
    (q : SupportCellDescendant μ R hR k z) (E : Set (Ambient d))
    (i : relativeSelectedRestartStops Bad q E)
    (j : supportImmediateChildren μ R hR (k + q.depth + i.val.depth)
      ⟨i.val.center, i.val.mem_net⟩) : selectedRestartNext Bad q E :=
…
```
Mentions: OAI.RieszRectifiability.SupportCellDescendant, OAI.RieszRectifiability.Ambient, OAI.RieszRectifiability.relativeSelectedRestartStops, OAI.RieszRectifiability.supportImmediateChildren, OAI.RieszRectifiability.selectedRestartNext
theorem OAI.RieszRectifiability.exists_chart_at_equal_radius line 54
theorem OAI.RieszRectifiability.relative_selected_stop_eq_root_of_bad line 61

theorem OAI.RieszRectifiability.has_selected_restart_assembly_of_surface_data line 75

Source documentation

Assemble child charts and the parent surface with a uniform two-step Lipschitz bound.

theorem has_selected_restart_assembly_of_surface_data (hn : 0 < n)
    (G : ℝ) (hG : 0 < G) (hg : GlobalUpperGrowth n G μ)
    (Bad : SupportCellDescendant μ R hR k z → Prop)
    (E : {q : SupportCellDescendant μ R hR k z // cellRestartsAfter Bad q} → Set (Ambient d))
    (ε : ℝ) (hε : 0 < ε) (hεfine : ε ≤ 1 / 281474976710656)
    (hsmall : activeProjectionError d ε ≤ 1 / 128) (N : ℕ) (P : ℝ≥0)
    (data : ∀ q : {q : SupportCellDescendant μ R hR k z // cellRestartsAfter Bad q},
      ¬ Bad q.val → SelectedRestartSurfaceData n Bad q.val (E q) ε N P) :
    HasSelectedRestartAssembly n Bad E
      (fun M => restartChartStepConstant d N P (restartChartStepConstant d N P M)) := by
…

Mentions: OAI.RieszRectifiability.GlobalUpperGrowth, OAI.RieszRectifiability.SupportCellDescendant, OAI.RieszRectifiability.cellRestartsAfter, OAI.RieszRectifiability.Ambient, OAI.RieszRectifiability.activeProjectionError, OAI.RieszRectifiability.SelectedRestartSurfaceData, OAI.RieszRectifiability.HasSelectedRestartAssembly, OAI.RieszRectifiability.restartChartStepConstant