SourceSelectedGoodEvent.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The reference event of a fixed selected packet family controls its actual stopped prefixes and every disjoint unary run at the same point.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedPhysicalPrefix_good_event_bound line 23

Source documentation

A good reference point bounds the selected physical stopping prefix at every angular horizon, with its original analyzing coefficients.

theorem selectedPhysicalPrefix_good_event_bound (Q : Finset P.PacketIndex)
    (stop : Fin N → ℕ) (hstop : Antitone stop) (z : ℝ×ℝ)
    (hz : z ∉ (P.restrictPackets Q).physicalReferenceBad (P.restrictedAlternate alt Q)
      (P.restrictedAlternate_bound alt hAlt Q) t a b v g (fun j l u => T j l u.val)
      L A e s r) (H : ℕ) :
    finiteCubicVariation (fun k => P.selectedPhysicalPrefix alt hAlt t b v g T L A Q stop z
      (min k H)) (2*H) ≤ (L^r)^3 := by
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.physicalReferenceBad, OAI.LipschitzHilbert.finiteCubicVariation

theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedPhysicalPrefix_unary_good_event_bound line 44

Source documentation

The same selected reference event bounds all disjoint unary runs; there is no factor counting runs or stopping levels.

theorem selectedPhysicalPrefix_unary_good_event_bound (Q : Finset P.PacketIndex)
    (stop : Fin N → ℕ) (hstop : Antitone stop) (z : ℝ×ℝ)
    (hz : z ∉ (P.restrictPackets Q).physicalReferenceBad (P.restrictedAlternate alt Q)
      (P.restrictedAlternate_bound alt hAlt Q) t a b v g (fun j l u => T j l u.val)
      L A e s r)
    {unary : ℕ → Prop} {n : ℕ → ℝ} {start finish : ℕ}
    (R : UnaryRunPartition unary start finish)
    (S : ∀ run : R.runs, UnarySegmentPartition n run.val.1 run.val.2)
    (level : ℕ → ℕ) (hlevel : StrictMono level) (H : ℕ) (hend : level finish ≤ H) :
    (∑ i : UnaryRunSegment R S,
      intervalOscillation (P.selectedPhysicalPrefix alt hAlt t b v g T L A Q stop z)
        H (level i.2.val.1) (level i.2.val.2)^3) ≤ (L^r)^3 := by
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.physicalReferenceBad, OAI.LipschitzHilbert.UnaryRunPartition, OAI.LipschitzHilbert.UnarySegmentPartition, OAI.LipschitzHilbert.UnaryRunSegment, OAI.LipschitzHilbert.intervalOscillation