AnalyticRateLemmas.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Elementary scalar estimates used to convert a collision-norm bound into the alphabet-independent repetition rate. These statements concern real numbers; they do not assume or assert any repetition theorem for games.

theorem OAI.UniqueGamesTheorem.Repetition.dsRatio_le_one_sub_gap_sq_div_eight line 19

Source documentation

The squared DS expression loses at least one eighth of the squared gap.

theorem dsRatio_le_one_sub_gap_sq_div_eight {gap : ℝ}
    (hgap₀ : 0 ≤ gap) (hgap₁ : gap ≤ 1) :
    2 * Real.sqrt (1 - gap) / (2 - gap) ≤ 1 - gap ^ 2 / 8 := by
…

theorem OAI.UniqueGamesTheorem.Repetition.le_dsRate_of_sq_le line 36
Source documentation
Passing from a squared contraction to the designated scalar rate.
```
theorem le_dsRate_of_sq_le {gap c : ℝ}
    (hgap₀ : 0 ≤ gap) (hgap₁ : gap ≤ 1)
    (hc : c ^ 2 ≤ 1 - gap ^ 2 / 8) : c ≤ dsRate gap := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.dsRate
theorem OAI.UniqueGamesTheorem.Repetition.le_dsRate_of_sq_le_dsRatio line 46
Source documentation
A squared DS bound implies the repetition rate directly.
```
theorem le_dsRate_of_sq_le_dsRatio {gap c : ℝ}
    (hgap₀ : 0 ≤ gap) (hgap₁ : gap ≤ 1)
    (hc : c ^ 2 ≤ 2 * Real.sqrt (1 - gap) / (2 - gap)) :
    c ≤ dsRate gap :=
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.dsRate
theorem OAI.UniqueGamesTheorem.Repetition.sqrt_dsRatio_le_dsRate line 54
Source documentation
The full DS scalar expression lies below the repetition rate.
```
theorem sqrt_dsRatio_le_dsRate {gap : ℝ}
    (hgap₀ : 0 ≤ gap) (hgap₁ : gap ≤ 1) :
    Real.sqrt (2 * Real.sqrt (1 - gap) / (2 - gap)) ≤ dsRate gap := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.dsRate

theorem OAI.UniqueGamesTheorem.Repetition.gap_sq_div_eight_le_of_le_two_sqrt line 62

Source documentation

The near-one rounding estimate forces a quadratic loss in the gap.

theorem gap_sq_div_eight_le_of_le_two_sqrt {gap η : ℝ}
    (hgap₀ : 0 ≤ gap) (hη₀ : 0 ≤ η)
    (hgap : gap ≤ 2 * Real.sqrt (2 * η)) : gap ^ 2 / 8 ≤ η := by
…

theorem OAI.UniqueGamesTheorem.Repetition.sequence_le_power line 79
theorem OAI.UniqueGamesTheorem.Repetition.squared_rate_le_dsRate_sq line 91
theorem OAI.UniqueGamesTheorem.Repetition.rate_of_squared_collision_recurrence line 97
def OAI.UniqueGamesTheorem.Repetition.IsProjection line 140
Source documentation
The left answer determines at most one accepting right answer. Partial projection predicates are included, as are total projection maps.
```
def IsProjection (G : Game Q₁ Q₂ A₁ A₂) : Prop :=
…
```
theorem OAI.UniqueGamesTheorem.Repetition.IsProjection.of_accepts_iff line 144
theorem OAI.UniqueGamesTheorem.Repetition.IsProjection.repetition line 153
Source documentation
Parallel repetition preserves projection constraints, including at n = 0. There is no restriction that a repeated strategy act coordinatewise.
```
theorem IsProjection.repetition {G : Game Q₁ Q₂ A₁ A₂}
    (hG : IsProjection G) (n : Nat) : IsProjection (G.repetition n) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.IsProjection
def OAI.UniqueGamesTheorem.Repetition.ofProjection line 163
Source documentation
Total projection maps give ordinary finite classical games. Question weights may be arbitrary nonnegative real weights summing to one.
```
def ofProjection (questions : FiniteDistribution (Q₁ × Q₂))
    (project : Q₁ → Q₂ → A₁ → A₂) : Game Q₁ Q₂ A₁ A₂ := by
…
```
theorem OAI.UniqueGamesTheorem.Repetition.ofProjection_accepts_iff line 168
theorem OAI.UniqueGamesTheorem.Repetition.ofProjection_isProjection line 175
def OAI.UniqueGamesTheorem.Repetition.productQuestionEquiv line 180
Source documentation
Regroup independently sampled question pairs into the two local questions.
```
def productQuestionEquiv :
    ((Q₁ × Q₂) × (R₁ × R₂)) ≃ ((Q₁ × R₁) × (Q₂ × R₂)) where
…
```
def OAI.UniqueGamesTheorem.Repetition.product line 189
Source documentation
Independent conjunction product. Each answer may depend on the full local pair of questions; locality is inherited from Game and Strategy.
```
def product (G : Game Q₁ Q₂ A₁ A₂) (H : Game R₁ R₂ B₁ B₂) :
    Game (Q₁ × R₁) (Q₂ × R₂) (A₁ × B₁) (A₂ × B₂) where
…
```
theorem OAI.UniqueGamesTheorem.Repetition.product_question_weight line 194
theorem OAI.UniqueGamesTheorem.Repetition.product_accepts_iff line 200
theorem OAI.UniqueGamesTheorem.Repetition.IsProjection.product line 207
def OAI.UniqueGamesTheorem.Repetition.productStrategy line 214
theorem OAI.UniqueGamesTheorem.Repetition.success_productStrategy line 220
Source documentation
The independent product of two strategies has exactly multiplicative success. This gives a lower bound for the maximum, not a decay upper bound.
```
theorem success_productStrategy (G : Game Q₁ Q₂ A₁ A₂) (H : Game R₁ R₂ B₁ B₂)
    (s : Strategy Q₁ Q₂ A₁ A₂) (t : Strategy R₁ R₂ B₁ B₂) :
    (product G H).success (productStrategy s t) = G.success s * H.success t := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.product, OAI.UniqueGamesTheorem.Repetition.productStrategy
theorem OAI.UniqueGamesTheorem.Repetition.mul_value_le_product_value line 237