OAI/Analysis/LipschitzHilbert/Packets/PacketDataReferenceMasked.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_physicalMaskedValue line 20
2. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_packetAmplitude_selected line 39

   Source documentation

   Angular amplitudes are invariant under the selected reference change of coordinates; no top or packet multiplicity is introduced.

   theorem referenceFamily_packetAmplitude_selected {E : Type*} [AddCommMonoid E] [Module ℂ E]
       (S : Finset P.PacketIndex)
       (hS : ∀ u ∈ S, P.referenceCondition oldSlope newSlope R cone w u.1 u.2.1)
       (grid : AngularGrid) (slope : P.PacketIndex → ℝ) (stop : P.PacketIndex → ℕ)
       (base : P.PacketIndex → E) (transition : ℕ → ℤ → ℂ) (level : ℕ) (cell : ℤ) :
       grid.packetAmplitude ((Finset.univ : Finset (Q).PacketIndex).filter
         (fun u => (⟨u.1,⟨orig u.1 u.2.1,u.2.2⟩⟩ : P.PacketIndex) ∈ S))
         (fun u => slope ⟨u.1,⟨orig u.1 u.2.1,u.2.2⟩⟩)
         (fun u => stop ⟨u.1,⟨orig u.1 u.2.1,u.2.2⟩⟩)
         (fun u => base ⟨u.1,⟨orig u.1 u.2.1,u.2.2⟩⟩) transition level cell =
         grid.packetAmplitude S slope stop base transition level cell := by
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.PacketLatticeData.PacketIndex

3. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_packetResidual_selected line 56
4. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_physicalSourceResidual_selected line 77

   Source documentation

   The physical residual identity includes the exact stopping mass and each original top mask, after recentering at the reference direction.

   theorem referenceFamily_physicalSourceResidual_selected {τ : Type*}
       (S : Finset P.PacketIndex)
       (hS : ∀ u ∈ S, P.referenceCondition oldSlope newSlope R cone w u.1 u.2.1)
       (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)
       (b : ∀ j, P.labels j → κ → ℝ → ℂ) (v : ℝ×ℝ → ℝ)
       (f : ℝ×ℝ → EuclideanSpace ℂ κ)
       (grid : AngularGrid) (tops : Finset τ) (slope precision : τ → ℝ)
       (cutoff : ℝ) (weight : τ → (ℝ×ℝ) → ℝ) (assigned : P.PacketIndex → τ)
       (stop : Fin N → ℕ) (T : τ → SlopeBox) (L A alpha : ℝ) (z : ℝ×ℝ)
       (transition : ℕ → ℤ → ℂ) (lower upper : ℕ) (cell : ℤ) :
       grid.packetResidual ((Finset.univ : Finset (Q).PacketIndex).filter
   …

   Mentions: OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.PacketLatticeData.PacketIndex