SourceAssignedStoppedInputs.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The original-packet local bounds give exactly the amplitude inputs of physicalStoppedBoundAt. The terminal distinguished top may disappear while other children remain; the actual cell loss is still bounded by the stopped path loss.

theorem OAI.LipschitzHilbert.AngularGrid.source_stopped_local_envelope line 19

Source documentation

Local node and off-child estimates transfer to the mass-stopped path without altering the packet coefficients or the terminal mass convention.

theorem source_stopped_local_envelope {Kb : ℕ}
    (g : AngularGrid) (tops : Finset τ) (slope precision : τ → ℝ)
    (cut : ℝ) (weight : τ → X → ℝ) (hw : ∀ t x, 0 ≤ weight t x)
    (K : ℕ) (gap : ℕ → ℝ) (packets : Finset σ) (assigned : σ → τ)
    (stop : σ → ℕ) (value : X → σ → EuclideanSpace ℂ κ)
    (phase : ℕ → ℂ) (a : ℝ) (hKb : 0 < Kb) (shift : Fin Kb)
    (top : τ) (x : X) (count : ℕ) (M C CW : ℝ) (hM : 0 ≤ M) (hCW : 0 ≤ CW)
    (hterminal : ¬g.eligible cut (precision top) (ShiftedBlocks.endpoint shift count))
    (hnode : ∀ level cell,
      ‖g.sourcePacketAmplitude tops slope precision cut weight K gap packets assigned stop
        (value x) phase a x level cell‖ ≤ C*g.mass tops slope precision cut weight level cell x)
    (hoff : ∀ lower upper, lower ≤ upper → ∀ s,
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.ShiftedBlocks.endpoint