PacketDataAssignedVertexPath.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The assigned-reference concentration supplies the actual original packet envelope used in stopped paths and the finite-tree vertex bound. All constants are chosen before the packet family.

theorem OAI.LipschitzHilbert.PacketLatticeData.eventually_assigned_original_node_envelope line 15

theorem OAI.LipschitzHilbert.PacketLatticeData.eventually_assigned_original_offchild line 111

Source documentation

The original off-child packets retain the exact lost-mass gain.

theorem eventually_assigned_original_offchild (C q : ℝ) (hC : 1 ≤ C) :
    ∀ᶠ L : ℝ in atTop,
    ∀ (τ : Type) (tops : Finset τ) (T : τ → SlopeBox)
      (N : ℕ) (κ : Type) (Label : Fin N → Type) (Item : ∀ j, Label j → Type)
      [Fintype κ] [∀ j l, Fintype (Item j l)]
      (P : PacketLatticeData N κ Label Item)
      (packets : Finset P.PacketIndex) (assigned : P.PacketIndex → τ)
      (oldSlope : ℝ) (R : τ → ℝ) (cone w F : ℝ)
      (hw : 0 < w) (hcone : 0 ≤ cone) (hF : 0 ≤ F) (hwide : cone*w ≤ P.width)
      (hfrequency : ∀ k, |P.frequency k| ≤ F/w)
      (alt : ∀ j (l : P.labels j), Item j l → κ → SchwartzMap (ℝ×ℝ) ℂ)
      (hAlt : ∀ j l u k, planarProfileConstant (alt j l u k) (2*P.order) ≤ P.profileBound)
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.PacketLatticeData, OAI.LipschitzHilbert.planarProfileConstant