PacketDataAssignedSupportedPath.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual selected centers supply the geometry of the inhabited reference families used by the supported plane estimate. Empty scales add no condition.

theorem OAI.LipschitzHilbert.PacketLatticeData.assignedInhabitedReference_supportedTopGeometry line 18

Source documentation

The exact assigned-and-recentered family satisfies the supported geometry using only the centers of packets actually assigned to this top.

theorem assignedInhabitedReference_supportedTopGeometry
    (P : PacketLatticeData N κ Label Item)
    (packets : Finset P.PacketIndex) (assigned : P.PacketIndex → τ)
    (T : τ → SlopeBox) (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)
    (top : τ) (K : ℝ) (D : ℕ)
    (hwidth : P.width ≤ K*(T top).width)
    (horder : 3+2*(8*D+1) ≤ P.order)
    (hscale : P.scale = 4*(K*(T top).width))
    (hX : ∀ q ∈ packets, assigned q = top →
      |P.actualX q.1 q.2.1 q.2.2-(T top).x|+P.length q.1 ≤ K*(T top).length)
…

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