measurable_singularPart_fun_right

English

The x-variation of the right-hand expression is measurable in x for fixed a.

Русский

Для фиксированного a выражение слева/права измеримо по x.

LaTeX

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

Lean4

theorem measurable_singularPart_fun_right (κ η : Kernel α γ) (a : α) :
    Measurable
      (fun x : γ ↦
        Real.toNNReal (rnDerivAux κ (κ + η) a x) - Real.toNNReal (1 - rnDerivAux κ (κ + η) a x) * rnDeriv κ η a x) :=
  by
  change
    Measurable
      ((Function.uncurry fun a b ↦
          ENNReal.ofReal (rnDerivAux κ (κ + η) a b) - ENNReal.ofReal (1 - rnDerivAux κ (κ + η) a b) * rnDeriv κ η a b) ∘
        (fun b ↦ (a, b)))
  exact (measurable_singularPart_fun κ η).comp measurable_prodMk_left

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