English
rnDerivAux κ η a x is an intermediate quantity used to define the RN-derivative rnDeriv κ η, balancing κ and η along the α and γ axes.
Русский
rnDerivAux κ η a x — промежуточная величина, используемая для определения rnDeriv κ η, балансирующая κ и η вдоль осей α и γ.
LaTeX
$$$$ rnDerivAux(κ,η)(a,x) $$$$
Lean4
@[fun_prop]
theorem measurable_rnDerivAux (κ η : Kernel α γ) : Measurable (fun p : α × γ ↦ Kernel.rnDerivAux κ η p.1 p.2) :=
by
simp_rw [rnDerivAux]
split_ifs with hα
· refine
Measurable.ennreal_toReal <|
measurable_from_prod_countable_right' (fun a ↦ Measure.measurable_rnDeriv (κ a) (η a)) fun a a' c ha'_mem_a ↦ ?_
have h_eq : ∀ κ : Kernel α γ, κ a' = κ a := fun κ ↦ by
ext s hs
exact mem_of_mem_measurableAtom ha'_mem_a (Kernel.measurable_coe κ hs (measurableSet_singleton (κ a s))) rfl
rw [h_eq κ, h_eq η]
· have := hαγ.countableOrCountablyGenerated.resolve_left hα
exact measurable_density _ η MeasurableSet.univ
