RepetitionUpper.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MaxCutGames.Soundness.RepetitionUpper.bernoulliAverage line 10
Source documentation
Expectation of f evaluated at the number of successes in n independent Bernoulli trials. The recursion itself specifies the product distribution.
```
def bernoulliAverage (p : Rat) : Nat → (Nat → Rat) → Rat
  | 0, f => f 0
  | n + 1, f =>
      (1 - p) * bernoulliAverage p n f +
        p * bernoulliAverage p n (fun k => f (k + 1))
```
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.bernoulliAverage_scale line 16
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.bernoulliAverage_geometric line 25
Source documentation
The exact binomial generating-function identity used in (6.25).
```
theorem bernoulliAverage_geometric (p a : Rat) (n : Nat) :
    bernoulliAverage p n (fun k => a ^ k) = (1 - p * (1 - a)) ^ n := by
…
```
Mentions: OAI.MaxCutGames.Soundness.RepetitionUpper.bernoulliAverage
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.bernoulliAverage_mono line 37

theorem OAI.MaxCutGames.Soundness.RepetitionUpper.success_le_geometric line 54

Source documentation

The repeated-game bound is the explicitly supplied premise conditional. The premise averaged is the separate law-of-total-probability obligation.

theorem success_le_geometric
    (p a success : Rat) (n : Nat) (conditionalSuccess : Nat → Rat)
    (hp : 0 ≤ p) (hp' : p ≤ 1)
    (conditional : ∀ k, conditionalSuccess k ≤ a ^ k)
    (averaged : success ≤ bernoulliAverage p n conditionalSuccess) :
    success ≤ (1 - p * (1 - a)) ^ n := by
…

Mentions: OAI.MaxCutGames.Soundness.RepetitionUpper.bernoulliAverage

theorem OAI.MaxCutGames.Soundness.RepetitionUpper.pow_mono_nonneg line 65
def OAI.MaxCutGames.Soundness.RepetitionUpper.zeroProbability line 79
Source documentation
A uniformly sampled vector in a d-dimensional binary space is zero with probability 2^(-d). The counting justification is a separate obligation.
```
def zeroProbability (d : Nat) : Rat := (1 / 2 : Rat) ^ d
```
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.zeroProbability_nonneg line 81
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.zeroProbability_le_one line 84
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.zeroProbability_antitone line 92
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.geometric_le_dimension_bound line 112
Source documentation
The last inequality in (6.25), including the sign obligations.
```
theorem geometric_le_dimension_bound (d L n : Nat) (hd : d ≤ L)
    (a : Rat) (ha : 0 ≤ a) (ha' : a ≤ 1) :
    (1 - zeroProbability d * (1 - a)) ^ n ≤
      (1 - zeroProbability L * (1 - a)) ^ n := by
…
```
Mentions: OAI.MaxCutGames.Soundness.RepetitionUpper.zeroProbability
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.projection_upper_bound line 129
Source documentation
Lemma 6.8's numerical conclusion, conditional on the repeated-game and averaging premises. In particular these hypotheses must be proved for the same augmented strategy, including its fixed advice.
```
theorem projection_upper_bound
    (d L n : Nat) (hd : d ≤ L) (a success : Rat)
    (ha : 0 ≤ a) (ha' : a ≤ 1) (conditionalSuccess : Nat → Rat)
    (conditional : ∀ k, conditionalSuccess k ≤ a ^ k)
    (averaged : success ≤ bernoulliAverage (zeroProbability d) n conditionalSuccess) :
    success ≤ (1 - zeroProbability L * (1 - a)) ^ n := by
…
```
Mentions: OAI.MaxCutGames.Soundness.RepetitionUpper.bernoulliAverage, OAI.MaxCutGames.Soundness.RepetitionUpper.zeroProbability
def OAI.MaxCutGames.Soundness.RepetitionUpper.decoderThreshold line 140
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.decoderThreshold_pos line 142
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.exists_pos_nat_gt line 152
Source documentation
An elementary Archimedean bound for rational parameters.
```
theorem exists_pos_nat_gt (x : Rat) : ∃ n : Nat, 0 < n ∧ x < (n : Rat) := by
…
```
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.power_mul_growth_le_one line 162
Source documentation
The estimate b^n ≤ 1 / (1+n(1-b)) without division.
```
theorem power_mul_growth_le_one (b : Rat) (hb : 0 ≤ b) (hb' : b ≤ 1)
    (n : Nat) : b ^ n * (1 + (n : Rat) * (1 - b)) ≤ 1 := by
…
```
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.exists_power_lt line 180
Source documentation
Positive powers of a rational base below one eventually fall below every positive rational threshold; this supplies the search target in (4.4).
```
theorem exists_power_lt (b threshold : Rat) (hb : 0 ≤ b) (hb' : b < 1)
    (ht : 0 < threshold) : ∃ n : Nat, 0 < n ∧ b ^ n < threshold := by
…
```
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.zeroProbability_pos line 197
theorem OAI.MaxCutGames.Soundness.RepetitionUpper.exists_repetition_length line 200

theorem OAI.MaxCutGames.Soundness.RepetitionUpper.soundness_of_bounds line 217

Source documentation

Proposition 6.9's contradiction, with its dependency boundary visible. extraction is the entire lower-bound implication; upper must bound every strategy of the same type, with all allowed advice; gap is (4.4).

theorem soundness_of_bounds
    {Labeling Strategy : Type} (acceptance : Labeling → Rat)
    (success : Strategy → Rat) (delta lower upperBound : Rat)
    (extraction : ∀ labeling, delta < acceptance labeling →
      ∃ strategy, lower ≤ success strategy)
    (upper : ∀ strategy, success strategy ≤ upperBound)
    (gap : upperBound < lower) :
    ∀ labeling, acceptance labeling ≤ delta := by
…

theorem OAI.MaxCutGames.Soundness.RepetitionUpper.soundness_from_repetition line 235

Source documentation

Proposition 6.9 specialized to (6.25) and (4.4). Every occurrence of strategy is the same object, so fixed advice cannot silently change between the lower and upper bounds.

theorem soundness_from_repetition
    {Labeling Strategy : Type} (acceptance : Labeling → Rat)
    (success : Strategy → Rat) (dimension : Strategy → Nat)
    (conditionalSuccess : Strategy → Nat → Rat)
    (delta a theta : Rat) (q L t : Nat) (ha : 0 ≤ a) (ha' : a ≤ 1)
    (dimension_le : ∀ strategy, dimension strategy ≤ L)
    (conditional : ∀ strategy k, conditionalSuccess strategy k ≤ a ^ k)
    (averaged : ∀ strategy, success strategy ≤
      bernoulliAverage (zeroProbability (dimension strategy)) t
        (conditionalSuccess strategy))
    (extraction : ∀ labeling, delta < acceptance labeling →
      ∃ strategy, decoderThreshold theta q ≤ success strategy)
…

Mentions: OAI.MaxCutGames.Soundness.RepetitionUpper.bernoulliAverage, OAI.MaxCutGames.Soundness.RepetitionUpper.zeroProbability, OAI.MaxCutGames.Soundness.RepetitionUpper.decoderThreshold