MovingProductGapBudget.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The recursive product budget is the prescribed compensation gap

def OAI.Ostmann.movingTargetPivotExponent line 9
theorem OAI.Ostmann.drop_sum_head line 12
theorem OAI.Ostmann.movingProductExponent_targets line 23
Source documentation
With exact target centers, the product remaining at depth n is precisely that of the protected slots and the as-yet unused compensation types.
```
theorem movingProductExponent_targets (G J : ℝ) (ws : List ℝ) (n : ℕ) :
    movingProductExponent (movingTargetPivotExponent G ws) (2 * G + J + ws.sum) n =
      2 * G + (2 : ℝ) ^ n * (J + (ws.drop n).sum) := by
…
```
Mentions: OAI.Ostmann.movingProductExponent, OAI.Ostmann.movingTargetPivotExponent
theorem OAI.Ostmann.target_drop_gap line 32
theorem OAI.Ostmann.movingProductExponent_target_gap line 47
Source documentation
This is the exact gap from the manuscript's backwards recursion, expressed in the product budget used by the integer-extended coefficients.
```
theorem movingProductExponent_target_gap (G J : ℝ) (ds : List ℝ)
    (n : ℕ) (hn : n < ds.length) :
    let ws := movingCompensationTargets J ds
…
```
Mentions: OAI.Ostmann.movingCompensationTargets

theorem OAI.Ostmann.movingProductExponent_rounding_bound line 59

Source documentation

A finite center-rounding loss grows only linearly with the depth after normalization by the number of leaves.

theorem movingProductExponent_rounding_bound (T U : ℕ → ℝ) (W Z C R : ℝ)
    (hW : W ≤ Z + C) (hTU : ∀ j, U j - (2 : ℝ) ^ j * R ≤ T j) (n : ℕ) :
    movingProductExponent T W n ≤ movingProductExponent U Z n +
      (2 : ℝ) ^ n * (C + n * R) := by
…

Mentions: OAI.Ostmann.movingProductExponent