Additional lemmas for interval integrals

This file records general-purpose lemmas about interval integrals ∫ x in a..b, f x ∂μ that do not belong to any particular application.

Main results

• TauCeti.intervalIntegral.monotoneOn_primitive_of_nonneg: the primitive t ↦ ∫ x in a..t, f x of a function that is nonnegative and interval integrable on [a, b] is nondecreasing on [a, b].
• TauCeti.intervalIntegral.eq_of_integral_eq_sub: if the increments of F are the interval integrals of a function vanishing outside [-r, r] with total integral zero, then F is constant outside [-r, r].
• TauCeti.intervalIntegral.integral_re_mul_im_sub_im_mul_re_eq: a polarization identity expressing ∫ (x v - y u) for f = x + i y and g = u + i v through the integrals of ‖g‖², ‖f‖² and ‖g - i k f‖².
• TauCeti.intervalIntegral.norm_sub_sub_integral_le: the defect a₂ - a₁ - ∫ g from an integral equation changes by at most the changes of the endpoint values plus δ |t₂ - t₁| when the integrand changes by at most δ.
• TauCeti.tendsto_intervalIntegral_atTop_atBot: the accumulated integral of a locally integrable function bounded below almost everywhere by a positive constant tends to +∞ at +∞ and to -∞ at -∞.
• MeasureTheory.IntegrableOn.intervalIntegrable_of_mem_Icc: a function integrable on (a, b) for a measure without mass at points is interval integrable between any two points of [a, b].
• ContinuousLinearEquiv.intervalIntegral_comp_comm: a continuous linear equivalence commutes with interval integrals, with no integrability assumption.
• MeasureTheory.LocallyIntegrableOn.intervalIntegrable_comp_max: if f is locally integrable on [c, ∞), then its constant extension x ↦ f (max x c) is interval integrable on every interval.

theorem TauCeti.intervalIntegral.monotoneOn_primitive_of_nonneg {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} {a b : ℝ} (hf : 0 ≤ᵐ[μ.restrict (Set.Ioc a b)] f) (hfi : IntervalIntegrable f μ a b) : MonotoneOn (fun (t : ℝ) => ∫ (x : ℝ) in a..t, f x ∂μ) (Set.Icc a b)

The primitive t ↦ ∫ x in a..t, f x ∂μ of a function that is almost everywhere nonnegative and interval integrable on [a, b] is nondecreasing on [a, b].

theorem TauCeti.intervalIntegral.eq_of_integral_eq_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f F : ℝ → E} {r : ℝ} (hF : ∀ (a b : ℝ), ∫ (t : ℝ) in a..b, f t = F b - F a) (hf : ∀ (t : ℝ), r < |t| → f t = 0) (h : ∫ (t : ℝ), f t = 0) {x y : ℝ} (hx : r < |x|) (hy : r < |y|) : F x = F y

If the increments of F are the interval integrals of a function f that vanishes outside [-r, r] and has total integral zero, then F is constant outside [-r, r].

theorem TauCeti.intervalIntegral.integral_re_mul_im_sub_im_mul_re_eq {a b k : ℝ} (hk : k ≠ 0) {f g : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Set.uIoc a b))) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.uIoc a b))) : ∫ (t : ℝ) in a..b, (f t).re * (g t).im - (f t).im * (g t).re = (((∫ (t : ℝ) in a..b, ‖g t‖ ^ 2) + k ^ 2 * ∫ (t : ℝ) in a..b, ‖f t‖ ^ 2) - ∫ (t : ℝ) in a..b, ‖g t - ↑k * Complex.I * f t‖ ^ 2) / (2 * k)

A polarization identity for complex functions f = x + i y and g = u + i v, square integrable on uIoc a b: for real k ≠ 0, ∫ₐᵇ (x v - y u) = (∫ₐᵇ ‖g‖² + k² ∫ₐᵇ ‖f‖² - ∫ₐᵇ ‖g - i k f‖²) / (2k). For a curve f with velocity g, the left side is twice the signed area of f.

