ConvexMicrosteps.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Convex control of the actual microstep sum

The unfinished final microstep is filled with one fixed label. Its cost is explicit, so the number of full steps need not divide the total time.

theorem OAI.PolycyclicRecognition.infDist_weighted_sum_le line 23

Source documentation

The convex error of a weighted sum is bounded by the sum of its label errors and the exact remainder error. The labels are chosen only in a finite sum; no measurable choice is used.

theorem infDist_weighted_sum_le
    {ι W : Type*} [Fintype ι] [NormedAddCommGroup W] [NormedSpace ℝ W]
    {S : Set W} (hS : IsCompact S) {w₀ : W} (hw₀ : w₀ ∈ S)
    (a : ι → ℝ) (ha : ∀ i, 0 ≤ a i) (hsum : ∑ i, a i ≤ 1)
    (x : ι → W) (e : W) :
    infDist ((∑ i, a i • x i) + e) (convexHull ℝ S) ≤
      (∑ i, a i * infDist (x i) S) + ‖e - (1 - ∑ i, a i) • w₀‖ := by
…