continuousOn_primitive_interval' — Mathlib

English

If f is integrable on a compact interval, then the map b ↦ ∫_a^b f t dt is continuous on the corresponding interval.

Русский

Если f интегрируема на компактном интервале, то карта b ↦ ∫_a^b f(t) dt непрерывна на соответствующем интервале.

LaTeX

$$$\\text{ContinuousOn}\\left( b \\mapsto \\int_a^b f(t) dt, \\ Icc a b \\right)$$$

Lean4

/-- Note: this assumes that `f` is `IntervalIntegrable`, in contrast to some other lemmas here. -/
theorem continuousOn_primitive_interval' (h_int : IntervalIntegrable f μ b₁ b₂) (ha : a ∈ [[b₁, b₂]]) :
    ContinuousOn (fun b => ∫ x in a..b, f x ∂μ) [[b₁, b₂]] := fun _ _ ↦
  by
  refine continuousWithinAt_primitive (measure_singleton _) ?_
  rw [min_eq_right ha.1, max_eq_right ha.2]
  simpa [intervalIntegrable_iff, uIoc] using h_int

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