measure_mutuallySingularSetSlice — Mathlib

English

For each a, η(a) assigns measure zero to the mutuallySingularSetSlice set.

Русский

Для каждого a мера η(a) обучает нулю множество mutuallySingularSetSlice κ η a.

LaTeX

$$$\eta\,a\big(\kappa.mutuallySingularSetSlice(\eta)\,a\big) = 0$$$

Lean4

theorem measure_mutuallySingularSetSlice (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) :
    η a (mutuallySingularSetSlice κ η a) = 0 :=
  by
  suffices
    withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) a {x | 1 ≤ rnDerivAux κ (κ + η) a x} =
      0
    by rwa [withDensity_one_sub_rnDerivAux κ η] at this
  simp_rw [ofNNReal_toNNReal]
  rw [Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq, ae_restrict_iff]
  rotate_left
  · exact (measurableSet_singleton 0).preimage (by fun_prop)
  · fun_prop
  · fun_prop
  refine ae_of_all _ (fun x hx ↦ ?_)
  simp only [mem_setOf_eq] at hx
  simp [hx]

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