DyadicErrors.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The final passage from positive dyadic error tolerances to arbitrary real error tolerances, with exact finite numerator/denominator encodings.

def OAI.MaxCutGames.Integration.DyadicErrors.dyadicError line 15
Source documentation
The index starts at denominator four, so every encoded error is below one half.
```
def dyadicError (n : Nat) : RationalError where
…
```
theorem OAI.MaxCutGames.Integration.DyadicErrors.errorValue_dyadic line 25
theorem OAI.MaxCutGames.Integration.DyadicErrors.exists_dyadic_below_real line 30
Source documentation
Positive dyadic errors are cofinal among all positive real tolerances.
```
theorem exists_dyadic_below_real {ε : ℝ} (hε : 0 < ε) :
    ∃ n : Nat, (errorValue (dyadicError n) : ℝ) < ε := by
…
```
Mentions: OAI.MaxCutGames.Integration.DyadicErrors.dyadicError
theorem OAI.MaxCutGames.Integration.DyadicErrors.exists_dyadic_below line 42

theorem OAI.MaxCutGames.Integration.DyadicErrors.completeAt_real_of_dyadic line 49

Source documentation

A proved dyadic completeness gap gives the claimed real tolerance.

theorem completeAt_real_of_dyadic {q n : Nat} {ε : ℝ} {g : Instance q}
    (hε : (errorValue (dyadicError n) : ℝ) ≤ ε)
    (hg : CompleteAt (dyadicError n) g) :
    ∃ labeling, 1 - ε ≤
      (countSatisfied labeling g.constraints : ℝ) / g.constraints.length := by
…

Mentions: OAI.MaxCutGames.Integration.DyadicErrors.dyadicError

theorem OAI.MaxCutGames.Integration.DyadicErrors.soundAt_real_of_dyadic line 57