The defect cube

Statements for paper Section 5.1 (sec:construction) and the Navascués–Wolfe part of Section 5.3 (sec:survival): Lemma 5.4 (lem:disjoint), Lemma 5.5 (lem:triangle-law), Lemma 5.6 (lem:symmetry) and Lemma 5.9 (lem:diag), together with the general independence lemma for functions of disjoint coordinate sets under a product weight that those proofs use. Proofs are deferred.

Independence under a product weight

The general fact behind the paper's repeated phrase "outputs that are functions of disjoint families of independent bits are independent".

theorem TriangleInflation.sum_prodLaw {ι : Type u_1} [Fintype ι] [DecidableEq ι] {w : ι → Bool → ℝ} (hw : ∀ (i : ι), IsLaw (w i)) : ∑ x : ι → Bool, prodLaw w x = 1

The total mass of a product weight is one.

def TriangleInflation.mixOn {ι : Type u_1} [DecidableEq ι] (I : Finset ι) (x y : ι → Bool) : ι → Bool

mixOn I x y takes its I-coordinates from x and all other coordinates from y.

Equations

• TriangleInflation.mixOn I x y i = if i ∈ I then x i else y i

theorem TriangleInflation.mixOn_mem {ι : Type u_1} [DecidableEq ι] {I : Finset ι} {x y : ι → Bool} {i : ι} (hi : i ∈ I) : mixOn I x y i = x i

theorem TriangleInflation.mixOn_not_mem {ι : Type u_1} [DecidableEq ι] {I : Finset ι} {x y : ι → Bool} {i : ι} (hi : i ∉ I) : mixOn I x y i = y i

theorem TriangleInflation.prodLaw_mixOn_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {w : ι → Bool → ℝ} (I : Finset ι) (x y : ι → Bool) : prodLaw w (mixOn I x y) * prodLaw w (mixOn I y x) = prodLaw w x * prodLaw w y

Swapping the I-coordinates of a pair of assignments preserves the product weight of the pair.

theorem TriangleInflation.sum_prodLaw_mul_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {w : ι → Bool → ℝ} (hw : ∀ (i : ι), IsLaw (w i)) {I J : Finset ι} (hIJ : Disjoint I J) {φ ψ : (ι → Bool) → ℝ} (hφ : ∀ (x y : ι → Bool), (∀ i ∈ I, x i = y i) → φ x = φ y) (hψ : ∀ (x y : ι → Bool), (∀ i ∈ J, x i = y i) → ψ x = ψ y) : ∑ x : ι → Bool, prodLaw w x * (φ x * ψ x) = (∑ x : ι → Bool, prodLaw w x * φ x) * ∑ x : ι → Bool, prodLaw w x * ψ x

The expectation form of independence: real-valued functions of disjoint coordinate sets have uncorrelated expectations under a product weight.

