English
If s is a subset of the complement of the mutual singular slice, then withDensity η (rnDeriv κ η) a s = κ a s.
Русский
Если s ⊆ complement(mutuallySingularSetSlice), то withDensity η (rnDeriv κ η) a s = κ a s.
LaTeX
$$$ withDensity(\eta)(rnDeriv(\kappa, \eta))(a)(s) = (\kappa a)(s) \quad\text{for } s \subseteq (mutuallySingularSetSlice(\kappa, \eta)(a))^{c} $$$
Lean4
theorem withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice [IsFiniteKernel κ] [IsFiniteKernel η] {a : α}
{s : Set γ} (hsm : MeasurableSet s) (hs : s ⊆ (mutuallySingularSetSlice κ η a)ᶜ) :
withDensity η (rnDeriv κ η) a s = κ a s :=
by
have :
withDensity η (rnDeriv κ η) =
withDensity (withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))) (rnDeriv κ η) :=
by
rw [rnDeriv_def']
congr
exact (withDensity_one_sub_rnDerivAux κ η).symm
rw [this, ← withDensity_mul, Kernel.withDensity_apply']
rotate_left
· fun_prop
· fun_prop
· exact measurable_rnDeriv _ _
simp_rw [rnDeriv]
have hs' : ∀ x ∈ s, rnDerivAux κ (κ + η) a x < 1 :=
by
simp_rw [← notMem_mutuallySingularSetSlice]
exact fun x hx hx_mem ↦ hs hx hx_mem
calc
∫⁻ x in s,
↑(Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) *
(ENNReal.ofReal (rnDerivAux κ (κ + η) a x) / ENNReal.ofReal (1 - rnDerivAux κ (κ + η) a x)) ∂(κ + η) a
_ = ∫⁻ x in s, ENNReal.ofReal (rnDerivAux κ (κ + η) a x) ∂(κ + η) a :=
by
refine setLIntegral_congr_fun hsm (fun x hx ↦ ?_)
rw [ofNNReal_toNNReal, ← ENNReal.ofReal_div_of_pos, div_eq_inv_mul, ← ENNReal.ofReal_mul, ← mul_assoc,
mul_inv_cancel₀, one_mul]
· rw [ne_eq, sub_eq_zero]
exact (hs' x hx).ne'
· simp [(hs' x hx).le]
· simp [hs' x hx]
_ = κ a s := setLIntegral_rnDerivAux κ η a hsm
