OAI/Analysis/LipschitzHilbert/Phase/AngularPacketAmplitude.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Finite packet amplitudes for the actual translated angular grid. The stopping level belongs to the packet, independently of when its assigned top loses eligibility.

  1. def OAI.LipschitzHilbert.AngularGrid.packetPathProduct line 15
  2. theorem OAI.LipschitzHilbert.AngularGrid.packetPathProduct_split line 19
  3. theorem OAI.LipschitzHilbert.AngularGrid.packetPathProduct_eq_of_cell line 25
  4. def OAI.LipschitzHilbert.AngularGrid.packetSet line 33
  5. def OAI.LipschitzHilbert.AngularGrid.packetAmplitude line 38
  6. def OAI.LipschitzHilbert.AngularGrid.packetResidual line 43
  7. theorem OAI.LipschitzHilbert.AngularGrid.packetAmplitude_eq_zero_above line 49
  8. theorem OAI.LipschitzHilbert.AngularGrid.packetAmplitude_split line 64

    Source documentation

    Splitting at a block endpoint isolates exactly the packets that stop inside the block. No eligibility mass is substituted for these packets.

    theorem packetAmplitude_split (g : AngularGrid) (packets : Finset σ)
    (slope : σ → ℝ) (stop : σ → ℕ) (base : σ → E) (transition : ℕ → ℤ → ℂ)
    {lower upper : ℕ} (hlu : lower ≤ upper) (cell : ℤ) :
    g.packetAmplitude packets slope stop base transition lower cell =
      g.packetResidual packets slope stop base transition lower upper cell +
      ∑ s ∈ (g.packetSet packets slope stop lower cell).filter (fun s => upper ≤ stop s),
        g.packetPathProduct transition lower upper (slope s) •
          (g.packetPathProduct transition upper (stop s) (slope s) • base s) := by
…

    Mentions: OAI.LipschitzHilbert.AngularGrid

  9. theorem OAI.LipschitzHilbert.AngularGrid.packetAmplitude_block line 87

    Source documentation

    The block decomposition of the finite packet amplitude. The cells are actual descendants of the parent and cover all packets surviving the block; empty cells contribute zero.

    theorem packetAmplitude_block (g : AngularGrid) (packets : Finset σ)
    (slope : σ → ℝ) (stop : σ → ℕ) (base : σ → E) (transition : ℕ → ℤ → ℂ)
    {lower upper : ℕ} (hlu : lower ≤ upper) (parent : ℤ)
    (cells : Finset ℤ) (representative : ℤ → ℝ)
    (hcell : ∀ c ∈ cells, g.index upper (representative c) = c)
    (hparent : ∀ c ∈ cells, g.index lower (representative c) = parent)
    (hcover : ∀ s ∈ g.packetSet packets slope stop lower parent,
      upper ≤ stop s → g.index upper (slope s) ∈ cells) :
    g.packetAmplitude packets slope stop base transition lower parent =
      g.packetResidual packets slope stop base transition lower upper parent +
      ∑ c ∈ cells, g.packetPathProduct transition lower upper (representative c) •
        g.packetAmplitude packets slope stop base transition upper c := by
…

    Mentions: OAI.LipschitzHilbert.AngularGrid

  10. def OAI.LipschitzHilbert.AngularGrid.packetBlockCells line 129
  11. def OAI.LipschitzHilbert.AngularGrid.packetBlockRepresentative line 135
  12. theorem OAI.LipschitzHilbert.AngularGrid.packetBlockRepresentative_spec line 141
  13. theorem OAI.LipschitzHilbert.AngularGrid.packetAmplitude_canonical_block line 151