measurable_singularPart_fun — Mathlib

English

The function p ↦ Real.toNNReal(rnDerivAux(κ+η) p.fst p.snd) − Real.toNNReal(1 − rnDerivAux(κ+η) p.fst p.snd) × rnDeriv κ η p.fst p.snd is measurable.

Русский

Функция p ↦ Real.toNNReal(rnDerivAux(κ+η) p.fst p.snd) − Real.toNNReal(1 − rnDerivAux(κ+η) p.fst p.snd) × rnDeriv κ η p.fst p.snd измерима.

LaTeX

$$$\text{Measurable}\left( p \mapsto \text{Real.toNNReal}(rnDerivAux(\kappa, \kappa + \eta)(p.fst, p.snd)) - \text{Real.toNNReal}(1 - rnDerivAux(\kappa, \kappa + \eta)(p.fst, p.snd)) \cdot rnDeriv(\kappa, \eta)(p.fst, p.snd) \right)$$$

Lean4

theorem measurable_singularPart_fun (κ η : Kernel α γ) :
    Measurable
      (fun p : α × γ ↦
        Real.toNNReal (rnDerivAux κ (κ + η) p.1 p.2) -
          Real.toNNReal (1 - rnDerivAux κ (κ + η) p.1 p.2) * rnDeriv κ η p.1 p.2) :=
  by fun_prop

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