rnDerivAux_nonneg — Mathlib

English

If κ ≤ η, then rnDerivAux κ η a x ≤ 1 almost everywhere with respect to η a.

Русский

Если κ ≤ η, то rnDerivAux κ η a x ≤ 1 почти наверняка по η a.

LaTeX

$$$$ rnDerivAux κ η a x ≤^{ae[η a]} 1. $$$$

Lean4

theorem rnDerivAux_nonneg (hκη : κ ≤ η) {a : α} {x : γ} : 0 ≤ rnDerivAux κ η a x :=
  by
  rw [rnDerivAux]
  split_ifs with hα
  · exact ENNReal.toReal_nonneg
  · have := hαγ.countableOrCountablyGenerated.resolve_left hα
    exact density_nonneg ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _

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