SourceRootCells.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The nonempty eligible root cells of the actual translated grid. They split the central packet sum exactly. A slope interval no wider than one root contains at most two roots, including its endpoints.

def OAI.LipschitzHilbert.AngularGrid.sourceRootCells line 15
theorem OAI.LipschitzHilbert.AngularGrid.mem_sourceRootCells line 20
theorem OAI.LipschitzHilbert.AngularGrid.sourceRootCells_card_le_two line 33
theorem OAI.LipschitzHilbert.AngularGrid.sourceRootCells_packet_cover line 56

theorem OAI.LipschitzHilbert.AngularGrid.sourceBoundarySum_root_decomposition line 71

Source documentation

The globally weighted central packet sum is the sum of its actual nonempty eligible roots; no packet is assigned to an artificial root.

theorem sourceBoundarySum_root_decomposition (g : AngularGrid) (tops : Finset τ)
    (slope precision : τ → ℝ) (cutoff : ℝ) (weight : τ → X → ℝ)
    (hp : ∀ t ∈ tops, 0 ≤ precision t) (hw : ∀ t x, 0 < weight t x)
    {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (packets : Finset σ)
    (assigned : σ → τ) (stop : σ → ℕ) (value : σ → E)
    (hassigned : ∀ s ∈ packets, assigned s ∈ tops)
    (heligible : ∀ s ∈ packets, g.eligible cutoff (precision (assigned s)) (stop s))
    (a : ℝ) (x : X) :
    (∑ s ∈ packets,
      ((g.sourceBoundaryCoefficient tops slope precision cutoff weight K gap
        (stop s) (assigned s) a x : ℝ):ℂ) • value s) =
    ∑ c ∈ g.sourceRootCells tops slope precision cutoff,
…

Mentions: OAI.LipschitzHilbert.AngularGrid