stronglyMeasurable_lineDeriv_uncurry

English

If f is continuous, then the lineDeriv function evaluated on p ∈ E × E is strongly measurable.

Русский

Если f непрерывна, то функция lineDeriv на паре (x, y) ∈ E × E совпадает с сильно измеримой функцией.

LaTeX

$$$ \\mathrm{StronglyMeasurable}\\big(p \\mapsto \\mathrm{lineDeriv}_{\\mathbb{k}}(f)(p_1)(p_2)\\big)$$$

Lean4

theorem stronglyMeasurable_lineDeriv_uncurry (hf : Continuous f) :
    StronglyMeasurable (fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2) :=
  by
  borelize 𝕜
  let g : (E × E) → 𝕜 → F := fun p t ↦ f (p.1 + t • p.2)
  have : Continuous g.uncurry :=
    hf.comp <| (continuous_fst.comp continuous_fst).add <| continuous_snd.smul (continuous_snd.comp continuous_fst)
  exact (stronglyMeasurable_deriv_with_param this).comp_measurable measurable_prodMk_right

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