theorem TriangleInflation.sum_prodLaw_prod {ι : Type u_1} [Fintype ι] [DecidableEq ι] {w : ι → Bool → ℝ} (hw : ∀ (i : ι), IsLaw (w i)) {n : ℕ} (I : Fin n → Finset ι) (χ : Fin n → (ι → Bool) → ℝ) : (∀ (m m' : Fin n), m ≠ m' → Disjoint (I m) (I m')) → (∀ (m : Fin n) (x y : ι → Bool), (∀ i ∈ I m, x i = y i) → χ m x = χ m y) → ∑ x : ι → Bool, prodLaw w x * ∏ m : Fin n, χ m x = ∏ m : Fin n, ∑ x : ι → Bool, prodLaw w x * χ m x

The finite-family expectation form: real-valued functions of pairwise disjoint coordinate sets have a product expectation under a product weight.

theorem TriangleInflation.indep_of_disjoint_support {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype ι] [DecidableEq ι] [DecidableEq α] [DecidableEq β] {w : ι → Bool → ℝ} (hw : ∀ (i : ι), IsLaw (w i)) {I J : Finset ι} (hIJ : Disjoint I J) {F : (ι → Bool) → α} {G : (ι → Bool) → β} (hF : ∀ (x y : ι → Bool), (∀ i ∈ I, x i = y i) → F x = F y) (hG : ∀ (x y : ι → Bool), (∀ i ∈ J, x i = y i) → G x = G y) : (pushforward (prodLaw w) fun (x : ι → Bool) => (F x, G x)) = fun (q : α × β) => pushforward (prodLaw w) F q.1 * pushforward (prodLaw w) G q.2

Two functions of disjoint coordinate sets are independent under a product weight.

theorem TriangleInflation.prod_ite_eq_ite_funext {n : ℕ} {β : Fin n → Type u_1} [(m : Fin n) → DecidableEq (β m)] (f g : (m : Fin n) → β m) : (∏ m : Fin n, if f m = g m then 1 else 0) = if f = g then 1 else 0

An indicator product collapses to the indicator of the full agreement.

theorem TriangleInflation.indep_of_disjoint_family {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {β : Fin n → Type u_2} [(m : Fin n) → DecidableEq (β m)] {w : ι → Bool → ℝ} (hw : ∀ (i : ι), IsLaw (w i)) {I : Fin n → Finset ι} (hI : ∀ (m m' : Fin n), m ≠ m' → Disjoint (I m) (I m')) {F : (m : Fin n) → (ι → Bool) → β m} (hF : ∀ (m : Fin n) (x y : ι → Bool), (∀ i ∈ I m, x i = y i) → F m x = F m y) : (pushforward (prodLaw w) fun (x : ι → Bool) (m : Fin n) => F m x) = fun (φ : (m : Fin n) → β m) => ∏ m : Fin n, pushforward (prodLaw w) (F m) (φ m)

The finite-family form: functions of pairwise disjoint coordinate sets are mutually independent under a product weight.

Disjoint ancestry gives disjoint inputs (Lemma 5.4)

theorem TriangleInflation.Obs.ancestors_nonempty {t : ℕ} (u : Obs t) : u.ancestors.Nonempty

Every copied observation has a copied latent ancestor.

theorem TriangleInflation.line_inter_ancestors {t : ℕ} {u v : Obs t} {c : Cell t} (hu : onLine u c = true) (hv : onLine v c = true) : u = v ∨ ¬Disjoint u.ancestors v.ancestors

The combinatorial half of paper Lemma 5.4 (lem:disjoint): two lines through the cube meet only if the corresponding observations share a copied latent ancestor.

theorem TriangleInflation.mem_rootSupport_inl {t : ℕ} {S : Finset (Obs t)} {c : Cell t} : Sum.inl c ∈ rootSupport S ↔ ∃ v ∈ S, onLine v c = true

Membership of a defect cell in the root support.

theorem TriangleInflation.mem_rootSupport_inr {t : ℕ} {S : Finset (Obs t)} {u : Obs t} : Sum.inr u ∈ rootSupport S ↔ u ∈ S

Membership of a private bit in the root support.

theorem TriangleInflation.rootSupport_disjoint {t : ℕ} {S T : Finset (Obs t)} (h : AncestrallyIndependent S T) : Disjoint (rootSupport S) (rootSupport T)

Paper Lemma 5.4 (lem:disjoint), "disjoint inputs": ancestrally independent sets of copied observations read disjoint sets of defect cells and have distinct private bits.

theorem TriangleInflation.disjoint_of_ancestrallyIndependent {t : ℕ} (ht : 1 ≤ t) {S T : Finset (Obs t)} (h : AncestrallyIndependent S T) : Disjoint S T

Ancestrally independent sets of copied observations are disjoint; each observation is its own ancestor's descendant, so an observation in both would share ancestry with itself.

theorem TriangleInflation.restrictAssign_outputsOf_congr {t : ℕ} (S : Finset (Obs t)) (x y : Root t → Bool) (h : ∀ i ∈ rootSupport S, x i = y i) : restrictAssign S (outputsOf x) = restrictAssign S (outputsOf y)

The restriction of the defect-cube outputs to a set of copied observations depends only on the root bits in its root support.

The defect law

theorem TriangleInflation.pushforward_pushforward {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [DecidableEq β] [DecidableEq γ] (w : α → ℝ) (F : α → β) (G : β → γ) : pushforward (pushforward w F) G = pushforward w fun (a : α) => G (F a)

Pushforwards compose.

theorem TriangleInflation.isLaw_bern {r : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) : IsLaw (bern r)

Bern(r) is a law for r ∈ [0,1].

theorem TriangleInflation.isLaw_rootWeight {t : ℕ} {ε s : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (i : Root t) : IsLaw (rootWeight t ε s i)

The per-root weights of the defect cube are laws for ε, s ∈ [0,1].

theorem TriangleInflation.pushforward_defectLaw {t : ℕ} {ε s : ℝ} {γ : Type u_1} [DecidableEq γ] (G : Assign t → γ) : pushforward (defectLaw t ε s) G = pushforward (prodLaw (rootWeight t ε s)) fun (x : Root t → Bool) => G (outputsOf x)

The defect law is the pushforward of the root product weight along a map of root bits.

theorem TriangleInflation.defect_independence {t : ℕ} {ε s : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) {S T : Finset (Obs t)} (h : AncestrallyIndependent S T) : (pushforward (defectLaw t ε s) fun (ω : Assign t) => (restrictAssign S ω, restrictAssign T ω)) = fun (q : (↥S → Bool) × (↥T → Bool)) => pushforward (defectLaw t ε s) (restrictAssign S) q.1 * pushforward (defectLaw t ε s) (restrictAssign T) q.2

Paper Lemma 5.4 (lem:disjoint), independence: under the defect law the outputs of two ancestrally independent sets of copied observations are independent.

theorem TriangleInflation.defect_independence_family {t : ℕ} {ε s : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) {n : ℕ} (S : Fin n → Finset (Obs t)) (h : ∀ (m m' : Fin n), m ≠ m' → AncestrallyIndependent (S m) (S m')) : (pushforward (defectLaw t ε s) fun (ω : Assign t) (m : Fin n) => restrictAssign (S m) ω) = fun (φ : (m : Fin n) → ↥(S m) → Bool) => ∏ m : Fin n, pushforward (defectLaw t ε s) (restrictAssign (S m)) (φ m)

The finite-family form of paper Lemma 5.4, which is what the ancestral-independence prescriptions of Definition 2.4 require.