English
For 𝕜 with RCLike structure and E a normed space, ∫ z f(z.fst) · g(z.snd) equals (∫ f) (∫ g).
Русский
Для упорядоченного над полем 𝕜 и пространства E выполняется формула: интеграл от f(z.fst)·g(z.snd) по μ×ν равен произведению интегралов ∫ f и ∫ g.
LaTeX
$$$$\\int_{μ×ν} f(z.fst) \\cdot g(z.snd) \\, dμ×ν = \\left(\\int_μ f \\right) \\cdot \\left(\\int_ν g \\right).$$$$
Lean4
theorem integral_prod_smul {𝕜 : Type*} [RCLike 𝕜] [NormedSpace 𝕜 E] (f : α → 𝕜) (g : β → E) :
∫ z, f z.1 • g z.2 ∂μ.prod ν = (∫ x, f x ∂μ) • ∫ y, g y ∂ν :=
by
by_cases hE : CompleteSpace E; swap; · simp [integral, hE]
by_cases h : Integrable (fun z : α × β => f z.1 • g z.2) (μ.prod ν)
· rw [integral_prod _ h]
simp_rw [integral_smul, integral_smul_const]
have H : ¬Integrable f μ ∨ ¬Integrable g ν := by
contrapose! h
exact h.1.smul_prod h.2
rcases H with H | H <;> simp [integral_undef h, integral_undef H]
