English
If s is contained in the mutually singular slice, then the singular part over s equals κ a s.
Русский
Если s ⊆ mutuallySingularSetSlice, то singularPart κ η a s = κ a s.
LaTeX
$$$ singularPart(\kappa, \eta)(a)(s) = (\kappa a)(s) \quad\text{for } s \subseteq mutuallySingularSetSlice(\kappa, \eta)(a)$$$
Lean4
theorem singularPart_of_subset_mutuallySingularSetSlice [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} {s : Set γ}
(hsm : MeasurableSet s) (hs : s ⊆ mutuallySingularSetSlice κ η a) : singularPart κ η a s = κ a s :=
by
have hs' : ∀ x ∈ s, 1 ≤ rnDerivAux κ (κ + η) a x := fun _ hx ↦ hs hx
rw [singularPart, Kernel.withDensity_apply']
swap; · exact measurable_singularPart_fun κ η
calc
∫⁻ x in s,
↑(Real.toNNReal (rnDerivAux κ (κ + η) a x)) -
↑(Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) * rnDeriv κ η a x ∂(κ + η) a =
∫⁻ _ in s, 1 ∂(κ + η) a :=
by
refine setLIntegral_congr_fun_ae hsm ?_
have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
filter_upwards [rnDerivAux_le_one h_le] with x hx hxs
have h_eq_one : rnDerivAux κ (κ + η) a x = 1 := le_antisymm hx (hs' x hxs)
simp [h_eq_one]
_ = (κ + η) a s := by simp
_ = κ a s := by
suffices η a s = 0 by simp [this]
exact measure_mono_null hs (measure_mutuallySingularSetSlice κ η a)
