Continuity of parametric integrals with compactly supported integrand

Mathlib's continuousOn_integral_of_compact_support gives continuity of a parametric integral on a set. This file records its global form: a jointly continuous integrand which vanishes unless the integration variable lies in a fixed compact set has a continuous parametric integral, against any measure which is finite on compact sets. It also records that the indicator function of a bounded interval [a, b) is integrable against a locally finite measure, that the integral of |f| over a set splits along the sign of f, and that a continuous square-integrable function h with ∫ conj (h x) * h x = 0 vanishes, against a measure positive on nonempty open sets.

Main statements

• TauCeti.continuous_integral_of_compact_support: the parametric integral of a jointly continuous integrand which vanishes unless r ∈ K, for compact K, is continuous.
• TauCeti.integrable_indicator_Ico_one: the indicator function of [a, b) is integrable.
• TauCeti.setIntegral_abs_eq_sub: the integral of |f| over s is the integral of f over the part of s where f ≥ 0 minus its integral over the rest of s.
• TauCeti.integrableOn_sin_of_measure_ne_top, TauCeti.integrableOn_exp_ofReal_mul_I_of_measure_ne_top: the sine and the unit-circle exponential exp (t x I) are integrable on a set of finite measure.
• MeasureTheory.setIntegral_mul_le_mul_setIntegral_abs: the pairing of an integrable f on Ω with a function g bounded by S on V ⊆ Ω is at most S ∫_Ω |f|.
• MeasureTheory.setLIntegral_enorm_sq_eq_ofReal_setIntegral: the Lebesgue integral of ‖f‖ₑ ^ 2 over A is ofReal of the Bochner integral of ‖f‖ ^ 2, and MeasureTheory.setLIntegral_enorm_sq_le_ofReal the corresponding bound.
• Continuous.eq_zero_of_integral_conj_mul_self_eq_zero: a continuous square-integrable function h with ∫ conj (h x) * h x = 0 vanishes.

theorem TauCeti.continuous_integral_of_compact_support {X : Type u_1} {Y : Type u_2} {E : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] [NormedAddCommGroup E] [NormedSpace ℝ E] {F : X → Y → E} {K : Set Y} (μ : MeasureTheory.Measure Y) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hK : IsCompact K) (hFc : Continuous (Function.uncurry F)) (hF : ∀ (s : X) (r : Y), F s r ≠ 0 → r ∈ K) : Continuous fun (s : X) => ∫ (r : Y), F s r ∂μ

The parametric integral s ↦ ∫ r, F s r of a jointly continuous integrand which vanishes unless r ∈ K, for compact K, is continuous.

