English
For κ and η kernels, the function p ↦ rnDerivAux κ η a p.2 is measurable in p for fixed a, ensuring well-defined RN-derivatives along the second variable.
Русский
Для ядер κ и η отображение p ↦ rnDerivAux κ η a p.2 обусловлено измеримостью по второй переменной.
LaTeX
$$$$ \text{Measurable}_{p}\; rnDerivAux (κ,η) (a) (p_1,p_2). $$$$
Lean4
theorem lintegral_mul (hπ : IsProper π) (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hf : Measurable[𝓧] f) (hg : Measurable[𝓑] g) (x₀ : X) :
∫⁻ x, g x * f x ∂(π x₀) = g x₀ * ∫⁻ x, f x ∂(π x₀) :=
by
refine hg.ennreal_induction ?_ ?_ ?_
· rintro c A hA
simp_rw [← smul_indicator_one_apply, smul_mul_assoc, smul_eq_mul]
rw [lintegral_const_mul, hπ.lintegral_indicator_mul h𝓑𝓧 hf hA]
· measurability
· rintro g₁ g₂ - _ hg₂_meas hg₁ hg₂
simp only [Pi.add_apply, add_mul]
rw [lintegral_add_right, hg₁, hg₂]
· exact (hg₂_meas.mono h𝓑𝓧 le_rfl).mul hf
· rintro g' hg'_meas hg'_mono hg'
simp_rw [ENNReal.iSup_mul]
rw [lintegral_iSup (fun n ↦ ((hg'_meas _).mono h𝓑𝓧 le_rfl).mul hf) (hg'_mono.mul_const (zero_le _))]
simp_rw [hg']
