ChartSymbolControl.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite derivative data for the graph localization

These records express cap and endpoint regularity bounds. They contain no oscillatory estimate or incidence conclusion. Spatial cell indicators preserve all the required angular derivative bounds.

structure OAI.Falconer.ChartSymbolControl line 17
structure OAI.Falconer.ChartCapControl line 27
theorem OAI.Falconer.ChartSymbolControl.cell line 38

theorem OAI.Falconer.exists_controlled_cap_partition line 60

Source documentation

The finite cap partition supplies the cap regularity bounds.

theorem exists_controlled_cap_partition (n m : ℕ) :
    ∃ H : ℝ, 0 ≤ H ∧ ∀ δ : ℝ, 0 < δ → δ ≤ 1 →
      ∃ (S : Finset (Sphere (n+2))) (η : Sphere (n+2) → Sphere (n+2) → ℝ),
        (S.card : ℝ) ≤ (4/δ+1)^(n+2) ∧
        (∀ w, ∑ c ∈ S, η c w = 1) ∧
        (∀ c ∈ S, ∀ w, 0 ≤ η c w) ∧
        ∀ c ∈ S, ChartCapControl m (η c) (c : Space (n+2)) δ H := by
…

Mentions: OAI.Falconer.Sphere, OAI.Falconer.ChartCapControl, OAI.Falconer.Space