MaxLeafFormal.RSCTreeDefs

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

import MaxLeafFormal.RSCRec
import MaxLeafFormal.Antinorm3

/-!
# Definitions of the tree model

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

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]

/-- `p_k`, total: only `k ≥ 2` is ever used with a nonzero exponent. -/
def pk (p₂ p₃ : ℝ) (k : ℕ) : ℝ := if k ≤ 2 then p₂ else p₃

/-- Product measure of `Υ ⊆ C` with inclusion probabilities `p`. -/
def prodMeas {α : Type*} [DecidableEq α] (p : α → ℝ) (C Υ : Finset α) : ℝ :=
  (∏ v ∈ Υ, p v) * ∏ v ∈ C \ Υ, (1 - p v)

/-- `k_F(v)`, `C_F(X')`, `π_{X'}(Υ)`, `Ψ_F(X)`. -/
def kF (F : SimpleGraph Vt) (X' : Finset Vt) (v : Vt) : ℕ := (X'.filter (F.Adj v)).card

def candF (F : SimpleGraph Vt) (X' : Finset Vt) : Finset Vt :=
  univ.filter (fun v => v ∉ X' ∧ 2 ≤ kF F X' v)

def piF (p₂ p₃ : ℝ) (F : SimpleGraph Vt) (X' Υ : Finset Vt) : ℝ :=
  prodMeas (fun v => pk p₂ p₃ (kF F X' v)) (candF F X') Υ

def psiF (F : SimpleGraph Vt) (X : Finset Vt) : ℕ :=
  (univ.filter (fun v => v ∉ X ∧ ∀ u, F.Adj v u → u ∉ X)).card + comp F X

/-- `ĥ_v(X)`; `lab v = (ν_v, c_{v,2}, c_{v,3})`. -/
def hhat (P : Par) (lab : Vt → Label) (v : Vt) (X : Finset Vt) : ℝ :=
  if v ∈ X then (1 - P.p₂) ^ (lab v).2.1 * (1 - P.p₃) ^ (lab v).2.2
  else (1/2 : ℝ) ^ (lab v).1 * P.ϖ₂ ^ (lab v).2.1 * P.ϖ₃ ^ (lab v).2.2

/-- `wt(X', Υ)`, `W^tm`, `Pr_tm`, `E_tm`. -/
def wt (P : Par) (F : SimpleGraph Vt) (lab : Vt → Label) (X' Υ : Finset Vt) : ℝ :=
  P.y ^ X'.card * piF P.p₂ P.p₃ F X' Υ * (1/2 : ℝ) ^ psiF F (X' ∪ Υ)
    * ∏ v, hhat P lab v (X' ∪ Υ)

def wsum (P : Par) (F : SimpleGraph Vt) (lab : Vt → Label)
    (E : Finset Vt → Finset Vt → Prop) : ℝ :=
  ∑ X' : Finset Vt, ∑ Υ ∈ (candF F X').powerset, if E X' Υ then wt P F lab X' Υ else 0

def Wtm (P : Par) (F : SimpleGraph Vt) (lab : Vt → Label) : ℝ := wsum P F lab (fun _ _ => True)

def Ptm (P : Par) (F : SimpleGraph Vt) (lab : Vt → Label) (E : Finset Vt → Finset Vt → Prop) : ℝ :=
  wsum P F lab E / Wtm P F lab

def Pcond (P : Par) (F : SimpleGraph Vt) (lab : Vt → Label)
    (E B : Finset Vt → Finset Vt → Prop) : ℝ :=
  Ptm P F lab (fun X' Υ => E X' Υ ∧ B X' Υ) / Ptm P F lab B

def Etm (P : Par) (F : SimpleGraph Vt) (lab : Vt → Label) (g : Finset Vt → Finset Vt → ℝ) : ℝ :=
  (∑ X' : Finset Vt, ∑ Υ ∈ (candF F X').powerset, wt P F lab X' Υ * g X' Υ) / Wtm P F lab

/-- `(X', Υ)` respects the forcing `f`. -/
def Respects (f : Vt → Option Force) (X' Υ : Finset Vt) : Prop :=
  ∀ v, (f v = some .inn → v ∈ X') ∧ (f v = some .out → v ∉ X') ∧
    (f v = some .excl → v ∉ X' ∪ Υ)

/-- `ord v` lists the children of `v` (tree rooted at `r`) without repetition. -/
def IsChildOrder {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt) (ord : Vt → List Vt) : Prop :=
  ∀ v, (ord v).Nodup ∧ ∀ w, w ∈ ord v ↔ w ∈ children hF r v

/-- The subtree of `v`, rooted at `r`, as an ordered labelled tree. -/
def toRTree {α : Type} {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt) (ord : Vt → List Vt)
    (lab : Vt → α) (v : Vt) : RTree α :=
  .node (lab v) (((ord v).filter (· ∈ children hF r v)).attach.map
    (fun w => toRTree hF r ord lab w.1))
termination_by (D hF r v).card
decreasing_by
  exact Antinorm3.card_D_child_lt hF r (by simpa using (List.mem_filter.1 w.2).2)

/-- `def:rsc-admissible` on a tree, with `d = d_F(v)`. -/
def AdmissibleG (P : Par) (F : SimpleGraph Vt) (lab : Vt → Label) : Prop :=
  ∀ v, (lab v).2.1 + (lab v).2.2 ≤ (lab v).1 ∧
    ((Light₂ P.p₂ P.p₃ P.y (lab v).1 (F.degree v) ∨ F.degree v = 0) → (lab v).2.1 = 0) ∧
    ((Light₃ P.p₂ P.p₃ P.y (lab v).1 (F.degree v) ∨ F.degree v = 0) → (lab v).2.2 = 0) ∧
    ((F.degree v = 1 ∧ 1 ≤ (lab v).2.1 + (lab v).2.2) →
      (lab v).2.1 + (lab v).2.2 ≤ (lab v).1 - 1)

/-- `p̃(v)` and `W̃`. -/
def ptil (P : Par) {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt) (X' : Finset Vt) (v : Vt) : ℝ :=
  if v ≠ r ∧ par hF r v ∈ X' ∧ 2 ≤ (X' ∩ children hF r v).card then P.p₃ else P.p₂

def Wrel (P : Par) {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt) (lab : Vt → Label) : ℝ :=
  ∑ X' : Finset Vt, ∑ Υ ∈ (candF F X').powerset,
    P.y ^ X'.card * prodMeas (ptil P hF r X') (candF F X') Υ * (1/2 : ℝ) ^ psiF F (X' ∪ Υ)
      * ∏ v, hhat P lab v (X' ∪ Υ)

end
end MaxLeafFormal.RSCTree
Back to top