theorem TauCeti.intervalIntegral.norm_sub_sub_integral_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a₁ a₂ b₁ b₂ : E} {g g' : ℝ → E} {t₁ t₂ δ : ℝ} (hg : IntervalIntegrable g MeasureTheory.volume t₁ t₂) (hg' : IntervalIntegrable g' MeasureTheory.volume t₁ t₂) (hgg : ∀ t ∈ Set.uIoc t₁ t₂, ‖g t - g' t‖ ≤ δ) : ‖a₂ - a₁ - ∫ (t : ℝ) in t₁..t₂, g t‖ ≤ ‖b₂ - b₁ - ∫ (t : ℝ) in t₁..t₂, g' t‖ + ‖a₁ - b₁‖ + ‖a₂ - b₂‖ + δ * |t₂ - t₁|

The defect a₂ - a₁ - ∫ g from an integral equation over [t₁, t₂] differs from the defect b₂ - b₁ - ∫ g' by at most ‖a₁ - b₁‖ + ‖a₂ - b₂‖ + δ |t₂ - t₁| when ‖g - g'‖ ≤ δ on the interval.

theorem TauCeti.integral_eq_zero_of_lt_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {a ε t : ℝ} {φ : ℝ → E} (hφ0 : ∀ x ≤ a, φ x = 0) (hφa : ∀ ⦃y : ℝ⦄, dist y a < ε → φ y = 0) (ht : t < a + ε) : ∫ (s : ℝ) in a..t, φ s ∂μ = 0

A function vanishing on (-∞, a] and on a ball around a has zero integral on a..t for every t < a + ε, where ε is the radius of that ball.

theorem TauCeti.add_integral_add_inv_smul_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≠ b) {s : ℝ → E} (hsi : IntervalIntegrable s MeasureTheory.volume a b) (x y : E) : x + ∫ (t : ℝ) in a..b, s t + (b - a)⁻¹ • (y - x - ∫ (t : ℝ) in a..b, s t) = y

The primitive of a step velocity corrected by its average defect reaches the prescribed endpoint.

theorem TauCeti.setIntegral_norm_inv_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (hab : a < b) (D : E) : ∫ (x : ℝ) in Set.Ioc a b, ‖(b - a)⁻¹ • D‖ = ‖D‖

The L¹ norm over (a, b] of the constant (b - a)⁻¹ • D is ‖D‖.

theorem TauCeti.tendsto_intervalIntegral_atTop_atBot {w : ℝ → ℝ} {a : ℝ} (hw : ∀ (t : ℝ), IntervalIntegrable w MeasureTheory.volume a t) {m : ℝ} (hm : 0 < m) (hwm : ∀ᵐ (t : ℝ), m ≤ w t) : Filter.Tendsto (fun (t : ℝ) => ∫ (r : ℝ) in a..t, w r) Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun (t : ℝ) => ∫ (r : ℝ) in a..t, w r) Filter.atBot Filter.atBot

The accumulated integral t ↦ ∫ r in a..t, w r of a locally integrable function bounded below almost everywhere by a positive constant tends to +∞ at +∞ and to -∞ at -∞.

theorem MeasureTheory.IntegrableOn.intervalIntegrable_of_mem_Icc {E : Type u_1} [NormedAddCommGroup E] {f : ℝ → E} {μ : Measure ℝ} [NullSingletonClass μ] {a b s t : ℝ} (hf : IntegrableOn f (Set.Ioo a b) μ) (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b) : IntervalIntegrable f μ s t

A function integrable on (a, b) for a measure without mass at points is interval integrable between any two points s, t ∈ [a, b].

theorem ContinuousLinearEquiv.intervalIntegral_comp_comm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure ℝ} {a b : ℝ} (L : E ≃L[𝕜] F) (f : ℝ → E) : ∫ (x : ℝ) in a..b, L (f x) ∂μ = L (∫ (x : ℝ) in a..b, f x ∂μ)

A continuous linear equivalence commutes with interval integrals of arbitrary functions; compare ContinuousLinearMap.intervalIntegral_comp_comm, which needs integrability.

theorem MeasureTheory.LocallyIntegrableOn.intervalIntegrable_comp_max {E : Type u_1} [NormedAddCommGroup E] {f : ℝ → E} {μ : Measure ℝ} [IsLocallyFiniteMeasure μ] {c : ℝ} (hf : LocallyIntegrableOn f (Set.Ici c) μ) (a b : ℝ) : IntervalIntegrable (fun (x : ℝ) => f (max x c)) μ a b

If f is locally integrable on [c, ∞) for a locally finite measure, then its constant extension x ↦ f (max x c) to all of ℝ is interval integrable between any two points.