English
Restricting kernels and then taking compProd equals restricting the compProd to the product of the restrictions.
Русский
Ограничение ядер и затем произведение композицией эквивалентно ограничению полученного компProd до произведения ограничений.
LaTeX
$$$$ \mathrm{restrict}(\kappa, hs) \otimes_k \mathrm{restrict}(\eta, ht) = \mathrm{restrict}(\kappa \otimes_k \eta, hs \times ht). $$$$
Lean4
theorem compProd_restrict {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) :
Kernel.restrict κ hs ⊗ₖ Kernel.restrict η ht = Kernel.restrict (κ ⊗ₖ η) (hs.prod ht) :=
by
ext a u hu
rw [compProd_apply hu, restrict_apply' _ _ _ hu, compProd_apply (hu.inter (hs.prod ht))]
simp only [restrict_apply, Set.preimage, Measure.restrict_apply' ht, Set.mem_inter_iff, Set.mem_prod]
have (b : _) :
η (a, b) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = s.indicator (fun b => η (a, b) ({c : γ | (b, c) ∈ u} ∩ t)) b := by
classical
rw [Set.indicator_apply]
split_ifs with h
· simp only [h, true_and, Set.inter_def, Set.mem_setOf]
· simp only [h, false_and, and_false, Set.setOf_false, measure_empty]
simp_rw [this]
rw [lintegral_indicator hs]
