FiniteGraphTransfer.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite Graph Transfer

def OAI.HadwigerCounterexample.badS line 18
Source documentation
k distinct samples in S (unordered).
```
private def badS (S : A → Prop) (k : ℕ) (x : V → A) :=
…
```
theorem OAI.HadwigerCounterexample.badS_pr line 21
def OAI.HadwigerCounterexample.badE line 45
Source documentation
k pair exceptions using disjoint sample positions (ordered pairs).
```
private def badE (E : A × A → Prop) (k : ℕ) (x : V → A) :=
…
```
theorem OAI.HadwigerCounterexample.badE_pr line 49
theorem OAI.HadwigerCounterexample.many_bad line 74

theorem OAI.HadwigerCounterexample.transfer line 125

Source documentation

Finite transfer with an explicit error term. If T denotes the terminal count bound, it suffices that T*(2^m*(2/M)^k + m^(2*k)*(1/D)^k) < 1. The rate version just instantiates these inequalities.

theorem transfer [Fintype A] [Nonempty A] (H : Holes A) {μ : Wgt A} (hμ : IsLaw μ)
    {M D ε : ℝ} (hM : 0 < M) (hD : 0 < D) (hε : 0 < ε)
    (hsat : ∀ w : Wgt (A × A), IsLaw w → pairCaps μ M D w → carried w H.unit →
      ε ≤ pr (pairW w w) (fun x => H.conflict x.1 x.2))
    {L m k : ℕ} (hL : Real.log (Fintype.card (A × A)) < L * (ε * Real.log 2))
    (hk : 200*k < m+200)
    (herr :
      ((Fintype.card (A × A) : ℝ) + 1)^L *
        (2^m * (2/M)^k + (m:ℝ)^(k+k) * D⁻¹^k) < 1) :
    ∃ x : Fin m → A,
      (H.graph x).indepNum ≤ 2 ∧
      (connectedMatchingNumber (H.graph x) : ℚ) < (m : ℚ)/100 := by
…

Mentions: OAI.HadwigerCounterexample.Holes, OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.IsLaw, OAI.HadwigerCounterexample.pairCaps, OAI.HadwigerCounterexample.carried, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.pairW