OAI/Analysis/LipschitzHilbert/Trees/SourceReferencePhysicalIdentity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_physicalMultiplierCoefficient line 25
2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_alternate_physicalPacket line 44
3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_physicalMaskedValue line 53
4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_referenceFamily_selected line 72

   Source documentation

   A selected set supported in the reference cone has the identical sum after the literal label restriction, including empty item fibers.

   theorem sum_referenceFamily_selected {E : Type*} [AddCommMonoid E]
       (S : Finset P.PacketIndex) (f : P.PacketIndex → E)
       (hS : ∀ u ∈ S, P.referenceCondition oldSlope newSlope R cone w u.1 u.2.1) :
       (∑ u ∈ (Finset.univ : Finset (Q).PacketIndex).filter
         (fun u => (⟨u.1,⟨orig u.1 u.2.1,u.2.2⟩⟩ : P.PacketIndex) ∈ S),
         f ⟨u.1,⟨orig u.1 u.2.1,u.2.2⟩⟩) = ∑ u ∈ S, f u := by
   …

   Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.PacketIndex

5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_packetAmplitude_selected line 94

   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.SourceLabeledLattice.PacketIndex

6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_packetResidual_selected line 111
7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_physicalSourceResidual_selected line 132

   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.SourceLabeledLattice.PacketIndex