PacketDataAssignedPhysical.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact assignment and length regrouping of the physical packet sum.

def OAI.LipschitzHilbert.PacketLatticeData.assignedPhysicalBands line 21
theorem OAI.LipschitzHilbert.PacketLatticeData.assignedPhysicalBands_eq line 25

theorem OAI.LipschitzHilbert.PacketLatticeData.physicalMaskedAmplitude_top_bands line 32

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 : PacketLatticeData 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.PacketLatticeData, OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.PacketLatticeData.physicalActivePathValue_top_bands line 56
theorem OAI.LipschitzHilbert.PacketLatticeData.physicalShiftedPathPrediction_top_bands line 79
theorem OAI.LipschitzHilbert.PacketLatticeData.physicalOffchildAmplitude_top_bands line 102