OAI/Analysis/LipschitzHilbert/Trees/SourceAmplitudeAssembly.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_top_fibers line 17

   Source documentation

   Regrouping the actual packet family by assigned top introduces exactly the eligible tops in the angular node. Empty packet fibers contribute zero.

   theorem sourcePacketAmplitude_top_fibers (g : AngularGrid) (tops : Finset ι)
       (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
       (hp : ∀ t ∈ tops, 0 ≤ precision t) (K : ℕ) (gap : ℕ → ℝ)
       (bands : Finset σ) (stop : ι → σ → ℕ) (value : ι → σ → E)
       (he : ∀ t ∈ tops, ∀ j ∈ bands, g.eligible cutoff (precision t) (stop t j))
       (phase : ℕ → ℂ) (a : ℝ) (z : X) (level : ℕ) (cell : ℤ) :
       g.sourcePacketAmplitude tops slope precision cutoff weight K gap (tops ×ˢ bands)
         Prod.fst (fun p => stop p.1 p.2) (fun p => value p.1 p.2) phase a z level cell =
         ∑ t ∈ g.cellTops tops slope precision cutoff level cell,
           g.sourcePacketAmplitude tops slope precision cutoff weight K gap bands
             (fun _ => t) (stop t) (value t) phase a z level (g.index level (slope t)) := by
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid

2. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_node_envelope line 46

   Source documentation

   The complete source family satisfies the linear node-mass envelope, including arbitrary original-length restrictions and insignificant masks.

   theorem sourcePacketAmplitude_node_envelope (grid : AngularGrid) (tops : Finset ι)
       (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
       (hp : ∀ t ∈ tops, 0 ≤ precision t) (hw : ∀ t z, 0 < weight t z)
       {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (phase : ℕ → ℂ)
       (M : ι → ℕ) (hM : ∀ t ∈ tops, grid.eligible cutoff (precision t) (M t))
       (hMmax : ∀ t ∈ tops, ∀ k, grid.eligible cutoff (precision t) k → k ≤ M t)
       (a Z : ℝ) (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (hZ : 0 ≤ Z)
       (hz0 : ∀ t ∈ tops, ∀ j < M t, 0 ≤ (phase j).re)
       (hz : ∀ t ∈ tops, ∀ j < M t, ‖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