English
Under hypothesis hη, fst κ ⊗ borelMarkovFromReal Ω η equals comapRight (fst (map κ (Prod.map id (embeddingReal Ω))) ⊗ η) (measurableEmbedding_embeddingReal Ω).
Русский
При условии hη выполняется равенство fst κ ⊗ borelMarkovFromReal Ω η = comapRight (fst (map κ (Prod.map id (embeddingReal Ω))) ⊗ η) (плотное вложение embeddingReal Ω).
LaTeX
$$$fst\\,κ \\otimes_{ℓ} borelMarkovFromReal\\,Ω\\,η = comapRight (fst (map κ (Prod.map (id) (embeddingReal\\,Ω))) \\otimes_{ℓ} η) (measurableEmbedding_embeddingReal Ω)$$$
Lean4
/-- For `κ' := map κ (Prod.map (id : β → β) e)`, the hypothesis `hη` is `fst κ' ⊗ₖ η = κ'`.
The conclusion of the lemma is `fst κ ⊗ₖ borelMarkovFromReal Ω η = comapRight (fst κ' ⊗ₖ η) _`. -/
theorem compProd_fst_borelMarkovFromReal_eq_comapRight_compProd (κ : Kernel α (β × Ω)) [IsSFiniteKernel κ]
(η : Kernel (α × β) ℝ) [IsSFiniteKernel η]
(hη :
(fst (map κ (Prod.map (id : β → β) (embeddingReal Ω)))) ⊗ₖ η = map κ (Prod.map (id : β → β) (embeddingReal Ω))) :
fst κ ⊗ₖ borelMarkovFromReal Ω η =
comapRight (fst (map κ (Prod.map (id : β → β) (embeddingReal Ω))) ⊗ₖ η)
(MeasurableEmbedding.id.prodMap (measurableEmbedding_embeddingReal Ω)) :=
by
let e := embeddingReal Ω
let he := measurableEmbedding_embeddingReal Ω
let κ' := map κ (Prod.map (id : β → β) e)
have hη' : fst κ' ⊗ₖ η = κ' := hη
have h_prod_embed : MeasurableEmbedding (Prod.map (id : β → β) e) := MeasurableEmbedding.id.prodMap he
change fst κ ⊗ₖ borelMarkovFromReal Ω η = comapRight (fst κ' ⊗ₖ η) h_prod_embed
rw [comapRight_compProd_id_prod _ _ he]
have h_fst : fst κ' = fst κ := by
ext a u
unfold κ'
rw [fst_apply, map_apply _ (by fun_prop), Measure.map_map measurable_fst h_prod_embed.measurable, fst_apply]
congr
rw [h_fst]
ext a t ht : 2
simp_rw [compProd_apply ht]
refine lintegral_congr_ae ?_
have h_ae : ∀ᵐ t ∂(fst κ a), (a, t) ∈ {p : α × β | η p (range e)ᶜ = 0} :=
by
rw [← h_fst]
have h_compProd : κ' a (univ ×ˢ range e)ᶜ = 0 := by
unfold κ'
rw [map_apply' _ (by fun_prop)]
swap; · exact (MeasurableSet.univ.prod he.measurableSet_range).compl
suffices Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ = ∅ by rw [this]; simp
ext x
simp
rw [← hη', compProd_null] at h_compProd
swap; · exact (MeasurableSet.univ.prod he.measurableSet_range).compl
simp only [preimage_compl, mem_univ, mk_preimage_prod_right] at h_compProd
exact h_compProd
filter_upwards [h_ae] with a ha
rw [borelMarkovFromReal, comapRight_apply', comapRight_apply']
rotate_left
· exact measurable_prodMk_left ht
· exact measurable_prodMk_left ht
classical
rw [piecewise_apply, if_pos]
exact ha
