Parameters.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Scalar parameter selection for the v2 repetition rate.

These results concern powers of real numbers only. In particular, they do not assert a parallel-repetition theorem for games. The exponent depends only on the gap and the desired error; no alphabet or logical dimension occurs here.

def OAI.MaxCutGames.Repetition.dsRate line 17
Source documentation
The scalar rate appearing in the alphabet-independent repetition estimate.
```
noncomputable def dsRate (gap : ℝ) : ℝ := 1 - gap ^ 2 / 16
```
theorem OAI.MaxCutGames.Repetition.dsRate_nonneg line 19
theorem OAI.MaxCutGames.Repetition.dsRate_lt_one line 24
theorem OAI.MaxCutGames.Repetition.exists_positive_power_lt line 30
Source documentation
A scalar contraction admits a strictly positive exponent for every positive target error. This lemma makes no assertion about any game value.
```
theorem exists_positive_power_lt {rate error : ℝ}
    (hrate₀ : 0 ≤ rate) (hrate₁ : rate < 1) (herror : 0 < error) :
    ∃ n : ℕ, 1 ≤ n ∧ rate ^ n < error := by
…
```
theorem OAI.MaxCutGames.Repetition.exists_dsRate_pow_le line 42
Source documentation
Select the repetition count before choosing any alphabet.
```
theorem exists_dsRate_pow_le {gap error : ℝ}
    (hgap₀ : 0 < gap) (hgap₁ : gap < 1) (herror : 0 < error) :
    ∃ n : ℕ, 1 ≤ n ∧ dsRate gap ^ n ≤ error := by
…
```
Mentions: OAI.MaxCutGames.Repetition.dsRate
theorem OAI.MaxCutGames.Repetition.dsRate_one_div_eight_hundred line 49
theorem OAI.MaxCutGames.Repetition.dsRate_one_div_fifteen line 53
theorem OAI.MaxCutGames.Repetition.exists_final_repetition_count line 59
Source documentation
The final soundness exponent depends only on error, even when the later construction chooses its alphabet after this exponent.
```
theorem exists_final_repetition_count {error : ℝ} (herror : 0 < error) :
    ∃ n : ℕ, 1 ≤ n ∧ (1 - (1 : ℝ) / 10240000) ^ n ≤ error := by
…
```
theorem OAI.MaxCutGames.Repetition.exists_preliminary_repetition_count line 65
Source documentation
The preliminary constant-gap specialization of the same scalar rate.
```
theorem exists_preliminary_repetition_count {error : ℝ} (herror : 0 < error) :
    ∃ n : ℕ, 1 ≤ n ∧ (1 - (1 : ℝ) / 3600) ^ n ≤ error := by
…
```