SourceAngularSupport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The simultaneous top count supplies exactly the graph bound used after zero snapshot children are removed. The unshrunk path is the sole exception.

theorem OAI.LipschitzHilbert.AngularGrid.supported_snapshot_independence line 16

Source documentation

Only supported snapshot children need significant top representatives.

theorem supported_snapshot_independence {ι κ : Type} [DecidableEq ι] [Fintype κ]
    (g : AngularGrid) (tops : Finset ι) (T : ι → SlopeBox) (d : ι → ℝ)
    (z : ℝ × ℝ) (cutoff : ℝ) (base level : ℕ) (parent : ℤ)
    (cells : Finset ℤ) (representative : cells → ℝ)
    (hcell : ∀ c, g.index (level+1) (representative c) = c.val)
    (hancestor : ∀ c, g.index base (representative c) = parent)
    (hd : ∀ i ∈ tops, 0 ≤ d i) (hle : base ≤ level)
    (X : cells → EuclideanSpace ℂ κ) (path : cells)
    {gap B K D : ℝ} (hD : 2 ≤ D)
    (hprecision : cutoff/(g.branching:ℝ)^(level+1) ≤ gap/B^2)
    (hspan : g.width base ≤ B*gap)
    (hsignificant : ∀ c, X c ≠ 0 → (c:ℤ) ≠ path.val →
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox

theorem OAI.LipschitzHilbert.AngularGrid.supported_shrink_significant line 65

Source documentation

The shrink threshold makes every supported non-path cell eligible for this count; no significant representative is imposed on a zero amplitude.

theorem supported_shrink_significant {ι κ : Type} [DecidableEq ι] [Fintype κ]
    (g : AngularGrid) (tops : Finset ι) (T : ι → SlopeBox) (d : ι → ℝ)
    (z : ℝ × ℝ) (cutoff : ℝ) (level : ℕ) (cells : Finset ℤ)
    (A : cells → EuclideanSpace ℂ κ) (c : cells → ℝ) (path : cells)
    {K ε : ℝ} (hε : 0 ≤ ε) (hc : ∀ i, 0 ≤ c i)
    (hsmall : ∀ j, (∀ i ∈ g.cellTops tops (fun i => (T i).slope) d cutoff level j.val,
      K < (T i).radius z) → ‖A j‖ ≤ 2*ε*c j) :
    ∀ j, (if j = path then A j else radialShrink (2*ε*c j) (A j)) ≠ 0 →
      j.val ≠ path.val →
      ∃ i ∈ g.cellTops tops (fun i => (T i).slope) d cutoff level j.val,
        (T i).radius z ≤ K := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.radialShrink