SourcePacketRegroup.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact regrouping of original packet amplitudes by assigned top and length. This connects the individual-packet residual estimates to the same top-band amplitudes appearing in the physical path integrals.

theorem OAI.LipschitzHilbert.weighted_sum_fibers line 14

def OAI.LipschitzHilbert.AngularGrid.sourceGroupedCoefficient line 33

Source documentation

The scalar factor at one node is constant on every top/length fiber.

def sourceGroupedCoefficient {N : ℕ} (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (K : ℕ) (gap : ℕ → ℝ) (stop : ι → Fin N → ℕ) (phase : ℕ → ℂ)
    (a : ℝ) (x : X) (level : ℕ) (cell : ℤ) (p : ι×Fin N) : ℂ :=
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_grouped_sum line 44

theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_regroup line 61

Source documentation

The original packet amplitude equals its literal top/length regrouping. No estimate, choice of signs, or bound on the number of fibers is used.

theorem sourcePacketAmplitude_regroup {N : ℕ} (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (K : ℕ) (gap : ℕ → ℝ) (packets : Finset σ) (assigned : σ → ι)
    (hassigned : ∀ q ∈ packets, assigned q ∈ tops)
    (lengthIndex : σ → Fin N) (stop : ι → Fin N → ℕ) (value : σ → E)
    (phase : ℕ → ℂ) (a : ℝ) (x : X) (level : ℕ) (cell : ℤ) :
    g.sourcePacketAmplitude tops slope precision cutoff weight K gap packets assigned
      (fun q => stop (assigned q) (lengthIndex q)) value phase a x level cell =
    g.sourcePacketAmplitude tops slope precision cutoff weight K gap
      (tops ×ˢ (Finset.univ : Finset (Fin N))) Prod.fst (fun p => stop p.1 p.2)
      (fun p => ∑ q ∈ packets.filter (fun q => (assigned q,lengthIndex q) = p), value q)
      phase a x level cell := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid