MovingRoundedCellSums.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The endpoint loss of rounded top and compensation cells

def OAI.Ostmann.movingSmallCellCenters line 11
Source documentation
A compensation type occurs four times in the full initial list.
```
noncomputable def movingSmallCellCenters (top compensation : List ℝ) : List ℝ :=
…
```
theorem OAI.Ostmann.movingSmallCellCenters_length line 14
theorem OAI.Ostmann.movingSmallCellCenters_sum line 23
theorem OAI.Ostmann.movingCompensationCenters_error line 33

theorem OAI.Ostmann.movingSmallCellCenters_lower line 48

Source documentation

Replacing each center by the bottom of its width-two cell loses exactly one per slot, in addition to the top and compensation rounding errors.

theorem movingSmallCellCenters_lower (J cb E et : ℝ)
    (top centers targets : List ℝ)
    (htop : J - et ≤ top.sum + cb)
    (hcomp : List.Forall₂ (fun c w => |4 * c - w| ≤ 4 * E) centers targets) :
    J + targets.sum - (et + 4 * E * centers.length +
      (top.length + 4 * centers.length : ℕ) + 1) ≤
      ((movingSmallCellCenters top centers).map (fun c => c - 1)).sum + (cb - 1) := by
…

Mentions: OAI.Ostmann.movingSmallCellCenters

theorem OAI.Ostmann.movingSmallCellCenters_lower_of_le line 65

Source documentation

One-sided rounding has no accumulated center error in the lower bound.

theorem movingSmallCellCenters_lower_of_le (J cb : ℝ)
    (top centers targets : List ℝ)
    (htop : J ≤ top.sum + cb)
    (hcomp : List.Forall₂ (fun c w => w ≤ 4 * c) centers targets) :
    J + targets.sum - ((top.length + 4 * centers.length : ℕ) + 1) ≤
      ((movingSmallCellCenters top centers).map (fun c => c - 1)).sum + (cb - 1) := by
…

Mentions: OAI.Ostmann.movingSmallCellCenters

theorem OAI.Ostmann.moving_rounded_cell_diagonal_gap line 85

Source documentation

The actual repeated cell endpoints satisfy the diagonal gap after paying for excluded integer centers and one unit per cell endpoint.

theorem moving_rounded_cell_diagonal_gap (k n : ℕ)
    (BD Bz C L J cb w b cg : ℝ) (top centers targets : List ℝ)
    (D : Finset ℤ)
    (hC : 0 ≤ C) (hk : 16 * C + 20 ≤ (k : ℝ) ^ 4)
    (hL : (top.length + 4 * centers.length : ℕ) + 9 ≤ L)
    (hD : (D.card : ℝ) ≤ C * L)
    (hcg : cg ≤ (91 / 100 : ℝ) * L)
    (htop : J ≤ top.sum + cb)
    (hcomp : List.Forall₂ (fun c t => t ≤ 4 * c) centers targets)
    (hupper : 4 * b ≤ w + 4 * (D.card + 2))
    (hbalance : (2 ^ n : ℕ) * w = (2 ^ n : ℕ) * (J + targets.sum) -
      spectatorStepGap BD Bz ((k : ℝ) ^ 4) (2 ^ n : ℕ) (spectatorBulkCount k L)) :
…

Mentions: OAI.Ostmann.spectatorStepGap, OAI.Ostmann.spectatorBulkCount