CouplingError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.ratio_error_bound line 16
lemma OAI.HyperbolicObstruction.StarModel.coupling_of_error line 31
Source documentation
The error statistic constructs the source coupling on the very same table. There is no independent choice of a table for different branch marginals.
```
lemma coupling_of_error (support : R → Finset F) (U I : Finset F) (hI : I ⊆ U)
    (e : F) (he : e ∉ U) (p : R → ℝ) (hp : ∀ r, p r ∈ Set.Icc (0 : ℝ) 1)
    (a₀ : A) (b₀ : Fin (k+1) ↪ A) (w : TableModel.Entry (A := A) support → Bool)
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.Entry