Stat.FinitePositiveTable
This roll-up module exports graph-independent finite positive tables, their marginals and conditionals, coordinate fixing, sequential expansions, and two-row cancellation identities.
Basic 7 core · 6 supporting This module provides graph-independent profile spaces and finite-fibre summation for real tables whose coordinates can have different finite cardinalities. ★ sum_fiberSum_insert_update
Finite dependent profile spaces and fibre sums
This module provides graph-independent profile spaces and finite-fibre summation for real tables whose coordinates can have different finite cardinalities.
abbrev ProfileSpace reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The coordinate cardinalities determine the finite dependent profile space by assigning one bounded state to each coordinate.
Definition (Lean source)
def CardinalitiesPositive reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The coordinate cardinalities satisfy strict positivity of every cardinality when every coordinate has at least one state.
Definition (Lean source)
parameters
V :
Type u
r :
V → ℕ
v :
def
CardinalitiesPositive r :
Prop
given by
0 < r v
abbrev Kernel reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The coordinate cardinalities determine a real-valued kernel on complete profiles as a real-valued function on profiles.
Definition (Lean source)
structure PositiveTable reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The coordinate cardinalities determine a strictly positive normalized real table: a real mass for every complete profile, with every mass strictly positive and the masses summing to one.
Definition (Lean source)
parameters
V :
Type u
r :
V → ℕ
fields
The table assigns a real mass to each complete profile.
mass :
ProfileSpace r → ℝ
Every complete profile receives strictly positive mass.
mass_pos :
∀ x, 0 < mass x
The complete-profile masses sum to one.
sum_mass_eq_one :
∑ x, mass x = 1
def AgreeOn reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The coordinate set and two complete profiles determine their agreement on that set by equality at every coordinate in the set.
Definition (Lean source)
parameters
def
AgreeOn S x y :
Prop
given by
x v = y v
def fiberSum reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The profile function, fixed coordinate set, and reference profile determine the sum over compatible complete profiles by retaining exactly the profiles that agree with the reference on the fixed set.
Definition (Lean source)
parameters
def
fiberSum f S x :
M
given by
by classical exact ∑ y : ProfileSpace r, if AgreeOn S y x then f y else 0
theorem sum_fiberSum_insert_update reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
For a profile function, a fixed coordinate set, a coordinate outside that set, and a reference profile, partitioning its fibre by the coordinate value recovers the original fibre sum: adding up, over every value of the outside coordinate, the fibre sum that additionally fixes that coordinate at that value gives the fibre sum that fixes only the original set.
Formal statement
hypotheses
Proof (Lean source)
theorem sum_fiberSum_insert_update {M : Type uM} [AddCommMonoid M]
(f : ProfileSpace r → M) {S : Finset V} {v : V} (hv : v ∉ S)
(x : ProfileSpace r) :
(∑ z : Fin (r v), fiberSum f (insert v S) (update x v z)) =
fiberSum f S x := by
classical
have hAgree (z : Fin (r v)) (y : ProfileSpace r) :
AgreeOn (insert v S) y (update x v z) ↔
AgreeOn S y x ∧ y v = z := by
constructor
· intro h
constructor
· intro w hw
have hwy := h w (mem_insert_of_mem hw)
simpa only [Function.update_of_ne (ne_of_mem_of_not_mem hw hv)] using hwy
· simpa only [Function.update_self] using h v (mem_insert_self v S)
· rintro ⟨hS, hyv⟩ w hw
rcases mem_insert.mp hw with rfl | hw
· simpa only [Function.update_self] using hyv
· simpa only [Function.update_of_ne (ne_of_mem_of_not_mem hw hv)] using hS w hw
unfold fiberSum
calc
(∑ z : Fin (r v), ∑ y : ProfileSpace r,
if AgreeOn (insert v S) y (update x v z) then f y else 0) =
∑ z : Fin (r v), ∑ y ∈ univ with y v = z,
if AgreeOn S y x then f y else 0 := by
apply Finset.sum_congr rfl
intro z hz
rw [Finset.sum_filter]
apply Finset.sum_congr rfl
intro y hy
rw [hAgree z y]
by_cases hS : AgreeOn S y x <;> by_cases hyv : y v = z <;> simp [hS, hyv]
_ = ∑ y : ProfileSpace r, if AgreeOn S y x then f y else 0 := by
exact Finset.sum_fiberwise univ (fun y : ProfileSpace r => y v)
(fun y => if AgreeOn S y x then f y else 0)
6 supporting declarations (lemmas, instances)
-
agreeOn_emptytheorem — The two complete profiles agree on the empty coordinate set.Proof (Lean source)
-
fiberSum_congr_referencetheorem — For a profile function, a fixed coordinate set, and two reference profiles, agreement of the reference profiles on the fixed set makes their fibre sums equal.hypothesesProof (Lean source)
theorem fiberSum_congr_reference {M : Type uM} [AddCommMonoid M] (f : ProfileSpace r → M) {S : Finset V} {x x' : ProfileSpace r} (h : AgreeOn S x x') : fiberSum f S x = fiberSum f S x' := by unfold fiberSum apply Finset.sum_congr rfl intro y hy congr 1 apply propext constructor <;> intro hyAgree · exact fun v hv => (hyAgree v hv).trans (h v hv) · exact fun v hv => (hyAgree v hv).trans (h v hv).symm -
fiberSum_emptytheorem — For a profile function and a reference profile, the unrestricted finite sum equals the fibre sum with no coordinates fixed.hypothesesconclusionfiberSum f ∅ x = ∑ y, f yProof (Lean source)
theorem fiberSum_empty {M : Type uM} [AddCommMonoid M] (f : ProfileSpace r → M) (x : ProfileSpace r) : fiberSum f ∅ x = ∑ y, f y := by simp [fiberSum, AgreeOn] -
fiberSum_univtheorem — For a profile function and a reference profile, fixing every coordinate leaves only that reference profile in the fibre sum.hypothesesProof (Lean source)
theorem fiberSum_univ {M : Type uM} [AddCommMonoid M] (f : ProfileSpace r → M) (x : ProfileSpace r) : fiberSum f univ x = f x := by unfold fiberSum classical simp_rw [show ∀ y, AgreeOn univ y x ↔ y = x by intro y constructor · intro h funext v exact h v (Finset.mem_univ v) · rintro rfl exact fun v hv => rfl] simp -
fiberSum_update_of_not_memtheorem — For a profile function, a fixed coordinate set, a coordinate outside that set, a reference profile, and a replacement state, updating the outside coordinate leaves the fibre sum unchanged.hypothesesV :sharedType uV → ℕM :Type uMf :ProfileSpace r → MS :Finset Vv :Vhv :v ∉ Sx :z :Fin (r v)Proof (Lean source)
theorem fiberSum_update_of_not_mem {M : Type uM} [AddCommMonoid M] (f : ProfileSpace r → M) {S : Finset V} {v : V} (hv : v ∉ S) (x : ProfileSpace r) (z : Fin (r v)) : fiberSum f S (update x v z) = fiberSum f S x := by apply fiberSum_congr_reference f intro w hw simp only [Function.update_of_ne (ne_of_mem_of_not_mem hw hv)] -
sum_fiberSum_singleton_updatetheorem — For a profile function, a coordinate, and a reference profile, summing its singleton-coordinate fibres recovers the unrestricted finite sum.hypothesesProof (Lean source)
theorem sum_fiberSum_singleton_update {M : Type uM} [AddCommMonoid M] (f : ProfileSpace r → M) (v : V) (x : ProfileSpace r) : (∑ z : Fin (r v), fiberSum f {v} (update x v z)) = ∑ y, f y := by simpa [fiberSum_empty] using sum_fiberSum_insert_update f (S := ∅) (v := v) (by simp) x
Marginals 6 core · 12 supporting This module defines marginals and conditional masses for finite real tables, proving positivity of conditioning denominators and normalization of each conditional row. ★ sum_conditionalMass
Marginals and finite conditional masses
This module defines marginals and conditional masses for finite real tables, proving positivity of conditioning denominators and normalization of each conditional row.
def kernelMarginalMass reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The kernel, fixed coordinate set, and reference profile determine the kernel's marginal mass by summing over compatible complete profiles.
Definition (Lean source)
def marginalMass reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The positive table, fixed coordinate set, and reference profile determine the table's marginal mass as its kernel marginal.
Definition (Lean source)
def IsStrictlyPositive reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.Kernel
The kernel has pointwise strict positivity when every complete profile has positive real mass.
Definition (Lean source)
def kernelConditionalMass reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The kernel, coordinate and conditioning set, reference profile, and proposed coordinate value determine the kernel conditional mass as the joint marginal divided by the conditioning marginal.
Definition (Lean source)
parameters
def
kernelConditionalMass q v C x z :
ℝ
given by
def conditionalMass reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The positive table, coordinate and conditioning set, reference profile, and proposed coordinate value determine the table conditional mass as its kernel conditional mass.
Definition (Lean source)
theorem sum_conditionalMass reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
For a positive table, a coordinate outside the conditioning set, and a reference profile, the conditional row sums to one.
Formal statement
hypotheses
conclusion
∑ z : Fin (r v), conditionalMass p v C x z = 1
Proof (Lean source)
theorem sum_conditionalMass (p : PositiveTable r)
(v : V) (C : Finset V) (hv : v ∉ C) (x : ProfileSpace r) :
∑ z : Fin (r v), conditionalMass p v C x z = 1 := by
exact sum_kernelConditionalMass p.mass_pos v C hv x
12 supporting declarations (lemmas, instances)
-
kernelMarginalMass_postheorem — For a pointwise strictly positive kernel, a fixed coordinate set, and a reference profile, the kernel marginal is strictly positive.hypothesesconclusion0 < kernelMarginalMass q S xProof (Lean source)
theorem kernelMarginalMass_pos {q : Kernel r} (hq : q.IsStrictlyPositive) (S : Finset V) (x : ProfileSpace r) : 0 < kernelMarginalMass q S x := by unfold kernelMarginalMass fiberSum apply Finset.sum_pos' · intro y hy split_ifs · exact (hq y).le · exact le_rfl · refine ⟨x, Finset.mem_univ x, ?_⟩ simp [AgreeOn, hq x] -
marginalMass_postheorem — For a positive table, a fixed coordinate set, and a reference profile, the table marginal is strictly positive.hypothesesconclusion0 < marginalMass p S xProof (Lean source)
theorem marginalMass_pos (p : PositiveTable r) (S : Finset V) (x : ProfileSpace r) : 0 < marginalMass p S x := by exact kernelMarginalMass_pos p.mass_pos S x -
marginalMass_ne_zerotheorem — For a positive table, a fixed coordinate set, and a reference profile, the table marginal is nonzero.hypothesesconclusionmarginalMass p S x ≠ 0Proof (Lean source)
theorem marginalMass_ne_zero (p : PositiveTable r) (S : Finset V) (x : ProfileSpace r) : marginalMass p S x ≠ 0 := by exact (marginalMass_pos p S x).ne' -
marginalMass_emptytheorem — For a positive table and a reference profile, the marginal with no coordinates fixed equals one.hypothesesconclusionmarginalMass p ∅ x = 1Proof (Lean source)
theorem marginalMass_empty (p : PositiveTable r) (x : ProfileSpace r) : marginalMass p ∅ x = 1 := by unfold marginalMass kernelMarginalMass rw [fiberSum_empty] exact p.sum_mass_eq_one -
marginalMass_univtheorem — For a positive table and a reference profile, the marginal fixing every coordinate equals the profile's own mass.hypothesesconclusionmarginalMass p univ x = p.mass xProof (Lean source)
theorem marginalMass_univ (p : PositiveTable r) (x : ProfileSpace r) : marginalMass p univ x = p.mass x := by exact fiberSum_univ p.mass x -
kernelConditionalMass_den_postheorem — For a pointwise strictly positive kernel, a conditioning set, and a reference profile, the conditional denominator is strictly positive.hypothesesconclusion0 < kernelMarginalMass q C xProof (Lean source)
theorem kernelConditionalMass_den_pos {q : Kernel r} (hq : q.IsStrictlyPositive) (C : Finset V) (x : ProfileSpace r) : 0 < kernelMarginalMass q C x := by exact kernelMarginalMass_pos hq C x -
conditionalMass_den_ne_zerotheorem — For a positive table, a conditioning set, and a reference profile, the conditional denominator is nonzero.hypothesesconclusionmarginalMass p C x ≠ 0Proof (Lean source)
theorem conditionalMass_den_ne_zero (p : PositiveTable r) (C : Finset V) (x : ProfileSpace r) : marginalMass p C x ≠ 0 := by exact marginalMass_ne_zero p C x -
kernelConditionalMass_mul_dentheorem — For a pointwise strictly positive kernel, a coordinate and conditioning set, a reference profile, and a proposed coordinate value, multiplying the conditional mass by its denominator recovers the joint marginal.hypothesesconclusionkernelConditionalMass q v C x z * kernelMarginalMass q C xProof (Lean source)
theorem kernelConditionalMass_mul_den {q : Kernel r} (hq : q.IsStrictlyPositive) (v : V) (C : Finset V) (x : ProfileSpace r) (z : Fin (r v)) : kernelConditionalMass q v C x z * kernelMarginalMass q C x = kernelMarginalMass q (insert v C) (update x v z) := by unfold kernelConditionalMass exact div_mul_cancel₀ _ (kernelMarginalMass_pos hq C x).ne' -
conditionalMass_mul_marginaltheorem — For a positive table, a coordinate and conditioning set, a reference profile, and a proposed coordinate value, multiplying the conditional mass by the conditioning marginal recovers the joint marginal.hypothesesProof (Lean source)
theorem conditionalMass_mul_marginal (p : PositiveTable r) (v : V) (C : Finset V) (x : ProfileSpace r) (z : Fin (r v)) : conditionalMass p v C x z * marginalMass p C x = marginalMass p (insert v C) (update x v z) := by exact kernelConditionalMass_mul_den p.mass_pos v C x z -
kernelConditionalMass_postheorem — For a pointwise strictly positive kernel, a coordinate and conditioning set, a reference profile, and a proposed coordinate value, the conditional mass is strictly positive.hypothesesconclusion0 < kernelConditionalMass q v C x zProof (Lean source)
theorem kernelConditionalMass_pos {q : Kernel r} (hq : q.IsStrictlyPositive) (v : V) (C : Finset V) (x : ProfileSpace r) (z : Fin (r v)) : 0 < kernelConditionalMass q v C x z := by unfold kernelConditionalMass exact div_pos (kernelMarginalMass_pos hq _ _) (kernelMarginalMass_pos hq _ _) -
conditionalMass_postheorem — For a positive table, a coordinate and conditioning set, a reference profile, and a proposed coordinate value, the conditional mass is strictly positive.hypothesesconclusion0 < conditionalMass p v C x zProof (Lean source)
theorem conditionalMass_pos (p : PositiveTable r) (v : V) (C : Finset V) (x : ProfileSpace r) (z : Fin (r v)) : 0 < conditionalMass p v C x z := by exact kernelConditionalMass_pos p.mass_pos v C x z -
sum_kernelConditionalMasstheorem — For a pointwise strictly positive kernel, a coordinate outside the conditioning set, and a reference profile, the conditional row sums to one.hypothesesconclusion∑ z : Fin (r v), kernelConditionalMass q v C x z = 1Proof (Lean source)
theorem sum_kernelConditionalMass {q : Kernel r} (hq : q.IsStrictlyPositive) (v : V) (C : Finset V) (hv : v ∉ C) (x : ProfileSpace r) : ∑ z : Fin (r v), kernelConditionalMass q v C x z = 1 := by unfold kernelConditionalMass kernelMarginalMass rw [← Finset.sum_div, sum_fiberSum_insert_update q hv x] exact div_self (kernelMarginalMass_pos hq C x).ne'
Fixing 8 core · 9 supporting This module defines graph-independent coordinate fixing for positive finite tables and records its one-step and sequential conditional-factor expansions. ★ fixSequence_eq_div_conditionalProduct
Coordinate fixing and sequential expansions
This module defines graph-independent coordinate fixing for positive finite tables and records its one-step and sequential conditional-factor expansions.
def fixKernelCoordinate reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The kernel, coordinate, and conditioning set determine the kernel after fixing that coordinate by dividing each profile's mass by the kernel's conditional mass of that profile's value at the coordinate given its values on the conditioning set. The division follows the real-number convention that division by zero gives zero, so the result is the intended quotient only when the conditional mass is nonzero, as it is for a strictly positive kernel.
Definition (Lean source)
def fixCoordinate reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The positive table, coordinate, and conditioning set determine the fixed kernel as the fixed mass kernel.
Definition (Lean source)
structure FixingStep reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The coordinate type determines one algebraic fixing step, consisting of the coordinate to remove and the coordinates used for conditioning.
Definition (Lean source)
parameters
V :
Type u
fields
The coordinate removed from the random kernel.
coordinate :
V
The coordinates conditioned on when the coordinate is fixed.
conditioning :
Finset V
def FixingSequenceValid reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The list of fixing steps satisfies algebraic validity when its fixed coordinates are distinct and no step conditions on its own coordinate.
Definition (Lean source)
parameters
V :
Type u
steps :
List (FixingStep V)
def
FixingSequenceValid steps :
Prop
given by
clause 1
(steps.map (fun s ↦ s.coordinate)).Nodup
clause 2
s ∈ steps :
s.coordinate ∉ s.conditioning
def fixKernelSequence reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The kernel and a list of fixing steps determine the sequentially fixed kernel: an empty list leaves the kernel unchanged, and a nonempty list fixes its head before continuing with its tail.
Definition (Lean source)
parameters
V :
Type u
V → ℕ
q :
Kernel r
def
given by
clause 1
| [] => q
clause 2
| s :: ss => fixKernelSequence (fixKernelCoordinate q s.coordinate s.conditioning) ss
def fixSequence reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The positive table and list of fixing steps determine the sequentially fixed kernel as the sequentially fixed mass kernel.
Definition (Lean source)
def fixingConditionalProduct reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The kernel and a list of fixing steps determine the product of the successive conditional factors, evaluated at a profile: an empty list has product one, and a nonempty list multiplies the kernel's conditional mass for its first step by the product for the remaining steps computed from the kernel after that first step has been fixed.
Definition (Lean source)
parameters
V :
Type u
V → ℕ
q :
Kernel r
def
given by
clause 1
| [], _ => 1
clause 2
| s :: ss, x
=> kernelConditionalMass q s.coordinate s.conditioning x (x s.coordinate) * fixingConditionalProduct (fixKernelCoordinate q s.coordinate s.conditioning) ss x
theorem fixSequence_eq_div_conditionalProduct reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
For a positive table, an algebraically valid list of fixing steps, and a profile, the sequentially fixed kernel at that profile equals the table's mass there divided by the product of the successive conditional factors, each computed from the kernel obtained after the earlier fixing steps.
Formal statement
hypotheses
conclusion
fixSequence p steps x = p.mass x / fixingConditionalProduct p.mass steps x
Proof (Lean source)
theorem fixSequence_eq_div_conditionalProduct (p : PositiveTable r)
(steps : List (FixingStep V)) (hvalid : FixingSequenceValid steps)
(x : ProfileSpace r) :
fixSequence p steps x = p.mass x / fixingConditionalProduct p.mass steps x := by
exact fixKernelSequence_eq_div_conditionalProduct p.mass_pos steps hvalid x
9 supporting declarations (lemmas, instances)
-
fixKernelCoordinate_applytheorem — For a kernel, a coordinate and conditioning set, and a profile, one fixing step has its defining pointwise quotient form.hypothesesconclusionfixKernelCoordinate q v C x = q x / kernelConditionalMass q v C x (x v)Proof (Lean source)
theorem fixKernelCoordinate_apply (q : Kernel r) (v : V) (C : Finset V) (x : ProfileSpace r) : fixKernelCoordinate q v C x = q x / kernelConditionalMass q v C x (x v) := by rfl -
fixKernelCoordinate_eq_mul_marginal_divtheorem — For a pointwise strictly positive kernel, a coordinate and conditioning set, and a profile, one fixing step equals the original mass times the conditioning marginal divided by the joint marginal.hypothesesconclusionfixKernelCoordinate q v C xProof (Lean source)
theorem fixKernelCoordinate_eq_mul_marginal_div {q : Kernel r} (hq : q.IsStrictlyPositive) (v : V) (C : Finset V) (x : ProfileSpace r) : fixKernelCoordinate q v C x = q x * kernelMarginalMass q C x / kernelMarginalMass q (insert v C) x := by unfold fixKernelCoordinate kernelConditionalMass rw [Function.update_eq_self] have hJoint : kernelMarginalMass q (insert v C) x ≠ 0 := (kernelMarginalMass_pos hq (insert v C) x).ne' by_cases hzero : kernelMarginalMass q (insert v C) x = 0 · exact (hJoint hzero).elim · exact div_div_eq_mul_div _ _ _ -
fixCoordinate_eq_mul_marginal_divtheorem — For a positive table, a coordinate and conditioning set, and a profile, one fixing step has the corresponding table marginal-ratio expansion.hypothesesconclusionfixCoordinate p v C x = p.mass x * marginalMass p C x / marginalMass p (insert v C) xProof (Lean source)
theorem fixCoordinate_eq_mul_marginal_div (p : PositiveTable r) (v : V) (C : Finset V) (x : ProfileSpace r) : fixCoordinate p v C x = p.mass x * marginalMass p C x / marginalMass p (insert v C) x := by exact fixKernelCoordinate_eq_mul_marginal_div p.mass_pos v C x -
fixKernelCoordinate_postheorem — For a pointwise strictly positive kernel, a coordinate, and a conditioning set, fixing preserves pointwise strict positivity.hypothesesconclusionProof (Lean source)
theorem fixKernelCoordinate_pos {q : Kernel r} (hq : q.IsStrictlyPositive) (v : V) (C : Finset V) : (fixKernelCoordinate q v C).IsStrictlyPositive := by intro x exact div_pos (hq x) (kernelConditionalMass_pos hq v C x (x v)) -
fixKernelSequence_postheorem — For a pointwise strictly positive kernel and a list of fixing steps, sequential fixing preserves pointwise strict positivity.hypothesesconclusion(fixKernelSequence q steps).IsStrictlyPositiveProof (Lean source)
theorem fixKernelSequence_pos {q : Kernel r} (hq : q.IsStrictlyPositive) (steps : List (FixingStep V)) : (fixKernelSequence q steps).IsStrictlyPositive := by induction steps generalizing q with | nil => exact hq | cons s ss ih => exact ih (fixKernelCoordinate_pos hq s.coordinate s.conditioning) -
fixSequence_nonnegtheorem — For a positive table, a list of fixing steps, and a profile, the sequentially fixed kernel is nonnegative.hypothesesconclusion0 ≤ fixSequence p steps xProof (Lean source)
theorem fixSequence_nonneg (p : PositiveTable r) (steps : List (FixingStep V)) (x : ProfileSpace r) : 0 ≤ fixSequence p steps x := by exact (fixKernelSequence_pos p.mass_pos steps x).le -
fixingConditionalProduct_postheorem — For a pointwise strictly positive kernel, a list of fixing steps, and a profile, the product of successive conditional factors is strictly positive.hypothesesconclusion0 < fixingConditionalProduct q steps xProof (Lean source)
theorem fixingConditionalProduct_pos {q : Kernel r} (hq : q.IsStrictlyPositive) (steps : List (FixingStep V)) (x : ProfileSpace r) : 0 < fixingConditionalProduct q steps x := by induction steps generalizing q with | nil => simp [fixingConditionalProduct] | cons s ss ih => exact mul_pos (kernelConditionalMass_pos hq s.coordinate s.conditioning x (x s.coordinate)) (ih (fixKernelCoordinate_pos hq s.coordinate s.conditioning)) -
fixKernelSequence_eq_div_conditionalProducttheorem — For a pointwise strictly positive kernel, an algebraically valid list of fixing steps, and a profile, sequential fixing equals the original mass divided by the product of its successive conditional factors.hypothesesV :sharedType uV → ℕq :Kernel rhq :q.IsStrictlyPositivesteps :List (FixingStep V)hvalid :FixingSequenceValid stepsx :conclusionfixKernelSequence q steps x = q x / fixingConditionalProduct q steps xProof (Lean source)
theorem fixKernelSequence_eq_div_conditionalProduct {q : Kernel r} (hq : q.IsStrictlyPositive) (steps : List (FixingStep V)) (hvalid : FixingSequenceValid steps) (x : ProfileSpace r) : fixKernelSequence q steps x = q x / fixingConditionalProduct q steps x := by induction steps generalizing q with | nil => simp [fixKernelSequence, fixingConditionalProduct] | cons s ss ih => rw [fixKernelSequence, ih (fixKernelCoordinate_pos hq s.coordinate s.conditioning)] · simp only [fixKernelCoordinate_apply, fixingConditionalProduct, div_div] · exact ⟨hvalid.1.tail, fun t ht ↦ hvalid.2 t (List.mem_cons_of_mem s ht)⟩ -
fixingConditionalProduct_cons_eq_marginal_ratiotheorem — For a kernel, a first fixing step, the remaining fixing steps, and a profile, the first conditional-product factor is the ratio of its joint and conditioning marginals.hypothesesconclusionfixingConditionalProduct q (s :: ss) x= (kernelMarginalMass q (insert s.coordinate s.conditioning) x / kernelMarginalMass q s.conditioning x) * fixingConditionalProduct (fixKernelCoordinate q s.coordinate s.conditioning) ss xProof (Lean source)
theorem fixingConditionalProduct_cons_eq_marginal_ratio {q : Kernel r} (s : FixingStep V) (ss : List (FixingStep V)) (x : ProfileSpace r) : fixingConditionalProduct q (s :: ss) x = (kernelMarginalMass q (insert s.coordinate s.conditioning) x / kernelMarginalMass q s.conditioning x) * fixingConditionalProduct (fixKernelCoordinate q s.coordinate s.conditioning) ss x := by simp only [fixingConditionalProduct, kernelConditionalMass, Function.update_eq_self]
TwoRow 9 core · 4 supporting This module proves the graph-independent row normalization, total normalization, and positive marginal cancellation identities used to read conditional independence from fixed kernels. ★ kernelRows_eq_of_condIndep
Row, total, and cancellation identities for fixed kernels
This module proves the graph-independent row normalization, total normalization, and positive marginal cancellation identities used to read conditional independence from fixed kernels.
def coordinateRowMass reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The kernel, row coordinate, and reference profile determine the kernel's coordinate-row mass by summing over that coordinate.
Definition (Lean source)
parameters
def
coordinateRowMass q d x :
ℝ
def coordinateRectangleMass reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The kernel, two varying coordinates, and reference profile determine the kernel's coordinate-rectangle mass by summing over both coordinates.
def coordinateColumnMass reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The kernel, column coordinate, and reference profile determine the kernel's coordinate-column mass by summing over that coordinate.
Definition (Lean source)
parameters
def
coordinateColumnMass q a x :
ℝ
def HasMarginalKernelForm reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The positive table, kernel, three distinct-role coordinates, and residual kernel determine the marginal-times-kernel representation when the kernel factors into the positive a marginal and the residual three-coordinate kernel.
Definition (Lean source)
parameters
def
HasMarginalKernelForm p q a c d K :
Prop
given by
q x = marginalMass p {a} x * K (x a) (x c) (x d)
def KernelRowsNormalized reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The residual kernel has normalized rows in its final coordinate when each such row sums to one.
def KernelNonnegative reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The residual kernel has pointwise nonnegativity when every entry is nonnegative.
def KernelCondIndepAt reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The kernel, two coordinates, and profile determine the multiplicative conditional-independence identity at that profile by equating the profile-and-rectangle product with the row-and-column product.
Definition (Lean source)
parameters
def
KernelCondIndepAt q a d x :
Prop
given by
q x * coordinateRectangleMass q a d x
= coordinateRowMass q d x * coordinateColumnMass q a x
def KernelCondIndep reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
The kernel and two coordinates determine their multiplicative conditional-independence identity at every profile by requiring the pointwise identity at each profile.
Definition (Lean source)
theorem kernelRows_eq_of_condIndep reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable
For a positive table, a kernel, three pairwise distinct coordinates, a residual kernel, its marginal-times-kernel form, normalized residual rows, and the kernel's multiplicative conditional-independence identity, the residual row is unchanged when the positive-marginal coordinate is replaced.
Formal statement
hypotheses
V :
Type u
V → ℕ
p :
q :
Kernel r
a c d :
V
hac :
a ≠ c
had :
a ≠ d
hcd :
c ≠ d
hform :
HasMarginalKernelForm p q a c d K
hrows :
hci :
KernelCondIndep q a d
x :
za :
Fin (r a)
conclusion
K (x a) (x c) (x d) = K za (x c) (x d)
Proof (Lean source)
theorem kernelRows_eq_of_condIndep
(p : PositiveTable r) (q : Kernel r) {a c d : V}
(hac : a ≠ c) (had : a ≠ d) (hcd : c ≠ d)
(K : Fin (r a) → Fin (r c) → Fin (r d) → ℝ)
(hform : HasMarginalKernelForm p q a c d K)
(hrows : KernelRowsNormalized K)
(hci : KernelCondIndep q a d) :
∀ (x : ProfileSpace r) (za : Fin (r a)),
K (x a) (x c) (x d) = K za (x c) (x d) := by
intro x za
have hKcol (y : ProfileSpace r) :
K (y a) (y c) (y d) = coordinateColumnMass q a y := by
have h := hci y
unfold KernelCondIndepAt at h
rw [coordinateRectangleMass_eq_one p q had hcd K hform hrows y,
coordinateRowMass_eq_marginalMass p q had hcd K hform hrows y,
hform y] at h
simp only [mul_one] at h
exact eq_of_pos_mul_eq_mul (marginalMass_pos p {a} y) h
have hcol :
coordinateColumnMass q a (update x a za) =
coordinateColumnMass q a x := by
unfold coordinateColumnMass
apply Finset.sum_congr rfl
intro z hz
rw [Function.update_idem]
calc
K (x a) (x c) (x d) = coordinateColumnMass q a x := hKcol x
_ = coordinateColumnMass q a (update x a za) := hcol.symm
_ = K ((update x a za) a) ((update x a za) c)
((update x a za) d) := (hKcol (update x a za)).symm
_ = K za (x c) (x d) := by
simp only [Function.update_self, Function.update_of_ne hac.symm,
Function.update_of_ne had.symm]
4 supporting declarations (lemmas, instances)
-
eq_of_pos_mul_eq_multheorem — For a positive common factor and an equality after multiplying two real numbers by it, the two real numbers are equal.hypothesesm x y :ℝhm :0 < mh :m * x = m * yconclusionx = yProof (Lean source)
theorem eq_of_pos_mul_eq_mul {m x y : ℝ} (hm : 0 < m) (h : m * x = m * y) : x = y := by exact mul_left_cancel₀ hm.ne' h -
coordinateRowMass_eq_marginalMasstheorem — For a positive table, a kernel, two coordinates distinct from the row coordinate, a residual kernel, its marginal-times-kernel form, normalized residual rows, and a profile, the kernel's row mass equals the positive table's a marginal.hypothesesV :sharedType uV → ℕp :q :Kernel ra c d :Vhad :a ≠ dhcd :c ≠ dhform :HasMarginalKernelForm p q a c d Khrows :x :conclusioncoordinateRowMass q d x = marginalMass p {a} xProof (Lean source)
theorem coordinateRowMass_eq_marginalMass (p : PositiveTable r) (q : Kernel r) {a c d : V} (had : a ≠ d) (hcd : c ≠ d) (K : Fin (r a) → Fin (r c) → Fin (r d) → ℝ) (hform : HasMarginalKernelForm p q a c d K) (hrows : KernelRowsNormalized K) (x : ProfileSpace r) : coordinateRowMass q d x = marginalMass p {a} x := by unfold HasMarginalKernelForm at hform unfold KernelRowsNormalized at hrows unfold coordinateRowMass have hm (zd : Fin (r d)) : marginalMass p {a} (update x d zd) = marginalMass p {a} x := by unfold marginalMass kernelMarginalMass exact fiberSum_update_of_not_mem p.mass (by simpa using had.symm) x zd simp_rw [hform, hm] simp only [Function.update_of_ne had, Function.update_of_ne hcd, Function.update_self] rw [← Finset.mul_sum, hrows] exact mul_one _ -
coordinateRectangleMass_eq_onetheorem — For a positive table, a kernel, two coordinates distinct from the row coordinate, a residual kernel, its marginal-times-kernel form, normalized residual rows, and a profile, the kernel's rectangle mass equals one.hypothesesV :sharedType uV → ℕp :q :Kernel ra c d :Vhad :a ≠ dhcd :c ≠ dhform :HasMarginalKernelForm p q a c d Khrows :x :conclusioncoordinateRectangleMass q a d x = 1Proof (Lean source)
theorem coordinateRectangleMass_eq_one (p : PositiveTable r) (q : Kernel r) {a c d : V} (had : a ≠ d) (hcd : c ≠ d) (K : Fin (r a) → Fin (r c) → Fin (r d) → ℝ) (hform : HasMarginalKernelForm p q a c d K) (hrows : KernelRowsNormalized K) (x : ProfileSpace r) : coordinateRectangleMass q a d x = 1 := by unfold coordinateRectangleMass change (∑ za : Fin (r a), coordinateRowMass q d (update x a za)) = 1 simp_rw [coordinateRowMass_eq_marginalMass p q had hcd K hform hrows] unfold marginalMass kernelMarginalMass rw [sum_fiberSum_singleton_update, p.sum_mass_eq_one] -
kernel_nonneg_of_marginalKernelFormtheorem — For a positive table, a kernel, three coordinates, a residual kernel, its marginal-times-kernel form, nonnegative residual entries, and a profile, the kernel is nonnegative.hypothesesV :sharedType uV → ℕp :q :Kernel ra c d :Vhform :HasMarginalKernelForm p q a c d KhK :x :conclusion0 ≤ q xProof (Lean source)
theorem kernel_nonneg_of_marginalKernelForm (p : PositiveTable r) (q : Kernel r) {a c d : V} (K : Fin (r a) → Fin (r c) → Fin (r d) → ℝ) (hform : HasMarginalKernelForm p q a c d K) (hK : KernelNonnegative K) (x : ProfileSpace r) : 0 ≤ q x := by rw [hform] exact mul_nonneg (marginalMass_pos p {a} x).le (hK (x a) (x c) (x d))