continuous_parametric_intervalIntegral_of_continuous

English

If f is continuous in the parameter, then the interval integral ∫ f(x,t) dt is continuous in x.

Русский

Если функция непрерывна по параметру, то интеграл по интервалу непрерывен по параметру x.

LaTeX

$$$\\text{Continuous}\\bigl(\\lambda x, \\int_a^b f(x,t) dt\\bigr)$$$

Lean4

@[fun_prop]
theorem continuous_parametric_intervalIntegral_of_continuous {a₀ : ℝ} (hf : Continuous f.uncurry) {s : X → ℝ}
    (hs : Continuous s) : Continuous fun x ↦ ∫ t in a₀..s x, f x t ∂μ :=
  show Continuous ((fun p : X × ℝ ↦ ∫ t in a₀..p.2, f p.1 t ∂μ) ∘ fun x ↦ (x, s x)) from
    (continuous_parametric_primitive_of_continuous hf).comp₂ continuous_id hs

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