OAI/Analysis/LipschitzHilbert/Phase/AngularAmplitudeIdentity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.AngularGrid.sourceBoundaryCoefficient line 17
2. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_entire_line line 25
3. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_equal_coordinates line 41

   Source documentation

   Exact source equation (30), summed over the packets of one root.

   theorem sourcePacketAmplitude_equal_coordinates (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 : ℕ → ℝ) (packets : Finset σ)
       (assigned : σ → ι) (stop : σ → ℕ) (value : σ → E)
       (hassigned : ∀ s ∈ packets, assigned s ∈ tops)
       (heligible : ∀ s ∈ packets, g.eligible cutoff (precision (assigned s)) (stop s))
       (a : ℝ) (x : X) (root : ℤ) :
       ((g.mass tops slope precision cutoff weight 0 root x ^ a : ℝ) : ℂ) •
         g.sourcePacketAmplitude tops slope precision cutoff weight K gap packets assigned stop
           value (fun _ => (a : ℂ)) a x 0 root =
         ∑ s ∈ g.packetSet packets (fun s => slope (assigned s)) stop 0 root,
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid

4. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_block line 71

   Source documentation

   The same family has the exact block decomposition at arbitrary endpoints. Shift-specific endpoints enter only as arguments here.

   theorem sourcePacketAmplitude_block (g : AngularGrid) (tops : Finset ι)
       (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
       (K : ℕ) (gap : ℕ → ℝ) (packets : Finset σ) (assigned : σ → ι)
       (stop : σ → ℕ) (value : σ → E) (phase : ℕ → ℂ) (a : ℝ) (x : X)
       {lower upper : ℕ} (hlu : lower ≤ upper) (parent : ℤ) :
       g.sourcePacketAmplitude tops slope precision cutoff weight K gap packets assigned stop
         value phase a x lower parent =
       g.packetResidual packets (fun s => slope (assigned s)) stop
         (g.sourcePacketBase tops slope precision cutoff weight assigned stop value a x)
         (g.sourceTransition tops slope precision cutoff weight K gap phase x) lower upper parent +
       ∑ c ∈ g.packetBlockCells packets (fun s => slope (assigned s)) stop lower upper parent,
         g.packetPathProduct (g.sourceTransition tops slope precision cutoff weight K gap phase x)
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid