MaxLeafFormal.RSCTreeModel

Source file MaxLeafFormal/RSCTreeModel.lean of the Lean project (how it is built).

Statements of the paper formalised here: Lemma D.5.20, Lemma D.5.2, Lemma D.5.18, Lemma D.5.8, Lemma D.5.12.

import MaxLeafFormal.RSC.TreeCore
import MaxLeafFormal.RSC.Bridge
import MaxLeafFormal.RSC.RelaxedLe
import MaxLeafFormal.RSC.Odds
import MaxLeafFormal.RSC.JLemma

/-!
# The tree model and the relaxed recursion

The weights `wt`, `W^tm`, `Pr_tm`, `E_tm` of `def:rsc-tm` on any finite tree with labels
`(ν_v, c_{v,2}, c_{v,3})`; `lem:rsc-recursion`, `lem:rsc-odds`, `eq:rsc-odds1`, the probabilistic
cores of `lem:rsc-credit` and `lem:rsc-jlemma`, the bridge to `RTree`, and `lem:rsc-relaxed`.
-/

namespace MaxLeafFormal.RSCTree
open Finset
open MaxLeafFormal.Antinorm8 (RTree size fin)
open MaxLeafFormal.RSCCert (Label nuSum Admissible Light₂ Light₃ eps delta₂ delta₃ rho₁)
open MaxLeafFormal.RSCRec
open MaxLeafFormal.Antinorm3 (children D)
open MaxLeafFormal.CDS (par comp)

noncomputable section
open Classical

variable {Vt : Type*} [Fintype Vt] [DecidableEq Vt]

/-- The monotone coupling. -/
theorem monotone_coupling {α : Type*} [DecidableEq α] (C : Finset α) (f : Finset α → ℝ)
    (hf0 : ∀ Υ ⊆ C, 0 ≤ f Υ) (hf : ∀ Υ Υ', Υ ⊆ Υ' → Υ' ⊆ C → f Υ ≤ f Υ')
    (p p' : α → ℝ) (hp : ∀ v ∈ C, 0 ≤ p v ∧ p v ≤ p' v ∧ p' v ≤ 1) :
    ∑ Υ ∈ C.powerset, prodMeas p C Υ * f Υ ≤ ∑ Υ ∈ C.powerset, prodMeas p' C Υ * f Υ :=
  monotone_coupling_core C f hf0 hf p p' hp

/-- `W^tm > 0`. -/
theorem Wtm_pos (P : Par) (hp : 0 ≤ P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ ≤ 1) (hy : 0 ≤ P.y)
    (hϖ : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃) (F : SimpleGraph Vt) (lab : Vt → Label) : 0 < Wtm P F lab :=
  Wtm_pos_core P hp hy hϖ F lab

/-- `lem:rsc-recursion`, any root `r`, any child order, any forcing `f`. -/
theorem rsc_recursion (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1) (hy : 0 ≤ P.y)
    (hϖ : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃) {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt)
    (ord : Vt → List Vt) (hord : IsChildOrder hF r ord) (lab : Vt → Label)
    (f : Vt → Option Force) :
    let M := message10 P (toRTree hF r ord (fun v => (lab v, f v)) r)
    (∀ v, 0 ≤ message10 P (toRTree hF r ord (fun v => (lab v, f v)) v)) ∧
    M 0 = wsum P F lab (fun X' Υ => Respects f X' Υ ∧ r ∈ X') ∧
    M 3 + lam P * M 4 = wsum P F lab (fun X' Υ => Respects f X' Υ ∧ r ∈ Υ) ∧
    M 5 / 2 + M 6 + M 7 + (1 - P.p₂) * M 8 + (1 - P.p₃) * M 9
      = wsum P F lab (fun X' Υ => Respects f X' Υ ∧ r ∉ X' ∪ Υ) :=
  recursion_core P hp hy hϖ hF r ord hord lab f

/-- "In particular" of `lem:rsc-recursion`. -/
theorem rsc_recursion_fin (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1) (hy : 0 ≤ P.y)
    (hϖ : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃) {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt)
    (ord : Vt → List Vt) (hord : IsChildOrder hF r ord) (lab : Vt → Label)
    (f : Vt → Option Force) :
    fin10 P (message10 P (toRTree hF r ord (fun v => (lab v, f v)) r))
        = wsum P F lab (fun X' Υ => Respects f X' Υ) ∧
    ((∀ v, f v = none) →
      fin10 P (message10 P (toRTree hF r ord (fun v => (lab v, f v)) r)) = Wtm P F lab) :=
  recursion_fin_core P hp hy hϖ hF r ord hord lab f

/-- `lem:rsc-odds`. -/
theorem rsc_odds (P : Par) (hP : P.Standing) {F : SimpleGraph Vt} (hF : F.IsTree)
    (lab : Vt → Label) (hc : ∀ v, (lab v).2.1 + (lab v).2.2 ≤ (lab v).1)
    (U : Finset Vt) (w : Vt) (hw : w ∉ U) (hU : (U.filter (F.Adj w)).card ≤ 1) :
    P.y / 2 * (1 - P.p₃) ^ (U.filter (F.Adj w)).card
        * Ptm P F lab (fun X' Υ => Disjoint U (X' ∪ Υ) ∧ w ∉ X' ∪ Υ)
      ≤ Ptm P F lab (fun X' Υ => Disjoint U (X' ∪ Υ) ∧ w ∈ X') :=
  odds_core P hP hF lab hc U w hw hU

/-- `eq:rsc-odds1`. -/
theorem odds1 (P : Par) (hP : P.Standing) {F : SimpleGraph Vt} (hF : F.IsTree)
    (lab : Vt → Label) (hc : ∀ v, (lab v).2.1 + (lab v).2.2 ≤ (lab v).1) (o w : Vt) (hwo : w ≠ o) :
    Pcond P F lab (fun X' Υ => w ∉ X' ∪ Υ) (fun X' Υ => o ∉ X' ∪ Υ) ≤ rho₁ P.p₃ P.y :=
  odds1_core P hP hF lab hc o w hwo

/-- The probabilistic core of `lem:rsc-credit`, for any set `N` not containing `o`. -/
theorem credit_tree (P : Par) (hP : P.Standing) {F : SimpleGraph Vt} (hF : F.IsTree)
    (lab : Vt → Label) (hc : ∀ v, (lab v).2.1 + (lab v).2.2 ≤ (lab v).1)
    (o : Vt) (N : Finset Vt) (ho : o ∉ N) :
    (N.Nonempty → 1 - rho₁ P.p₃ P.y
        ≤ Pcond P F lab (fun X' Υ => (N ∩ (X' ∪ Υ)).Nonempty) (fun X' Υ => o ∉ X' ∪ Υ)) ∧
    (2 ≤ N.card → 1 - rho₁ P.p₃ P.y ^ 2
        ≤ Pcond P F lab (fun X' Υ => (N ∩ (X' ∪ Υ)).Nonempty) (fun X' Υ => o ∉ X' ∪ Υ)) :=
  credit_tree_core P hP hF lab hc o N ho

