Nesting, soundness, and source-disjoint independence

Statements split from the original Statements.lean skeleton (one file per proving task); see AUDIT-NOTES for the mathematics.

The witness that a genuine model gives at order t is Sound.inflLaw: sample every copied source independently from the model's source law and answer every copied observation with the model's response kernel. It is a mixture, over copied latent configurations, of product laws on the copied observations, so all of its marginals are computed by the two facts that Sound.pushforward_prodLaw_sel (an injectively selected block of a product law is the product law of the block) and Sound.sum_dprod_prod (functions of disjoint coordinate blocks are independent under a product weight) supply.

The four statements below are proved. sourceDisjoint_independent of the original skeleton was false as stated (it quantified over arbitrary sets of copied observations rather than vertex blocks) and has been removed; the vertex-block form is blockMarg_union_of_sourceDisjoint in DoubleStar.lean. compatible_gExpFeasible is proved in RootSink.lean from the root-sink lemma.

Generic finite-sum toolkit

theorem TriangleInflation.Graph.Sound.sum_pi_prod {κ : Type u_1} [Fintype κ] [DecidableEq κ] {A : κ → Type u_2} [(k : κ) → Fintype (A k)] (f : (k : κ) → A k → ℝ) : ∑ x : (k : κ) → A k, ∏ k : κ, f k (x k) = ∏ k : κ, ∑ a : A k, f k a

A sum over all configurations of a dependent product factorizes.

theorem TriangleInflation.Graph.Sound.ite_funext_prod {κ : Type u_1} [Fintype κ] {B : κ → Type u_2} [(k : κ) → DecidableEq (B k)] (f g : (k : κ) → B k) : (if f = g then 1 else 0) = ∏ k : κ, if f k = g k then 1 else 0

The indicator of an equality of configurations is a product of coordinate indicators.

theorem TriangleInflation.Graph.Sound.sum_dprod_sel {κ : Type u_1} [Fintype κ] [DecidableEq κ] {A : κ → Type u_2} {B : κ → Type u_3} [(k : κ) → Fintype (A k)] [(k : κ) → DecidableEq (B k)] (W : (k : κ) → A k → ℝ) (sel : (k : κ) → A k → B k) (y : (k : κ) → B k) : ∑ x : (k : κ) → A k, (if (fun (k : κ) => sel k (x k)) = y then 1 else 0) * ∏ k : κ, W k (x k) = ∏ k : κ, ∑ a : A k, (if sel k a = y k then 1 else 0) * W k a

A dependent product weight pushed forward along a coordinatewise map.

