English
If f is deterministic and measurable, then (κ ⊗ₖ deterministic f) x on s equals κ x {b | (b, f(x,b)) ∈ s}.
Русский
Если f детерминированно и измеримо, то (κ ⊗ₖ deterministic f) x (s) = κ x { b : β | (b, f(x,b)) ∈ s }.
LaTeX
$$$$ (κ \otimes_k \text{deterministic } f) x(s) = κ x \{ b \mid (b, f(x,b)) \in s \}. $$$$
Lean4
theorem compProd_deterministic_apply [MeasurableSingletonClass γ] {f : α × β → γ} (hf : Measurable f) {s : Set (β × γ)}
(hs : MeasurableSet s) (κ : Kernel α β) [IsSFiniteKernel κ] (x : α) :
(κ ⊗ₖ deterministic f hf) x s = κ x {b | (b, f (x, b)) ∈ s} := by
classical
simp only [deterministic_apply, Measure.dirac_apply, Set.indicator_apply, Pi.one_apply, compProd_apply hs]
let t := {b | (b, f (x, b)) ∈ s}
have ht : MeasurableSet t := (measurable_id.prodMk (hf.comp measurable_prodMk_left)) hs
rw [← lintegral_add_compl _ ht]
convert add_zero _
· suffices ∀ b ∈ tᶜ, (if f (x, b) ∈ Prod.mk b ⁻¹' s then (1 : ℝ≥0∞) else 0) = 0 by
rw [setLIntegral_congr_fun ht.compl this, lintegral_zero]
intro b hb
simp only [t, Set.mem_compl_iff, Set.mem_setOf_eq] at hb
simp [hb]
· suffices ∀ b ∈ t, (if f (x, b) ∈ Prod.mk b ⁻¹' s then (1 : ℝ≥0∞) else 0) = 1 by
rw [setLIntegral_congr_fun ht this, setLIntegral_one]
intro b hb
simp only [t, Set.mem_setOf_eq] at hb
simp [hb]
