MaxLeafFormal.RSCGraphDefs

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

import MaxLeafFormal.RSCTreeDefs
import MaxLeafFormal.CDS

/-!
# Definitions of the graph level

The definitions of `RSCGraph`, kept in their own file so that the proof files can import them.
-/

namespace MaxLeafFormal.RSCGraph
open Finset
open MaxLeafFormal.CDS (IsCDS γc termCount)
open MaxLeafFormal.Antinorm8 (RTree size fin cZ PZ initInf)
open MaxLeafFormal.RSCCert (Label nuSum Admissible Light₂ Light₃ eps delta₂ delta₃ rho₁ Credits)
open MaxLeafFormal.RSCRec (Par)
open MaxLeafFormal.RSCTree

noncomputable section
open Classical

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

/-- `|N(v) ∩ X'|` and `C(X')`. -/
def nbrCount (G : SimpleGraph V) [DecidableRel G.Adj] (X' : Finset V) (v : V) : ℕ :=
  (X'.filter (G.Adj v)).card

def cand (G : SimpleGraph V) [DecidableRel G.Adj] (X' : Finset V) : Finset V :=
  univ.filter (fun v => v ∉ X' ∧ 2 ≤ nbrCount G X' v)

/-- `W^cl_S(y)` (def:rsc-gf), the expectation over `Υ` as a finite sum. -/
def Wcl (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (p₂ p₃ y : ℝ) : ℝ :=
  ∑ X' ∈ S.powerset, y ^ X'.card *
    ∑ Υ ∈ (cand G X').powerset,
      prodMeas (fun v => pk p₂ p₃ (nbrCount G X' v)) (cand G X') Υ *
        (if Υ ⊆ S then 1 else 0) * (1/2 : ℝ) ^ termCount G (X' ∪ Υ)

/-- Outside vertices `O = V \ S`. -/
abbrev Out (S : Finset V) := {v : V // v ∉ S}

def NS (G : SimpleGraph V) (S : Finset V) (u : Out S) : Finset S :=
  univ.filter (fun v => G.Adj u.1 v.1)

def Private (G : SimpleGraph V) (S : Finset V) (u : Out S) : Prop := (NS G S u).card = 1

def Shared (G : SimpleGraph V) (S : Finset V) (u : Out S) : Prop := 2 ≤ (NS G S u).card

def typ (G : SimpleGraph V) (S : Finset V) (u : Out S) : ℕ := if (NS G S u).card = 2 then 2 else 3

def ind (b : Prop) : ℝ := if b then 1 else 0

/-- `h_u(X', X)`, `h̄_u(X)`, `N'_u`. -/
def hfac (p₂ p₃ : ℝ) (G : SimpleGraph V) (S : Finset V) (u : Out S) (X' X : Finset S) : ℝ :=
  (1/2 : ℝ) ^ (if Disjoint (NS G S u) X then 1 else 0) *
    (1 - pk p₂ p₃ (NS G S u ∩ X').card) ^ (if 2 ≤ (NS G S u ∩ X').card then 1 else 0)

def hbar {S : Finset V} (o : Out S → S) (u : Out S) (X : Finset S) : ℝ :=
  (1/2 : ℝ) ^ (if o u ∈ X then 0 else 1)

def Nprime (G : SimpleGraph V) (S : Finset V) (o : Out S → S) (u : Out S) : Finset S :=
  (NS G S u).erase (o u)

def qT (p₂ p₃ : ℝ) (τ : ℕ) : ℝ := if τ = 2 then 1 - p₂ else 1 - p₃

def deltaT (p₃ : ℝ) (τ : ℕ) : ℝ := if τ = 2 then delta₂ else delta₃ p₃

def ϖT (P : Par) (τ : ℕ) : ℝ := if τ = 2 then P.ϖ₂ else P.ϖ₃

def LightT (P : Par) (τ ν d : ℕ) : Prop :=
  if τ = 2 then Light₂ P.p₂ P.p₃ P.y ν d else Light₃ P.p₂ P.p₃ P.y ν d

/-- `ν_v`, `c_{v,τ}`, the labels, and `O^co` (def:rsc-owner, def:rsc-tm). -/
def nuOf {S : Finset V} (o : Out S → S) (v : S) : ℕ := (univ.filter (fun u => o u = v)).card

def cOf (G : SimpleGraph V) (S : Finset V) (o : Out S → S) (Oex : Finset (Out S)) (τ : ℕ)
    (v : S) : ℕ :=
  (univ.filter (fun u => o u = v ∧ u ∈ Oex ∧ typ G S u = τ)).card

def labOf (G : SimpleGraph V) (S : Finset V) (o : Out S → S) (Oex : Finset (Out S)) :
    S → Label :=
  fun v => (nuOf o v, cOf G S o Oex 2 v, cOf G S o Oex 3 v)

def Oco (G : SimpleGraph V) (S : Finset V) (Oex : Finset (Out S)) : Finset (Out S) :=
  univ.filter (fun u => Shared G S u ∧ u ∉ Oex)

/-- `h̃_u` and `h̃^ex_u`. -/
def htil (P : Par) (G : SimpleGraph V) (S : Finset V) (o : Out S → S) (u : Out S)
    (X' X : Finset S) : ℝ :=
  hfac P.p₂ P.p₃ G S u X' X / hbar o u X

def htilEx (P : Par) (G : SimpleGraph V) (S : Finset V) (o : Out S → S) (u : Out S)
    (X' X : Finset S) : ℝ :=
  hfac P.p₂ P.p₃ G S u X' X /
    (hbar o u X * qT P.p₂ P.p₃ (typ G S u) ^ (if o u ∈ X then 1 else 0)
      * ϖT P (typ G S u) ^ (if o u ∈ X then 0 else 1))

/-- `T_u`, leaves, the owner rule and `O^ex` under it (def:rsc-rule). -/
def span {S : Finset V} (F : SimpleGraph S) (N : Finset S) : Finset S :=
  univ.filter (fun x => ∃ a ∈ N, ∃ b ∈ N, ∃ p : F.Walk a b, p.IsPath ∧ x ∈ p.support)

def IsLeafIn {S : Finset V} (F : SimpleGraph S) (T : Finset S) (v : S) : Prop :=
  v ∈ T ∧ (T.filter (F.Adj v)).card = 1

def OwnerRule (G : SimpleGraph V) (S : Finset V) (F : SimpleGraph S) (o : Out S → S) : Prop :=
  ∀ u, Shared G S u → IsLeafIn F (span F (NS G S u)) (o u)

def OwnerOK (G : SimpleGraph V) (S : Finset V) (F : SimpleGraph S) (o : Out S → S) : Prop :=
  ∀ u, Shared G S u → ((Nprime G S o u).filter (F.Adj (o u))).card ≤ 1

def OexRule (P : Par) (G : SimpleGraph V) (S : Finset V) (F : SimpleGraph S) (o : Out S → S) :
    Finset (Out S) :=
  univ.filter (fun u => Shared G S u ∧ ¬ LightT P (typ G S u) (nuOf o (o u)) (F.degree (o u)))

end
end MaxLeafFormal.RSCGraph
Back to top