English
For finite η, the product kernel applied to Set.univ is bounded by the product of the marginal κ a Set.univ and η.bound; i.e., (κ ⊗ η) a Set.univ ≤ κ a Set.univ · η.bound.
Русский
Для конечного η произведение ядра ограничено произведением маргинала: (κ ⊗ η) a Set.univ ≤ κ a Set.univ · η.bound.
LaTeX
$$$$ (κ ⊗ₖ η) a \\ Set.univ \\le κ a \\ Set.univ \\cdot η.bound. $$$$
Lean4
theorem hasFiniteIntegral_prodMk_left (a : α) {s : Set (β × γ)} (h2s : (κ ⊗ₖ η) a s ≠ ∞) :
HasFiniteIntegral (fun b => (η (a, b)).real (Prod.mk b ⁻¹' s)) (κ a) :=
by
let t := toMeasurable ((κ ⊗ₖ η) a) s
simp_rw [hasFiniteIntegral_iff_enorm, measureReal_def, enorm_eq_ofReal toReal_nonneg]
calc
∫⁻ b, ENNReal.ofReal (η (a, b) (Prod.mk b ⁻¹' s)).toReal ∂κ a
_ ≤ ∫⁻ b, η (a, b) (Prod.mk b ⁻¹' t) ∂κ a :=
by
refine lintegral_mono_ae ?_
filter_upwards [ae_kernel_lt_top a h2s] with b hb
rw [ofReal_toReal hb.ne]
exact measure_mono (preimage_mono (subset_toMeasurable _ _))
_ ≤ (κ ⊗ₖ η) a t := (le_compProd_apply _ _ _ _)
_ = (κ ⊗ₖ η) a s := (measure_toMeasurable s)
_ < ⊤ := h2s.lt_top
