Parameters.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MaxCutGames.Integration.SourceParameters.rate line 9
theorem OAI.MaxCutGames.Integration.SourceParameters.rate_bounds line 11
theorem OAI.MaxCutGames.Integration.SourceParameters.fourth_power_comparison line 17
theorem OAI.MaxCutGames.Integration.SourceParameters.four_bit_rate_comparison line 36
Source documentation
The answer alphabet product is 16, so its binary logarithm is four. This converts the genuine repetition theorem's real exponent to a rational base raised to the integral repetition length.
```
theorem four_bit_rate_comparison {gap : ℚ}
    (hgap : 0 < gap) (hgap1 : gap ≤ 1) (n : Nat) :
    (1 - (gap : ℝ) ^ 3 / 6000) ^ ((n : ℝ) / 4) ≤ (rate gap : ℝ) ^ n := by
…
```
Mentions: OAI.MaxCutGames.Integration.SourceParameters.rate
theorem OAI.MaxCutGames.Integration.SourceParameters.logTwo_sixteen line 51

theorem OAI.MaxCutGames.Integration.SourceParameters.game_repetition_rate line 59

Source documentation

The actual finite game's repetition rate, with its answer cardinality checked as an ordinary finite count. No repetition estimate is assumed.

theorem game_repetition_rate {Q₁ Q₂ A₁ A₂ : Type*}
    [Fintype Q₁] [Fintype Q₂] [Fintype A₁] [Fintype A₂]
    [Nonempty A₁] [Nonempty A₂] [DecidableEq Q₁] [DecidableEq Q₂]
    (G : MaxCutGames.Foundations.Games.Game Q₁ Q₂ A₁ A₂)
    {gap : ℚ} (hgap : 0 < gap) (hgap1 : gap ≤ 1)
    (hcards : Fintype.card A₁ * Fintype.card A₂ = 16)
    (hvalue : G.value ≤ 1 - (gap : ℝ)) (n : Nat) :
    (G.repetition n).value ≤ (rate gap : ℝ) ^ n := by
…

Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Integration.SourceParameters.rate

def OAI.MaxCutGames.Integration.SourceParameters.sourceThreshold line 77
theorem OAI.MaxCutGames.Integration.SourceParameters.sourceThreshold_pos line 79
theorem OAI.MaxCutGames.Integration.SourceParameters.exists_repetition_length line 84
def OAI.MaxCutGames.Integration.SourceParameters.repetitionLength line 91
Source documentation
Exact rational search, independent of the input formula.
```
def repetitionLength (gap δ : ℚ) (hgap : 0 < gap) (hgap1 : gap ≤ 1)
    (hδ : 0 < δ) (D : Nat) (hD : 0 < D) : Nat :=
…
```
theorem OAI.MaxCutGames.Integration.SourceParameters.repetitionLength_spec line 95
theorem OAI.MaxCutGames.Integration.SourceParameters.repetitionLength_real_bound line 101