SourceRestrictedPacketAmplitude.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The angular sums of a literal packet restriction are the original selected sums. Stopping levels, top assignments, hierarchy masses and analyzing coefficients are unchanged.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.restrictPackets_packetAmplitude line 19

Source documentation

Exact transport of a selected angular amplitude to restricted item fibers.

theorem restrictPackets_packetAmplitude {E : Type*} [AddCommMonoid E] [Module ℂ E]
    (Q : Finset P.PacketIndex) (grid : AngularGrid) (slope : P.PacketIndex → ℝ)
    (stop : P.PacketIndex → ℕ) (base : P.PacketIndex → E)
    (transition : ℕ → ℤ → ℂ) (level : ℕ) (cell : ℤ) :
    grid.packetAmplitude (Finset.univ : Finset (P.restrictPackets Q).PacketIndex)
      (fun u => slope ⟨u.1,⟨u.2.1,u.2.2.val⟩⟩)
      (fun u => stop ⟨u.1,⟨u.2.1,u.2.2.val⟩⟩)
      (fun u => base ⟨u.1,⟨u.2.1,u.2.2.val⟩⟩) transition level cell =
      grid.packetAmplitude Q slope stop base transition level cell := by
…

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

theorem OAI.LipschitzHilbert.SourceLabeledLattice.restrictPackets_packetResidual line 35

Source documentation

The residual is transported exactly, including both stopping filters.

theorem restrictPackets_packetResidual {E : Type*} [AddCommMonoid E] [Module ℂ E]
    (Q : Finset P.PacketIndex) (grid : AngularGrid) (slope : P.PacketIndex → ℝ)
    (stop : P.PacketIndex → ℕ) (base : P.PacketIndex → E)
    (transition : ℕ → ℤ → ℂ) (lower upper : ℕ) (cell : ℤ) :
    grid.packetResidual (Finset.univ : Finset (P.restrictPackets Q).PacketIndex)
      (fun u => slope ⟨u.1,⟨u.2.1,u.2.2.val⟩⟩)
      (fun u => stop ⟨u.1,⟨u.2.1,u.2.2.val⟩⟩)
      (fun u => base ⟨u.1,⟨u.2.1,u.2.2.val⟩⟩) transition lower upper cell =
      grid.packetResidual Q slope stop base transition lower upper cell := by
…

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

theorem OAI.LipschitzHilbert.SourceLabeledLattice.restrictPackets_physicalSourceResidual line 57

Source documentation

Physical residual transport preserves the original analyzing integral and the same hierarchy mass at every packet's stopping level.

theorem restrictPackets_physicalSourceResidual {τ : Type*}
    (Q : Finset P.PacketIndex) (t : ℝ) (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 (P.restrictPackets Q).PacketIndex)
      (fun u => slope (assigned ⟨u.1,⟨u.2.1,u.2.2.val⟩⟩)) (fun u => stop u.1)
      (grid.sourcePacketBase tops slope precision cutoff weight
        (fun u => assigned ⟨u.1,⟨u.2.1,u.2.2.val⟩⟩) (fun u => stop u.1)
        ((P.restrictPackets Q).physicalMaskedValue (P.restrictedAlternate alt Q)
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SourceLabeledLattice.PacketIndex, OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedValue