SourceAngularIdentity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Identification of each single-top contribution to the shared analytic family with the stopping-weighted source band sum.

theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_single_top line 16

theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_single_top_bound line 60

Source documentation

The interval concentration bound now controls the actual single-top contribution to the shared analytic family, on every starting level.

theorem sourcePacketAmplitude_single_top_bound (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)
    (coeff : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
…

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