FinishBounds.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Scalar estimates for the last paragraph of the v2 construction. These lemmas only perform the stated rounding/subdivision/repetition arithmetic; they do not assume or assert an unproved repetition theorem or hardness result.

theorem OAI.MaxCutGames.Explicit.FinishBounds.exists_reciprocal_tolerance line 14
theorem OAI.MaxCutGames.Explicit.FinishBounds.subdivision_completeness line 33
theorem OAI.MaxCutGames.Explicit.FinishBounds.subdivision_soundness line 40

theorem OAI.MaxCutGames.Explicit.FinishBounds.final_completeness line 48

Source documentation

The full completeness loss after the coordinatewise product labeling.

theorem final_completeness (vB vG d τ ε₀ ε : ℝ) (t : Nat) (ht : 0 < t)
    (hB : 1 - (d + τ) / 4 ≤ vB)
    (hG : 1 - (t : ℝ) * (1 - vB) ≤ vG)
    (hd : d ≤ ε₀ / t) (hτ : τ ≤ ε₀ / t)
    (hε₀ : 0 ≤ ε₀) (hε : ε₀ ≤ ε) :
    1 - ε ≤ vG := by
…

structure OAI.MaxCutGames.ParameterSelection.OuterParameters line 74
theorem OAI.MaxCutGames.ParameterSelection.exists_outerParameters line 92
Source documentation
Choose the alphabet-independent exponent and both rational budgets using only the two prescribed real errors.
```
theorem exists_outerParameters (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
    Nonempty (OuterParameters ε δ) := by
…
```
Mentions: OAI.MaxCutGames.ParameterSelection.OuterParameters
def OAI.MaxCutGames.ParameterSelection.OuterParameters.pStar line 109
theorem OAI.MaxCutGames.ParameterSelection.OuterParameters.pStar_pos line 111
theorem OAI.MaxCutGames.ParameterSelection.OuterParameters.pStar_lt_one line 113
theorem OAI.MaxCutGames.ParameterSelection.OuterParameters.exists_parity_error line 116
theorem OAI.MaxCutGames.ParameterSelection.OuterParameters.matrix_error_budget line 135
Source documentation
Both matrix-test completeness losses fit the budget fixed before the alphabet, for the later chosen positive tuple length.
```
theorem matrix_error_budget (k : ℕ) (hk : 0 < k) (ξ : ℚ)
    (hξ : ξ ≤ P.epsilon0 / (2 * k * P.repetitions)) :
    (k : ℚ) * ξ + P.pStar / 2 ≤ P.epsilon0 / P.repetitions := by
…
```