English
A final simplification of the fst_compProd_apply lemma, giving the explicit expression for the first marginal of the product kernel.
Русский
Финальное упрощение леммы fst_compProd_apply, явное выражение первого маргинала произведения ядра.
LaTeX
$$$$ (κ ⊗ₖ η)^{{\\text{fst}}} x\, s = \\int^\\!- b \\, s.indicator(b) \\, η(x,b) Set.univ \\, d(κ x). $$$$
Lean4
theorem hasFiniteIntegral_compProd_iff ⦃f : β × γ → E⦄ (h1f : StronglyMeasurable f) :
HasFiniteIntegral f ((κ ⊗ₖ η) a) ↔
(∀ᵐ x ∂κ a, HasFiniteIntegral (fun y => f (x, y)) (η (a, x))) ∧
HasFiniteIntegral (fun x => ∫ y, ‖f (x, y)‖ ∂η (a, x)) (κ a) :=
by
simp only [hasFiniteIntegral_iff_enorm]
rw [lintegral_compProd _ _ _ h1f.enorm]
have : ∀ x, ∀ᵐ y ∂η (a, x), 0 ≤ ‖f (x, y)‖ := fun x => Eventually.of_forall fun y => norm_nonneg _
simp_rw [integral_eq_lintegral_of_nonneg_ae (this _)
(h1f.norm.comp_measurable measurable_prodMk_left).aestronglyMeasurable,
enorm_eq_ofReal toReal_nonneg, ofReal_norm_eq_enorm]
have : ∀ {p q r : Prop} (_ : r → p), (r ↔ p ∧ q) ↔ p → (r ↔ q) := fun {p q r} h1 => by
rw [← and_congr_right_iff, and_iff_right_of_imp h1]
rw [this]
· intro h2f; rw [lintegral_congr_ae]
filter_upwards [h2f] with x hx
rw [ofReal_toReal]; finiteness
· intro h2f; refine ae_lt_top ?_ h2f.ne; exact h1f.enorm.lintegral_kernel_prod_right''
