English
Let κ and η be finite kernels. Then the density of κ+η with respect to a function f, where f(a,x) = Real.toNNReal(1 − rnDerivAux κ (κ+η) a x), equals η.
Русский
Пусть κ и η — конечные ядра. Тогда плотность ядра κ+η по отношению к функции f, где f(a,x) = Real.toNNReal(1 − rnDerivAux κ (κ+η) a x), равна η.
LaTeX
$$$\text{withDensity}(\kappa + \eta)(a, x) = \text{Real.toNNReal}(1 - \mathrm{rnDerivAux}(\kappa, \kappa + \eta)(a, x)) \\quad = \eta$$$
Lean4
theorem withDensity_one_sub_rnDerivAux (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) = η :=
by
have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
suffices
withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) +
withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x)) =
κ + η
by
ext a s
have h :
(withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) +
withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x)))
a s =
κ a s + η a s :=
by
rw [this]
simp
simp only [coe_add, Pi.add_apply, Measure.coe_add] at h
rwa [withDensity_rnDerivAux, add_comm, ENNReal.add_right_inj (measure_ne_top _ _)] at h
simp_rw [ofNNReal_toNNReal, ENNReal.ofReal_sub _ (rnDerivAux_nonneg h_le), ENNReal.ofReal_one]
rw [withDensity_sub_add_cancel]
· rw [withDensity_one']
· exact measurable_const
· fun_prop
· intro a
filter_upwards [rnDerivAux_le_one h_le] with x hx
simp only [ENNReal.ofReal_le_one]
exact hx