theorem TriangleInflation.Graph.Sound.sum_pushforward {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (w : α → ℝ) (F : α → β) : ∑ b : β, pushforward w F b = ∑ a : α, w a

Total mass is preserved by pushforward.

theorem TriangleInflation.Graph.Sound.sum_mul_comp {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (w : α → ℝ) (F : α → β) (G : β → ℝ) : ∑ a : α, w a * G (F a) = ∑ b : β, pushforward w F b * G b

Integrating against a pushforward is integrating the pullback.

theorem TriangleInflation.Graph.Sound.pushforward_comp_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq β] [DecidableEq γ] (w : α → ℝ) (F : α → β) (E : β ≃ γ) : (pushforward w fun (a : α) => E (F a)) = fun (c : γ) => pushforward w F (E.symm c)

Postcomposing the read map with a bijection transports the pushforward.

theorem TriangleInflation.Graph.Sound.pushforward_mix {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {ι : Type u_4} [Fintype ι] (c : ι → ℝ) (ν : ι → α → ℝ) (F : α → β) : pushforward (fun (a : α) => ∑ i : ι, c i * ν i a) F = fun (b : β) => ∑ i : ι, c i * pushforward (ν i) F b

Pushing forward a finite mixture.

Marginals of a product law along an injective selection

theorem TriangleInflation.Graph.Sound.pushforward_prodLaw_sel {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {w : ι → Bool → ℝ} (hw : ∀ (i : ι), ∑ b : Bool, w i b = 1) {ν : κ → ι} (hν : Function.Injective ν) : (pushforward (prodLaw w) fun (x : ι → Bool) (k : κ) => x (ν k)) = prodLaw fun (k : κ) => w (ν k)

The marginal of a product weight on an injectively selected set of coordinates is the product weight of the selected coordinates.

Independence of functions of disjoint coordinate blocks, dependent fibres

def TriangleInflation.Graph.Sound.dprod {ι : Type u_1} [Fintype ι] {A : ι → Type u_2} (w : (i : ι) → A i → ℝ) (x : (i : ι) → A i) : ℝ

The product weight of independent coordinates with dependent alphabets.

Equations

• TriangleInflation.Graph.Sound.dprod w x = ∏ i : ι, w i (x i)

theorem TriangleInflation.Graph.Sound.sum_dprod {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : ι → Type u_2} [(i : ι) → Fintype (A i)] {w : (i : ι) → A i → ℝ} (hw : ∀ (i : ι), ∑ a : A i, w i a = 1) : ∑ x : (i : ι) → A i, dprod w x = 1

def TriangleInflation.Graph.Sound.dmix {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} (I : Finset ι) (x y : (i : ι) → A i) (i : ι) : A i

dmix I x y takes its I-coordinates from x and the others from y.

Equations

• TriangleInflation.Graph.Sound.dmix I x y i = if i ∈ I then x i else y i

theorem TriangleInflation.Graph.Sound.dmix_mem {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {I : Finset ι} {x y : (i : ι) → A i} {i : ι} (hi : i ∈ I) : dmix I x y i = x i

theorem TriangleInflation.Graph.Sound.dmix_not_mem {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {I : Finset ι} {x y : (i : ι) → A i} {i : ι} (hi : i ∉ I) : dmix I x y i = y i

theorem TriangleInflation.Graph.Sound.dprod_dmix_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : ι → Type u_2} {w : (i : ι) → A i → ℝ} (I : Finset ι) (x y : (i : ι) → A i) : dprod w (dmix I x y) * dprod w (dmix I y x) = dprod w x * dprod w y

theorem TriangleInflation.Graph.Sound.sum_dprod_mul_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : ι → Type u_2} [(i : ι) → Fintype (A i)] {w : (i : ι) → A i → ℝ} (hw : ∀ (i : ι), ∑ a : A i, w i a = 1) {I J : Finset ι} (hIJ : Disjoint I J) {φ ψ : ((i : ι) → A i) → ℝ} (hφ : ∀ (x y : (i : ι) → A i), (∀ i ∈ I, x i = y i) → φ x = φ y) (hψ : ∀ (x y : (i : ι) → A i), (∀ i ∈ J, x i = y i) → ψ x = ψ y) : ∑ x : (i : ι) → A i, dprod w x * (φ x * ψ x) = (∑ x : (i : ι) → A i, dprod w x * φ x) * ∑ x : (i : ι) → A i, dprod w x * ψ x

Functions of disjoint coordinate blocks are uncorrelated under a product weight.

theorem TriangleInflation.Graph.Sound.sum_dprod_prod {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : ι → Type u_2} [(i : ι) → Fintype (A i)] {w : (i : ι) → A i → ℝ} (hw : ∀ (i : ι), ∑ a : A i, w i a = 1) {n : ℕ} (I : Fin n → Finset ι) (χ : Fin n → ((i : ι) → A i) → ℝ) : (∀ (m m' : Fin n), m ≠ m' → Disjoint (I m) (I m')) → (∀ (m : Fin n) (x y : (i : ι) → A i), (∀ i ∈ I m, x i = y i) → χ m x = χ m y) → ∑ x : (i : ι) → A i, dprod w x * ∏ m : Fin n, χ m x = ∏ m : Fin n, ∑ x : (i : ι) → A i, dprod w x * χ m x

Functions of pairwise disjoint coordinate blocks have a product expectation.

theorem TriangleInflation.Graph.Sound.sum_sel_coord {B : Type u_1} [Fintype B] [DecidableEq B] {n : Type u_2} [Fintype n] [DecidableEq n] (ρ : B → ℝ) (hρ : ∑ b : B, ρ b = 1) (r₀ : n) (b₀ : B) : ∑ v : n → B, (if v r₀ = b₀ then 1 else 0) * ∏ r : n, ρ (v r) = ρ b₀

The marginal of an i.i.d. family at a single coordinate.

Graph helpers

theorem TriangleInflation.Graph.Sound.inc_nonempty (Γ : PairGraph) (v : Γ.V) : (Γ.inc v).Nonempty

theorem TriangleInflation.Graph.Sound.gAncestors_nonempty {Γ : PairGraph} {t : ℕ} (o : GObs Γ t) : (gAncestors o).Nonempty

theorem TriangleInflation.Graph.Sound.disjoint_of_gAI {Γ : PairGraph} {t : ℕ} {S T : Finset (GObs Γ t)} (h : GAncestrallyIndependent S T) : Disjoint S T

theorem TriangleInflation.Graph.Sound.eq_copyObs {Γ : PairGraph} {t : ℕ} {ι : Γ.Edge → Fin t} {o : GObs Γ t} (h : o ∈ copySet ι) : o = copyObs ι o.fst

theorem TriangleInflation.Graph.Sound.vertex_injective {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} (hS : GInjectable S) : Function.Injective fun (o : ↥S) => (↑o).fst

The inflated model

@[reducible, inline]

abbrev TriangleInflation.Graph.Sound.GCfg {Γ : PairGraph} (M : GModel Γ) (t : ℕ) : Type

Latent configurations of the order-t inflation.

Equations

• TriangleInflation.Graph.Sound.GCfg M t = ((l : TriangleInflation.Graph.GLatent Γ t) → M.L l.1)

@[reducible, inline]

abbrev TriangleInflation.Graph.Sound.MCfg {Γ : PairGraph} (M : GModel Γ) : Type

Latent configurations of the model itself.

Equations

• TriangleInflation.Graph.Sound.MCfg M = ((e : Γ.Edge) → M.L e)

def TriangleInflation.Graph.Sound.obsResp {Γ : PairGraph} {t : ℕ} (M : GModel Γ) (o : GObs Γ t) (x : GCfg M t) : ℝ

The response probability of a copied observation under a copied latent configuration.

Equations

• TriangleInflation.Graph.Sound.obsResp M o x = M.resp o.fst fun (e : ↥(Γ.inc o.fst)) => x (↑e, o.snd e)

def TriangleInflation.Graph.Sound.inflCond {Γ : PairGraph} {t : ℕ} (M : GModel Γ) (x : GCfg M t) : GObs Γ t → Bool → ℝ

The conditional per-observation weights of the inflated model.

Equations

• TriangleInflation.Graph.Sound.inflCond M x o b = TriangleInflation.respMass (TriangleInflation.Graph.Sound.obsResp M o x) b

def TriangleInflation.Graph.Sound.cfgW {Γ : PairGraph} (M : GModel Γ) (t : ℕ) : GCfg M t → ℝ

The weight of a copied latent configuration.

Equations

• TriangleInflation.Graph.Sound.cfgW M t = TriangleInflation.Graph.Sound.dprod fun (l : TriangleInflation.Graph.GLatent Γ t) (a : M.L l.1) => M.μ l.1 a

def TriangleInflation.Graph.Sound.mcfgW {Γ : PairGraph} (M : GModel Γ) : MCfg M → ℝ

The weight of a latent configuration of the model.

Equations

• TriangleInflation.Graph.Sound.mcfgW M = TriangleInflation.Graph.Sound.dprod fun (e : Γ.Edge) (a : M.L e) => M.μ e a

def TriangleInflation.Graph.Sound.inflLaw {Γ : PairGraph} (M : GModel Γ) (t : ℕ) : GAssign Γ t → ℝ

The witness produced by running the model on the order-t inflation: sample every copied source independently and answer every copied observation with the model's response kernel.

Equations

• One or more equations did not get rendered due to their size.

theorem TriangleInflation.Graph.Sound.respMass_sum (q : ℝ) : ∑ b : Bool, respMass q b = 1

theorem TriangleInflation.Graph.Sound.inflCond_sum {Γ : PairGraph} {t : ℕ} {M : GModel Γ} (x : GCfg M t) (o : GObs Γ t) : ∑ b : Bool, inflCond M x o b = 1

theorem TriangleInflation.Graph.Sound.inflCond_isLaw {Γ : PairGraph} {t : ℕ} {M : GModel Γ} (hM : M.Valid) (x : GCfg M t) (o : GObs Γ t) : IsLaw (inflCond M x o)

theorem TriangleInflation.Graph.Sound.sum_cfgW {Γ : PairGraph} {t : ℕ} {M : GModel Γ} (hM : M.Valid) : ∑ x : GCfg M t, cfgW M t x = 1

theorem TriangleInflation.Graph.Sound.cfgW_nonneg {Γ : PairGraph} {t : ℕ} {M : GModel Γ} (hM : M.Valid) (x : GCfg M t) : 0 ≤ cfgW M t x

theorem TriangleInflation.Graph.Sound.mcfgW_nonneg {Γ : PairGraph} {M : GModel Γ} (hM : M.Valid) (y : MCfg M) : 0 ≤ mcfgW M y

theorem TriangleInflation.Graph.Sound.pushforward_inflLaw {Γ : PairGraph} {t : ℕ} {M : GModel Γ} {β : Type u_1} [DecidableEq β] (F : GAssign Γ t → β) : pushforward (inflLaw M t) F = fun (b : β) => ∑ x : GCfg M t, cfgW M t x * pushforward (prodLaw (inflCond M x)) F b

The witness is a mixture of product laws, so its pushforwards are mixtures.

theorem TriangleInflation.Graph.Sound.latent_marginal {Γ : PairGraph} {t : ℕ} {M : GModel Γ} (hM : M.Valid) (ι : Γ.Edge → Fin t) (F : MCfg M → ℝ) : (∑ x : GCfg M t, cfgW M t x * F fun (e : Γ.Edge) => x (e, ι e)) = ∑ y : MCfg M, mcfgW M y * F y

Marginalizing the copied latent configuration onto one copy of the original scenario.

The witness built from a model

def TriangleInflation.Graph.Sound.gLatentPerm {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) : GLatent Γ t ≃ GLatent Γ t

Relabelling copy indices, as a bijection of copied latents.

Equations

• One or more equations did not get rendered due to their size.

def TriangleInflation.Graph.Sound.gObsPerm {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) : GObs Γ t ≃ GObs Γ t

Relabelling copy indices, as a bijection of copied observations.

Equations

• One or more equations did not get rendered due to their size.

def TriangleInflation.Graph.Sound.gCfgPerm {Γ : PairGraph} {t : ℕ} (M : GModel Γ) (π : Γ.Edge → Equiv.Perm (Fin t)) : GCfg M t ≃ GCfg M t

Relabelling copy indices, as a bijection of copied latent configurations.

Equations

• One or more equations did not get rendered due to their size.

theorem TriangleInflation.Graph.Sound.isLaw_inflLaw {Γ : PairGraph} {t : ℕ} {M : GModel Γ} (hM : M.Valid) : IsLaw (inflLaw M t)

The witness is a law.

theorem TriangleInflation.Graph.Sound.symmetric_inflLaw {Γ : PairGraph} (M : GModel Γ) (t : ℕ) : GSymmetric t (inflLaw M t)

The witness is symmetric: the copies of each source are i.i.d.

theorem TriangleInflation.Graph.Sound.inflLaw_block {Γ : PairGraph} {t : ℕ} {M : GModel Γ} (S : Finset (GObs Γ t)) (φ : ↥S → Bool) : pushforward (inflLaw M t) (gRestrict S) φ = ∑ x : GCfg M t, cfgW M t x * ∏ o : ↥S, respMass (obsResp M (↑o) x) (φ o)

The marginal of the witness on a block of copied observations.

theorem TriangleInflation.Graph.Sound.copySet_snd {Γ : PairGraph} {t : ℕ} {ι : Γ.Edge → Fin t} {o : GObs Γ t} (h : o ∈ copySet ι) (e : ↥(Γ.inc o.fst)) : o.snd e = ι ↑e

On a copy of the original scenario the copy indices are those of the copy.

theorem TriangleInflation.Graph.Sound.inflLaw_injectable {Γ : PairGraph} {t : ℕ} {M : GModel Γ} (hM : M.Valid) {S : Finset (GObs Γ t)} (hS : GInjectable S) : pushforward (inflLaw M t) (gRestrict S) = pushforward M.law (gPartyRead S)

Every injectable set carries the corresponding marginal of the model's law: the copied observations of an injectable set read one copy of the original scenario.

The diagonal law of the witness

def TriangleInflation.Graph.Sound.diagObs (Γ : PairGraph) (t : ℕ) (p : Fin t × Γ.V) : GObs Γ t

The copied observation that diagonal row r reads at the vertex v.

Equations

• TriangleInflation.Graph.Sound.diagObs Γ t p = ⟨p.2, fun (x : ↥(Γ.inc p.2)) => p.1⟩

theorem TriangleInflation.Graph.Sound.diagObs_injective (Γ : PairGraph) (t : ℕ) : Function.Injective (diagObs Γ t)

The t · |V| diagonal observations are distinct.

theorem TriangleInflation.Graph.Sound.readDiag_factor (Γ : PairGraph) (t : ℕ) : readDiag = fun (ω : GAssign Γ t) => (Equiv.curry (Fin t) Γ.V Bool) fun (p : Fin t × Γ.V) => ω (diagObs Γ t p)

theorem TriangleInflation.Graph.Sound.inflLaw_diag {Γ : PairGraph} {t : ℕ} {M : GModel Γ} (_hM : M.Valid) : pushforward (inflLaw M t) readDiag = gTensorPow t M.law

The diagonal law of the witness is the tensor power of the model's law: the t copies of the scenario use disjoint copies of every source.

The ancestral-independence prescriptions

def TriangleInflation.Graph.Sound.sigCurry {Γ : PairGraph} {t n : ℕ} (S : Fin n → Finset (GObs Γ t)) : ((m : Fin n) × ↥(S m) → Bool) ≃ ((m : Fin n) → ↥(S m) → Bool)

Currying a Bool-valued function on a disjoint union of blocks.

Equations

• One or more equations did not get rendered due to their size.

theorem TriangleInflation.Graph.Sound.sigma_val_injective {Γ : PairGraph} {t n : ℕ} {S : Fin n → Finset (GObs Γ t)} (hd : ∀ (m m' : Fin n), m ≠ m' → Disjoint (S m) (S m')) : Function.Injective fun (p : (m : Fin n) × ↥(S m)) => ↑p.snd

theorem TriangleInflation.Graph.Sound.mem_gAncestorsOf {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} {o : GObs Γ t} (ho : o ∈ S) (e : ↥(Γ.inc o.fst)) : (↑e, o.snd e) ∈ gAncestorsOf S

theorem TriangleInflation.Graph.Sound.inflLaw_ai {Γ : PairGraph} {t : ℕ} {M : GModel Γ} (hM : M.Valid) : GAncestralProducts t (inflLaw M t) M.law

The witness satisfies every ancestral-independence prescription: blocks with disjoint copied ancestries are functions of disjoint families of independent copied sources.

From the expressible closure to the ancestral-independence prescriptions

theorem TriangleInflation.Graph.Sound.pushforward_id {α : Type u_1} [Fintype α] [DecidableEq α] (w : α → ℝ) : pushforward w id = w

theorem TriangleInflation.Graph.Sound.pushforward_prod {α : Type u_1} {β : Type u_2} {α' : Type u_3} {β' : Type u_4} [Fintype α] [Fintype β] [DecidableEq α'] [DecidableEq β'] (A : α → ℝ) (B : β → ℝ) (f : α → α') (g : β → β') : (pushforward (fun (p : α × β) => A p.1 * B p.2) fun (p : α × β) => (f p.1, g p.2)) = fun (q : α' × β') => pushforward A f q.1 * pushforward B g q.2

theorem TriangleInflation.Graph.Sound.subRestrict_injective {Γ : PairGraph} {t : ℕ} {A B : Finset (GObs Γ t)} (hAB : A ⊆ B) (hBA : B ⊆ A) : Function.Injective (subRestrict hAB)

Restriction to a subset that contains everything is injective.

theorem TriangleInflation.Graph.Sound.pushforward_subRestrict_self {Γ : PairGraph} {t : ℕ} {A B : Finset (GObs Γ t)} (hAB : A ⊆ B) (hBA : B ⊆ A) (μ : (↥B → Bool) → ℝ) (b : ↥B → Bool) : pushforward μ (subRestrict hAB) (subRestrict hAB b) = μ b

A law is recovered from its restriction to a set with the same elements.

theorem TriangleInflation.Graph.Sound.empty_fun_eq {Γ : PairGraph} {t : ℕ} (f g : ↥∅ → Bool) : f = g

theorem TriangleInflation.Graph.Sound.left_sub {Γ : PairGraph} {t : ℕ} (X Y : Finset (GObs Γ t)) : X ⊆ X ∪ Y ∪ ∅

theorem TriangleInflation.Graph.Sound.right_sub {Γ : PairGraph} {t : ℕ} (X Y : Finset (GObs Γ t)) : Y ⊆ X ∪ Y ∪ ∅

theorem TriangleInflation.Graph.Sound.union_empty_sub {Γ : PairGraph} {t : ℕ} (X : Finset (GObs Γ t)) : X ∪ ∅ ⊆ X

theorem TriangleInflation.Graph.Sound.sub_union_empty {Γ : PairGraph} {t : ℕ} (X : Finset (GObs Γ t)) : X ⊆ X ∪ ∅

theorem TriangleInflation.Graph.Sound.dsep_empty_of_ai {Γ : PairGraph} {t : ℕ} {X Y : Finset (GObs Γ t)} (h : GAncestrallyIndependent X Y) : dsep X Y ∅

Ancestrally disjoint sets are d-separated given the empty set: a trail between them would have to be a single edge, and that edge is a shared copied parent.

theorem TriangleInflation.Graph.Sound.gAncestorsOf_biUnion {Γ : PairGraph} {t n : ℕ} (T : Fin n → Finset (GObs Γ t)) : gAncestorsOf (Finset.univ.biUnion T) = Finset.univ.biUnion fun (m : Fin n) => gAncestorsOf (T m)

def TriangleInflation.Graph.Sound.pairSel {Γ : PairGraph} {t : ℕ} (X Y : Finset (GObs Γ t)) (χ : ↥(X ∪ Y ∪ ∅) → Bool) : (↥X → Bool) × (↥Y → Bool)

Splitting a Bool-valued function on a disjoint union into its two halves.

Equations

• TriangleInflation.Graph.Sound.pairSel X Y χ = (TriangleInflation.Graph.subRestrict ⋯ χ, TriangleInflation.Graph.subRestrict ⋯ χ)

theorem TriangleInflation.Graph.Sound.pairSel_bijective {Γ : PairGraph} {t : ℕ} {X Y : Finset (GObs Γ t)} (hXY : Disjoint X Y) : Function.Bijective (pairSel X Y)

noncomputable def TriangleInflation.Graph.Sound.pairEquiv {Γ : PairGraph} {t : ℕ} {X Y : Finset (GObs Γ t)} (hXY : Disjoint X Y) : (↥(X ∪ Y ∪ ∅) → Bool) ≃ (↥X → Bool) × (↥Y → Bool)

The two halves of a Bool-valued function on a disjoint union determine it.

Equations

• TriangleInflation.Graph.Sound.pairEquiv hXY = Equiv.ofBijective (TriangleInflation.Graph.Sound.pairSel X Y) ⋯

def TriangleInflation.Graph.Sound.consEquiv {n : ℕ} (β : Fin (n + 1) → Type u_1) : β 0 × ((m : Fin n) → β m.succ) ≃ ((m : Fin (n + 1)) → β m)

Splitting a dependent family over Fin (n+1) into its head and tail.

Equations

• One or more equations did not get rendered due to their size.

def TriangleInflation.Graph.Sound.tailSel {Γ : PairGraph} {t n : ℕ} (S : Fin (n + 1) → Finset (GObs Γ t)) : (↥(Finset.univ.biUnion fun (m : Fin n) => S m.succ) → Bool) → (m : Fin n) → ↥(S m.succ) → Bool

Restricting a function on the union of the tail blocks to each tail block.

Equations

• TriangleInflation.Graph.Sound.tailSel S b m = TriangleInflation.Graph.subRestrict ⋯ b

def TriangleInflation.Graph.Sound.headTailSel {Γ : PairGraph} {t n : ℕ} (S : Fin (n + 1) → Finset (GObs Γ t)) : (↥(S 0) → Bool) × (↥(Finset.univ.biUnion fun (m : Fin n) => S m.succ) → Bool) → (↥(S 0) → Bool) × ((m : Fin n) → ↥(S m.succ) → Bool)

The head block keeps its function, the tail block is split.

Equations

• TriangleInflation.Graph.Sound.headTailSel S q = (id q.1, TriangleInflation.Graph.Sound.tailSel S q.2)

theorem TriangleInflation.Graph.Sound.glue_pair {Γ : PairGraph} {t : ℕ} {P : GTarget Γ} {Δ : GAssign Γ t → ℝ} (hPsum : ∑ w : Γ.V → Bool, P w = 1) (hexp : ∀ (S : Finset (GObs Γ t)) (μ : (↥S → Bool) → ℝ), Expressible t P S μ → pushforward Δ (gRestrict S) = μ) {X Y : Finset (GObs Γ t)} {μY : (↥Y → Bool) → ℝ} (hX : GInjectable X) (hμY : Expressible t P Y μY) (haiXY : GAncestrallyIndependent X Y) : Expressible t P (X ∪ Y ∪ ∅) (glueLaw X Y ∅ (pushforward P (gPartyRead (X ∪ ∅))) (pushforward μY (subRestrict ⋯))) ∧ (pushforward Δ fun (ω : GAssign Γ t) => (gRestrict X ω, gRestrict Y ω)) = fun (q : (↥X → Bool) × (↥Y → Bool)) => pushforward P (gPartyRead X) q.1 * pushforward Δ (gRestrict Y) q.2

One gluing step with an empty conditioning set: an injectable block and an expressible block with disjoint copied ancestries glue to their product.

theorem TriangleInflation.Graph.Sound.ancestral_zero {Γ : PairGraph} {t : ℕ} {P : GTarget Γ} {Δ : GAssign Γ t → ℝ} (hlaw : IsLaw Δ) (S : Fin 0 → Finset (GObs Γ t)) : (pushforward Δ fun (ω : GAssign Γ t) (m : Fin 0) => gRestrict (S m) ω) = fun (φ : (m : Fin 0) → ↥(S m) → Bool) => ∏ m : Fin 0, pushforward P (gPartyRead (S m)) (φ m)

With no blocks the ancestral-independence prescription is the total mass.

theorem TriangleInflation.Graph.Sound.exp_induct {Γ : PairGraph} {t : ℕ} {P : GTarget Γ} {Δ : GAssign Γ t → ℝ} (hlaw : IsLaw Δ) (hPsum : ∑ w : Γ.V → Bool, P w = 1) (hexp : ∀ (S : Finset (GObs Γ t)) (μ : (↥S → Bool) → ℝ), Expressible t P S μ → pushforward Δ (gRestrict S) = μ) (ι : Γ.Edge → Fin t) (n : ℕ) (S : Fin n → Finset (GObs Γ t)) : (∀ (m : Fin n), GInjectable (S m)) → (∀ (m m' : Fin n), m ≠ m' → GAncestrallyIndependent (S m) (S m')) → (∃ (μ : (↥(Finset.univ.biUnion S) → Bool) → ℝ), Expressible t P (Finset.univ.biUnion S) μ) ∧ (pushforward Δ fun (ω : GAssign Γ t) (m : Fin n) => gRestrict (S m) ω) = fun (φ : (m : Fin n) → ↥(S m) → Bool) => ∏ m : Fin n, pushforward P (gPartyRead (S m)) (φ m)

The expressible closure prescribes the ancestral-independence products: the blocks are glued one at a time with an empty conditioning set, and the glue law with an empty conditioning set is the product of the two block laws.

theorem TriangleInflation.Graph.Sound.gAncestralProducts_of_exp {Γ : PairGraph} {t : ℕ} {Δ : GAssign Γ t → ℝ} {P : GTarget Γ} (hlaw : IsLaw Δ) (hexp : ∀ (S : Finset (GObs Γ t)) (μ : (↥S → Bool) → ℝ), Expressible t P S μ → pushforward Δ (gRestrict S) = μ) : GAncestralProducts t Δ P

Expressible prescriptions imply the ancestral products for the same witness law.

Nesting of the three hierarchies

theorem TriangleInflation.Graph.gAIFeasible_of_gExpFeasible (Γ : PairGraph) (t : ℕ) (P : GTarget Γ) : GExpFeasible Γ t P → GAIFeasible Γ t P

The expressible feasible set is contained in the AI feasible set: the AI prescriptions are the injectable and ancestrally independent instances of the expressible closure (paper equation (eq:nested)).

theorem TriangleInflation.Graph.gNWFeasible_of_gAIFeasible (Γ : PairGraph) (t : ℕ) (P : GTarget Γ) : GAIFeasible Γ t P → GNWFeasible Γ t P

The AI feasible set is contained in the Navascués–Wolfe feasible set.

theorem TriangleInflation.Graph.compatible_gNWFeasible (Γ : PairGraph) (t : ℕ) (P : GTarget Γ) (h : GCompatible Γ P) : GNWFeasible Γ t P

A genuine model gives a witness at every order: run the inflated model. Hence the compatible set is contained in every Navascués–Wolfe feasible set.

theorem TriangleInflation.Graph.compatible_gAIFeasible (Γ : PairGraph) (t : ℕ) (P : GTarget Γ) (h : GCompatible Γ P) : GAIFeasible Γ t P

A genuine model gives a witness satisfying all injectable and ancestral-independence prescriptions.