English
For kernels κ, η, the L-integral over s with density rnDerivAux equals κ a s, connecting the RN derivative to the kernel’s action on sets.
Русский
Для κ, η: линеграл по s плотности rnDerivAux равен κ a s, связывая RN-дериватив с действием ядра на множества.
LaTeX
$$$$ \lintegral_{s} ENNReal.ofReal(rnDerivAux κ (κ+η) a x) d(κ+η) a = κ a s. $$$$
Lean4
theorem setLIntegral_rnDerivAux (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) {s : Set γ}
(hs : MeasurableSet s) : ∫⁻ x in s, ENNReal.ofReal (rnDerivAux κ (κ + η) a x) ∂(κ + η) a = κ a s :=
by
have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
simp_rw [rnDerivAux]
split_ifs with hα
· have h_ac : κ a ≪ (κ + η) a := Measure.absolutelyContinuous_of_le (h_le a)
rw [← Measure.setLIntegral_rnDeriv h_ac]
refine setLIntegral_congr_fun_ae hs ?_
filter_upwards [Measure.rnDeriv_lt_top (κ a) ((κ + η) a)] with x hx_lt _
rw [ENNReal.ofReal_toReal hx_lt.ne]
· have := hαγ.countableOrCountablyGenerated.resolve_left hα
rw [setLIntegral_density ((fst_map_id_prod _ measurable_const).trans_le h_le) _ MeasurableSet.univ hs,
map_apply' _ (by fun_prop) _ (hs.prod MeasurableSet.univ)]
congr 1 with x
simp
