withDensity_rnDeriv_mutuallySingularSetSlice

English

The withDensity of η on the slice with rnDeriv equals zero.

Русский

С плотностью η на срезе взаимной сингулярности равна нулю.

LaTeX

$$$ withDensity(\eta)(rnDeriv(\kappa, \eta))(a, (mutuallySingularSetSlice(\kappa, \eta)(a))) = 0 $$$

Lean4

theorem withDensity_rnDeriv_mutuallySingularSetSlice (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) :
    withDensity η (rnDeriv κ η) a (mutuallySingularSetSlice κ η a) = 0 :=
  by
  rw [Kernel.withDensity_apply']
  · exact setLIntegral_measure_zero _ _ (measure_mutuallySingularSetSlice κ η a)
  · exact measurable_rnDeriv κ η

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