UnarySegmentation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual stopping indices for the greedy unary-segment decomposition.

theorem OAI.LipschitzHilbert.exists_first_unit_drop line 13

Source documentation

End a completed unary segment at the first accumulated unit drop. Since each constituent drop is smaller than one, its total is below two.

theorem exists_first_unit_drop (n : ℕ → ℝ) (start finish : ℕ)
    (horder : start ≤ finish) (htotal : 1 ≤ n start - n finish)
    (hstep : ∀ j, start ≤ j → j < finish → n j - n (j + 1) < 1) :
    ∃ cut, start < cut ∧ cut ≤ finish ∧ 1 ≤ n start - n cut ∧
      n start - n cut < 2 ∧ ∀ j, start ≤ j → j < cut → n start - n j < 1 := by
…

structure OAI.LipschitzHilbert.UnarySegmentPartition line 43
Source documentation
A finite partition of a unary run into its actual successive segments.
```
structure UnarySegmentPartition (n : ℕ → ℝ) (start finish : ℕ) where
…
```
theorem OAI.LipschitzHilbert.exists_unary_segment_partition line 53
Source documentation
Greedy unit-drop stopping constructs the partition, with at most the last segment incomplete. There is no bound on the number of tiny drops.
```
theorem exists_unary_segment_partition (n : ℕ → ℝ) (start finish : ℕ)
    (horder : start ≤ finish)
    (hstep : ∀ j, start ≤ j → j < finish → n j - n (j + 1) < 1) :
    Nonempty (UnarySegmentPartition n start finish) := by
…
```
Mentions: OAI.LipschitzHilbert.UnarySegmentPartition