feat(probability/kernel/integral_comp_prod): Bochner integral against…

… the composition-product of two kernels (#18976)

src/probability/kernel/composition.lean

@@ -223,6 +223,101 @@ lemma comp_prod_apply (κ : kernel α β) [is_s_finite_kernel κ] (η : kernel (
   (κ ⊗ₖ η) a s = ∫⁻ b, η (a, b) {c | (b, c) ∈ s} ∂(κ a) :=
 comp_prod_apply_eq_comp_prod_fun κ η a hs
 
+lemma le_comp_prod_apply (κ : kernel α β) [is_s_finite_kernel κ] (η : kernel (α × β) γ)
+  [is_s_finite_kernel η] (a : α) (s : set (β × γ)) :
+  ∫⁻ b, η (a, b) {c | (b, c) ∈ s} ∂(κ a) ≤ (κ ⊗ₖ η) a s :=
+calc ∫⁻ b, η (a, b) {c | (b, c) ∈ s} ∂(κ a)
+    ≤ ∫⁻ b, η (a, b) {c | (b, c) ∈ (to_measurable ((κ ⊗ₖ η) a) s)} ∂(κ a) :
+      lintegral_mono (λ b, measure_mono (λ _ h_mem, subset_to_measurable _ _ h_mem))
+... = (κ ⊗ₖ η) a (to_measurable ((κ ⊗ₖ η) a) s) :
+      (kernel.comp_prod_apply_eq_comp_prod_fun κ η a (measurable_set_to_measurable _ _)).symm
+... = (κ ⊗ₖ η) a s : measure_to_measurable s
+
+section ae
+/-! ### `ae` filter of the composition-product -/
+
+variables {κ : kernel α β} [is_s_finite_kernel κ] {η : kernel (α × β) γ} [is_s_finite_kernel η]
+  {a : α}
+
+lemma ae_kernel_lt_top (a : α) (h2s : (κ ⊗ₖ η) a s ≠ ∞) :
+  ∀ᵐ b ∂(κ a), η (a, b) (prod.mk b ⁻¹' s) < ∞ :=
+begin
+  let t := to_measurable ((κ ⊗ₖ η) a) s,
+  have : ∀ (b : β), η (a, b) (prod.mk b ⁻¹' s) ≤ η (a, b) (prod.mk b ⁻¹' t),
+  { exact λ b, measure_mono (set.preimage_mono (subset_to_measurable _ _)), },
+  have ht : measurable_set t := measurable_set_to_measurable _ _,
+  have h2t : (κ ⊗ₖ η) a t ≠ ∞, by rwa measure_to_measurable,
+  have ht_lt_top : ∀ᵐ b ∂(κ a), η (a, b) (prod.mk b ⁻¹' t) < ∞,
+  { rw kernel.comp_prod_apply _ _ _ ht at h2t,
+    exact ae_lt_top (kernel.measurable_kernel_prod_mk_left' ht a) h2t, },
+  filter_upwards [ht_lt_top] with b hb,
+  exact (this b).trans_lt hb,
+end
+
+lemma comp_prod_null (a : α) (hs : measurable_set s) :
+  (κ ⊗ₖ η) a s = 0 ↔ (λ b, η (a, b) (prod.mk b ⁻¹' s)) =ᵐ[κ a] 0 :=
+begin
+  rw [kernel.comp_prod_apply _ _ _ hs, lintegral_eq_zero_iff],
+  { refl, },
+  { exact kernel.measurable_kernel_prod_mk_left' hs a, },
+end
+
+lemma ae_null_of_comp_prod_null (h : (κ ⊗ₖ η) a s = 0) :
+  (λ b, η (a, b) (prod.mk b ⁻¹' s)) =ᵐ[κ a] 0 :=
+begin
+  obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h,
+  simp_rw [comp_prod_null a mt] at ht,
+  rw [filter.eventually_le_antisymm_iff],
+  exact ⟨filter.eventually_le.trans_eq
+    (filter.eventually_of_forall $ λ x, (measure_mono (set.preimage_mono hst) : _)) ht,
+    filter.eventually_of_forall $ λ x, zero_le _⟩
+end
+
+lemma ae_ae_of_ae_comp_prod {p : β × γ → Prop} (h : ∀ᵐ bc ∂((κ ⊗ₖ η) a), p bc) :
+  ∀ᵐ b ∂(κ a), ∀ᵐ c ∂(η (a, b)), p (b, c) :=
+ae_null_of_comp_prod_null h
+
+end ae
+
+section restrict
+
+variables {κ : kernel α β} [is_s_finite_kernel κ] {η : kernel (α × β) γ} [is_s_finite_kernel η]
+  {a : α}
+
+lemma comp_prod_restrict {s : set β} {t : set γ} (hs : measurable_set s) (ht : measurable_set t) :
+  (kernel.restrict κ hs) ⊗ₖ (kernel.restrict η ht) = kernel.restrict (κ ⊗ₖ η) (hs.prod ht) :=
+begin
+  ext a u hu : 2,
+  rw [comp_prod_apply _ _ _ hu, restrict_apply' _ _ _ hu,
+    comp_prod_apply _ _ _ (hu.inter (hs.prod ht))],
+  simp only [kernel.restrict_apply, measure.restrict_apply' ht, set.mem_inter_iff,
+    set.prod_mk_mem_set_prod_eq],
+  have : ∀ b, η (a, b) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t}
+    = s.indicator (λ b, η (a, b) ({c : γ | (b, c) ∈ u} ∩ t)) b,
+  { intro b,
+    classical,
+    rw set.indicator_apply,
+    split_ifs with h,
+    { simp only [h, true_and],
+      refl, },
+    { simp only [h, false_and, and_false, set.set_of_false, measure_empty], }, },
+  simp_rw this,
+  rw lintegral_indicator _ hs,
+end
+
+lemma comp_prod_restrict_left {s : set β} (hs : measurable_set s) :
+  (kernel.restrict κ hs) ⊗ₖ η = kernel.restrict (κ ⊗ₖ η) (hs.prod measurable_set.univ) :=
+by { rw ← comp_prod_restrict, congr, exact kernel.restrict_univ.symm, }
+
+lemma comp_prod_restrict_right {t : set γ} (ht : measurable_set t) :
+  κ ⊗ₖ (kernel.restrict η ht) = kernel.restrict (κ ⊗ₖ η) (measurable_set.univ.prod ht) :=
+by { rw ← comp_prod_restrict, congr, exact kernel.restrict_univ.symm, }
+
+end restrict
+
+section lintegral
+/-! ### Lebesgue integral -/
+
 /-- Lebesgue integral against the composition-product of two kernels. -/
 theorem lintegral_comp_prod' (κ : kernel α β) [is_s_finite_kernel κ] (η : kernel (α × β) γ)
   [is_s_finite_kernel η] (a : α) {f : β → γ → ℝ≥0∞} (hf : measurable (function.uncurry f)) :
@@ -290,6 +385,41 @@ begin
   { simp_rw [g, function.uncurry_curry], exact hf, },
 end
 
+/-- Lebesgue integral against the composition-product of two kernels. -/
+lemma lintegral_comp_prod₀ (κ : kernel α β) [is_s_finite_kernel κ] (η : kernel (α × β) γ)
+  [is_s_finite_kernel η] (a : α) {f : β × γ → ℝ≥0∞} (hf : ae_measurable f ((κ ⊗ₖ η) a)) :
+  ∫⁻ z, f z ∂((κ ⊗ₖ η) a) = ∫⁻ x, ∫⁻ y, f (x, y) ∂(η (a, x)) ∂(κ a) :=
+begin
+  have A : ∫⁻ z, f z ∂((κ ⊗ₖ η) a) = ∫⁻ z, hf.mk f z ∂((κ ⊗ₖ η) a) :=
+    lintegral_congr_ae hf.ae_eq_mk,
+  have B : ∫⁻ x, ∫⁻ y, f (x, y) ∂(η (a, x)) ∂(κ a) = ∫⁻ x, ∫⁻ y, hf.mk f (x, y) ∂(η (a, x)) ∂(κ a),
+  { apply lintegral_congr_ae,
+    filter_upwards [ae_ae_of_ae_comp_prod hf.ae_eq_mk] with _ ha using lintegral_congr_ae ha, },
+  rw [A, B, lintegral_comp_prod],
+  exact hf.measurable_mk,
+end
+
+lemma set_lintegral_comp_prod (κ : kernel α β) [is_s_finite_kernel κ] (η : kernel (α × β) γ)
+  [is_s_finite_kernel η] (a : α) {f : β × γ → ℝ≥0∞} (hf : measurable f)
+  {s : set β} {t : set γ} (hs : measurable_set s) (ht : measurable_set t) :
+  ∫⁻ z in s ×ˢ t, f z ∂((κ ⊗ₖ η) a) = ∫⁻ x in s, ∫⁻ y in t, f (x, y) ∂(η (a, x)) ∂(κ a) :=
+by simp_rw [← kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← comp_prod_restrict,
+    lintegral_comp_prod _ _ _ hf, kernel.restrict_apply]
+
+lemma set_lintegral_comp_prod_univ_right (κ : kernel α β) [is_s_finite_kernel κ]
+  (η : kernel (α × β) γ) [is_s_finite_kernel η] (a : α) {f : β × γ → ℝ≥0∞} (hf : measurable f)
+  {s : set β} (hs : measurable_set s) :
+  ∫⁻ z in s ×ˢ set.univ, f z ∂((κ ⊗ₖ η) a) = ∫⁻ x in s, ∫⁻ y, f (x, y) ∂(η (a, x)) ∂(κ a) :=
+by simp_rw [set_lintegral_comp_prod κ η a hf hs measurable_set.univ, measure.restrict_univ]
+
+lemma set_lintegral_comp_prod_univ_left (κ : kernel α β) [is_s_finite_kernel κ]
+  (η : kernel (α × β) γ) [is_s_finite_kernel η] (a : α) {f : β × γ → ℝ≥0∞} (hf : measurable f)
+  {t : set γ} (ht : measurable_set t) :
+  ∫⁻ z in set.univ ×ˢ t, f z ∂((κ ⊗ₖ η) a) = ∫⁻ x, ∫⁻ y in t, f (x, y) ∂(η (a, x)) ∂(κ a) :=
+by simp_rw [set_lintegral_comp_prod κ η a hf measurable_set.univ ht, measure.restrict_univ]
+
+end lintegral
+
 lemma comp_prod_eq_tsum_comp_prod (κ : kernel α β) [is_s_finite_kernel κ] (η : kernel (α × β) γ)
   [is_s_finite_kernel η] (a : α) (hs : measurable_set s) :
   (κ ⊗ₖ η) a s = ∑' (n m : ℕ), (seq κ n ⊗ₖ seq η m) a s :=