Primitives of integrable functions on the line

Facts about the primitive t ↦ ∫ s in t₀..t, f s of a vector-valued function f, which are used to identify weak derivatives on an interval with ordinary primitives.

• TauCeti.intervalIntegral.exists_continuous_primitive_Icc: a continuous integrand on a closed interval has a globally continuous primitive with the prescribed derivative there and the expected increments between points of the interval.
• TauCeti.intervalIntegral.continuousOn_primitive_interval_of_locallyIntegrableOn: if f is only locally integrable on an open interval, its primitive based at a point of the interval is continuous on the interval. Mathlib's intervalIntegral.continuousOn_primitive_interval' covers a compact interval on which f is integrable.
• TauCeti.intervalIntegral.continuousOn_primitive_interval_of_integrableOn_Ioo: if f is integrable on the open interval (a, b), its primitive based at a point of [a, b] is continuous on the closed interval [a, b].
• TauCeti.intervalIntegral.integral_deriv_smul_primitive_eq_sub_of_le: integration by parts between a C¹ real function φ and the primitive of an integrable f, which need not be differentiable anywhere: ∫ t in a..b, φ' t • ∫ s in a..t, f s = φ b • ∫ s in a..b, f s - ∫ t in a..b, φ t • f t. It is proved by exchanging the order of integration (Fubini's theorem), so no differentiation of the primitive is needed.

theorem TauCeti.intervalIntegral.continuousOn_primitive_interval_of_locallyIntegrableOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] {t₀ : ℝ} (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioo a b) μ) (ht₀ : t₀ ∈ Set.Ioo a b) : ContinuousOn (fun (t : ℝ) => ∫ (s : ℝ) in t₀..t, f s ∂μ) (Set.Ioo a b)

The primitive t ↦ ∫ s in t₀..t, f s ∂μ of a function locally integrable on the open interval Ioo a b, based at a point t₀ of the interval, is continuous on the interval.

theorem TauCeti.intervalIntegral.continuousOn_primitive_interval_of_integrableOn_Ioo {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] {t₀ : ℝ} (hf : MeasureTheory.IntegrableOn f (Set.Ioo a b) μ) (ht₀ : t₀ ∈ Set.Icc a b) : ContinuousOn (fun (t : ℝ) => ∫ (s : ℝ) in t₀..t, f s ∂μ) (Set.Icc a b)

The primitive t ↦ ∫ s in t₀..t, f s ∂μ of a function integrable on the open interval Ioo a b, based at a point t₀ of Icc a b, is continuous on the closed interval Icc a b.

theorem TauCeti.intervalIntegral.exists_continuous_primitive_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E] (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) : ∃ (F : ℝ → E), Continuous F ∧ (∀ x ∈ Set.Icc a b, HasDerivAt F (f x) x) ∧ ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, F y - F x = ∫ (z : ℝ) in x..y, f z

A continuous integrand on a nonempty closed interval has a globally continuous primitive whose derivative agrees with the integrand throughout that interval, including its endpoints. The primitive increments are the oriented integrals between points of the interval.

theorem TauCeti.intervalIntegral.integral_deriv_smul_primitive_eq_sub_of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E] {φ : ℝ → ℝ} (hab : a ≤ b) (hφ : ContDiff ℝ 1 φ) (hf : IntervalIntegrable f MeasureTheory.volume a b) : ∫ (t : ℝ) in a..b, deriv φ t • ∫ (s : ℝ) in a..t, f s = (φ b • ∫ (s : ℝ) in a..b, f s) - ∫ (t : ℝ) in a..b, φ t • f t

Integration by parts against a primitive. For a ≤ b, f integrable on [a, b] and a C¹ function φ : ℝ → ℝ, ∫ t in a..b, φ' t • ∫ s in a..t, f s = φ b • ∫ s in a..b, f s - ∫ t in a..b, φ t • f t.