PositiveScheduling.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

A fixed positive coefficient schedule, dense for every bounded sequence.

abbrev OAI.Tingley.RationalPrefix line 30
Source documentation
A rational probability vector on an initial, nonempty list of indices.
```
abbrev RationalPrefix :=
…
```
def OAI.Tingley.prefixZeroExtend line 34
Source documentation
Extend a finite vector by zero, using the actual natural-number indices.
```
def prefixZeroExtend {A : Type*} [Zero A] {k : ℕ} (f : Fin k → A) (i : ℕ) : A :=
…
```
theorem OAI.Tingley.prefixZeroExtend_apply line 37
theorem OAI.Tingley.sum_prefixZeroExtend line 41
def OAI.Tingley.baseStageWeights line 52
Source documentation
A failed or premature code is replaced by the point mass at the first index.
```
def baseStageWeights (n : ℕ) : Fin (n + 1) → ℚ :=
…
```
theorem OAI.Tingley.baseStageWeights_nonneg line 58
theorem OAI.Tingley.baseStageWeights_sum line 74
theorem OAI.Tingley.baseStageWeights_pair line 84
def OAI.Tingley.stageMixing line 90
theorem OAI.Tingley.stageMixing_pos line 92
theorem OAI.Tingley.stageMixing_lt_one line 96
def OAI.Tingley.positiveStageWeights line 102
Source documentation
Mix with the uniform vector on all available indices.
```
def positiveStageWeights (n : ℕ) (i : Fin (n + 1)) : ℝ :=
…
```
theorem OAI.Tingley.positiveStageWeights_pos line 106
theorem OAI.Tingley.positiveStageWeights_sum line 114
def OAI.Tingley.stageMean line 126
def OAI.Tingley.rationalPrefixMean line 129
theorem OAI.Tingley.norm_probability_sum_le line 132
theorem OAI.Tingley.sum_padded_mean line 142
theorem OAI.Tingley.norm_stageMean_sub_rational_le line 153
theorem OAI.Tingley.exists_late_stageMean_close_rational line 196

theorem OAI.Tingley.exists_rational_simplex_l1_close line 214

Source documentation

Rational simplex approximation by flooring the tail and assigning the residual to index zero.

theorem exists_rational_simplex_l1_close
    (m : ℕ) (α : Fin (m+1) → ℝ) (hα : ∀ i, 0 ≤ α i)
    (hsum : ∑ i, α i = 1) (δ : ℝ) (hδ : 0 < δ) :
    ∃ q : Fin (m+1) → ℚ, (∀ i, 0 ≤ q i) ∧ (∑ i, q i = 1) ∧
      (∑ i, |(q i : ℝ)-α i|) < δ := by
…

theorem OAI.Tingley.stageMean_mem_convexHull line 285
theorem OAI.Tingley.rationalPrefixMean_mem_closure line 291
theorem OAI.Tingley.prefixMean_mem_closure line 299

theorem OAI.Tingley.convexHull_range_subset_of_prefixes line 331

Source documentation

Every finite convex combination of a sequence fits in one initial prefix.

theorem convexHull_range_subset_of_prefixes (v : ℕ → X) (E : Set X)
    (hprefix : ∀ n, convexHull ℝ (Set.range (fun i : Fin (n+1) => v i.val)) ⊆ E) :
    convexHull ℝ (Set.range v) ⊆ E := by
…

theorem OAI.Tingley.closure_range_stageMean_eq line 350