AnalyticCheegerLemmas.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Finite threshold-overlap estimates used in the Dinur--Steurer argument. These statements are numerical inequalities, not parallel-repetition premises. The Boolean gate keeps the constraint predicate inside the overlap energy. Weights need not be normalized: a finite auxiliary measure is permitted.

def OAI.UniqueGamesTheorem.Repetition.Analytic.quadraticMass line 29
def OAI.UniqueGamesTheorem.Repetition.Analytic.gatedCorrelation line 32
def OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMinimum line 35
def OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMaximum line 38
theorem OAI.UniqueGamesTheorem.Repetition.Analytic.quadraticMass_nonnegative line 41
theorem OAI.UniqueGamesTheorem.Repetition.Analytic.gatedCorrelation_nonnegative line 48
theorem OAI.UniqueGamesTheorem.Repetition.Analytic.gatedCorrelation_le_mass line 57
theorem OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMinimum_nonnegative line 68
theorem OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMinimum_le_mass line 76
theorem OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMinimum_add_maximum_le line 89
theorem OAI.UniqueGamesTheorem.Repetition.Analytic.gatedCorrelation_sq_le_min_mul_max line 108
Source documentation
A gated finite Cauchy--Schwarz estimate. This is the algebraic heart of the threshold-rounding inequality, with no independence assumption.
```
theorem gatedCorrelation_sq_le_min_mul_max (w f g : ι → ℝ) (gate : ι → Bool)
    (hw : ∀ i, 0 ≤ w i) :
    gatedCorrelation w f g gate ^ 2 ≤
      gatedMinimum w f g gate * gatedMaximum w f g gate := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.Analytic.gatedCorrelation, OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMinimum, OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMaximum
theorem OAI.UniqueGamesTheorem.Repetition.Analytic.gatedCorrelation_sq_le_min_quadratic line 133
theorem OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMinimum_cheeger line 145
Source documentation
Sharp homogeneous Cheeger form. The expression under the square root is nonnegative by the preceding proved inequality.
```
theorem gatedMinimum_cheeger (w f g : ι → ℝ) (gate : ι → Bool)
    (hw : ∀ i, 0 ≤ w i) :
    quadraticMass w f g -
        Real.sqrt (quadraticMass w f g ^ 2 - gatedCorrelation w f g gate ^ 2) ≤
      gatedMinimum w f g gate := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.Analytic.quadraticMass, OAI.UniqueGamesTheorem.Repetition.Analytic.gatedCorrelation, OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMinimum
theorem OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMinimum_near_one line 159
Source documentation
The near-perfect form suffices for alphabet-independent repetition. The total squared mass may be at most one, rather than exactly one.
```
theorem gatedMinimum_near_one (w f g : ι → ℝ) (gate : ι → Bool)
    (hw : ∀ i, 0 ≤ w i) {η : ℝ} (hη : 0 ≤ η) (hη₁ : η ≤ 1)
    (hmass : quadraticMass w f g ≤ 1)
    (hcorrelation : 1 - η ≤ gatedCorrelation w f g gate) :
    1 - Real.sqrt (2 * η) ≤ gatedMinimum w f g gate := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.Analytic.quadraticMass, OAI.UniqueGamesTheorem.Repetition.Analytic.gatedCorrelation, OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMinimum
theorem OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMinimum_unit_mass line 180
Source documentation
Unit-mass form for the joint question-pair and auxiliary-coordinate law.
```
theorem gatedMinimum_unit_mass (w f g : ι → ℝ) (gate : ι → Bool)
    (hw : ∀ i, 0 ≤ w i) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i)
    (hmass : quadraticMass w f g = 1) :
    1 - Real.sqrt (2 * (1 - gatedCorrelation w f g gate)) ≤
      gatedMinimum w f g gate := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.Analytic.quadraticMass, OAI.UniqueGamesTheorem.Repetition.Analytic.gatedCorrelation, OAI.UniqueGamesTheorem.Repetition.Analytic.gatedMinimum
def OAI.UniqueGamesTheorem.Repetition.dsRate line 212
Source documentation
The scalar rate appearing in the alphabet-independent repetition estimate.
```
noncomputable def dsRate (gap : ℝ) : ℝ := 1 - gap ^ 2 / 16
```
theorem OAI.UniqueGamesTheorem.Repetition.dsRate_nonneg line 214
theorem OAI.UniqueGamesTheorem.Repetition.dsRate_lt_one line 219
theorem OAI.UniqueGamesTheorem.Repetition.exists_positive_power_lt line 225
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.UniqueGamesTheorem.Repetition.exists_dsRate_pow_le line 237
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.UniqueGamesTheorem.Repetition.dsRate
theorem OAI.UniqueGamesTheorem.Repetition.dsRate_one_div_eight_hundred line 244
theorem OAI.UniqueGamesTheorem.Repetition.dsRate_one_div_fifteen line 248
theorem OAI.UniqueGamesTheorem.Repetition.exists_final_repetition_count line 254
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.UniqueGamesTheorem.Repetition.exists_preliminary_repetition_count line 260
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
…
```