SCM.ID.Density.ChainRuleDensity
The joint density of the observed variables of a structural causal model, with respect to a product of σ-finite reference measures, factorizes along the topological order as the product of one-node conditional densities
Core 6 core · 10 supporting This file defines the measurable fibre Radon--Nikodym data and prefix-density products used by the chain rule. ★ rnDeriv_compProd_prod_sigmaFinite_of_fiber_ac
Core constructions for the observational chain-rule density
This file defines the measurable fibre Radon--Nikodym data and prefix-density
products used by the chain rule. It also establishes the reference-measure
reindexing and product-measure Radon--Nikodym lemmas needed for the induction;
the final observational factorization is proved in RadonNikodym.
def obsStepCondDensity reviewed
⚑ flagged
Causalean.SCM
For a finite collection of distinguishable node labels with measurable value spaces, a structural causal model, a family of -finite reference measures for its node values, a fixed-node assignment, an observed-node position, and assuming finite observational kernels, standard-Borel and nonempty one-node value spaces, and countably generated prefix value spaces, the one-node conditional density factor maps each full observed assignment to the Radon--Nikodym derivative of the conditional law of the node at that position, given its preceding observed values, with respect to that node's reference measure.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
ref :
s :
M.FixedValues
i :
Fin M.observed.card
∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')
given by
fun x
=> ((M.obsStepCondKernel i.isLt) (s, valuesProjection (M.prefixNodes_subset_observed i.val) x)).rnDeriv (ref.μ (M.observedAt i).val) (x (M.observedAt i))
def qFactorDensityProduct reviewed
⚑ flagged
Causalean.SCM
For a finite collection of distinguishable node labels with measurable value spaces, a structural causal model, a family of -finite reference measures for its node values, and a fixed-node assignment, assuming finite observational kernels, standard-Borel and nonempty one-node value spaces, and countably generated prefix value spaces, the chain-rule density product maps each full observed assignment to the product of all one-node conditional density factors in the canonical observed topological order.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
ref :
s :
M.FixedValues
∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')
∀ (k : ℕ) (hk : k < M.observed.card),
∀ k : ℕ,
given by
fun x => ∏ i : Fin M.observed.card, M.obsStepCondDensity ref s i x
def prefixDensityProduct reviewed
⚑ flagged
Causalean.SCM
For a finite collection of distinguishable node labels with measurable value spaces, a structural causal model, a family of -finite reference measures for its node values, and a fixed-node assignment, assuming finite observational kernels, standard-Borel and nonempty one-node value spaces, and countably generated prefix value spaces, the recursive prefix-density product maps every prefix length and assignment on that prefix to the value for the empty prefix, and otherwise the preceding prefix density multiplied by the conditional density of the newly appended node, or by when that position is not observed.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
ref :
s :
M.FixedValues
∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')
∀ (k : ℕ) (hk : k < M.observed.card),
∀ k : ℕ,
k :
ℕ
given by
clause 1
| 0, _ => 1
clause 2
| k + 1, z
=> M.prefixDensityProduct ref s k (valuesProjection (M.prefixNodes_mono (le_succ k)) z) * if h : k < M.observed.card then ((M.obsStepCondKernel h) (s, valuesProjection (M.prefixNodes_mono (le_succ k)) z)).rnDeriv (ref.μ (M.observedAt ⟨k, h⟩).val) (z ⟨(M.observedAt ⟨k, h⟩).val, by rw [M.prefixNodes_succ h] exact mem_union_right _ (mem_singleton_self _)⟩) else 1
def ObsStepFiberRN reviewed
⚑ flagged
Causalean.SCM
For a finite collection of distinguishable node labels with measurable value spaces, a structural causal model, a family of -finite reference measures for its node values, and a fixed-node assignment, assuming finite observational kernels, standard-Borel and nonempty one-node value spaces, and countably generated prefix value spaces, the stepwise fibre Radon--Nikodym condition requires that, at every observed position, the next observed node is selected, the product reference measure on its preceding prefix is formed, the observational law of that prefix is formed, the conditional kernel of that next node given the prefix is formed, and that kernel is almost surely dominated by its reference measure under the prefix law while its fibre derivative is jointly almost-everywhere measurable under the product reference measure.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
ref :
s :
M.FixedValues
∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')
∀ (k : ℕ) (hk : k < M.observed.card),
∀ k : ℕ,
k :
ℕ
hk :
k < M.observed.card
def
ObsStepFiberRN M ref s :
Prop
given by
node :
(M.observedAt ⟨k, hk⟩).val (: SWIGNode N)
∀ᵐ a ∂chain, stepK a ≪ ref.μ node
AEMeasurable (fun p : ValuesOn (M.prefixNodes k) (swigΩ Ω) × swigΩ Ω node => (stepK p.1).rnDeriv (ref.μ node) p.2) (νk.prod (ref.μ node))
def prefixStepDensityInPrefix reviewed
⚑ flagged
Causalean.SCM
For a finite collection of distinguishable node labels with measurable value spaces, a structural causal model, a family of -finite reference measures for its node values, a fixed-node assignment, a prefix length , an assignment on its prefix, and a natural-number position , assuming finite observational kernels, standard-Borel and nonempty one-node value spaces, and countably generated prefix value spaces, the prefix-read one-step density factor is the conditional density factor at position when and that position is observed, the value when but the position is not observed, and the value when .
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
ref :
s :
M.FixedValues
∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')
∀ (i : ℕ) (hi : i < M.observed.card),
∀ i : ℕ,
k :
ℕ
i :
ℕ
def
given by
if hi : i < k then if hcard : i < M.observed.card then ((M.obsStepCondKernel hcard) (s, valuesProjection (M.prefixNodes_mono (le_of_lt hi)) z)).rnDeriv (ref.μ (M.observedAt ⟨i, hcard⟩).val) (z ⟨(M.observedAt ⟨i, hcard⟩).val, by rw [M.observedAt_mem_prefixNodes_iff k ⟨i, hcard⟩] exact hi⟩) else 1 else 1
lemma rnDeriv_compProd_prod_sigmaFinite_of_fiber_ac reviewed
⚑ flagged
Causalean.SCM
For two measurable spaces, a finite source measure, a source reference measure, a target reference measure, a finite transition kernel, and a proposed source density, if the source measure is dominated by its reference, almost every transition fibre is dominated by the target reference, the fibre density is jointly almost-everywhere measurable, and the proposed source density is the source Radon–Nikodym derivative, then the joint composition-product density is almost surely the product of the source and conditional densities.
Formal statement
hypotheses
α β :
μ ν :
Measure α
ρ :
Measure β
κ :
Kernel α β
f :
α → ENNReal
hμν :
μ ≪ ν
hfiber :
∀ᵐ a ∂μ, κ a ≪ ρ
hfiber_meas :
AEMeasurable (fun p : α × β => (κ p.1).rnDeriv ρ p.2) (ν.prod ρ)
hf :
μ.rnDeriv ν =ᵐ[ν] f
conclusion
(μ ⊗ₘ κ).rnDeriv (ν.prod ρ) =ᵐ[ν.prod ρ] fun p => f p.1 * (κ p.1).rnDeriv ρ p.2
Proof (Lean source)
lemma rnDeriv_compProd_prod_sigmaFinite_of_fiber_ac {α β : Type*}
[MeasurableSpace α] [MeasurableSpace β]
(μ ν : Measure α) (ρ : Measure β)
(κ : Kernel α β)
(f : α → ENNReal)
[IsFiniteMeasure μ]
[SigmaFinite ν] [SigmaFinite ρ]
[IsFiniteKernel κ]
(hμν : μ ≪ ν) (hfiber : ∀ᵐ a ∂μ, κ a ≪ ρ)
(hfiber_meas :
AEMeasurable
(fun p : α × β => (κ p.1).rnDeriv ρ p.2) (ν.prod ρ))
(hf : μ.rnDeriv ν =ᵐ[ν] f) :
(μ ⊗ₘ κ).rnDeriv (ν.prod ρ)
=ᵐ[ν.prod ρ] fun p => f p.1 * (κ p.1).rnDeriv ρ p.2 := by
exact rnDeriv_compProd_prod_sigmaFinite
μ ν ρ κ f hμν hfiber hfiber_meas hf
10 supporting declarations (lemmas, instances)
-
prefixNodes_monolemma — Prefix node sets are monotone in the prefix length.hypothesesconclusionM.prefixNodes m ⊆ M.prefixNodes kProof (Lean source)
lemma prefixNodes_mono (M : SCM N Ω) {m k : ℕ} (h : m ≤ k) : M.prefixNodes m ⊆ M.prefixNodes k := by intro v hv rcases (M.mem_prefixNodes_iff m v).mp hv with ⟨hobs, hlt⟩ exact (M.mem_prefixNodes_iff k v).mpr ⟨hobs, lt_of_lt_of_le hlt h⟩ -
map_pi_valuesEquivOfEqlemma — Measure.pi reindexes along valuesEquivOfEq, with no probability-measure hypothesis (the index equality reduces the equiv to the identity). This is the σ-finite-friendly companion of measurePreserving_valuesEquivOfEq.hypothesesconclusion= pi (fun j : {j // j ∈ J} => μ ⟨j.val, h ▸ j.property⟩)Proof (Lean source)
lemma map_pi_valuesEquivOfEq {M' : Type*} [DecidableEq M'] {I J : Finset M'} {Ω' : M' → Type*} [∀ n, MeasurableSpace (Ω' n)] (h : I = J) (μ : (i : {i // i ∈ I}) → Measure (Ω' i.val)) : (pi μ).map (valuesEquivOfEq (Ω := Ω') h) = pi (fun j : {j // j ∈ J} => μ ⟨j.val, h ▸ j.property⟩) := by subst h have hid : (⇑(valuesEquivOfEq (Ω := Ω') (rfl : I = I)) : ValuesOn I Ω' → ValuesOn I Ω') = id := by funext ξ; rfl rw [hid, MeasureTheory.Measure.map_id] -
singletonValues_map_ref_eq_jointReflemma — The scalar reference on one node maps to the singleton product reference.hypothesesProof (Lean source)
lemma singletonValues_map_ref_eq_jointRef (ref : ReferenceMeasures Ω) (v : SWIGNode N) : (ref.μ v).map (singletonValues (α := swigΩ Ω) (v := v)) = jointRef ref ({v} : Finset (SWIGNode N)) := by classical rw [jointRef] let e := MeasurableEquiv.piUnique (fun i : {i // i ∈ ({v} : Finset (SWIGNode N))} => swigΩ Ω i.val) have hfun : (singletonValues (α := swigΩ Ω) (v := v)) = (fun x : swigΩ Ω v => (e.symm) (by simpa using x)) := by funext x ext i obtain ⟨w, hw⟩ := i have hwv : w = v := by simpa using hw subst w rfl calc map (singletonValues (α := swigΩ Ω) (v := v)) (ref.μ v) = map (fun x : swigΩ Ω v => (e.symm) (by simpa using x)) (ref.μ v) := by rw [hfun] _ = pi (fun i : {i // i ∈ ({v} : Finset (SWIGNode N))} => ref.μ i.val) := by have hmp := (MeasureTheory.measurePreserving_piUnique (fun i : {i // i ∈ ({v} : Finset (SWIGNode N))} => ref.μ i.val)).symm e simpa using hmp.map_eq -
jointRef_prefix_card_maplemma — Transport the full-prefix reference measure to the observed-value reference.hypothesesProof (Lean source)
lemma jointRef_prefix_card_map (M : SCM N Ω) (ref : ReferenceMeasures Ω) : (jointRef ref (M.prefixNodes M.observed.card)).map (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) = jointRef ref M.observed := by rw [jointRef, jointRef, map_pi_valuesEquivOfEq (M.prefixNodes_card M.observed.card (le_refl _)) (fun i => ref.μ i.val)] -
jointRef_extendObsPrefixlemma — The successor prefix extension carries the product of the old-prefix reference and the next-node reference to the successor-prefix reference.hypothesesProof (Lean source)
lemma jointRef_extendObsPrefix (M : SCM N Ω) (ref : ReferenceMeasures Ω) {k : ℕ} (hk : k < M.observed.card) : ((jointRef ref (M.prefixNodes k)).prod (ref.μ (M.observedAt ⟨k, hk⟩).val)).map (M.extendObsPrefix hk) = jointRef ref (M.prefixNodes (k + 1)) := by classical let v : SWIGNode N := (M.observedAt ⟨k, hk⟩).val let A : Finset (SWIGNode N) := M.prefixNodes k let B : Finset (SWIGNode N) := ({v} : Finset (SWIGNode N)) let hDisj : Disjoint A B := by simpa [A, B, v] using M.prefixNodes_disjoint_singleton_next hk have hsing : (ref.μ v).map (singletonValues (α := swigΩ Ω) (v := v)) = jointRef ref B := by simpa [B] using singletonValues_map_ref_eq_jointRef (Ω := Ω) ref v have hprod : ((jointRef ref A).prod (ref.μ v)).map (map id (singletonValues (α := swigΩ Ω) (v := v))) = (jointRef ref A).prod (jointRef ref B) := by rw [← MeasureTheory.Measure.map_prod_map (jointRef ref A) (ref.μ v) measurable_id (measurable_singletonValues (α := swigΩ Ω))] simp [hsing] have hunion : ((jointRef ref A).prod (jointRef ref B)).map ((valuesUnionEquiv (Ω := Ω) hDisj).symm) = jointRef ref (A ∪ B) := by have hmp := (measurePreserving_valuesUnionEquiv (Ω := Ω) hDisj ref.μ).symm (valuesUnionEquiv (Ω := Ω) hDisj) simpa [jointRef] using hmp.map_eq unfold extendObsPrefix change (((jointRef ref A).prod (ref.μ v)).map ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hk).symm) ∘ (fun p : ValuesOn A (swigΩ Ω) × swigΩ Ω v => valuesUnionMk p.1 (singletonValues (α := swigΩ Ω) (v := v) p.2)))) = jointRef ref (M.prefixNodes (k + 1)) rw [← MeasureTheory.Measure.map_map] · have hinner : (fun p : ValuesOn A (swigΩ Ω) × swigΩ Ω v => valuesUnionMk p.1 (singletonValues (α := swigΩ Ω) (v := v) p.2)) = ((fun q : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω) => valuesUnionMk q.1 q.2) ∘ (map id (singletonValues (α := swigΩ Ω) (v := v)))) := by rfl rw [hinner] rw [← MeasureTheory.Measure.map_map] · have hunion_fun : (fun q : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω) => valuesUnionMk q.1 q.2) = ((valuesUnionEquiv (Ω := Ω) hDisj).symm) := by rfl rw [hunion_fun, hprod, hunion] rw [jointRef, map_pi_valuesEquivOfEq] rfl · exact measurable_valuesUnionMk (Ω := swigΩ Ω) · exact measurable_id.prodMap (measurable_singletonValues (α := swigΩ Ω)) · exact (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hk).symm).measurable · exact (measurable_valuesUnionMk (Ω := swigΩ Ω)).comp (measurable_id.prodMap (measurable_singletonValues (α := swigΩ Ω))) -
prefixDensityProduct_eq_range_productlemma — The recursive prefix density product is the range product of its one-step factors.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωref :s :M.FixedValues∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,k :ℕhk :k ≤ M.observed.cardconclusionM.prefixDensityProduct ref s k z= ∏ i ∈ range k, M.prefixStepDensityInPrefix ref s k z iProof (Lean source)
lemma prefixDensityProduct_eq_range_product (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] (k : ℕ) (hk : k ≤ M.observed.card) (z : ValuesOn (M.prefixNodes k) (swigΩ Ω)) : M.prefixDensityProduct ref s k z = ∏ i ∈ range k, M.prefixStepDensityInPrefix ref s k z i := by induction k with | zero => simp [prefixDensityProduct] | succ k ih => have hkcard : k < M.observed.card := Nat.lt_of_succ_le hk rw [prefixDensityProduct] rw [ih (le_of_succ_le hk) (valuesProjection (M.prefixNodes_mono (le_succ k)) z)] rw [Finset.prod_range_succ] congr 1 · refine Finset.prod_congr rfl ?_ intro i hi have hik : i < k := Finset.mem_range.mp hi have hisucc : i < k + 1 := Nat.lt_succ_of_lt hik have hicard : i < M.observed.card := lt_of_lt_of_le hik (le_of_succ_le hk) have hproj : valuesProjection (M.prefixNodes_mono (le_of_lt hik)) (valuesProjection (M.prefixNodes_mono (le_succ k)) z) = valuesProjection (M.prefixNodes_mono (le_of_lt hisucc)) z := by funext a rfl simp [prefixStepDensityInPrefix, hik, hisucc, hicard, hproj, valuesProjection] · simp [prefixStepDensityInPrefix, hkcard] -
prefixDensityProduct_card_eq_qFactorDensityProductlemma — At the full observed prefix, the recursive prefix density product is the existing finite product over observed indices.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωref :s :M.FixedValues∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,conclusionM.prefixDensityProduct ref s M.observed.card y= M.qFactorDensityProduct ref s ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) y)Proof (Lean source)
lemma prefixDensityProduct_card_eq_qFactorDensityProduct (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] (y : ValuesOn (M.prefixNodes M.observed.card) (swigΩ Ω)) : M.prefixDensityProduct ref s M.observed.card y = M.qFactorDensityProduct ref s ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) y) := by rw [prefixDensityProduct_eq_range_product M ref s M.observed.card (le_refl _) y] rw [Finset.prod_range] simp only [qFactorDensityProduct, obsStepCondDensity, prefixStepDensityInPrefix, valuesEquivOfEq] refine Finset.prod_congr rfl ?_ intro i _hi have hproj : valuesProjection (M.prefixNodes_subset_observed i.val) (valuesProjection (le_of_eq (M.prefixNodes_card M.observed.card (le_refl _)).symm) y) = valuesProjection (M.prefixNodes_mono (le_of_lt i.isLt)) y := by funext a rfl simp only [i.isLt] rfl -
rnDeriv_compProd_same_leftlemma — Conditional factor of the composition-product Radon–Nikodym derivative.hypothesesconclusion(μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) =ᵐ[μ ⊗ₘ η] fun p => rnDeriv κ η p.1 p.2Proof (Lean source)
lemma rnDeriv_compProd_same_left {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [CountableOrCountablyGenerated α β] (μ : Measure α) (κ η : Kernel α β) [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] (h_ac : ∀ a, κ a ≪ η a) : (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) =ᵐ[μ ⊗ₘ η] fun p => rnDeriv κ η p.1 p.2 := by have hκeq : η.withDensity (rnDeriv κ η) = κ := ProbabilityTheory.Kernel.ext fun a => ProbabilityTheory.Kernel.withDensity_rnDeriv_eq (h_ac a) haveI : IsSFiniteKernel (η.withDensity (rnDeriv κ η)) := by rw [hκeq]; infer_instance have hcp : μ ⊗ₘ κ = (μ ⊗ₘ η).withDensity (fun p => rnDeriv κ η p.1 p.2) := by conv_lhs => rw [← hκeq] exact MeasureTheory.Measure.compProd_withDensity (ProbabilityTheory.Kernel.measurable_rnDeriv κ η) rw [hcp] exact MeasureTheory.Measure.rnDeriv_withDensity (μ ⊗ₘ η) (ProbabilityTheory.Kernel.measurable_rnDeriv κ η) -
absolutelyContinuous_of_map_measurableEmbeddinglemma — Pull absolute continuity back through a measurable embedding.Proof (Lean source)
lemma absolutelyContinuous_of_map_measurableEmbedding {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) {μ ν : Measure α} (h : μ.map f ≪ ν.map f) : μ ≪ ν := by intro A hνA have hν_image : ν.map f (f '' A) = 0 := by rw [hf.map_apply ν (f '' A), hf.injective.preimage_image] exact hνA have hμ_image : μ.map f (f '' A) = 0 := h hν_image rw [hf.map_apply μ (f '' A), hf.injective.preimage_image] at hμ_image exact hμ_image -
rnDeriv_compProd_same_left_aelemma — Same-left composition-product RN derivative under a.e. fibre absolute continuity. This is the a.e. variant needed after extracting fibre domination from product domination.hypothesesconclusion(μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) =ᵐ[μ ⊗ₘ η] fun p => rnDeriv κ η p.1 p.2Proof (Lean source)
lemma rnDeriv_compProd_same_left_ae {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [CountableOrCountablyGenerated α β] (μ : Measure α) (κ η : Kernel α β) [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] (h_ac : ∀ᵐ a ∂μ, κ a ≪ η a) : (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) =ᵐ[μ ⊗ₘ η] fun p => rnDeriv κ η p.1 p.2 := by have hκeq : κ =ᵐ[μ] η.withDensity (rnDeriv κ η) := by filter_upwards [h_ac] with a ha exact (ProbabilityTheory.Kernel.withDensity_rnDeriv_eq ha).symm haveI : IsSFiniteKernel (η.withDensity (rnDeriv κ η)) := by infer_instance have hcp : μ ⊗ₘ κ = (μ ⊗ₘ η).withDensity (fun p => rnDeriv κ η p.1 p.2) := by calc μ ⊗ₘ κ = μ ⊗ₘ (η.withDensity (rnDeriv κ η)) := MeasureTheory.Measure.compProd_congr hκeq _ = (μ ⊗ₘ η).withDensity (fun p => rnDeriv κ η p.1 p.2) := by exact MeasureTheory.Measure.compProd_withDensity (ProbabilityTheory.Kernel.measurable_rnDeriv κ η) rw [hcp] exact MeasureTheory.Measure.rnDeriv_withDensity (μ ⊗ₘ η) (ProbabilityTheory.Kernel.measurable_rnDeriv κ η)
RadonNikodym 1 core · 8 supporting This file proves the prefix induction that turns stepwise conditional Radon--Nikodym derivatives into the density of the observational chain kernel. ★ obsDensity_eq_qFactorDensityProduct
Radon--Nikodym chain rule for observational densities
This file proves the prefix induction that turns stepwise conditional
Radon--Nikodym derivatives into the density of the observational chain kernel.
It concludes that obsDensity equals the product of the one-node q-factor
densities under the stated domination and measurability assumptions.
theorem obsDensity_eq_qFactorDensityProduct reviewed
⚑ flagged
Causalean.SCM
Observational density chain rule. In a structural causal model whose observational law is absolutely continuous with respect to the joint reference measure on the observed nodes, if in addition the stepwise fibre Radon--Nikodym condition holds along the observed topological order, then the joint observational density agrees, almost everywhere with respect to that joint reference measure, with the product of the one-node conditional density factors taken in observed topological order.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M :
SCM N Ω
ref :
hdom :
DominatedObs M ref
s :
M.FixedValues
∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')
∀ (k : ℕ) (hk : k < M.observed.card),
∀ k : ℕ,
hstep :
ObsStepFiberRN M ref s
conclusion
M.obsDensity ref s =ᵐ[jointRef ref M.observed] M.qFactorDensityProduct ref s
Proof (Lean source)
theorem obsDensity_eq_qFactorDensityProduct
(M : SCM N Ω) (ref : ReferenceMeasures Ω)
(hdom : DominatedObs M ref) (s : M.FixedValues)
[∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')]
[∀ (k : ℕ) (hk : k < M.observed.card),
StandardBorelSpace
(ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))]
[∀ (k : ℕ) (hk : k < M.observed.card),
Nonempty
(ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))]
[∀ k : ℕ,
CountableOrCountablyGenerated
M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))]
(hstep : ObsStepFiberRN M ref s) :
M.obsDensity ref s =ᵐ[jointRef ref M.observed]
M.qFactorDensityProduct ref s := by
unfold obsDensity
rw [obsKernel_eq_chainRuleProduct M s]
exact M.qFactorProduct_rnDeriv_eq_qFactorDensityProduct ref hdom s hstep
8 supporting declarations (lemmas, instances)
-
obsChainKernel_absolutelyContinuous_jointRef_prefixlemma — Domination of the recursive observed-prefix chain by the prefix reference.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωref :hdom :DominatedObs M refs :M.FixedValues∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,k :ℕhk :k ≤ M.observed.cardconclusionM.obsChainKernel k hk s ≪ jointRef ref (M.prefixNodes k)Proof (Lean source)
lemma obsChainKernel_absolutelyContinuous_jointRef_prefix (M : SCM N Ω) (ref : ReferenceMeasures Ω) (hdom : DominatedObs M ref) (s : M.FixedValues) [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] (k : ℕ) (hk : k ≤ M.observed.card) : M.obsChainKernel k hk s ≪ jointRef ref (M.prefixNodes k) := by classical -- The chain kernel is the prefix marginal of the (dominated) observational law. rw [← M.obsKernel_map_prefixNodes s k hk] have hsubset : M.prefixNodes k ⊆ M.observed := M.prefixNodes_subset_observed k have hDisj : Disjoint (M.prefixNodes k) (M.observed \ M.prefixNodes k) := disjoint_sdiff_self_right have hAB : M.prefixNodes k ∪ (M.observed \ M.prefixNodes k) = M.observed := Finset.union_sdiff_of_subset hsubset -- The prefix projection factors as `fst ∘ union-equiv ∘ reindex`. have hfun : (valuesProjection (Ω := swigΩ Ω) hsubset) = fst ∘ (valuesUnionEquiv (Ω := Ω) hDisj) ∘ (valuesEquivOfEq (Ω := swigΩ Ω) hAB.symm) := by funext ω i; rfl -- The reference marginal is a scalar multiple of the prefix reference. have hmarg : (jointRef ref M.observed).map (valuesProjection hsubset) = (jointRef ref (M.observed \ M.prefixNodes k) univ) • jointRef ref (M.prefixNodes k) := by rw [hfun] rw [← MeasureTheory.Measure.map_map measurable_fst ((valuesUnionEquiv (Ω := Ω) hDisj).measurable.comp (valuesEquivOfEq (Ω := swigΩ Ω) hAB.symm).measurable)] rw [← MeasureTheory.Measure.map_map (valuesUnionEquiv (Ω := Ω) hDisj).measurable (valuesEquivOfEq (Ω := swigΩ Ω) hAB.symm).measurable] rw [jointRef, map_pi_valuesEquivOfEq hAB.symm (fun i : {i // i ∈ M.observed} => ref.μ i.val)] have hsplit : (pi (fun j : {j // j ∈ M.prefixNodes k ∪ (M.observed \ M.prefixNodes k)} => ref.μ j.val)).map (valuesUnionEquiv (Ω := Ω) hDisj) = (jointRef ref (M.prefixNodes k)).prod (jointRef ref (M.observed \ M.prefixNodes k)) := by have hmp := measurePreserving_valuesUnionEquiv (Ω := Ω) hDisj ref.μ simpa [jointRef] using hmp.map_eq rw [hsplit, MeasureTheory.Measure.map_fst_prod] -- Push the joint domination forward and absorb the scalar. refine ((hdom s).map (measurable_valuesProjection hsubset)).trans ?_ rw [hmarg] intro t ht simp [MeasureTheory.Measure.smul_apply, ht] -
obsChainKernel_rnDeriv_eq_prefixDensityProductlemma — General prefix-level RN derivative for the recursive observational chain.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωref :hdom :DominatedObs M refs :M.FixedValues∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,hstep :ObsStepFiberRN M ref sk :ℕhk :k ≤ M.observed.cardProof (Lean source)
lemma obsChainKernel_rnDeriv_eq_prefixDensityProduct (M : SCM N Ω) (ref : ReferenceMeasures Ω) (hdom : DominatedObs M ref) (s : M.FixedValues) [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] (hstep : ObsStepFiberRN M ref s) : ∀ (k : ℕ) (hk : k ≤ M.observed.card), (M.obsChainKernel k hk s).rnDeriv (jointRef ref (M.prefixNodes k)) =ᵐ[jointRef ref (M.prefixNodes k)] M.prefixDensityProduct ref s k := by intro k induction k with | zero => intro hk -- `ValuesOn (prefixNodes 0)` is a one-point space; both measures are probability -- measures there, hence equal, and `rnDeriv_self =ᵐ 1 = prefixDensityProduct 0`. have hsub : Subsingleton (ValuesOn (M.prefixNodes 0) (swigΩ Ω)) := ⟨fun a b => funext fun i => absurd (M.prefixNodes_zero ▸ i.property) (notMem_empty i.val)⟩ have heq : M.obsChainKernel 0 hk s = jointRef ref (M.prefixNodes 0) := by refine MeasureTheory.Measure.ext fun A _ => ?_ rcases Set.eq_empty_or_nonempty A with rfl | hA · simp · obtain ⟨a, ha⟩ := hA have hAuniv : A = univ := Set.eq_univ_of_forall fun x => (hsub.elim x a) ▸ ha subst hAuniv rw [MeasureTheory.measure_univ, jointRef, MeasureTheory.Measure.pi_univ] symm apply Finset.prod_eq_one intro i _ obtain ⟨_, hlt⟩ := (M.mem_prefixNodes_iff 0 i.val).mp i.property exact absurd hlt (Nat.not_lt_zero _) rw [heq] have h1 : M.prefixDensityProduct ref s 0 = (fun _ => (1 : ENNReal)) := rfl rw [h1] exact MeasureTheory.Measure.rnDeriv_self _ | succ k ih => intro hk classical have hkc : k < M.observed.card := Nat.lt_of_succ_le hk have hkprev : k ≤ M.observed.card := Nat.le_of_succ_le hk let node : SWIGNode N := (M.observedAt ⟨k, hkc⟩).val let νk : Measure (ValuesOn (M.prefixNodes k) (swigΩ Ω)) := jointRef ref (M.prefixNodes k) let refnode : Measure (swigΩ Ω node) := ref.μ node let chain : Measure (ValuesOn (M.prefixNodes k) (swigΩ Ω)) := M.obsChainKernel k hkprev s let stepK : Kernel (ValuesOn (M.prefixNodes k) (swigΩ Ω)) (swigΩ Ω node) := (M.obsStepCondKernel hkc).sectR s let ext : ValuesOn (M.prefixNodes k) (swigΩ Ω) × swigΩ Ω node → ValuesOn (M.prefixNodes (k + 1)) (swigΩ Ω) := M.extendObsPrefix hkc have hchainSucc : M.obsChainKernel (k + 1) hk s = (chain ⊗ₘ stepK).map ext := by dsimp [chain, stepK, ext] change ((((M.obsChainKernel k hkprev) ⊗ₖ (M.obsStepCondKernel hkc)).map (M.extendObsPrefix hkc)) s) = (((M.obsChainKernel k hkprev) s) ⊗ₘ ((M.obsStepCondKernel hkc).sectR s)).map (M.extendObsPrefix hkc) rw [ProbabilityTheory.Kernel.map_apply _ (M.measurable_extendObsPrefix hkc)] rw [ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR] have hrefSucc : jointRef ref (M.prefixNodes (k + 1)) = (νk.prod refnode).map ext := by dsimp [νk, refnode, node, ext] exact (jointRef_extendObsPrefix M ref hkc).symm have hsingle_emb : MeasurableEmbedding (singletonValues (α := swigΩ Ω) (v := node)) := by refine ⟨?_, measurable_singletonValues (α := swigΩ Ω), ?_⟩ · intro x y hxy have := congrArg (singletonValue (α := swigΩ Ω) (v := node)) hxy simpa using this · intro A hA have hpre : singletonValues (α := swigΩ Ω) (v := node) '' A = (singletonValue (α := swigΩ Ω) (v := node)) ⁻¹' A := by ext x constructor · rintro ⟨a, ha, rfl⟩ simpa using ha · intro hx refine ⟨singletonValue (α := swigΩ Ω) (v := node) x, hx, ?_⟩ exact singletonValues_singletonValue (α := swigΩ Ω) x rw [hpre] exact hA.preimage (measurable_singletonValue (α := swigΩ Ω)) have hext_emb : MeasurableEmbedding ext := by dsimp [ext, node] unfold extendObsPrefix refine (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hkc).symm).measurableEmbedding.comp ?_ change MeasurableEmbedding ((fun q : ValuesOn (M.prefixNodes k) (swigΩ Ω) × ValuesOn ({(M.observedAt ⟨k, hkc⟩).val} : Finset (SWIGNode N)) (swigΩ Ω) => valuesUnionMk q.1 q.2) ∘ map id (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨k, hkc⟩).val))) refine ((valuesUnionEquiv (Ω := Ω) (M.prefixNodes_disjoint_singleton_next hkc)).symm.measurableEmbedding).comp ?_ exact MeasurableEmbedding.id.prodMap hsingle_emb have hcore : (chain ⊗ₘ stepK).rnDeriv (νk.prod refnode) =ᵐ[νk.prod refnode] fun p => M.prefixDensityProduct ref s k p.1 * (stepK p.1).rnDeriv refnode p.2 := by have hchain_ac : chain ≪ νk := by dsimp [chain, νk] exact M.obsChainKernel_absolutelyContinuous_jointRef_prefix ref hdom s k hkprev have hfiber := hstep k hkc have hfiber_meas : AEMeasurable (fun p : ValuesOn (M.prefixNodes k) (swigΩ Ω) × swigΩ Ω node => (stepK p.1).rnDeriv refnode p.2) (νk.prod refnode) := hfiber.2 exact rnDeriv_compProd_prod_sigmaFinite_of_fiber_ac chain νk refnode stepK (M.prefixDensityProduct ref s k) hchain_ac hfiber.1 hfiber_meas (ih hkprev) rw [hchainSucc, hrefSucc, EventuallyEq, hext_emb.ae_map_iff] filter_upwards [hext_emb.rnDeriv_map (chain ⊗ₘ stepK) (νk.prod refnode), hcore] with p hmap hp rw [hmap, hp] dsimp [ext, stepK, node] have hpair := M.valuesUnionEquiv_extendObsPrefix hkc p have hproj_ext : valuesProjection (M.prefixNodes_mono (le_succ k)) (M.extendObsPrefix hkc p) = p.1 := by funext i have hi := congrArg (fun q => q.1 i) hpair exact hi have hcoord_ext : M.extendObsPrefix hkc p ⟨(M.observedAt ⟨k, hkc⟩).val, by rw [M.prefixNodes_succ hkc] exact mem_union_right _ (mem_singleton_self _)⟩ = p.2 := by have hnext := congrArg (fun q => singletonValue (α := swigΩ Ω) (v := (M.observedAt ⟨k, hkc⟩).val) q.2) hpair exact hnext rw [prefixDensityProduct] simp [hkc, hproj_ext, hcoord_ext, refnode] rfl -
qFactorProduct_rnDeriv_eq_obsChainKernel_card_pullback_of_jointReflemma — RN-derivative transport for qFactorProduct, assuming the final reference transport has already been identified.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωref :s :M.FixedValueshref :∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,Proof (Lean source)
lemma qFactorProduct_rnDeriv_eq_obsChainKernel_card_pullback_of_jointRef (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) (href : (jointRef ref (M.prefixNodes M.observed.card)).map (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) = jointRef ref M.observed) [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] : (M.qFactorProduct s).rnDeriv (jointRef ref M.observed) =ᵐ[jointRef ref M.observed] fun x => ((M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card))) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))).symm x) := by classical set e := valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _)) with he have hf : MeasurableEmbedding (e : ValuesOn (M.prefixNodes M.observed.card) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) := e.measurableEmbedding have hq : M.qFactorProduct s = (M.obsChainKernel M.observed.card (le_refl _) s).map e := by rw [qFactorProduct, ProbabilityTheory.Kernel.map_apply _ e.measurable] rw [hq, ← href, EventuallyEq, hf.ae_map_iff] filter_upwards [hf.rnDeriv_map (M.obsChainKernel M.observed.card (le_refl _) s) (jointRef ref (M.prefixNodes M.observed.card))] with y hy simpa using hy -
qFactorProduct_rnDeriv_eq_obsChainKernel_card_pullbacklemma — Peel the final qFactorProduct map back to the full prefix chain kernel.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωref :s :M.FixedValues∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,Proof (Lean source)
lemma qFactorProduct_rnDeriv_eq_obsChainKernel_card_pullback (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] : (M.qFactorProduct s).rnDeriv (jointRef ref M.observed) =ᵐ[jointRef ref M.observed] fun x => ((M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card))) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))).symm x) := by exact qFactorProduct_rnDeriv_eq_obsChainKernel_card_pullback_of_jointRef M ref s (jointRef_prefix_card_map M ref) -
obsChainKernel_card_rnDeriv_eq_qFactorDensityProduct_prefixlemma — The analytic prefix induction for the density chain rule.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωref :hdom :DominatedObs M refs :M.FixedValues∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,hstep :ObsStepFiberRN M ref sProof (Lean source)
lemma obsChainKernel_card_rnDeriv_eq_qFactorDensityProduct_prefix (M : SCM N Ω) (ref : ReferenceMeasures Ω) (hdom : DominatedObs M ref) (s : M.FixedValues) [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] (hstep : ObsStepFiberRN M ref s) : (M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card)) =ᵐ[jointRef ref (M.prefixNodes M.observed.card)] fun y => M.qFactorDensityProduct ref s ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) y) := by exact (obsChainKernel_rnDeriv_eq_prefixDensityProduct M ref hdom s hstep M.observed.card (le_refl _)).trans (Filter.EventuallyEq.of_eq (funext (prefixDensityProduct_card_eq_qFactorDensityProduct M ref s))) -
obsChainKernel_card_rnDeriv_pullback_eq_qFactorDensityProduct_of_prefixlemma — Push the full-prefix a.e. density identity forward, assuming the reference transport and prefix-level chain rule.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωref :s :M.FixedValueshref :∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,Proof (Lean source)
lemma obsChainKernel_card_rnDeriv_pullback_eq_qFactorDensityProduct_of_prefix (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) (href : (jointRef ref (M.prefixNodes M.observed.card)).map (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) = jointRef ref M.observed) [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] (hprefix : (M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card)) =ᵐ[jointRef ref (M.prefixNodes M.observed.card)] fun y => M.qFactorDensityProduct ref s ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) y)) : (fun x => ((M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card))) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))).symm x)) =ᵐ[jointRef ref M.observed] M.qFactorDensityProduct ref s := by classical set e := valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _)) with he have hf : MeasurableEmbedding (e : ValuesOn (M.prefixNodes M.observed.card) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) := e.measurableEmbedding rw [← href, EventuallyEq, hf.ae_map_iff] filter_upwards [hprefix] with y hy simpa using hy -
obsChainKernel_card_rnDeriv_pullback_eq_qFactorDensityProductlemma — Push the full-prefix a.e. density identity forward to observed coordinates.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωref :hdom :DominatedObs M refs :M.FixedValues∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,hstep :ObsStepFiberRN M ref sProof (Lean source)
lemma obsChainKernel_card_rnDeriv_pullback_eq_qFactorDensityProduct (M : SCM N Ω) (ref : ReferenceMeasures Ω) (hdom : DominatedObs M ref) (s : M.FixedValues) [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] (hstep : ObsStepFiberRN M ref s) : (fun x => ((M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card))) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))).symm x)) =ᵐ[jointRef ref M.observed] M.qFactorDensityProduct ref s := by exact obsChainKernel_card_rnDeriv_pullback_eq_qFactorDensityProduct_of_prefix M ref s (jointRef_prefix_card_map M ref) (obsChainKernel_card_rnDeriv_eq_qFactorDensityProduct_prefix M ref hdom s hstep) -
qFactorProduct_rnDeriv_eq_qFactorDensityProducttheorem — Analytic chain rule for the mapped observational product kernel.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωref :hdom :DominatedObs M refs :M.FixedValues∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,hstep :ObsStepFiberRN M ref sProof (Lean source)
theorem qFactorProduct_rnDeriv_eq_qFactorDensityProduct (M : SCM N Ω) (ref : ReferenceMeasures Ω) (hdom : DominatedObs M ref) (s : M.FixedValues) [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] (hstep : ObsStepFiberRN M ref s) : (M.qFactorProduct s).rnDeriv (jointRef ref M.observed) =ᵐ[jointRef ref M.observed] M.qFactorDensityProduct ref s := by exact (qFactorProduct_rnDeriv_eq_obsChainKernel_card_pullback M ref s).trans (obsChainKernel_card_rnDeriv_pullback_eq_qFactorDensityProduct M ref hdom s hstep)