AngularSourceWeight.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Boundary masses and logarithmic variation along actual eligible top paths. Every boundary uses the start of the block whose last transition is the current level, in the shared family of all shifted groupings.

theorem OAI.LipschitzHilbert.AngularGrid.index_center line 19
theorem OAI.LipschitzHilbert.AngularGrid.boundaryTops_eq_of_cell line 33
theorem OAI.LipschitzHilbert.AngularGrid.boundaryMass_eq_of_cell line 42
def OAI.LipschitzHilbert.AngularGrid.sourceBoundaryMass line 51
theorem OAI.LipschitzHilbert.AngularGrid.sourceBoundaryMass_path line 57
theorem OAI.LipschitzHilbert.AngularGrid.sourceBoundaryMass_bounds line 66

theorem OAI.LipschitzHilbert.AngularGrid.source_full_root_log_variation line 81

Source documentation

The source's full-root logarithmic bound follows from actual top masses, including all losses of eligibility.

theorem source_full_root_log_variation (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hp : ∀ i ∈ tops, 0 ≤ precision i) (hw : ∀ i x, 0 < weight i x)
    {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (N : ℕ) (top : ι)
    (htop : top ∈ tops) (he : g.eligible cutoff (precision top) N) (x : X) :
    let n := fun j => g.mass tops slope precision cutoff weight j (g.index j (slope top)) x
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.source_hierarchyWeight_variation line 108

Source documentation

No positive lower cutoff on a mass is imposed: the assigned top's own weight supplies the endpoint bound.

theorem source_hierarchyWeight_variation (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hp : ∀ i ∈ tops, 0 ≤ precision i) (hw : ∀ i x, 0 < weight i x)
    {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (phase : ℕ → ℂ)
    (N : ℕ) (top : ι) (htop : top ∈ tops)
    (he : g.eligible cutoff (precision top) N) (x : X)
    (a Z : ℝ) (ha : 0 ≤ a) (hZ : 0 ≤ Z)
    (hz0 : ∀ j < N, 0 ≤ (phase j).re) (hz : ∀ j < N, ‖phase j‖ ≤ Z) :
    let n := fun j => g.mass tops slope precision cutoff weight j (g.index j (slope top)) x
…

Mentions: OAI.LipschitzHilbert.AngularGrid