PacketDataReferenceSelectedVariation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A good event in recentered reference coordinates bounds the original selected stopping prefix exactly, including its clamped variation.

theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_selectedPhysicalPrefix line 27

theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_selected_good_bound line 50

Source documentation

The reference good event controls every original selected prefix after recentering, with no angular-horizon or label-count factor.

theorem referenceFamily_selected_good_bound
    (S : Finset P.PacketIndex)
    (hS : ∀ u ∈ S, P.referenceCondition oldSlope newSlope R cone w u.1 u.2.1)
    (stop : Fin N → ℕ) (hstop : Antitone stop) (a e s r : ℝ) (z : ℝ×ℝ)
    (hgood : z ∉ ((Q).restrictPackets ((Finset.univ : Finset (Q).PacketIndex).filter
      (fun u => (⟨u.1,⟨orig u.1 u.2.1,u.2.2⟩⟩ : P.PacketIndex) ∈ S))).physicalReferenceBad
      ((Q).restrictedAlternate (fun j l => alt j (orig j l)) _)
      ((Q).restrictedAlternate_bound (fun j l => alt j (orig j l)) (fun j l => hAlt j (orig j l)) _)
      newSlope a (fun j l => b j (orig j l)) v f (fun j l u => T j (orig j l) u.val)
      L A e s r) (H : ℕ) :
    finiteCubicVariation (fun k => P.selectedPhysicalPrefix alt hAlt oldSlope b v f T L A
      S stop z (min k H)) (2*H) ≤ (L^r)^3 := by
…

Mentions: OAI.LipschitzHilbert.PacketLatticeData.PacketIndex, OAI.LipschitzHilbert.finiteCubicVariation