English
For κ and ν and fixed x, the map a ↦ density κ ν a x s is measurable for any measurable s.
Русский
Для κ и ν и фиксированного x отображение a ↦ density κ ν a x s измеримо.
LaTeX
$$Measurable (fun a => density κ ν a x s)$$
Lean4
theorem setIntegral_density (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ}
(hA : MeasurableSet A) : ∫ x in A, density κ ν a x s ∂(ν a) = (κ a).real (A ×ˢ s) :=
by
have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
have hgen : ‹MeasurableSpace γ› = .generateFrom {s | ∃ n, MeasurableSet[countableFiltration γ n] s} := by
rw [setOf_exists, generateFrom_iUnion_measurableSet (countableFiltration γ), iSup_countableFiltration]
have hpi : IsPiSystem {s | ∃ n, MeasurableSet[countableFiltration γ n] s} :=
by
rw [setOf_exists]
exact
isPiSystem_iUnion_of_monotone _ (fun n ↦ @isPiSystem_measurableSet _ (countableFiltration γ n)) fun _ _ ↦
(countableFiltration γ).mono
induction A, hA using induction_on_inter hgen hpi with
| empty => simp
| basic s hs =>
rcases hs with ⟨n, hn⟩
exact setIntegral_density_of_measurableSet hκν n a hs hn
| compl A hA hA_eq =>
have h := integral_add_compl hA (integrable_density hκν a hs)
rw [hA_eq, integral_density hκν a hs] at h
have : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s :=
by
rw [prod_diff_prod, compl_eq_univ_diff]
simp
rw [this, measureReal_def, measure_diff (by intro; simp) (hA.prod hs).nullMeasurableSet (measure_ne_top (κ a) _),
ENNReal.toReal_sub_of_le (measure_mono (by intro x; simp)) (measure_ne_top _ _)]
rw [eq_tsub_iff_add_eq_of_le, add_comm]
· exact h
· gcongr <;> simp
| iUnion f hf_disj hf
h_eq =>
rw [integral_iUnion hf hf_disj (integrable_density hκν _ hs).integrableOn]
simp_rw [h_eq, measureReal_def]
rw [← ENNReal.tsum_toReal_eq (fun _ ↦ measure_ne_top _ _)]
congr
rw [iUnion_prod_const, measure_iUnion]
· exact hf_disj.mono fun _ _ h ↦ h.set_prod_left _ _
· exact fun i ↦ (hf i).prod hs