theorem TauCeti.integrable_indicator_Ico_one {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [OpensMeasurableSpace α] [CompactIccSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] (a b : α) : MeasureTheory.Integrable ((Set.Ico a b).indicator 1) μ

The indicator function of a bounded interval [a, b) is integrable against a locally finite measure.

theorem TauCeti.setIntegral_abs_eq_sub {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} {s : Set α} (hf : MeasureTheory.IntegrableOn f s μ) : ∫ (x : α) in s, |f x| ∂μ = ∫ (x : α) in s ∩ {x : α | 0 ≤ f x}, f x ∂μ - ∫ (x : α) in s \ {x : α | 0 ≤ f x}, f x ∂μ

The integral of |f| over a set s is the integral of f over the part of s where f is nonnegative minus the integral of f over the part where it is negative.

theorem TauCeti.integral_norm_add_const_sub_le {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {S : Set α} {g f : α → E} (c : E) (hS : μ S ≠ ⊤) (hg : MeasureTheory.IntegrableOn g S μ) (hf : MeasureTheory.IntegrableOn f S μ) : ∫ (t : α) in S, ‖g t + c - f t‖ ∂μ ≤ ∫ (t : α) in S, ‖g t - f t‖ ∂μ + ∫ (x : α) in S, ‖c‖ ∂μ

Perturbing g by a constant c changes the L¹ distance over S to f by at most the L¹ norm of c.

theorem TauCeti.mul_integral_image_eq_sum_pieces {E : Type u_1} {M : Type u_2} {ι : Type u_3} [MeasurableSpace E] [Fintype ι] {Q : ι → E → M} {D : Set E} {Z : Set M} (hZ : Z.Finite) (himage : ⋃ (i : ι), Q i '' D = Zᶜ) (hdisj : Pairwise fun (i j : ι) => Disjoint (Q i '' D) (Q j '' D)) {g : M → E} {s : Set M} (hg : Set.InjOn g s) (μ : MeasureTheory.Measure E) [MeasureTheory.NullSingletonClass μ] {C : E → ℝ} (hC : MeasureTheory.IntegrableOn C (g '' s) μ) (c : ℝ) (V : ι → E → ℝ) (hT : ∀ (i : ι), MeasurableSet (g ∘ Q i '' (D ∩ Q i ⁻¹' s))) (hpiece : ∀ (i : ι), c * ∫ (y : E) in g ∘ Q i '' (D ∩ Q i ⁻¹' s), C y ∂μ = ∫ (z : E) in D ∩ Q i ⁻¹' s, V i z ∂μ) : c * ∫ (y : E) in g '' s, C y ∂μ = ∑ i : ι, ∫ (z : E) in D ∩ Q i ⁻¹' s, V i z ∂μ

If disjoint parametrizations Q i of a domain D cover the complement of a finite set Z, and g is injective on s, the integral over g '' s is the sum of the integrals over the images (g ∘ Q i) '' (D ∩ Q i ⁻¹' s) of the pieces cut out by each parametrization, up to the transport identity hpiece for each piece. The integrand need only be integrable on g '' s, and the measure needs null singletons only to discard the seams.

theorem TauCeti.integrableOn_sin_of_measure_ne_top {ν : MeasureTheory.Measure ℝ} {s : Set ℝ} (hs : ν s ≠ ⊤) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.sin x) s ν

The sine is integrable on a set of finite measure.

theorem TauCeti.integrableOn_exp_ofReal_mul_I_of_measure_ne_top {ν : MeasureTheory.Measure ℝ} {s : Set ℝ} (t : ℝ) (hs : ν s ≠ ⊤) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Complex.exp (↑(t * x) * Complex.I)) s ν

The unit-circle exponential x ↦ exp (t x I) is integrable on a set of finite measure.

theorem Continuous.eq_zero_of_integral_conj_mul_self_eq_zero {X : Type u_1} {𝕜 : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [RCLike 𝕜] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {h : X → 𝕜} (hc : Continuous h) (hL : MeasureTheory.MemLp h 2 μ) (h0 : ∫ (x : X), (starRingEnd 𝕜) (h x) * h x ∂μ = 0) : h = 0

A continuous square-integrable function h with ∫ conj (h x) * h x = 0 vanishes, against a measure positive on nonempty open sets.

theorem MeasureTheory.setIntegral_mul_le_mul_setIntegral_abs {α : Type u_1} [MeasurableSpace α] {ν : Measure α} {V Ω : Set α} {f g : α → ℝ} {S : ℝ} (hVΩ : V ⊆ Ω) (hf : IntegrableOn f Ω ν) (hS0 : 0 ≤ S) (hgS : ∀ᵐ (x : α) ∂ν.restrict V, |g x| ≤ S) : ∫ (x : α) in V, f x * g x ∂ν ≤ S * ∫ (x : α) in Ω, |f x| ∂ν

The pairing of an integrable function f on Ω with a function g bounded by S on V ⊆ Ω is at most S ∫_Ω |f|.

theorem MeasureTheory.setLIntegral_enorm_sq_eq_ofReal_setIntegral {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {ν : Measure α} {A : Set α} {f : α → E} (hf : IntegrableOn (fun (x : α) => ‖f x‖ ^ 2) A ν) : ∫⁻ (x : α) in A, ‖f x‖ₑ ^ 2 ∂ν = ENNReal.ofReal (∫ (x : α) in A, ‖f x‖ ^ 2 ∂ν)

The Lebesgue integral of ‖f‖ₑ ^ 2 over A is the ENNReal.ofReal of the Bochner integral of ‖f‖ ^ 2, when ‖f‖ ^ 2 is integrable on A.

theorem MeasureTheory.setLIntegral_enorm_sq_le_ofReal {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {ν : Measure α} {A : Set α} {f : α → E} {c : ℝ} (hf : IntegrableOn (fun (x : α) => ‖f x‖ ^ 2) A ν) (h : ∫ (x : α) in A, ‖f x‖ ^ 2 ∂ν ≤ c) : ∫⁻ (x : α) in A, ‖f x‖ₑ ^ 2 ∂ν ≤ ENNReal.ofReal c

A bound on the Bochner integral of ‖f‖ ^ 2 over A bounds the Lebesgue integral of ‖f‖ₑ ^ 2.