/-- The probabilistic core of `lem:rsc-jlemma`, for any `N ∌ o` with at most one
`F`-neighbour of `o`. -/
theorem jlemma_tree (P : Par) (hP : P.Standing) {F : SimpleGraph Vt} (hF : F.IsTree)
    (lab : Vt → Label) (hc : ∀ v, (lab v).2.1 + (lab v).2.2 ≤ (lab v).1)
    (o : Vt) (N : Finset Vt) (ho : o ∉ N) (hN : (N.filter (F.Adj o)).card ≤ 1) :
    (Light₃ P.p₂ P.p₃ P.y (lab o).1 (F.degree o) →
      eps P.p₃ * Ptm P F lab (fun X' Υ => (N ∩ X').Nonempty ∧ o ∈ X' ∪ Υ)
        ≤ delta₃ P.p₃ * Ptm P F lab (fun X' Υ => (N ∩ X').Nonempty ∧ o ∉ X' ∪ Υ)) ∧
    (Light₂ P.p₂ P.p₃ P.y (lab o).1 (F.degree o) →
      eps P.p₂ * Ptm P F lab (fun X' _Υ => (N ∩ X').Nonempty ∧ o ∈ X')
        ≤ delta₂ * Ptm P F lab (fun X' Υ => (N ∩ X').Nonempty ∧ o ∉ X' ∪ Υ)) :=
  jlemma_tree_core P hP hF lab hc o N ho hN

/-- The inequality of `lem:rsc-relaxed`. -/
theorem relaxed_le (P : Par) (hP : P.Standing) {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt)
    (lab : Vt → Label) (hc : ∀ v, (lab v).2.1 + (lab v).2.2 ≤ (lab v).1) :
    Wrel P hF r lab ≤ Wtm P F lab :=
  relaxed_le_core P hP hF r lab hc

/-- `lem:rsc-relaxed`, any root, any child order; `RSCCert.message` is s1's `M̃`. -/
theorem rsc_relaxed (P : Par) (hP : P.Standing) {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt)
    (ord : Vt → List Vt) (hord : IsChildOrder hF r ord) (lab : Vt → Label)
    (hc : ∀ v, (lab v).2.1 + (lab v).2.2 ≤ (lab v).1) :
    Wrel P hF r lab ≤ Wtm P F lab ∧
    Wrel P hF r lab
      = fin P.p₂ (RSCCert.message P.p₂ P.p₃ P.y P.ϖ₂ P.ϖ₃ (toRTree hF r ord lab r)) :=
  ⟨relaxed_le P hP hF r lab hc, relaxed_eq_core P hP hF r ord hord lab hc⟩

/-- Bridge to s1. -/
theorem isChildOrder_toList {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt) :
    IsChildOrder hF r (fun v => (children hF r v).toList) :=
  isChildOrder_toList_core hF r

theorem size_toRTree {α : Type} {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt)
    (ord : Vt → List Vt) (hord : IsChildOrder hF r ord) (lab : Vt → α) :
    size (toRTree hF r ord lab r) = Fintype.card Vt :=
  size_toRTree_core hF r ord hord lab

theorem nuSum_toRTree {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt)
    (ord : Vt → List Vt) (hord : IsChildOrder hF r ord) (lab : Vt → Label) :
    nuSum (toRTree hF r ord lab r) = ∑ v, (lab v).1 :=
  nuSum_toRTree_core hF r ord hord lab

theorem admissible_toRTree (P : Par) {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt)
    (ord : Vt → List Vt) (hord : IsChildOrder hF r ord) (lab : Vt → Label)
    (h : AdmissibleG P F lab) : Admissible P.p₂ P.p₃ P.y (toRTree hF r ord lab r) :=
  admissible_toRTree_core P hF r ord hord lab h

end
end MaxLeafFormal.RSCTree