CompanionPhaseOracleError.lean`

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Error contributed by the actual fresh weight calls in a phase

lemma OAI.ContingencyTables.CompanionPhaseWords.average_ext_instances line 16
lemma OAI.ContingencyTables.CompanionPhaseWords.failure_of_success line 21
lemma OAI.ContingencyTables.CompanionPhaseWords.independent_pair_failure line 33
lemma OAI.ContingencyTables.CompanionPhaseWords.independent_reindex_failure line 61
def OAI.ContingencyTables.CompanionPhaseWords.accurateCalls line 83
lemma OAI.ContingencyTables.CompanionPhaseWords.accurateCall_failure line 90
lemma OAI.ContingencyTables.CompanionPhaseWords.pairedCalls_failure line 102
theorem OAI.ContingencyTables.CompanionPhaseWords.accurateCalls_failure line 121
Source documentation
The calls use independent actual finite words even for a fixed, arbitrary sequence of observed states. No sampling assumption on that sequence is required for this oracle-error estimate.
```
theorem accurateCalls_failure (A : Instance I J) (C : ℕ) (hC : 0 < C) (K j N : ℕ)
    (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C)
    (hj : j+1 ≤ rationalHeight A C) (xi : ℚ) (hx0 : 0 < xi) (hx1 : xi < 1)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
…
```
Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger
def OAI.ContingencyTables.CompanionPhaseWords.exactObservedRatio line 167
Source documentation
The exact empirical ratio written as the plain-state sum divided by its integer plain-state population.
```
def exactObservedRatio (A : Instance I J) (j N : ℕ)
    (states : Fin N → Set (Labels A×Bool)) : ℝ :=
…
```
lemma OAI.ContingencyTables.CompanionPhaseWords.indicator_list_sum_real line 172
lemma OAI.ContingencyTables.CompanionPhaseWords.exactObservedRatio_eq line 178
lemma OAI.ContingencyTables.CompanionPhaseWords.ratio_exponential_bounds line 192
lemma OAI.ContingencyTables.CompanionPhaseWords.observedTerm_bounds line 213
lemma OAI.ContingencyTables.CompanionPhaseWords.exactObservedRatio_positive line 234
theorem OAI.ContingencyTables.CompanionPhaseWords.observedRatio_bounds line 258
Source documentation
Relative errors of all fresh calls remain bounded after averaging the state ratios. The number of observations does not enlarge this deterministic multiplicative error.
```
theorem observedRatio_bounds (A : Instance I J) (C K j N : ℕ)
    (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (xi : ℚ) (hx0 : 0 ≤ xi) (hx1 : xi ≤ 1/4)
    (v : Grid (I := Fin (dimension A)) K) (states : Fin N → Set (Labels A×Bool))
…
```
theorem OAI.ContingencyTables.CompanionPhaseWords.observedRatio_log_error line 280