AnalyticCheeger.lean`

29 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.MaxCutGames.Repetition.Analytic.quadraticMass line 21
def OAI.MaxCutGames.Repetition.Analytic.gatedCorrelation line 24
def OAI.MaxCutGames.Repetition.Analytic.gatedMinimum line 27
def OAI.MaxCutGames.Repetition.Analytic.gatedMaximum line 30
theorem OAI.MaxCutGames.Repetition.Analytic.quadraticMass_nonnegative line 33
theorem OAI.MaxCutGames.Repetition.Analytic.gatedCorrelation_nonnegative line 40
theorem OAI.MaxCutGames.Repetition.Analytic.gatedCorrelation_le_mass line 49
theorem OAI.MaxCutGames.Repetition.Analytic.gatedMinimum_nonnegative line 60
theorem OAI.MaxCutGames.Repetition.Analytic.gatedMinimum_le_mass line 68
theorem OAI.MaxCutGames.Repetition.Analytic.gatedMinimum_add_maximum_le line 81
theorem OAI.MaxCutGames.Repetition.Analytic.gatedCorrelation_sq_le_min_mul_max line 99
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.MaxCutGames.Repetition.Analytic.gatedCorrelation, OAI.MaxCutGames.Repetition.Analytic.gatedMinimum, OAI.MaxCutGames.Repetition.Analytic.gatedMaximum
theorem OAI.MaxCutGames.Repetition.Analytic.gatedCorrelation_sq_le_min_quadratic line 122
theorem OAI.MaxCutGames.Repetition.Analytic.gatedMinimum_cheeger line 134
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.MaxCutGames.Repetition.Analytic.quadraticMass, OAI.MaxCutGames.Repetition.Analytic.gatedCorrelation, OAI.MaxCutGames.Repetition.Analytic.gatedMinimum
theorem OAI.MaxCutGames.Repetition.Analytic.gatedMinimum_near_one line 148
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.MaxCutGames.Repetition.Analytic.quadraticMass, OAI.MaxCutGames.Repetition.Analytic.gatedCorrelation, OAI.MaxCutGames.Repetition.Analytic.gatedMinimum
theorem OAI.MaxCutGames.Repetition.Analytic.gatedMinimum_unit_mass line 169
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.MaxCutGames.Repetition.Analytic.quadraticMass, OAI.MaxCutGames.Repetition.Analytic.gatedCorrelation, OAI.MaxCutGames.Repetition.Analytic.gatedMinimum
def OAI.MaxCutGames.Repetition.rowSquareMass line 197
def OAI.MaxCutGames.Repetition.paddedAmplitude line 199
def OAI.MaxCutGames.Repetition.paddedLabel line 203
theorem OAI.MaxCutGames.Repetition.paddedAmplitude_nonnegative line 208
theorem OAI.MaxCutGames.Repetition.paddedAmplitude_row line 219
def OAI.MaxCutGames.Repetition.pairEnergy line 230
def OAI.MaxCutGames.Repetition.pairOverlap line 236
theorem OAI.MaxCutGames.Repetition.pairEnergy_nonnegative line 243
theorem OAI.MaxCutGames.Repetition.pairEnergy_le_padded line 255
theorem OAI.MaxCutGames.Repetition.pairQuadraticMass_eq_one line 293
theorem OAI.MaxCutGames.Repetition.pairGatedCorrelation_eq_energy line 315
theorem OAI.MaxCutGames.Repetition.pairGatedMinimum_eq_overlap line 325
theorem OAI.MaxCutGames.Repetition.pairEnergy_le_one_of_unit_rows line 335

theorem OAI.MaxCutGames.Repetition.pairOverlap_ge_energy line 348

Source documentation

The overlap used by finite threshold sampling is large whenever the actual weighted occurrence energy is large.

theorem pairOverlap_ge_energy (ν : FiniteDistribution E) (left right : E → V)
    (R : E → A → A → Bool) (a : V → Ω → A) (f : V → Ω → ℝ)
    (hf : ∀ v ω, 0 ≤ f v ω) (hrow : ∀ v, rowSquareMass f v = 1) :
    1 - Real.sqrt (2 * (1 - pairEnergy ν left right R a f)) ≤
      pairOverlap ν left right R a f := by
…

Mentions: OAI.MaxCutGames.Repetition.rowSquareMass, OAI.MaxCutGames.Repetition.pairEnergy, OAI.MaxCutGames.Repetition.pairOverlap