BackwardTargets.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The backwards pivot-target recurrence

For coefficients c_j = 2^j J + a_j - Delta_j, the pivot target is c_j plus the sum of all later pivot targets. This constructs the recurrence, rather than assuming that its simultaneous equations have a solution.

def OAI.Ostmann.backwardTargets line 17
theorem OAI.Ostmann.backwardTargets_length line 21
theorem OAI.Ostmann.backwardTargets_sum_cons line 26
theorem OAI.Ostmann.backwardTargets_drop line 31
theorem OAI.Ostmann.backwardTargets_get line 40
theorem OAI.Ostmann.backwardTargets_nonneg line 52
theorem OAI.Ostmann.backwardTargets_sum_upper line 65
theorem OAI.Ostmann.backwardTargets_lower_last line 78
Source documentation
Every target is at least the final coefficient when the coefficients are nonnegative. Thus the last pivot controls the common lower scale.
```
theorem backwardTargets_lower_last (cs : List ℝ) (hne : cs ≠ [])
    (hcs : ∀ c ∈ cs, 0 ≤ c) :
    ∀ t ∈ backwardTargets cs, cs.getLast hne ≤ t := by
…
```
Mentions: OAI.Ostmann.backwardTargets
theorem OAI.Ostmann.backwardTargets_each_upper line 102