SourcePhysicalPacketAssembly.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Individual original physical packets and their top/length bands produce the same angular node amplitude, with all masks and analyzing coefficients retained.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedAmplitude_top_bands line 19

Source documentation

The angular amplitude of the original masked packets is exactly its amplitude assembled from literal assigned-top physical bands.

theorem physicalMaskedAmplitude_top_bands
    (P : SourceLabeledLattice N κ Label Item)
    (alt : ∀ j (l : P.labels j), Item j l → κ → SchwartzMap (ℝ×ℝ) ℂ)
    (hAlt : ∀ j l u k, planarProfileConstant (alt j l u k) (2*P.order) ≤ P.profileBound)
    (t : ℝ) (b : ∀ j, P.labels j → κ → ℝ → ℂ)
    (v : ℝ×ℝ → ℝ) (f : ℝ×ℝ → EuclideanSpace ℂ κ)
    (T : ∀ j (l : P.labels j), Item j l → SlopeBox) (L A : ℝ)
    (grid : AngularGrid) (tops : Finset τ) (slope precision : τ → ℝ) (cutoff : ℝ)
    (weight : τ → ℝ×ℝ → ℝ) (K : ℕ) (gap : ℕ → ℝ)
    (packets : Finset P.PacketIndex) (assigned : P.PacketIndex → τ)
    (hassigned : ∀ q ∈ packets, assigned q ∈ tops)
    (stop : τ → Fin N → ℕ) (phase : ℕ → ℂ) (a : ℝ)
…

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