SourceResidualVariation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The fixed residual collection is grouped by stopping level in the unary recurrence and by packet length in the reference-line variation. Antitone stopping transports every disjoint collection of level bands to disjoint length bands. Empty bands contribute zero.

theorem OAI.LipschitzHilbert.packetPartialSum_sub_eq_band line 19

theorem OAI.LipschitzHilbert.sum_packet_stopping_fibers line 34

Source documentation

Exact regrouping by stopping levels for any fixed packet subset.

theorem sum_packet_stopping_fibers {σ E : Type*} [AddCommMonoid E]
    (Q : Finset σ) (stop : σ → ℕ) (value : σ → E) (a b : ℕ) :
    (∑ k ∈ Finset.Ico a b, ∑ q ∈ Q.filter (fun q => stop q = k), value q) =
      ∑ q ∈ Q.filter (fun q => a ≤ stop q ∧ stop q < b), value q := by
…

theorem OAI.LipschitzHilbert.packet_stopping_band_eq_length_band line 54

Source documentation

Grouping by packet length preserves multiplicities and arbitrary fixed packet selection.

theorem packet_stopping_band_eq_length_band {σ E : Type*} [AddCommMonoid E]
    {N : ℕ} (Q : Finset σ) (lengthIndex : σ → Fin N) (stop : Fin N → ℕ)
    (value : σ → E) (a b : ℕ) :
    (∑ q ∈ Q.filter (fun q => a ≤ stop (lengthIndex q) ∧ stop (lengthIndex q) < b), value q) =
      ∑ j ∈ Finset.univ.filter (fun j => a ≤ stop j ∧ stop j < b),
        ∑ q ∈ Q.filter (fun q => lengthIndex q = j), value q := by
…

theorem OAI.LipschitzHilbert.disjoint_increment_cube_sum line 66

Source documentation

Zero-length intervals may be discarded before applying the finite disjoint-interval variation bound.

theorem disjoint_increment_cube_sum {ι E : Type*} [Fintype ι]
    [NormedAddCommGroup E] (F : ℕ → E) (N : ℕ) (a b : ι → ℕ)
    (hab : ∀ i, a i ≤ b i) (hb : ∀ i, b i ≤ N)
    (hdisjoint : ∀ i j, i ≠ j → a i < b i → a j < b j → b i ≤ a j ∨ b j ≤ a i) :
    (∑ i, ‖F (b i)-F (a i)‖^3) ≤ finiteCubicVariation F N := by
…

Mentions: OAI.LipschitzHilbert.finiteCubicVariation

theorem OAI.LipschitzHilbert.disjoint_stopping_band_cube_sum line 91

Source documentation

Disjoint stopping-level intervals become disjoint intervals of the one fixed length sequence, including when some length fibers are empty.

theorem disjoint_stopping_band_cube_sum {ι E : Type*} [Fintype ι]
    [NormedAddCommGroup E] {N : ℕ} (f : Fin N → E)
    (stop : Fin N → ℕ) (hstop : Antitone stop) (a b : ι → ℕ)
    (hdisjoint : ∀ i j, i ≠ j → b i ≤ a j ∨ b j ≤ a i) :
    (∑ i, ‖∑ j ∈ Finset.univ.filter (fun j => a i ≤ stop j ∧ stop j < b i), f j‖^3) ≤
      finiteCubicVariation (packetPartialSum f) N := by
…

Mentions: OAI.LipschitzHilbert.finiteCubicVariation, OAI.LipschitzHilbert.packetPartialSum

theorem OAI.LipschitzHilbert.stopping_prefix_cubic_variation line 125

Source documentation

The cubic variation of the stop-grouped raw prefix is controlled by the original length-grouped raw prefix, independently of angular depth.

theorem stopping_prefix_cubic_variation {σ E : Type*} [NormedAddCommGroup E]
    {N : ℕ} (Q : Finset σ) (lengthIndex : σ → Fin N)
    (stop : Fin N → ℕ) (hstop : Antitone stop) (value : σ → E) (H : ℕ) :
    let raw := fun k => ∑ q ∈ Q.filter (fun q => stop (lengthIndex q) = k), value q
…

theorem OAI.LipschitzHilbert.unary_runs_stopping_oscillation_cube_sum line 160

Source documentation

All unary runs and their point-dependent greedy segments use this single length variation of the fixed packet collection.

theorem unary_runs_stopping_oscillation_cube_sum {σ E : Type*} [NormedAddCommGroup E]
    {unary : ℕ → Prop} {n : ℕ → ℝ} {start finish : ℕ}
    (R : UnaryRunPartition unary start finish)
    (P : ∀ r : R.runs, UnarySegmentPartition n r.val.1 r.val.2)
    {N : ℕ} (Q : Finset σ) (lengthIndex : σ → Fin N)
    (stop : Fin N → ℕ) (hstop : Antitone stop) (value : σ → E)
    (level : ℕ → ℕ) (hlevel : StrictMono level) (H : ℕ) (hend : level finish ≤ H) :
    let raw := fun k => ∑ q ∈ Q.filter (fun q => stop (lengthIndex q) = k), value q
…

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