rnDerivAux_le_one — Mathlib

English

For kernels κ and η, the function x ↦ rnDerivAux κ η a x is measurable for each a, ensuring the RN-derivative construction is well-behaved in x.

Русский

Для κ и η, функция x ↦ rnDerivAux κ η a x измерима по x для каждого a.

LaTeX

$$$$ Measurable_{x} ( rnDerivAux κ η a x ). $$$$

Lean4

theorem rnDerivAux_le_one [IsFiniteKernel η] (hκη : κ ≤ η) {a : α} : rnDerivAux κ η a ≤ᵐ[η a] 1 :=
  by
  filter_upwards [Measure.rnDeriv_le_one_of_le (hκη a)] with x hx_le_one
  simp_rw [rnDerivAux]
  split_ifs with hα
  · refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_
    simp only [Pi.one_apply, ENNReal.ofReal_one]
    exact hx_le_one
  · have := hαγ.countableOrCountablyGenerated.resolve_left hα
    exact density_le_one ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _

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