English
The singular part on the complement of the mutually singular slice is zero.
Русский
Сингулярная часть на дополнении к срезу взаимной сингулярности равна нулю.
LaTeX
$$$ singularPart(\kappa, \eta)(a) (mutuallySingularSetSlice(\kappa, \eta)(a))^{c} = 0 $$$
Lean4
theorem singularPart_compl_mutuallySingularSetSlice (κ η : Kernel α γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) :
singularPart κ η a (mutuallySingularSetSlice κ η a)ᶜ = 0 :=
by
rw [singularPart, Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq, ae_restrict_iff]
all_goals simp_rw [ofNNReal_toNNReal]
rotate_left
· exact measurableSet_preimage (measurable_singularPart_fun_right κ η a) (measurableSet_singleton _)
· exact measurable_singularPart_fun_right κ η a
· exact measurable_singularPart_fun κ η
refine ae_of_all _ (fun x hx ↦ ?_)
simp only [mem_compl_iff, mutuallySingularSetSlice, mem_setOf, not_le] at hx
simp_rw [rnDeriv]
rw [← ENNReal.ofReal_div_of_pos, div_eq_inv_mul, ← ENNReal.ofReal_mul, ← mul_assoc, mul_inv_cancel₀, one_mul,
tsub_self, Pi.zero_apply]
· simp only [ne_eq, sub_eq_zero, hx.ne', not_false_eq_true]
· simp only [sub_nonneg, hx.le]
· simp only [sub_pos, hx]
