SourceLabeledStoppingVariation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The original masked physical packets, grouped by their actual stopping levels, have the same fixed length-variation bound used in the reference event. This includes clamped prefixes and every disjoint unary run.

theorem OAI.LipschitzHilbert.cubicVariation_cube line 15
def OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedValue line 30
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedValue_length_sum line 35
def OAI.LipschitzHilbert.SourceLabeledLattice.physicalStoppingPrefix line 49
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalStoppingPrefix_variation_le line 55
Source documentation
One fixed original variation controls the stopping prefix at every angular horizon, without a factor depending on that horizon.
```
theorem physicalStoppingPrefix_variation_le (stop : Fin N → ℕ)
    (hstop : Antitone stop) (y x : ℝ) (H : ℕ) :
    finiteCubicVariation (P.physicalStoppingPrefix alt hAlt t b v g T L A stop (x,y+t*x)) H ≤
      P.physicalMaskedVariation alt hAlt t b v g T L A y x ^ 3 := by
…
```
Mentions: OAI.LipschitzHilbert.finiteCubicVariation

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalStoppingPrefix_clamped_variation_le line 67

Source documentation

The clamping in the stopped path theorem preserves this bound.

theorem physicalStoppingPrefix_clamped_variation_le (stop : Fin N → ℕ)
    (hstop : Antitone stop) (y x : ℝ) (H : ℕ) :
    finiteCubicVariation (fun k =>
      P.physicalStoppingPrefix alt hAlt t b v g T L A stop (x,y+t*x) (min k H)) (2*H) ≤
        P.physicalMaskedVariation alt hAlt t b v g T L A y x ^ 3 := by
…

Mentions: OAI.LipschitzHilbert.finiteCubicVariation

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalStoppingPrefix_good_bound line 76

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_unary_runs_variation_le line 85

Source documentation

The same original reference event bounds all greedy unary segments.

theorem physical_unary_runs_variation_le
    {unary : ℕ → Prop} {n : ℕ → ℝ} {start finish : ℕ}
    (R : UnaryRunPartition unary start finish)
    (S : ∀ r : R.runs, UnarySegmentPartition n r.val.1 r.val.2)
    (stop : Fin N → ℕ) (hstop : Antitone stop) (y x : ℝ)
    (level : ℕ → ℕ) (hlevel : StrictMono level) (H : ℕ) (hend : level finish ≤ H) :
    (∑ i : UnaryRunSegment R S,
      intervalOscillation (P.physicalStoppingPrefix alt hAlt t b v g T L A stop (x,y+t*x))
        H (level i.2.val.1) (level i.2.val.2)^3) ≤
      P.physicalMaskedVariation alt hAlt t b v g T L A y x ^ 3 := by
…

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