SourceAngularAmplitude.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Interval concentration controls the actual source sums weighted by angular stopping levels. The finite regrouping and summation by parts introduce no factor depending on the number of scales.

theorem OAI.LipschitzHilbert.stopping_weighted_sum_eq line 19
theorem OAI.LipschitzHilbert.SourceLabeledLattice.angular_stopping_amplitude_bound line 45

theorem OAI.LipschitzHilbert.source_angular_stopping_amplitude_bound line 76

Source documentation

Specialization to the actual angular mass and boundary sets. The individual top weight supplies the positive endpoint normalization.

theorem source_angular_stopping_amplitude_bound
    {ι X : Type*} (grid : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hp : ∀ i ∈ tops, 0 ≤ precision i) (hw : ∀ i z, 0 < weight i z)
    {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (phase : ℕ → ℂ)
    (M : ℕ) (top : ι) (htop : top ∈ tops)
    (he : grid.eligible cutoff (precision top) M) (z : X)
    (a Z : ℝ) (ha : 0 ≤ a) (hZ : 0 ≤ Z)
    (hz0 : ∀ j < M, 0 ≤ (phase j).re) (hz : ∀ j < M, ‖phase j‖ ≤ Z)
    {N : ℕ} {κ : Type} {Label : Fin N → Type} {Item : ∀ j, Label j → Type}
    [Fintype κ] [∀ j l, Fintype (Item j l)]
    (P : SourceLabeledLattice N κ Label Item)
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceLabeledLattice