Stat.RandomGraph
This topic supplies a reusable spanning-parent union bound for expected counts of finite connected components meeting a designated root set under finite product measures.
RootedTree 7 core · 14 supporting This module encodes finite rooted spanning trees as parent functions and proves their product-measure event bound by successive leaf elimination. ★ pi_measure_rooted_tree_event_le
Finite rooted-tree events under product measures
This module encodes finite rooted spanning trees as parent functions and proves their product-measure event bound by successive leaf elimination. It is independent of a particular random-graph model: an injectively embedded finite tree, measurable root and edge events, and uniform child-coordinate section bounds are sufficient.
abbrev ParentEncoding reviewed
⚑ flagged
Causalean.Stat.RandomGraph
A vertex type and root determine the candidate parent encodings: one vertex-valued parent choice for each nonroot vertex.
Definition (Lean source)
parameters
V :
Type u
r :
V
def
ParentEncoding V r :
Type u
given by
{v : V // v ≠ r} → V
def Valid reviewed
⚑ flagged
Causalean.Stat.RandomGraph.ParentEncoding
A parent encoding is valid when a natural-number height is zero at the root and strictly decreases along every parent edge.
Definition (Lean source)
parameters
V :
Type u
V
P :
ParentEncoding V r
def
Valid P :
Prop
given by
∃ height : V → ℕ,
height r = 0
clause 1
v :
height (P v) < height v.val
def step reviewed
⚑ flagged
Causalean.Stat.RandomGraph.ParentEncoding
The parent step for an encoding fixes the root and sends every other vertex to its chosen parent.
Definition (Lean source)
parameters
def
step P v :
V
given by
if h : v = r then r else P ⟨v, h⟩
def graph reviewed
⚑ flagged
Causalean.Stat.RandomGraph.ParentEncoding
The undirected graph of a parent encoding joins distinct vertices when one is the chosen parent of the other.
Definition (Lean source)
def ParentClosed reviewed
⚑ flagged
Causalean.Stat.RandomGraph.ParentEncoding
An active set of nonroot vertices is parent closed for an encoding if every active vertex has its parent at the root or in the active set.
Definition (Lean source)
parameters
def
ParentClosed P A :
Prop
given by
P v = r ∨ ∃ h : P v ≠ r, (⟨P v, h⟩ : {v : V // v ≠ r}) ∈ A
def partialTreeEvent reviewed
⚑ flagged
Causalean.Stat.RandomGraph
The partial rooted-tree event for an embedded tree requires the root event and the edge events of the active nonroot vertices.
Definition (Lean source)
parameters
V :
Type u
W :
Type v
X :
V → Type w
r :
W
e :
W ↪ V
P :
ParentEncoding W r
rootEvent :
Set (X (e r))
edgeEvent :
∀ i j, Set (X i × X j)
A :
Finset {v : W // v ≠ r}
def
given by
{x | x (e r) ∈ rootEvent ∧ ∀ v ∈ A, (x (e v.val), x (e (P v))) ∈ edgeEvent (e v.val) (e (P v))}
theorem pi_measure_rooted_tree_event_le reviewed
⚑ flagged
Causalean.Stat.RandomGraph
Under independent coordinate probability laws, take an embedded parent tree that is valid, a root event and edge events that are measurable, and two bounds α and β. If the root event has probability at most α and for any two distinct coordinates and any value of the second, the values of the first that satisfy their edge event have probability at most β, then the event that the root event and every edge event of the tree occur has probability at most α times β to the power p minus one, where p is the tree's vertex count.
Formal statement
hypotheses
V :
Type u
W :
Type v
X :
V → Type w
Fintype V
Fintype W
μ :
∀ i, Measure (X i)
∀ i, IsProbabilityMeasure (μ i)
r :
W
e :
W ↪ V
P :
ParentEncoding W r
hP :
P.Valid
rootEvent :
Set (X (e r))
edgeEvent :
∀ i j, Set (X i × X j)
α β :
ℝ≥0∞
hroot :
MeasurableSet rootEvent
hedge :
∀ i j, MeasurableSet (edgeEvent i j)
hrootMass :
μ (e r) rootEvent ≤ α
hsection :
∀ (i j : V)
if
i ≠ j
then
∀ y : X j, μ i {z | (z, y) ∈ edgeEvent i j} ≤ β
conclusion
Measure.pi μ (partialTreeEvent e P rootEvent edgeEvent univ)
≤ α * β ^ (card W - 1)
Proof (Lean source)
theorem pi_measure_rooted_tree_event_le [Fintype V] [Fintype W] [DecidableEq W]
(μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)]
{r : W} (e : W ↪ V) (P : ParentEncoding W r) (hP : P.Valid)
(rootEvent : Set (X (e r))) (edgeEvent : ∀ i j, Set (X i × X j))
(α β : ℝ≥0∞) (hroot : MeasurableSet rootEvent)
(hedge : ∀ i j, MeasurableSet (edgeEvent i j)) (hrootMass : μ (e r) rootEvent ≤ α)
(hsection : ∀ (i j : V), i ≠ j → ∀ y : X j,
μ i {z | (z, y) ∈ edgeEvent i j} ≤ β) :
Measure.pi μ (partialTreeEvent e P rootEvent edgeEvent univ) ≤
α * β ^ (card W - 1) := by
have hclosed : P.ParentClosed univ := by
intro v hv
by_cases h : P v = r
· exact inl h
· exact inr ⟨h, Finset.mem_univ _⟩
simpa using pi_measure_partial_tree_event_le μ e P hP rootEvent edgeEvent α β
univ hclosed hroot hedge hrootMass hsection
14 supporting declarations (lemmas, instances)
-
card_parentEncodingtheorem — The number of all candidate parent encodings on a finite vertex type is exactly the number of vertices raised to one less than that number, for a chosen root.hypothesesr :VconclusionProof (Lean source)
theorem card_parentEncoding [Fintype V] [DecidableEq V] (r : V) : card (ParentEncoding V r) = card V ^ (card V - 1) := by rw [Fintype.card_fun] congr 1 simp -
parent_netheorem — In a valid parent encoding, no nonroot vertex is equal to its own chosen parent.hypothesesconclusionP v ≠ v.valProof (Lean source)
theorem ParentEncoding.parent_ne (P : ParentEncoding V r) (hP : P.Valid) (v : {v : V // v ≠ r}) : P v ≠ v.val := by obtain ⟨height, _, hheight⟩ := hP intro h have := hheight v rw [h] at this exact (Nat.lt_irrefl _) this -
iterate_eq_roottheorem — Iterating the parent step in a valid encoding eventually reaches the root from any starting vertex.hypothesesconclusion∃ k : ℕ, (P.step)^[k] v = rProof (Lean source)
theorem ParentEncoding.iterate_eq_root [DecidableEq V] (P : ParentEncoding V r) (hP : P.Valid) (v : V) : ∃ k : ℕ, (P.step)^[k] v = r := by obtain ⟨height, _, hheight⟩ := hP have arrival : ∀ n, ∀ w : V, height w = n → ∃ k : ℕ, (P.step)^[k] w = r := by intro n induction n using Nat.strong_induction_on with | h n ih => intro w hw by_cases hr : w = r · exact ⟨0, hr⟩ · obtain ⟨k, hk⟩ := ih (height (P ⟨w, hr⟩)) (hw ▸ hheight ⟨w, hr⟩) (P ⟨w, hr⟩) rfl refine ⟨k + 1, ?_⟩ simpa [Function.iterate_succ_apply, ParentEncoding.step, hr] using hk exact arrival (height v) v rfl -
isTreetheorem — The graph of a valid parent encoding is a tree.Proof (Lean source)
theorem ParentEncoding.isTree (P : ParentEncoding V r) (hP : P.Valid) : P.graph.IsTree := by classical have stepReach (v : V) : P.graph.Reachable v (P.step v) := by by_cases hv : v = r · simp [ParentEncoding.step, hv] · have ha : P.graph.Adj v (P ⟨v, hv⟩) := ⟨(P.parent_ne hP ⟨v, hv⟩).symm, inl ⟨hv, rfl⟩⟩ simpa [ParentEncoding.step, hv] using ha.reachable have rootReach (v : V) : P.graph.Reachable v r := by obtain ⟨k, hk⟩ := P.iterate_eq_root hP v have reach : ∀ n : ℕ, ∀ w : V, P.graph.Reachable w ((P.step)^[n] w) := by intro n induction n with | zero => intro w; exact SimpleGraph.Reachable.refl w | succ n ih => intro w rw [Function.iterate_succ_apply] exact (stepReach w).trans (ih (P.step w)) simpa [hk] using reach k v refine ⟨?_, ?_⟩ · have : Nonempty V := ⟨r⟩ exact SimpleGraph.Connected.mk (fun u v => (rootReach u).trans (rootReach v).symm) · obtain ⟨height, _, hheight⟩ := hP intro v c hc obtain ⟨l, hl, hmax⟩ := c.support.toFinset.exists_max_image height ⟨v, by simp⟩ have hlc : l ∈ c.support := List.mem_toFinset.mp hl let q := c.rotate l hlc have hq : q.IsCycle := hc.rotate hlc have bound (w : V) (hw : w ∈ q.support) : height w ≤ height l := hmax w (List.mem_toFinset.mpr ((c.mem_support_rotate_iff l hlc).mp hw)) -- At a maximum-height vertex, every cycle neighbor must be its chosen parent. have parent (w : V) (ha : P.graph.Adj l w) (hw : height w ≤ height l) : ∃ h : l ≠ r, P ⟨l, h⟩ = w := by rcases ha.2 with h | ⟨h, he⟩ · exact h · have hlt := hheight ⟨w, h⟩ rw [he] at hlt exact False.elim ((not_lt_of_ge hw) hlt) obtain ⟨hs, hes⟩ := parent q.snd (q.adj_snd hq.not_nil) (bound q.snd (q.getVert_mem_support 1)) obtain ⟨hp, hep⟩ := parent q.penultimate (q.adj_penultimate hq.not_nil).symm (bound q.penultimate (q.getVert_mem_support (q.length - 1))) exact hq.snd_ne_penultimate (hes.symm.trans hep) -
exists_parent_step_closertheorem — In a connected graph, every nonroot vertex has an adjacent vertex exactly one step closer to the root.hypothesesconclusion∃ w : V,conclusion 1G.Adj v.val wconclusion 2G.dist r w + 1 = G.dist r v.valProof (Lean source)
theorem exists_parent_step_closer (G : SimpleGraph V) (hG : G.Connected) (r : V) (v : {v : V // v ≠ r}) : ∃ w : V, G.Adj v.val w ∧ G.dist r w + 1 = G.dist r v.val := by obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist v.val r have hn := p.not_nil_of_ne v.property refine ⟨p.snd, p.adj_snd hn, ?_⟩ have hlow := G.dist_le p.tail obtain ⟨s, hs⟩ := hG.exists_walk_length_eq_dist p.snd r have hupp := G.dist_le (s.cons (p.adj_snd hn)) have hlen := p.length_tail_add_one hn rw [G.dist_comm] at hp hlow rw [SimpleGraph.Walk.length_cons, hs, G.dist_comm (u := p.snd) (v := r), G.dist_comm (u := v.val) (v := r)] at hupp omega -
rooted_spanning_parent_covertheorem — A connected finite graph with a chosen root admits a valid parent encoding using its edges, with at most p to the power p minus one candidates, where p is the number of vertices.hypothesesProof (Lean source)
theorem rooted_spanning_parent_cover [Fintype V] [DecidableEq V] (G : SimpleGraph V) (hG : G.Connected) (r : V) : ∃ P : ParentEncoding V r, P.Valid ∧ (∀ v, G.Adj v.val (P v)) ∧ card (ParentEncoding V r) ≤ card V ^ (card V - 1) := by classical choose P hadj hdist using (fun v => exists_parent_step_closer G hG r v) refine ⟨P, ⟨G.dist r, G.dist_self, ?_⟩, hadj, (card_parentEncoding r).le⟩ intro v rw [← hdist v] exact lt_succ_self _ -
exists_leaftheorem — In a valid parent encoding, every nonempty active set of nonroot vertices contains a vertex that is not the parent of any active vertex.hypothesesconclusion∃ l ∈ A, ∀ v ∈ A, P v ≠ l.valProof (Lean source)
theorem ParentEncoding.exists_leaf (P : ParentEncoding V r) (hP : P.Valid) (A : Finset {v : V // v ≠ r}) (hA : A.Nonempty) : ∃ l ∈ A, ∀ v ∈ A, P v ≠ l.val := by obtain ⟨height, _, hheight⟩ := hP obtain ⟨l, hl, hmax⟩ := A.exists_max_image (fun v => height v.val) hA refine ⟨l, hl, ?_⟩ intro v hv heq have hlt := hheight v rw [heq] at hlt exact (not_lt_of_ge (hmax v hv)) hlt -
parentClosed_erasetheorem — For a parent encoding, deleting from a parent-closed active set of nonroot vertices a vertex that is not the parent of any active vertex leaves a parent-closed set.hypothesesP :ParentEncoding V rA :Finset {v : V // v ≠ r}hA :P.ParentClosed Al :{v : V // v ≠ r}hl :∀ v ∈ A, P v ≠ l.valconclusionP.ParentClosed (A.erase l)Proof (Lean source)
theorem ParentEncoding.parentClosed_erase [DecidableEq V] (P : ParentEncoding V r) (A : Finset {v : V // v ≠ r}) (hA : P.ParentClosed A) (l : {v : V // v ≠ r}) (hl : ∀ v ∈ A, P v ≠ l.val) : P.ParentClosed (A.erase l) := by intro v hv rcases hA v (mem_of_mem_erase hv) with h | ⟨h, hm⟩ · exact inl h · exact inr ⟨h, Finset.mem_erase.mpr ⟨fun he => hl v (mem_of_mem_erase hv) (congrArg val he), hm⟩⟩ -
pi_measure_intersection_le_of_sectiontheorem — Under independent coordinate probability laws, the probability that two events both occur is at most the probability of the first event times β. Here the two events are measurable, the first event does not depend on a chosen coordinate, and β is a number such that, whatever the other coordinates are, the values of the chosen coordinate that put the outcome in the second event have probability at most β.hypothesesV :sharedType uV → Type vμ :∀ i, Measure (X i)∀ i, IsProbabilityMeasure (μ i)i :VA B :Set (∀ i, X i)β :ℝ≥0∞hA :hB :hinvariant :∀ (x : ∀ i, X i) (z : X i), update x i z ∈ A ↔ x ∈ Ahsection :∀ x : ∀ i, X i, μ i {z | update x i z ∈ B} ≤ βconclusionMeasure.pi μ (A ∩ B) ≤ Measure.pi μ A * βProof (Lean source)
theorem pi_measure_intersection_le_of_section (μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)] (i : V) (A B : Set (∀ i, X i)) (β : ℝ≥0∞) (hA : MeasurableSet A) (hB : MeasurableSet B) (hinvariant : ∀ (x : ∀ i, X i) (z : X i), update x i z ∈ A ↔ x ∈ A) (hsection : ∀ x : ∀ i, X i, μ i {z | update x i z ∈ B} ≤ β) : Measure.pi μ (A ∩ B) ≤ Measure.pi μ A * β := by classical have hbound : (∫⁻ x, (A ∩ B).indicator (fun _ => (1 : ℝ≥0∞)) x ∂Measure.pi μ) ≤ ∫⁻ x, A.indicator (fun _ => β) x ∂Measure.pi μ := by apply lintegral_le_of_lmarginal_le {i} (measurable_const.indicator (hA.inter hB)) (measurable_const.indicator hA) rw [lmarginal_singleton, lmarginal_singleton] intro x dsimp only by_cases hx : x ∈ A · have hleft : (fun z => (A ∩ B).indicator (fun _ => (1 : ℝ≥0∞)) (update x i z)) = {z | update x i z ∈ B}.indicator (fun _ => (1 : ℝ≥0∞)) := by funext z simp [indicator, hinvariant x z, hx] have hright : (fun z => A.indicator (fun _ => β) (update x i z)) = (fun _ => β) := by funext z simp [indicator, hinvariant x z, hx] rw [hleft, hright] change (∫⁻ z, {z | update x i z ∈ B}.indicator (fun _ => (1 : ℝ≥0∞)) z ∂μ i) ≤ ∫⁻ (_ : X i), β ∂μ i have hmeas : MeasurableSet {z | update x i z ∈ B} := hB.preimage (measurable_update x (a := i)) rw [lintegral_indicator_const hmeas 1, lintegral_const] simpa using hsection x · have hleft : (fun z => (A ∩ B).indicator (fun _ => (1 : ℝ≥0∞)) (update x i z)) = (fun _ => 0) := by funext z simp [indicator, hinvariant x z, hx] have hright : (fun z => A.indicator (fun _ => β) (update x i z)) = (fun _ => 0) := by funext z simp [indicator, hinvariant x z, hx] rw [hleft, hright] simpa only [lintegral_indicator_const (hA.inter hB), one_mul, lintegral_indicator_const hA, mul_comm β] using hbound -
measurableSet_partialTreeEventtheorem — For an embedded parent tree and an active set of nonroot vertices, a root event and edge events that are measurable give a measurable partial rooted-tree event.hypothesesV :sharedType uW :sharedType vX :sharedV → Type wr :We :W ↪ VP :ParentEncoding W rrootEvent :Set (X (e r))edgeEvent :∀ i j, Set (X i × X j)A :Finset {v : W // v ≠ r}hroot :MeasurableSet rootEventhedge :∀ i j, MeasurableSet (edgeEvent i j)conclusionMeasurableSet (partialTreeEvent e P rootEvent edgeEvent A)Proof (Lean source)
theorem measurableSet_partialTreeEvent {r : W} (e : W ↪ V) (P : ParentEncoding W r) (rootEvent : Set (X (e r))) (edgeEvent : ∀ i j, Set (X i × X j)) (A : Finset {v : W // v ≠ r}) (hroot : MeasurableSet rootEvent) (hedge : ∀ i j, MeasurableSet (edgeEvent i j)) : MeasurableSet (partialTreeEvent e P rootEvent edgeEvent A) := by classical change MeasurableSet ({x : ∀ i, X i | x (e r) ∈ rootEvent} ∩ {x : ∀ i, X i | ∀ v ∈ A, (x (e v.val), x (e (P v))) ∈ edgeEvent (e v.val) (e (P v))}) refine (hroot.preimage (measurable_pi_apply (e r))).inter ?_ have hset : {x : ∀ i, X i | ∀ v ∈ A, (x (e v.val), x (e (P v))) ∈ edgeEvent (e v.val) (e (P v))} = ⋂ v ∈ A, (fun x : ∀ i, X i => (x (e v.val), x (e (P v)))) ⁻¹' edgeEvent (e v.val) (e (P v)) := by ext x simp rw [hset] exact A.measurableSet_biInter (fun v hv => (hedge (e v.val) (e (P v))).preimage ((measurable_pi_apply (e v.val)).prodMk (measurable_pi_apply (e (P v))))) -
partialTreeEvent_erase_intertheorem — For any vertex in the active set, the partial tree event is exactly the partial tree event of the active set with that vertex removed, intersected with the edge event joining that vertex to its parent.hypothesesV :sharedType uW :sharedType vX :sharedV → Type wr :We :W ↪ VP :ParentEncoding W rrootEvent :Set (X (e r))edgeEvent :∀ i j, Set (X i × X j)A :Finset {v : W // v ≠ r}l :{v : W // v ≠ r}hl :l ∈ AconclusionpartialTreeEvent e P rootEvent edgeEvent A= partialTreeEvent e P rootEvent edgeEvent (A.erase l) ∩ {x | (x (e l.val), x (e (P l))) ∈ edgeEvent (e l.val) (e (P l))}Proof (Lean source)
theorem partialTreeEvent_erase_inter [DecidableEq W] {r : W} (e : W ↪ V) (P : ParentEncoding W r) (rootEvent : Set (X (e r))) (edgeEvent : ∀ i j, Set (X i × X j)) (A : Finset {v : W // v ≠ r}) (l : {v : W // v ≠ r}) (hl : l ∈ A) : partialTreeEvent e P rootEvent edgeEvent A = partialTreeEvent e P rootEvent edgeEvent (A.erase l) ∩ {x | (x (e l.val), x (e (P l))) ∈ edgeEvent (e l.val) (e (P l))} := by ext x constructor · intro hx exact ⟨⟨hx.1, fun v hv => hx.2 v (mem_of_mem_erase hv)⟩, hx.2 l hl⟩ · rintro ⟨hx, hedge⟩ refine ⟨hx.1, fun v hv => ?_⟩ by_cases h : v = l · subst v exact hedge · exact hx.2 v (Finset.mem_erase.mpr ⟨h, hv⟩) -
partialTreeEvent_update_erasetheorem — After deleting from the active set of an embedded partial tree a vertex that is not the parent of any active vertex, membership in the remaining partial tree event is unaffected by replacing the deleted vertex's coordinate, for every outcome and replacement value.hypothesesV :sharedType uW :sharedType vX :sharedV → Type wr :We :W ↪ VP :ParentEncoding W rrootEvent :Set (X (e r))edgeEvent :∀ i j, Set (X i × X j)A :Finset {v : W // v ≠ r}l :{v : W // v ≠ r}hleaf :∀ v ∈ A, P v ≠ l.valx :∀ i, X iz :X (e l.val)conclusionupdate x (e l.val) z ∈ partialTreeEvent e P rootEvent edgeEvent (A.erase l)↔ x ∈ partialTreeEvent e P rootEvent edgeEvent (A.erase l)Proof (Lean source)
theorem partialTreeEvent_update_erase [DecidableEq V] [DecidableEq W] {r : W} (e : W ↪ V) (P : ParentEncoding W r) (rootEvent : Set (X (e r))) (edgeEvent : ∀ i j, Set (X i × X j)) (A : Finset {v : W // v ≠ r}) (l : {v : W // v ≠ r}) (hleaf : ∀ v ∈ A, P v ≠ l.val) (x : ∀ i, X i) (z : X (e l.val)) : update x (e l.val) z ∈ partialTreeEvent e P rootEvent edgeEvent (A.erase l) ↔ x ∈ partialTreeEvent e P rootEvent edgeEvent (A.erase l) := by have hr : e r ≠ e l.val := fun h => l.property (e.injective h).symm have hv : ∀ v ∈ A.erase l, e v.val ≠ e l.val := by intro v hv h exact (Finset.mem_erase.mp hv).1 (Subtype.ext (e.injective h)) have hp : ∀ v ∈ A.erase l, e (P v) ≠ e l.val := by intro v hv h exact hleaf v (mem_of_mem_erase hv) (e.injective h) simp only [partialTreeEvent, Set.mem_ofPred_eq, Function.update_of_ne hr] constructor <;> rintro ⟨hroot, hedge⟩ <;> refine ⟨hroot, fun v hmem => ?_⟩ · simpa only [Function.update_of_ne (hv v hmem), Function.update_of_ne (hp v hmem)] using hedge v hmem · simpa only [Function.update_of_ne (hv v hmem), Function.update_of_ne (hp v hmem)] using hedge v hmem -
pi_measure_partialTreeEvent_emptytheorem — Under coordinate probability laws, the partial tree with no active edges has exactly the mass of its measurable root event, for measurable root events.hypothesesV :sharedType uW :sharedType vX :sharedV → Type wFintype Vμ :∀ i, Measure (X i)∀ i, IsProbabilityMeasure (μ i)r :We :W ↪ VP :ParentEncoding W rrootEvent :Set (X (e r))edgeEvent :∀ i j, Set (X i × X j)hroot :MeasurableSet rootEventconclusionMeasure.pi μ (partialTreeEvent e P rootEvent edgeEvent ∅) = μ (e r) rootEventProof (Lean source)
theorem pi_measure_partialTreeEvent_empty [Fintype V] (μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)] {r : W} (e : W ↪ V) (P : ParentEncoding W r) (rootEvent : Set (X (e r))) (edgeEvent : ∀ i j, Set (X i × X j)) (hroot : MeasurableSet rootEvent) : Measure.pi μ (partialTreeEvent e P rootEvent edgeEvent ∅) = μ (e r) rootEvent := by have hevent : partialTreeEvent e P rootEvent edgeEvent ∅ = Function.eval (e r) ⁻¹' rootEvent := by ext x simp [partialTreeEvent, Function.eval] rw [hevent] exact (measurePreserving_eval μ (e r)).measure_preimage hroot.nullMeasurableSet -
pi_measure_partial_tree_event_letheorem — Under independent coordinate probability laws, take an embedded parent tree that is valid, a root event and edge events that are measurable, two bounds α and β, and an active set of nonroot vertices that is parent closed. If the root event has probability at most α and for any two distinct coordinates and any value of the second, the values of the first that satisfy their edge event have probability at most β, then the partial tree event has probability at most α times β raised to the number of active vertices.hypothesesV :sharedType uW :sharedType vX :sharedV → Type wFintype Vμ :∀ i, Measure (X i)∀ i, IsProbabilityMeasure (μ i)r :We :W ↪ VP :ParentEncoding W rhP :P.ValidrootEvent :Set (X (e r))edgeEvent :∀ i j, Set (X i × X j)α β :ℝ≥0∞A :Finset {v : W // v ≠ r}hA :P.ParentClosed Ahroot :MeasurableSet rootEventhedge :∀ i j, MeasurableSet (edgeEvent i j)hrootMass :μ (e r) rootEvent ≤ αhsection :∀ (i j : V)ifi ≠ jthen∀ y : X j, μ i {z | (z, y) ∈ edgeEvent i j} ≤ βconclusionMeasure.pi μ (partialTreeEvent e P rootEvent edgeEvent A) ≤ α * β ^ A.cardProof (Lean source)
theorem pi_measure_partial_tree_event_le [Fintype V] (μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)] {r : W} (e : W ↪ V) (P : ParentEncoding W r) (hP : P.Valid) (rootEvent : Set (X (e r))) (edgeEvent : ∀ i j, Set (X i × X j)) (α β : ℝ≥0∞) (A : Finset {v : W // v ≠ r}) (hA : P.ParentClosed A) (hroot : MeasurableSet rootEvent) (hedge : ∀ i j, MeasurableSet (edgeEvent i j)) (hrootMass : μ (e r) rootEvent ≤ α) (hsection : ∀ (i j : V), i ≠ j → ∀ y : X j, μ i {z | (z, y) ∈ edgeEvent i j} ≤ β) : Measure.pi μ (partialTreeEvent e P rootEvent edgeEvent A) ≤ α * β ^ A.card := by classical induction A using Finset.strongInductionOn with | _ A ih => by_cases hempty : A = ∅ · subst A simpa only [pi_measure_partialTreeEvent_empty μ e P rootEvent edgeEvent hroot, Finset.card_empty, pow_zero, mul_one] using hrootMass · obtain ⟨l, hl, hleaf⟩ := P.exists_leaf hP A (Finset.nonempty_iff_ne_empty.mpr hempty) have hparent : e (P l) ≠ e l.val := fun h => P.parent_ne hP l (e.injective h) have hstep : Measure.pi μ (partialTreeEvent e P rootEvent edgeEvent A) ≤ Measure.pi μ (partialTreeEvent e P rootEvent edgeEvent (A.erase l)) * β := by rw [partialTreeEvent_erase_inter e P rootEvent edgeEvent A l hl] apply pi_measure_intersection_le_of_section μ (e l.val) (partialTreeEvent e P rootEvent edgeEvent (A.erase l)) {x | (x (e l.val), x (e (P l))) ∈ edgeEvent (e l.val) (e (P l))} β (measurableSet_partialTreeEvent e P rootEvent edgeEvent (A.erase l) hroot hedge) ((hedge (e l.val) (e (P l))).preimage ((measurable_pi_apply (e l.val)).prodMk (measurable_pi_apply (e (P l))))) (partialTreeEvent_update_erase e P rootEvent edgeEvent A l hleaf) intro x simpa only [Set.mem_ofPred_eq, Function.update_self, Function.update_of_ne hparent] using hsection (e l.val) (e (P l)) hparent.symm (x (e (P l))) calc Measure.pi μ (partialTreeEvent e P rootEvent edgeEvent A) ≤ Measure.pi μ (partialTreeEvent e P rootEvent edgeEvent (A.erase l)) * β := hstep _ ≤ (α * β ^ (A.erase l).card) * β := mul_le_mul_left (ih (A.erase l) (Finset.erase_ssubset hl) (P.parentClosed_erase A hA l hleaf)) β _ = α * β ^ A.card := by rw [← Finset.card_erase_add_one hl, pow_succ, mul_assoc]
Components 9 core · 7 supporting Coordinate-local, symmetric measurable edge events define a random simple graph. ★ labeledComponentCount_le_treeWitnessCount
Root-qualified component counts and their finite witness cover
Coordinate-local, symmetric measurable edge events define a random simple graph. Components are counted once by their vertex sets. A component qualifies only if it contains a distinguished root whose coordinate satisfies its root event. Its spanning-parent witnesses are enumerated by a root, an unordered selection of remaining vertices, and a candidate parent array.
This avoids assuming edge independence: edges sharing coordinates may be dependent. The parent witness count may overcount components and is used only as an upper bound.
structure CoordinateGraph reviewed
⚑ flagged
Causalean.Stat.RandomGraph
Coordinate spaces determine a measurable symmetric edge-event model, where an edge depends only on its two endpoint coordinates.
Definition (Lean source)
parameters
V :
Type u
X :
V → Type v
∀ i, MeasurableSpace (X i)
fields
The event for an oriented pair of endpoint coordinates.
edgeEvent :
∀ i j, Set (X i × X j)
Every pair event is measurable in the product endpoint space.
measurable_edgeEvent :
∀ i j, MeasurableSet (edgeEvent i j)
Reversing endpoints leaves the undirected edge event unchanged.
symmetric :
∀ i j (z : X i) (y : X j), (z, y) ∈ edgeEvent i j ↔ (y, z) ∈ edgeEvent j i
def graph reviewed
⚑ flagged
Causalean.Stat.RandomGraph.CoordinateGraph
An edge-event model and coordinate outcome determine the simple graph of occurring edges.
Definition (Lean source)
parameters
def
def IsComponent reviewed
⚑ flagged
Causalean.Stat.RandomGraph
A finite vertex set is a component of a graph when its induced graph is connected and all neighbors of its vertices stay in that set.
Definition (Lean source)
parameters
def
IsComponent G S :
Prop
def selectedEmbedding reviewed
⚑ flagged
Causalean.Stat.RandomGraph
The inclusion embedding of a selected finite vertex set sends each selected vertex to the ambient population.
Definition (Lean source)
parameters
V :
Type u
S :
Finset V
def
selectedEmbedding S :
S ↪ V
given by
⟨Subtype.val, Subtype.val_injective⟩
def componentEvent reviewed
⚑ flagged
Causalean.Stat.RandomGraph
The qualified component event for an edge model, distinguished roots, coordinate root events, and vertex set is the set of coordinate outcomes at which that vertex set is a component of the outcome's graph and contains at least one distinguished root whose root event occurs.
Definition (Lean source)
parameters
def
given by
{x | IsComponent (M.graph x) S ∧ ∃ r ∈ R, r ∈ S ∧ x r ∈ rootEvent r}
def labeledComponentCount reviewed
⚑ flagged
Causalean.Stat.RandomGraph
The labeled component count for an edge model, roots, root events, size, and outcome counts each qualifying size-p component of the outcome's graph once, irrespective of how many qualifying roots it contains.
Definition (Lean source)
parameters
def
labeledComponentCount M R rootEvent p x :
ℝ
given by
by classical exact ∑ S ∈ (Finset.univ : Finset V).powersetCard p, if x ∈ componentEvent M R rootEvent S then (1 : ℝ) else 0
def rootTreeWitnessCount reviewed
⚑ flagged
Causalean.Stat.RandomGraph
The rooted witness count on a root and completion set, for an edge model, root events, and outcome, is the number of valid parent encodings of the root together with the completion set, rooted at that root, for which the root's event occurs at the outcome and so does the edge event joining every nonroot vertex to its chosen parent.
Definition (Lean source)
parameters
def
rootTreeWitnessCount M rootEvent r T x :
ℝ
given by
by classical let s : Finset V := insert r T let root : s := ⟨r, Finset.mem_insert_self r T⟩ exact ∑ P : ParentEncoding s root, if P.Valid ∧
def treeWitnessCount reviewed
⚑ flagged
Causalean.Stat.RandomGraph
The total witness count enumerates distinguished roots, unordered selections of p minus one other vertices, and parent arrays, for an edge model, root events, size, and outcome.
Definition (Lean source)
parameters
def
treeWitnessCount M R rootEvent p x :
ℝ
given by
∑ r ∈ R, ∑ T ∈ ((Finset.univ : Finset V).erase r).powersetCard (p - 1), rootTreeWitnessCount M rootEvent r T x
theorem labeledComponentCount_le_treeWitnessCount reviewed
⚑ flagged
Causalean.Stat.RandomGraph
For an edge model, distinguished roots, root events, and a component size, the labeled component count is at most the total rooted witness count at every outcome.
Formal statement
hypotheses
conclusion
labeledComponentCount M R rootEvent p x ≤ treeWitnessCount M R rootEvent p x
Proof (Lean source)
theorem labeledComponentCount_le_treeWitnessCount [Fintype V] [DecidableEq V]
(M : CoordinateGraph X) (R : Finset V)
(rootEvent : ∀ r, Set (X r)) (p : ℕ) (x : ∀ i, X i) :
labeledComponentCount M R rootEvent p x ≤ treeWitnessCount M R rootEvent p x := by
classical
-- Use the same equality decision procedure as the dependent witness-count definition.
cases Subsingleton.elim (inferInstance : DecidableEq V) (Classical.decEq V)
let source := ((Finset.univ : Finset V).powersetCard p).filter
(fun S => x ∈ componentEvent M R rootEvent S)
let A := {S : Finset V // S ∈ source}
have hA (S : A) : S.val.card = p ∧ x ∈ componentEvent M R rootEvent S.val := by
have h := Finset.mem_filter.mp S.property
exact ⟨(Finset.mem_powersetCard.mp h.1).2, h.2⟩
let root (S : A) : V :=
(component_event_parent_cover M R rootEvent S.val x (hA S).2).choose
have hroot (S : A) : root S ∈ R ∧ ∃ hr : root S ∈ S.val,
∃ P : ParentEncoding S.val (⟨root S, hr⟩ : S.val),
P.Valid ∧ x ∈ partialTreeEvent (selectedEmbedding S.val) P
(rootEvent (root S)) M.edgeEvent Finset.univ :=
(component_event_parent_cover M R rootEvent S.val x (hA S).2).choose_spec
let slots := R.sigma (fun r => ((Finset.univ : Finset V).erase r).powersetCard (p - 1))
let e (S : A) : Σ _ : V, Finset V := ⟨root S, S.val.erase (root S)⟩
-- Reinsert the chosen root to recover the component, proving slot injectivity.
have hrecover (S : A) : insert (root S) (S.val.erase (root S)) = S.val :=
Finset.insert_erase (hroot S).2.choose
have hinj : Injective e := by
intro S U h
apply Subtype.ext
calc
S.val = insert (e S).1 (e S).2 := (hrecover S).symm
_ = insert (e U).1 (e U).2 := congrArg (fun q => insert q.1 q.2) h
_ = U.val := hrecover U
have hslot (S : A) : e S ∈ slots := by
refine Finset.mem_sigma.mpr ⟨(hroot S).1, Finset.mem_powersetCard.mpr ⟨?_, ?_⟩⟩
· intro v hv
exact Finset.mem_erase.mpr ⟨(Finset.mem_erase.mp hv).1, Finset.mem_univ v⟩
· rw [Finset.card_erase_of_mem (hroot S).2.choose, (hA S).1]
-- Every parent-array summand is nonnegative, and the selected witness contributes one.
have hnonneg (r : V) (T : Finset V) : 0 ≤ rootTreeWitnessCount M rootEvent r T x := by
unfold rootTreeWitnessCount
exact Finset.sum_nonneg fun P _ => by split_ifs <;> norm_num
have hone (S : A) : 1 ≤ rootTreeWitnessCount M rootEvent (root S)
(S.val.erase (root S)) x := by
-- Transport the witness before unfolding the sum over its dependent parent type.
have hex (s : Finset V) (hs : s = S.val) : ∃ hr : root S ∈ s,
∃ P : ParentEncoding s (⟨root S, hr⟩ : s),
P.Valid ∧ x ∈ partialTreeEvent (selectedEmbedding s) P
(rootEvent (root S)) M.edgeEvent Finset.univ := by
subst s
exact (hroot S).2
obtain ⟨hr, P, hP⟩ := hex _ (hrecover S)
unfold rootTreeWitnessCount
dsimp only
have hterm : (if P.Valid ∧ x ∈ partialTreeEvent
(selectedEmbedding (insert (root S) (S.val.erase (root S)))) P
(rootEvent (root S)) M.edgeEvent Finset.univ then (1 : ℝ) else 0) = 1 :=
if_pos hP
conv_lhs => rw [← hterm]
exact Finset.single_le_sum
(f := fun Q : ParentEncoding ↥(insert (root S) (S.val.erase (root S))) ⟨root S, hr⟩ =>
if Q.Valid ∧ x ∈ partialTreeEvent
(selectedEmbedding (insert (root S) (S.val.erase (root S)))) Q
(rootEvent (root S)) M.edgeEvent Finset.univ then (1 : ℝ) else 0)
(fun Q _ => by split_ifs <;> norm_num) (Finset.mem_univ P)
have hcount : labeledComponentCount M R rootEvent p x = ∑ _S : A, (1 : ℝ) := by
unfold labeledComponentCount
rw [← Finset.sum_filter]
exact Finset.sum_subtype source (fun _ => Iff.rfl) (fun _ => (1 : ℝ))
rw [hcount]
change (∑ _S : A, (1 : ℝ)) ≤ ∑ r ∈ R,
∑ T ∈ ((Finset.univ : Finset V).erase r).powersetCard (p - 1),
rootTreeWitnessCount M rootEvent r T x
rw [Finset.sum_sigma']
let g (q : Σ _ : V, Finset V) : ℝ := rootTreeWitnessCount M rootEvent q.1 q.2 x
calc
(∑ _S : A, (1 : ℝ)) ≤ ∑ S : A, g (e S) :=
Finset.sum_le_sum (fun S _ => hone S)
_ = ∑ q ∈ Finset.univ.image e, g q :=
(Finset.sum_image (fun _ _ _ _ h => hinj h)).symm
_ ≤ ∑ q ∈ slots, g q := Finset.sum_le_sum_of_subset_of_nonneg
(by intro q hq; obtain ⟨S, _, rfl⟩ := Finset.mem_image.mp hq; exact hslot S)
(fun q _ _ => hnonneg q.1 q.2)
7 supporting declarations (lemmas, instances)
-
measurableSet_graph_eqtheorem — With finitely many vertices, the event that a coordinate edge model equals a specified graph is measurable.hypothesesconclusionMeasurableSet {x | M.graph x = G}Proof (Lean source)
theorem CoordinateGraph.measurableSet_graph_eq [Finite V] (M : CoordinateGraph X) (G : SimpleGraph V) : MeasurableSet {x | M.graph x = G} := by classical have heq : {x | M.graph x = G} = ⋂ i : V, ⋂ j : V, {x | (i ≠ j ∧ (x i, x j) ∈ M.edgeEvent i j) ↔ G.Adj i j} := by ext x simp only [Set.mem_ofPred_eq, Set.mem_iInter] constructor · intro h i j change (M.graph x).Adj i j ↔ G.Adj i j rw [h] · intro h ext i j exact h i j rw [heq] apply MeasurableSet.iInter intro i apply MeasurableSet.iInter intro j exact ((MeasurableSet.const (i ≠ j)).inter ((M.measurable_edgeEvent i j).preimage ((measurable_pi_apply i).prodMk (measurable_pi_apply j)))).iff (MeasurableSet.const (G.Adj i j)) -
isComponent_iff_exists_connectedComponenttheorem — The finite-set component predicate is equivalent to being the support of a connected component in Mathlib.hypothesesconclusionIsComponent G S ↔ ∃ C : G.ConnectedComponent, C.supp = (S : Set V)Proof (Lean source)
theorem isComponent_iff_exists_connectedComponent (G : SimpleGraph V) (S : Finset V) : IsComponent G S ↔ ∃ C : G.ConnectedComponent, C.supp = (S : Set V) := by constructor · rintro ⟨hconn, hclosed⟩ obtain ⟨r⟩ := hconn.nonempty refine ⟨G.connectedComponentMk r.val, ?_⟩ ext v rw [SimpleGraph.ConnectedComponent.mem_supp_iff, SimpleGraph.ConnectedComponent.eq] constructor · rintro ⟨w⟩ -- Neighbor closure propagates membership from the start of every walk. have hwalk : ∀ {a b : V}, G.Walk a b → a ∈ S → b ∈ S := by intro a b w induction w with | nil => exact id | cons hadj w ih => exact fun ha => ih (hclosed _ ha _ hadj) exact hwalk w.reverse r.property · intro hv exact (hconn.preconnected (⟨v, hv⟩ : (S : Set V)) r).map ⟨Subtype.val, fun h => h⟩ · rintro ⟨C, hC⟩ refine ⟨?_, ?_⟩ · have hconn := C.connected_toSimpleGraph change (G.induce C.supp).Connected at hconn rwa [hC] at hconn · intro i hi j hadj have hiC : i ∈ C.supp := by simpa [hC] using hi simpa [hC] using C.mem_supp_of_adj_mem_supp hiC hadj -
component_event_parent_covertheorem — For an edge model, distinguished roots, root events, a vertex set, and an outcome, whenever the vertex set is a qualifying component at that outcome, some distinguished root in the set whose root event occurs carries a valid parent encoding of the set, rooted there, all of whose edge events occur.hypothesesM :R :Finset VrootEvent :∀ r, Set (X r)S :Finset Vx :∀ i, X ihcomponent :x ∈ componentEvent M R rootEvent Sconclusion∃ r ∈ R, ∃ hr : r ∈ S, ∃ P : ParentEncoding S (⟨r, hr⟩ : S),conclusion 1P.Validconclusion 2Proof (Lean source)
theorem component_event_parent_cover [DecidableEq V] (M : CoordinateGraph X) (R : Finset V) (rootEvent : ∀ r, Set (X r)) (S : Finset V) (x : ∀ i, X i) (hcomponent : x ∈ componentEvent M R rootEvent S) : ∃ r ∈ R, ∃ hr : r ∈ S, ∃ P : ParentEncoding S (⟨r, hr⟩ : S), P.Valid ∧ x ∈ partialTreeEvent (selectedEmbedding S) P (rootEvent r) M.edgeEvent univ := by classical obtain ⟨hS, r, hrR, hrS, hroot⟩ := hcomponent obtain ⟨P, hP, hadj, _⟩ := rooted_spanning_parent_cover ((M.graph x).induce (S : Set V)) hS.1 (⟨r, hrS⟩ : S) refine ⟨r, hrR, hrS, P, hP, hroot, ?_⟩ intro v _ exact (hadj v).2 -
measurableSet_componentEventtheorem — A qualified component event is measurable when the coordinate root events are measurable.hypothesesV :sharedType uV → Type vFinite VM :R :Finset VrootEvent :∀ r, Set (X r)S :Finset Vhroot :∀ r, MeasurableSet (rootEvent r)conclusionMeasurableSet (componentEvent M R rootEvent S)Proof (Lean source)
theorem measurableSet_componentEvent [Finite V] (M : CoordinateGraph X) (R : Finset V) (rootEvent : ∀ r, Set (X r)) (S : Finset V) (hroot : ∀ r, MeasurableSet (rootEvent r)) : MeasurableSet (componentEvent M R rootEvent S) := by classical have hgraph : {x | IsComponent (M.graph x) S} = ⋃ G : SimpleGraph V, {x | M.graph x = G} ∩ {x | IsComponent G S} := by ext x simp only [Set.mem_ofPred_eq, Set.mem_iUnion, Set.mem_inter_iff] constructor · intro h exact ⟨M.graph x, rfl, h⟩ · rintro ⟨G, hG, h⟩ simpa only [hG] using h have hgraphMeas : MeasurableSet {x | IsComponent (M.graph x) S} := by rw [hgraph] exact MeasurableSet.iUnion fun G => (M.measurableSet_graph_eq G).inter (MeasurableSet.const (IsComponent G S)) have hroots : {x : ∀ i, X i | ∃ r ∈ R, r ∈ S ∧ x r ∈ rootEvent r} = ⋃ r ∈ R, {x : ∀ i, X i | r ∈ S} ∩ {x | x r ∈ rootEvent r} := by ext x simp [and_left_comm] change MeasurableSet ({x | IsComponent (M.graph x) S} ∩ {x | ∃ r ∈ R, r ∈ S ∧ x r ∈ rootEvent r}) rw [hroots] exact hgraphMeas.inter (R.measurableSet_biUnion fun r hr => (MeasurableSet.const (r ∈ S)).inter ((hroot r).preimage (measurable_pi_apply r))) -
measurable_labeledComponentCounttheorem — The finite component count is measurable for measurable coordinate root events.hypothesesconclusionMeasurable (labeledComponentCount M R rootEvent p)Proof (Lean source)
@[fun_prop] theorem measurable_labeledComponentCount [Fintype V] (M : CoordinateGraph X) (R : Finset V) (rootEvent : ∀ r, Set (X r)) (p : ℕ) (hroot : ∀ r, MeasurableSet (rootEvent r)) : Measurable (labeledComponentCount M R rootEvent p) := by classical unfold labeledComponentCount apply Finset.measurable_sum intro S hS apply Measurable.ite (measurableSet_componentEvent M R rootEvent S hroot) measurable_const measurable_const -
labeledComponentCount_boundstheorem — The component count lies between zero and the number of size-p subsets of the population.hypothesesProof (Lean source)
theorem labeledComponentCount_bounds [Fintype V] (M : CoordinateGraph X) (R : Finset V) (rootEvent : ∀ r, Set (X r)) (p : ℕ) (x : ∀ i, X i) : 0 ≤ labeledComponentCount M R rootEvent p x ∧ labeledComponentCount M R rootEvent p x ≤ (choose (card V) p : ℝ) := by classical unfold labeledComponentCount constructor · exact Finset.sum_nonneg fun S _ => by by_cases h : x ∈ componentEvent M R rootEvent S <;> simp [h] · calc (∑ S ∈ (Finset.univ : Finset V).powersetCard p, if x ∈ componentEvent M R rootEvent S then (1 : ℝ) else 0) ≤ ∑ _S ∈ (Finset.univ : Finset V).powersetCard p, (1 : ℝ) := by apply Finset.sum_le_sum intro S hS by_cases h : x ∈ componentEvent M R rootEvent S <;> simp [h] _ = (choose (card V) p : ℝ) := by simp -
integrable_labeledComponentCounttheorem — The finite component count is integrable under coordinate probability laws, for measurable root events.hypothesesμ :∀ i, Measure (X i)∀ i, IsProbabilityMeasure (μ i)M :R :Finset VrootEvent :∀ r, Set (X r)p :ℕhroot :∀ r, MeasurableSet (rootEvent r)conclusionIntegrable (labeledComponentCount M R rootEvent p) (Measure.pi μ)Proof (Lean source)
theorem integrable_labeledComponentCount [Fintype V] (μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)] (M : CoordinateGraph X) (R : Finset V) (rootEvent : ∀ r, Set (X r)) (p : ℕ) (hroot : ∀ r, MeasurableSet (rootEvent r)) : Integrable (labeledComponentCount M R rootEvent p) (Measure.pi μ) := by exact (integrable_const (choose (card V) p : ℝ)).mono_nonneg (measurable_labeledComponentCount M R rootEvent p hroot).aestronglyMeasurable (Filter.Eventually.of_forall fun x => (labeledComponentCount_bounds M R rootEvent p x).1) (Filter.Eventually.of_forall fun x => (labeledComponentCount_bounds M R rootEvent p x).2)
Expectation 1 core · 6 supporting The final estimate combines root choices, unordered completion choices, the parent-array envelope, and the fixed-tree probability bound. ★ expected_labeled_component_count_le
Expected numbers of root-qualified finite components
The final estimate combines root choices, unordered completion choices, the parent-array envelope, and the fixed-tree probability bound. The count includes only components containing a distinguished root satisfying its measurable root event. Constants are real and nonnegative; the underlying event estimates use extended nonnegative measures.
Reference grounding: the spanning-tree union-bound argument appears in Lemma 4.14 of the 2014 draft of Foundations of Data Science (Hopcroft, Kannan), https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/book-No-Solutions-Aug-21-2014.pdf . That reference concerns independent edges. Here the edge factors are instead justified by coordinate-section Tonelli elimination; no edge independence is assumed. We count all parent arrays rather than using Cayley's sharper enumeration. The primary PDF was fetched and the lemma and its proof on printed pages 116--117 were checked on 2026-10-01; the proof explicitly covers connectivity by the union of spanning-tree events. We discard its additional isolation factor, so it supplies context rather than a premise. Penrose's Random Geometric Graphs, Chapter 3, is the geometric context; its publisher-hosted chapter was not accessible.
theorem expected_labeled_component_count_le reviewed
⚑ flagged
Causalean.Stat.RandomGraph
For an edge model, distinguished roots, root events, a size p that is at least two, and constants α and β that are nonnegative, under independent coordinate probability laws with measurable root events, root-event probabilities at most α, and oriented child-section probabilities at most β for distinct coordinates, the expected number of size-p components containing a distinguished root satisfying its root event is at most n times choose(N minus one, p minus one) times p to the power p minus one times α times β to the power p minus one. Here n is the root-set size and N the population size.
Formal statement
hypotheses
V :
Type u
V → Type v
μ :
∀ i, Measure (X i)
∀ i, IsProbabilityMeasure (μ i)
M :
R :
Finset V
rootEvent :
∀ r, Set (X r)
p :
ℕ
hp :
2 ≤ p
α β :
ℝ
hα :
0 ≤ α
hβ :
0 ≤ β
hroot :
∀ r, MeasurableSet (rootEvent r)
hrootMass :
∀ r ∈ R, μ r (rootEvent r) ≤ ofReal α
hsection :
∀ (i j : V)
if
i ≠ j
then
∀ y : X j, μ i {z | (z, y) ∈ M.edgeEvent i j} ≤ ofReal β
conclusion
(∫ x, labeledComponentCount M R rootEvent p x ∂Measure.pi μ)
Proof (Lean source)
theorem expected_labeled_component_count_le
(μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)]
(M : CoordinateGraph X) (R : Finset V) (rootEvent : ∀ r, Set (X r))
(p : ℕ) (hp : 2 ≤ p) (α β : ℝ) (hα : 0 ≤ α) (hβ : 0 ≤ β)
(hroot : ∀ r, MeasurableSet (rootEvent r))
(hrootMass : ∀ r ∈ R, μ r (rootEvent r) ≤ ofReal α)
(hsection : ∀ (i j : V), i ≠ j → ∀ y : X j,
μ i {z | (z, y) ∈ M.edgeEvent i j} ≤ ofReal β) :
(∫ x, labeledComponentCount M R rootEvent p x ∂Measure.pi μ) ≤
(R.card : ℝ) * (choose (card V - 1) (p - 1) : ℝ) *
(p : ℝ) ^ (p - 1) * α * β ^ (p - 1) := by
classical
have hp1 : 1 ≤ p := le_trans (by decide : 1 ≤ 2) hp
exact (integral_mono (integrable_labeledComponentCount μ M R rootEvent p hroot)
(integrable_treeWitnessCount μ M R rootEvent p hroot)
(labeledComponentCount_le_treeWitnessCount M R rootEvent p)).trans
(integral_treeWitnessCount_le μ M R rootEvent p hp1 α β hα hβ hroot hrootMass hsection)
6 supporting declarations (lemmas, instances)
-
card_root_completionstheorem — For a root, the number of unordered completion sets of size p minus one is the population size minus one choose p minus one.hypothesesProof (Lean source)
theorem card_root_completions [DecidableEq V] (r : V) (p : ℕ) : (((Finset.univ : Finset V).erase r).powersetCard (p - 1)).card = choose (card V - 1) (p - 1) := by simp -
card_insert_root_of_mem_completionstheorem — For p at least one, adjoining the root to a completion set of size p minus one gives a selected set of size p.Proof (Lean source)
theorem card_insert_root_of_mem_completions [DecidableEq V] (r : V) (p : ℕ) (hp : 1 ≤ p) (T : Finset V) (hT : T ∈ ((Finset.univ : Finset V).erase r).powersetCard (p - 1)) : (insert r T).card = p := by obtain ⟨hsub, hcard⟩ := Finset.mem_powersetCard.mp hT have hr : r ∉ T := fun h => (Finset.mem_erase.mp (hsub h)).1 rfl rw [Finset.card_insert_of_notMem hr, hcard] exact Nat.sub_add_cancel hp -
integrable_rootTreeWitnessCounttheorem — The witness count for one root and completion set is integrable under coordinate probability laws, provided the root event is measurable.hypothesesV :sharedType uV → Type vμ :∀ i, Measure (X i)∀ i, IsProbabilityMeasure (μ i)M :rootEvent :∀ r, Set (X r)r :VT :Finset Vhroot :MeasurableSet (rootEvent r)conclusionIntegrable (rootTreeWitnessCount M rootEvent r T) (Measure.pi μ)Proof (Lean source)
@[fun_prop] theorem integrable_rootTreeWitnessCount (μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)] (M : CoordinateGraph X) (rootEvent : ∀ r, Set (X r)) (r : V) (T : Finset V) (hroot : MeasurableSet (rootEvent r)) : Integrable (rootTreeWitnessCount M rootEvent r T) (Measure.pi μ) := by classical unfold rootTreeWitnessCount dsimp only apply integrable_finsetSum intro P hP by_cases hv : P.Valid · simp only [hv, true_and] have hm := measurableSet_partialTreeEvent (selectedEmbedding _) P (rootEvent r) M.edgeEvent univ hroot M.measurable_edgeEvent apply (integrable_const (1 : ℝ)).mono_nonneg · exact (Measurable.ite hm measurable_const measurable_const).aestronglyMeasurable · exact Filter.Eventually.of_forall (fun x => by split_ifs <;> norm_num) · exact Filter.Eventually.of_forall (fun x => by split_ifs <;> norm_num) · simp only [hv, false_and, ite_false] exact integrable_const 0 -
integrable_treeWitnessCounttheorem — The rooted witness count is integrable under coordinate probability laws when root events are measurable.hypothesesμ :∀ i, Measure (X i)∀ i, IsProbabilityMeasure (μ i)M :R :Finset VrootEvent :∀ r, Set (X r)p :ℕhroot :∀ r, MeasurableSet (rootEvent r)conclusionIntegrable (treeWitnessCount M R rootEvent p) (Measure.pi μ)Proof (Lean source)
@[fun_prop] theorem integrable_treeWitnessCount [DecidableEq V] (μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)] (M : CoordinateGraph X) (R : Finset V) (rootEvent : ∀ r, Set (X r)) (p : ℕ) (hroot : ∀ r, MeasurableSet (rootEvent r)) : Integrable (treeWitnessCount M R rootEvent p) (Measure.pi μ) := by classical unfold treeWitnessCount apply integrable_finsetSum intro r hr apply integrable_finsetSum intro T hT exact integrable_rootTreeWitnessCount μ M rootEvent r T (hroot r) -
integral_rootTreeWitnessCount_letheorem — Under coordinate probability laws, the expected witness count for a root and completion set is at most the parent-array cardinality times the fixed-tree mass bound, for nonnegative constants, a measurable root event, root mass at most α, and oriented child-section masses at most β.hypothesesμ :∀ i, Measure (X i)∀ i, IsProbabilityMeasure (μ i)M :rootEvent :∀ r, Set (X r)r :VT :Finset Vα β :ℝhα :0 ≤ αhβ :0 ≤ βhroot :MeasurableSet (rootEvent r)hrootMass :μ r (rootEvent r) ≤ ofReal αhsection :∀ (i j : V)ifi ≠ jthen∀ y : X j, μ i {z | (z, y) ∈ M.edgeEvent i j} ≤ ofReal βconclusion(∫ x, rootTreeWitnessCount M rootEvent r T x ∂Measure.pi μ)Proof (Lean source)
theorem integral_rootTreeWitnessCount_le [DecidableEq V] (μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)] (M : CoordinateGraph X) (rootEvent : ∀ r, Set (X r)) (r : V) (T : Finset V) (α β : ℝ) (hα : 0 ≤ α) (hβ : 0 ≤ β) (hroot : MeasurableSet (rootEvent r)) (hrootMass : μ r (rootEvent r) ≤ ofReal α) (hsection : ∀ (i j : V), i ≠ j → ∀ y : X j, μ i {z | (z, y) ∈ M.edgeEvent i j} ≤ ofReal β) : (∫ x, rootTreeWitnessCount M rootEvent r T x ∂Measure.pi μ) ≤ ((insert r T).card : ℝ) ^ ((insert r T).card - 1) * α * β ^ ((insert r T).card - 1) := by classical let : DecidableEq V := fun a b => propDecidable (a = b) unfold rootTreeWitnessCount dsimp only have hInt (P : ParentEncoding ↥(insert r T) ⟨r, Finset.mem_insert_self r T⟩) : Integrable (fun x => if P.Valid ∧ x ∈ partialTreeEvent (selectedEmbedding _) P (rootEvent r) M.edgeEvent univ then (1 : ℝ) else 0) (Measure.pi μ) := by by_cases hv : P.Valid · simp only [hv, true_and] have hm := measurableSet_partialTreeEvent (selectedEmbedding _) P (rootEvent r) M.edgeEvent univ hroot M.measurable_edgeEvent apply (integrable_const (1 : ℝ)).mono_nonneg · exact (Measurable.ite hm measurable_const measurable_const).aestronglyMeasurable · exact Filter.Eventually.of_forall (fun x => by split_ifs <;> norm_num) · exact Filter.Eventually.of_forall (fun x => by split_ifs <;> norm_num) · simp only [hv, false_and, ite_false] exact integrable_const 0 rw [integral_finsetSum _ (fun P _ => hInt P)] calc _ ≤ ∑ _P : ParentEncoding ↥(insert r T) ⟨r, Finset.mem_insert_self r T⟩, α * β ^ ((insert r T).card - 1) := by apply Finset.sum_le_sum intro P hP by_cases hv : P.Valid · simp only [hv, true_and] have hm := measurableSet_partialTreeEvent (selectedEmbedding _) P (rootEvent r) M.edgeEvent univ hroot M.measurable_edgeEvent have hb := pi_measure_rooted_tree_event_le μ (selectedEmbedding _) P hv (rootEvent r) M.edgeEvent (ofReal α) (ofReal β) hroot M.measurable_edgeEvent hrootMass hsection have hr := ENNReal.toReal_mono (by finiteness) hb change (∫ x, (partialTreeEvent (selectedEmbedding _) P (rootEvent r) M.edgeEvent univ).indicator (fun _ => (1 : ℝ)) x ∂Measure.pi μ) ≤ _ calc _ = (Measure.pi μ).real _ := integral_indicator_one hm _ ≤ _ := by simpa only [Measure.real, ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_ofReal hα, ENNReal.toReal_ofReal hβ, Fintype.card_coe] using hr · simp only [hv, false_and, ite_false, integral_zero] exact mul_nonneg hα (pow_nonneg hβ _) _ = _ := by simp only [Finset.sum_const, Finset.card_univ, card_parentEncoding, Fintype.card_coe, nsmul_eq_mul, Nat.cast_pow] convert (by ring : ((insert r T).card : ℝ) ^ ((insert r T).card - 1) * (α * β ^ ((insert r T).card - 1)) = ((insert r T).card : ℝ) ^ ((insert r T).card - 1) * α * β ^ ((insert r T).card - 1)) using 1 congr 7 <;> exact Subsingleton.elim _ _ -
integral_treeWitnessCount_letheorem — For an edge model, distinguished roots, root events, a size p that is at least one, and constants α and β that are nonnegative, under independent coordinate probability laws with measurable root events, root-event probabilities at most α, and oriented child-section probabilities at most β for distinct coordinates, the expected total rooted witness count is at most n times choose(N minus one, p minus one) times p to the power p minus one times α times β to the power p minus one. Here n is the root-set size and N the population size.hypothesesμ :∀ i, Measure (X i)∀ i, IsProbabilityMeasure (μ i)M :R :Finset VrootEvent :∀ r, Set (X r)p :ℕhp :1 ≤ pα β :ℝhα :0 ≤ αhβ :0 ≤ βhroot :∀ r, MeasurableSet (rootEvent r)hrootMass :∀ r ∈ R, μ r (rootEvent r) ≤ ofReal αhsection :∀ (i j : V)ifi ≠ jthen∀ y : X j, μ i {z | (z, y) ∈ M.edgeEvent i j} ≤ ofReal βconclusion(∫ x, treeWitnessCount M R rootEvent p x ∂Measure.pi μ)Proof (Lean source)
theorem integral_treeWitnessCount_le [DecidableEq V] (μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)] (M : CoordinateGraph X) (R : Finset V) (rootEvent : ∀ r, Set (X r)) (p : ℕ) (hp : 1 ≤ p) (α β : ℝ) (hα : 0 ≤ α) (hβ : 0 ≤ β) (hroot : ∀ r, MeasurableSet (rootEvent r)) (hrootMass : ∀ r ∈ R, μ r (rootEvent r) ≤ ofReal α) (hsection : ∀ (i j : V), i ≠ j → ∀ y : X j, μ i {z | (z, y) ∈ M.edgeEvent i j} ≤ ofReal β) : (∫ x, treeWitnessCount M R rootEvent p x ∂Measure.pi μ) ≤ (R.card : ℝ) * (choose (card V - 1) (p - 1) : ℝ) * (p : ℝ) ^ (p - 1) * α * β ^ (p - 1) := by classical have hsum : (∫ x, treeWitnessCount M R rootEvent p x ∂Measure.pi μ) = ∑ r ∈ R, ∑ T ∈ ((Finset.univ : Finset V).erase r).powersetCard (p - 1), ∫ x, rootTreeWitnessCount M rootEvent r T x ∂Measure.pi μ := by unfold treeWitnessCount rw [integral_finsetSum R (fun r _ => integrable_finsetSum _ (fun T _ => integrable_rootTreeWitnessCount μ M rootEvent r T (hroot r)))] apply Finset.sum_congr rfl intro r hr exact integral_finsetSum _ (fun T _ => integrable_rootTreeWitnessCount μ M rootEvent r T (hroot r)) rw [hsum] calc (∑ r ∈ R, ∑ T ∈ ((Finset.univ : Finset V).erase r).powersetCard (p - 1), ∫ x, rootTreeWitnessCount M rootEvent r T x ∂Measure.pi μ) ≤ ∑ r ∈ R, ∑ _T ∈ ((Finset.univ : Finset V).erase r).powersetCard (p - 1), (p : ℝ) ^ (p - 1) * α * β ^ (p - 1) := by apply Finset.sum_le_sum intro r hr apply Finset.sum_le_sum intro T hT have hb := integral_rootTreeWitnessCount_le μ M rootEvent r T α β hα hβ (hroot r) (hrootMass r hr) hsection simpa only [card_insert_root_of_mem_completions r p hp T hT] using hb _ = (R.card : ℝ) * (choose (card V - 1) (p - 1) : ℝ) * (p : ℝ) ^ (p - 1) * α * β ^ (p - 1) := by simp only [Finset.sum_const, card_root_completions, nsmul_eq_mul] ring