WeightRounding.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

def OAI.UniqueGamesTheorem.Reduction.WeightRounding.floorMass line 9

def OAI.UniqueGamesTheorem.Reduction.WeightRounding.roundCounts line 13

Source documentation

Increment the first r floors, in the original occurrence order.

def roundCounts (D q : Nat) : Nat → List Nat → List Nat
  | _, [] => []
  | 0, p :: ps => (D * p / q) :: roundCounts D q 0 ps
  | r + 1, p :: ps => (D * p / q + 1) :: roundCounts D q r ps

def OAI.UniqueGamesTheorem.Reduction.WeightRounding.deficit line 18
def OAI.UniqueGamesTheorem.Reduction.WeightRounding.rounded line 20
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.length_roundCounts line 23
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.sum_roundCounts line 29
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.floorMass_mul_le line 45
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.scaled_sum_lt line 55
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.floorMass_le_target line 71
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.deficit_lt_length line 76
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.sum_rounded line 87
Source documentation
Equation (4.7), total mass: the output has exactly the chosen denominator.
```
theorem sum_rounded (D q : Nat) (ps : List Nat) (hq : 0 < q)
    (hmass : ps.sum = q) : (rounded D q ps).sum = D := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.WeightRounding.rounded

def OAI.UniqueGamesTheorem.Reduction.WeightRounding.selectedSum line 96

Source documentation

Sum only the positions selected by an arbitrary predicate.

def selectedSum : List Nat → (Nat → Bool) → Nat
  | [], _ => 0
  | p :: ps, keep => (if keep 0 then p else 0) +
      selectedSum ps (fun i => keep (i + 1))

/-- The two inequalities encode `|nᵢ − D pᵢ/q| ≤ 1`. -/

theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.floor_entry_bounds line 102
Source documentation
The two inequalities encode |nᵢ − D pᵢ/q| ≤ 1.
```
theorem floor_entry_bounds (D q p : Nat) (hq : 0 < q) (b : Bool) :
    let n := D * p / q + if b then 1 else 0
…
```
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.selected_roundCounts_error line 113
Source documentation
Equation (4.8) for every selection of occurrences, before dividing by Dq. The selection can be the equations satisfied by any particular assignment.
```
theorem selected_roundCounts_error (D q r : Nat) (ps : List Nat)
    (keep : Nat → Bool) (hq : 0 < q) :
    selectedSum (roundCounts D q r ps) keep * q ≤
        D * selectedSum ps keep + ps.length * q ∧
    D * selectedSum ps keep ≤
        selectedSum (roundCounts D q r ps) keep * q + ps.length * q := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.WeightRounding.selectedSum, OAI.UniqueGamesTheorem.Reduction.WeightRounding.roundCounts
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.selected_rounded_error line 138
def OAI.UniqueGamesTheorem.Reduction.WeightRounding.replicateOccurrences line 146
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.length_replicateOccurrences line 150
def OAI.UniqueGamesTheorem.Reduction.WeightRounding.copyIndices line 159
Source documentation
Output occurrence indices; each integer count gives that many separate copies.
```
def copyIndices : List Nat → List Nat
  | [] => []
  | n :: ns => List.replicate n 0 ++ (copyIndices ns).map Nat.succ
```
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.length_copyIndices line 163
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.mem_copyIndices_lt line 168
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.count_copyIndices line 184
Source documentation
Copying occurrences preserves the satisfaction test for every assignment.
```
theorem count_copyIndices (ns : List Nat) (keep : Nat → Bool) :
    ((copyIndices ns).filter keep).length = selectedSum ns keep := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.WeightRounding.copyIndices, OAI.UniqueGamesTheorem.Reduction.WeightRounding.selectedSum
def OAI.UniqueGamesTheorem.Reduction.WeightRounding.uniformSource line 193
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.uniformSource_indices_lt line 195
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.length_uniformSource line 200
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.uniformSource_nonempty line 204

theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.uniformSource_error line 213

Source documentation

Full occurrence-list form of (4.8), quantified over all satisfaction tests.

theorem uniformSource_error (D q : Nat) (ps : List Nat)
    (keep : Nat → Bool) (hq : 0 < q) :
    ((uniformSource D q ps).filter keep).length * q ≤
        D * selectedSum ps keep + ps.length * q ∧
    D * selectedSum ps keep ≤
        ((uniformSource D q ps).filter keep).length * q + ps.length * q := by
…

Mentions: OAI.UniqueGamesTheorem.Reduction.WeightRounding.uniformSource, OAI.UniqueGamesTheorem.Reduction.WeightRounding.selectedSum

def OAI.UniqueGamesTheorem.Reduction.WeightRounding.ceilQuotient line 222
Source documentation
Integer ceiling; valid for positive a.
```
def ceilQuotient (n a : Nat) : Nat := (n + a - 1) / a
```
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.le_ceilQuotient_mul line 224
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.ceilQuotient_le line 232
def OAI.UniqueGamesTheorem.Reduction.WeightRounding.targetDenominator line 239
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.targetDenominator_error_budget line 242
Source documentation
Cross-multiplied statement m / D ≤ γ₀ / 4.
```
theorem targetDenominator_error_budget (m a b : Nat) (ha : 0 < a) :
    4 * m * b ≤ targetDenominator m a b * a :=
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.WeightRounding.targetDenominator
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.targetDenominator_size line 248
Source documentation
At fixed rational γ₀, the number of output occurrences is linear in m. This is an output-size bound, not a machine-model complexity theorem.
```
theorem targetDenominator_size (m a b : Nat) (ha : 0 < a) :
    targetDenominator m a b ≤ 4 * b * m := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.WeightRounding.targetDenominator
theorem OAI.UniqueGamesTheorem.Reduction.WeightRounding.targetDenominator_positive line 253