English
If hη holds, then fst κ ⊗ borelMarkovFromReal Ω η equals κ.
Русский
Если выполняется условие hη, то fst κ ⊗ borelMarkovFromReal Ω η равно κ.
LaTeX
$$$fst\\,κ \\otimes_{ℓ} borelMarkovFromReal\\,Ω\\,η = κ$$$
Lean4
/-- For `κ' := map κ (Prod.map (id : β → β) e)`, the hypothesis `hη` is `fst κ' ⊗ₖ η = κ'`.
With that hypothesis, `fst κ ⊗ₖ borelMarkovFromReal κ η = κ`. -/
theorem compProd_fst_borelMarkovFromReal (κ : Kernel α (β × Ω)) [IsSFiniteKernel κ] (η : Kernel (α × β) ℝ)
[IsSFiniteKernel η]
(hη :
(fst (map κ (Prod.map (id : β → β) (embeddingReal Ω)))) ⊗ₖ η = map κ (Prod.map (id : β → β) (embeddingReal Ω))) :
fst κ ⊗ₖ borelMarkovFromReal Ω η = κ := 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
have : κ = comapRight κ' h_prod_embed := by
ext c t : 2
unfold κ'
rw [comapRight_apply, map_apply _ (by fun_prop), h_prod_embed.comap_map]
conv_rhs => rw [this, ← hη']
exact compProd_fst_borelMarkovFromReal_eq_comapRight_compProd κ η hη
