SourceTreePacketPath.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The finite tree conservation law uses precisely the original packet active path. The node envelope controls its terminal cost, so deleting the small bad-top mass yields domination by the good physical paths.

theorem OAI.LipschitzHilbert.AngularGrid.sourceTree_packet_path_mass line 19
theorem OAI.LipschitzHilbert.AngularGrid.sourceTree_packet_path_ratio line 23
theorem OAI.LipschitzHilbert.AngularGrid.sourceTree_packet_active_path line 31
theorem OAI.LipschitzHilbert.AngularGrid.sourceTree_packet_good_path_domination line 48

theorem OAI.LipschitzHilbert.AngularGrid.sourceTree_packet_vertex_bound line 97

Source documentation

A single pointwise majorant treats both small and active root masses. Its two terms are the ordinary top mass and the already integrated good physical paths, with the same terminal-envelope constant.

theorem sourceTree_packet_vertex_bound
    (hp : ∀ t ∈ tops, 0 ≤ precision t) (hw : ∀ t x, 0 < weight t x) (hKb : 0 < Kb)
    (count : ℕ) (cell : ℤ) (M C : ℝ) (hM : 1 ≤ M) (hC : 0 ≤ C)
    (hα : 1 ≤ α) (hp0 : 0 ≤ p)
    (hne : (g.cellTops tops slope precision cutoff (ShiftedBlocks.endpoint shift 0) cell).Nonempty)
    (hterminal : ∀ t ∈ g.cellTops tops slope precision cutoff (ShiftedBlocks.endpoint shift 0) cell,
      ¬g.eligible cutoff (precision t) (ShiftedBlocks.endpoint shift count))
    (henvelope : ∀ j ≤ count, ∀ cell,
      ‖g.sourcePacketAmplitude tops slope precision cutoff weight K gap packets assigned stop
        (value x) phase a x (ShiftedBlocks.endpoint shift j) cell‖ ≤
        C*g.mass tops slope precision cutoff weight (ShiftedBlocks.endpoint shift j) cell x)
    (bad : Finset τ)
…

Mentions: OAI.LipschitzHilbert.ShiftedBlocks.endpoint