SourceBlockChildren.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Actual block children are the nonempty eligible-top cells. Their canonical representatives are slopes of eligible tops, including cells whose packet amplitude is zero.

def OAI.LipschitzHilbert.AngularGrid.sourceBlockCells line 15
def OAI.LipschitzHilbert.AngularGrid.sourceBlockTop line 20
theorem OAI.LipschitzHilbert.AngularGrid.sourceBlockTop_spec line 25
theorem OAI.LipschitzHilbert.AngularGrid.sourceBlockTop_mem_child line 36
theorem OAI.LipschitzHilbert.AngularGrid.sourceBlockCells_nonempty_child line 44

theorem OAI.LipschitzHilbert.AngularGrid.mem_sourceBlockCells_of_top line 51

Source documentation

Every eligible top in the parent selects one of these children.

theorem mem_sourceBlockCells_of_top {ι : Type*} (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (lower upper : ℕ) (parent : ℤ)
    (hp : ∀ t ∈ tops, 0 ≤ precision t) (hle : lower ≤ upper)
    (top : ι) (htop : top ∈ tops) (hparent : g.index lower (slope top) = parent)
    (he : g.eligible cutoff (precision top) upper) :
    g.index upper (slope top) ∈ g.sourceBlockCells tops slope precision cutoff lower upper parent := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_block_children line 64

Source documentation

Using the nonempty top children gives the exact packet decomposition. A child with no surviving packet contributes its actual zero amplitude.

theorem sourcePacketAmplitude_block_children {ι σ X E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℂ E]
    (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ) (cutoff : ℝ)
    (weight : ι → X → ℝ) (hp : ∀ t ∈ tops, 0 ≤ precision t)
    (K : ℕ) (gap : ℕ → ℝ) (packets : Finset σ) (assigned : σ → ι)
    (stop : σ → ℕ) (value : σ → E) (phase : ℕ → ℂ) (a : ℝ) (x : X)
    (hassigned : ∀ s ∈ packets, assigned s ∈ tops)
    (heligible : ∀ s ∈ packets, g.eligible cutoff (precision (assigned s)) (stop s))
    {lower upper : ℕ} (hle : lower ≤ upper) (parent : ℤ) :
    g.sourcePacketAmplitude tops slope precision cutoff weight K gap packets assigned stop
      value phase a x lower parent =
    g.packetResidual packets (fun s => slope (assigned s)) stop
…

Mentions: OAI.LipschitzHilbert.AngularGrid