RoundingLemmas.lean`

79 declarations, 0 contain sorry, 0 declared as axioms

Largest-remainder rounding for the occurrence game

The input is an indexed list of nonnegative rational weights, represented exactly by natural numerators with a common positive denominator. The order uses decreasing fractional remainders, with the original occurrence index as a deterministic tie-break. No constraint, endpoint or occurrence identity is changed by rounding.

abbrev OAI.UniqueGamesTheorem.Explicit.Rounding.IntegerRounding line 31
def OAI.UniqueGamesTheorem.Explicit.Rounding.denominator line 34
Source documentation
Exact integer implementation of ceil(h / (a/b)).
```
def denominator (h a b : Nat) : Nat := IntegerRounding (h * b) a
```
Mentions: OAI.UniqueGamesTheorem.Explicit.Rounding.IntegerRounding
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.denominator_budget line 36
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.denominator_size line 40
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.denominator_positive line 45
def OAI.UniqueGamesTheorem.Explicit.Rounding.remainder line 58
Source documentation
The fractional part of Q * (p i / q), with denominator q.
```
def remainder (Q q : Nat) (p : Fin h → Nat) (i : Fin h) : Nat :=
…
```
def OAI.UniqueGamesTheorem.Explicit.Rounding.priority line 61
instance OAI.UniqueGamesTheorem.Explicit.Rounding.priorityDecidable line 65
instance OAI.UniqueGamesTheorem.Explicit.Rounding.priorityTrans line 69
instance OAI.UniqueGamesTheorem.Explicit.Rounding.priorityAntisymm line 76
instance OAI.UniqueGamesTheorem.Explicit.Rounding.priorityTotal line 84
def OAI.UniqueGamesTheorem.Explicit.Rounding.remainderOrder line 92
Source documentation
Executable merge-sort of occurrence indices, rather than their records.
```
def remainderOrder (Q q : Nat) (p : Fin h → Nat) : List (Fin h) :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.remainderOrder_sorted line 95
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.remainderOrder_length line 99
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.remainderOrder_nodup line 103
def OAI.UniqueGamesTheorem.Explicit.Rounding.floorCount line 106
def OAI.UniqueGamesTheorem.Explicit.Rounding.deficit line 109
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.floor_sum_le line 112
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.deficit_lt line 119
def OAI.UniqueGamesTheorem.Explicit.Rounding.incremented line 128
Source documentation
Precisely the first deficit indices in decreasing remainder order.
```
def incremented (Q q : Nat) (p : Fin h → Nat) : Finset (Fin h) :=
…
```
def OAI.UniqueGamesTheorem.Explicit.Rounding.count line 131
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.incremented_card line 134
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.sum_count line 141
Source documentation
Largest-remainder rounding preserves total mass exactly.
```
theorem sum_count (Q q : Nat) (p : Fin h → Nat) (hq : 0 < q)
    (hmass : ∑ i, p i = q) : ∑ i, count Q q p i = Q := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.Rounding.count
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.count_error line 151
Source documentation
Cross-multiplied pointwise error, independent of the rounding order.
```
theorem count_error (Q q : Nat) (p : Fin h → Nat) (hq : 0 < q) (i : Fin h) :
    count Q q p i * q ≤ Q * p i + q ∧
      Q * p i ≤ count Q q p i * q + q := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.Rounding.count
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.incremented_priority line 162
Source documentation
Every incremented entry precedes every entry that is not incremented. This records the largest-remainder requirement, including deterministic ties.
```
theorem incremented_priority (Q q : Nat) (p : Fin h → Nat) (i j : Fin h)
    (hi : i ∈ incremented Q q p) (hj : j ∉ incremented Q q p) :
    priority Q q p i j := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.Rounding.incremented, OAI.UniqueGamesTheorem.Explicit.Rounding.priority

theorem OAI.UniqueGamesTheorem.Explicit.Rounding.selected_count_error line 180

Source documentation

Error on any selected set of occurrences, before division.

theorem selected_count_error (Q q : Nat) (p : Fin h → Nat) (hq : 0 < q)
    (s : Finset (Fin h)) :
    (∑ i ∈ s, count Q q p i) * q ≤ Q * (∑ i ∈ s, p i) + s.card * q ∧
    Q * (∑ i ∈ s, p i) ≤ (∑ i ∈ s, count Q q p i) * q + s.card * q := by
…

Mentions: OAI.UniqueGamesTheorem.Explicit.Rounding.count

theorem OAI.UniqueGamesTheorem.Explicit.Rounding.ratio_error line 191

Source documentation

Convert the integer error certificate to its normalized rational form.

theorem ratio_error (n p m Q q : Nat) (hQ : 0 < Q) (hq : 0 < q)
    (hu : n * q ≤ Q * p + m * q) (hl : Q * p ≤ n * q + m * q) :
    |(n : ℚ) / Q - (p : ℚ) / q| ≤ (m : ℚ) / Q := by
…

theorem OAI.UniqueGamesTheorem.Explicit.Rounding.count_ratio_error line 205
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.selected_ratio_error line 212
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.denominator_ratio_budget line 223
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.denominator_eq_ceil line 235
Source documentation
The algorithm's natural-number division is exactly the claimed ceiling.
```
theorem denominator_eq_ceil (h a b : Nat) (ha : 0 < a) (hb : 0 < b) :
    denominator h a b = Nat.ceil ((h : ℚ) / ((a : ℚ) / b)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.Rounding.denominator

theorem OAI.UniqueGamesTheorem.Explicit.Rounding.selected_tolerance line 255

Source documentation

Every satisfied-occurrence set has error at most the prescribed tolerance.

theorem selected_tolerance (a b q : Nat) (p : Fin h → Nat)
    (hh : 0 < h) (ha : 0 < a) (hb : 0 < b) (hq : 0 < q)
    (s : Finset (Fin h)) :
    |((∑ i ∈ s, count (denominator h a b) q p i : Nat) : ℚ) /
          denominator h a b - ((∑ i ∈ s, p i : Nat) : ℚ) / q| ≤
      (a : ℚ) / b :=
…

Mentions: OAI.UniqueGamesTheorem.Explicit.Rounding.count, OAI.UniqueGamesTheorem.Explicit.Rounding.denominator

theorem OAI.UniqueGamesTheorem.Explicit.Rounding.selected_weight_error line 265

Source documentation

Satisfaction-predicate form, with individually normalized rational weights.

theorem selected_weight_error (Q q : Nat) (p : Fin h → Nat)
    (hQ : 0 < Q) (hq : 0 < q) (keep : Fin h → Bool) :
    |(∑ i, if keep i then (count Q q p i : ℚ) / Q else 0) -
      (∑ i, if keep i then (p i : ℚ) / q else 0)| ≤ (h : ℚ) / Q := by
…

Mentions: OAI.UniqueGamesTheorem.Explicit.Rounding.count

theorem OAI.UniqueGamesTheorem.Explicit.Rounding.selected_weight_tolerance line 272
def OAI.UniqueGamesTheorem.Explicit.Rounding.copies line 281
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.copies_length line 284
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.copies_nonempty line 288
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.copies_filter_length line 296
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.count_le line 303
Source documentation
An individual multiplicity is bounded by the chosen output size.
```
theorem count_le (Q q : Nat) (p : Fin h → Nat) (hq : 0 < q)
    (hmass : ∑ i, p i = q) (i : Fin h) : count Q q p i ≤ Q := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.Rounding.count
structure OAI.UniqueGamesTheorem.Explicit.RationalWeights line 317
Source documentation
Normalized rational occurrence weights; zero weights are also permitted.
```
structure RationalWeights (h : Nat) where
…
```
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.length_positive line 326
def OAI.UniqueGamesTheorem.Explicit.RationalWeights.denominator line 334
Source documentation
An executable exact common denominator, not the number of output copies.
```
def denominator : Nat := ∏ i, (w.weight i).den
```
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.denominator_positive line 336
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.den_dvd_denominator line 340
def OAI.UniqueGamesTheorem.Explicit.RationalWeights.numerator line 343
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.numerator_cast line 346
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.weight_eq_ratio line 364
Source documentation
Every original weight is represented exactly.
```
theorem weight_eq_ratio (i : Fin h) :
    w.weight i = (w.numerator i : ℚ) / w.denominator := by
…
```
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.sum_numerator line 370
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.numerator_positive line 376
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.positive_ratio line 385
Source documentation
Exact positive-rational numerator conversion used for the tolerance.
```
theorem positive_ratio (τ : ℚ) (hτ : 0 < τ) :
    (τ.num.toNat : ℚ) / τ.den = τ := by
…
```
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.positive_numerator line 392
def OAI.UniqueGamesTheorem.Explicit.RationalWeights.outputSize line 395
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.outputSize_positive line 398
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.outputSize_eq_ceil line 402
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.outputSize_le line 407
def OAI.UniqueGamesTheorem.Explicit.RationalWeights.multiplicity line 411
Source documentation
Largest-remainder multiplicities computed from the exact input weights.
```
def multiplicity (τ : ℚ) (i : Fin h) : Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.sum_multiplicity line 414
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.multiplicity_weight_error line 417

theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.selected_weight_error line 425

Source documentation

Error for every labeling's satisfaction predicate on the original IDs.

theorem selected_weight_error (τ : ℚ) (hτ : 0 < τ) (keep : Fin h → Bool) :
    |(∑ i, if keep i then (w.multiplicity τ i : ℚ) / w.outputSize τ else 0) -
      (∑ i, if keep i then w.weight i else 0)| ≤ τ := by
…

def OAI.UniqueGamesTheorem.Explicit.RationalWeights.copies line 435
Source documentation
List of output IDs, preserving different occurrences with equal records.
```
def copies (τ : ℚ) : List (Fin h) :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.copies_length line 438
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.copies_nonempty line 441
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.copies_filter_length line 445
theorem OAI.UniqueGamesTheorem.Explicit.RationalWeights.copies_weight_error line 449
def OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.weightedScore line 469
def OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.weightedValue line 474
theorem OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.weightedScore_le_weightedValue line 478
theorem OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.weightedValue_attained line 483
theorem OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.weightedValue_error line 492
Source documentation
A uniform per-labeling error controls both maxima, without identifying their optimizing labelings.
```
theorem weightedValue_error (g : OccurrenceGame V E A) (w w' : E → ℝ) (τ : ℝ)
    (h : ∀ a, |g.weightedScore w' a - g.weightedScore w a| ≤ τ) :
    |g.weightedValue w' - g.weightedValue w| ≤ τ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.OccurrenceGame
theorem OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.weightedScore_uniform line 506
theorem OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.weightedValue_uniform line 516
def OAI.UniqueGamesTheorem.Explicit.Rounding.copied line 535
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.copied_isTranslation line 541
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.copied_card line 546
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.copied_satisfiedCount line 550
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.copied_value line 561
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.rounded_value_error line 578
Source documentation
The actual copied occurrence game's maximum differs from the input weighted maximum by at most h/Q.
```
theorem rounded_value_error (g : OccurrenceGame V (Fin h) A)
    (Q q : Nat) (p : Fin h → Nat) (hQ : 0 < Q) (hq : 0 < q)
    (hmass : ∑ i, p i = q) :
    |(copied g (count Q q p)).value -
      g.weightedValue (fun e => (p e : ℝ) / q)| ≤ (h : ℝ) / Q := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.OccurrenceGame, OAI.UniqueGamesTheorem.Explicit.Rounding.copied, OAI.UniqueGamesTheorem.Explicit.Rounding.count
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.rounded_value_tolerance line 597
theorem OAI.UniqueGamesTheorem.Explicit.Rounding.rounded_subdivision_value line 609
Source documentation
The rounding/subdivision error, for the constructed simple bipartite game.
```
theorem rounded_subdivision_value (g : OccurrenceGame V (Fin h) A)
    (a b q : Nat) (p : Fin h → Nat) (hh : 0 < h)
    (ha : 0 < a) (hb : 0 < b) (hq : 0 < q) (hmass : ∑ i, p i = q) :
    |(Subdivision.game (copied g (count (denominator h a b) q p))).value -
      (1 - (1 - g.weightedValue (fun e => (p e : ℝ) / q)) / 4)| ≤
      ((a : ℝ) / b) / 4 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.OccurrenceGame, OAI.UniqueGamesTheorem.Explicit.Subdivision.game, OAI.UniqueGamesTheorem.Explicit.Rounding.copied, OAI.UniqueGamesTheorem.Explicit.Rounding.count, OAI.UniqueGamesTheorem.Explicit.Rounding.denominator