rnDeriv_add — Mathlib

English

For kernels κ, ν, η, the RN-derivative of the sum κ + ν with respect to η is the sum of RN-derivs: rnDeriv(κ + ν, η) = rnDeriv κ η + rnDeriv ν η almost everywhere w.r.t. η.

Русский

Плотность rnDeriv сумм κ+ν по отношению к η равна сумме rnDeriv κ η и rnDeriv ν η почти всюду по η.

LaTeX

$$rnDeriv(κ + ν) η a =ᵐ[η a] rnDeriv κ η a + rnDeriv ν η a$$

Lean4

theorem rnDeriv_add (κ ν η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel ν] [IsFiniteKernel η] (a : α) :
    rnDeriv (κ + ν) η a =ᵐ[η a] rnDeriv κ η a + rnDeriv ν η a :=
  by
  filter_upwards [(κ + ν).rnDeriv_eq_rnDeriv_measure, κ.rnDeriv_eq_rnDeriv_measure, ν.rnDeriv_eq_rnDeriv_measure,
    (κ a).rnDeriv_add (ν a) (η a)] with x h1 h2 h3 h4
  rw [h1, Pi.add_apply, h2, h3, coe_add, Pi.add_apply, h4, Pi.add_apply]

Похожие утверждения