Integrability criteria

Taking the absolute value of an almost everywhere measurable real coefficient does not change integrability of its scalar product with a real normed-space-valued function, even when that function is not measurable by itself. The equivalence permits signed Jacobians in oriented change of variables for arbitrary rough-form coefficients.

For absolute moments, membership of the identity in Lᵖ gives integrability of its norm power even on a seminormed group. On the real line, positive-order Lᵖ membership is equivalent to integrability of the corresponding absolute power.

The pointwise supremum of finitely many integrable lattice-valued functions is integrable (MeasureTheory.integrable_finset_sup').

theorem MeasureTheory.integrable_smul_iff_abs_smul {X : Type u_1} {F : Type u_2} [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : Measure X} {d : X → ℝ} {f : X → F} (hd : AEStronglyMeasurable d μ) : Integrable (fun (x : X) => d x • f x) μ ↔ Integrable (fun (x : X) => |d x| • f x) μ

Multiplication by an almost everywhere measurable real coefficient preserves integrability exactly when its absolute value does, without assuming measurability of the vector-valued f.

theorem MeasureTheory.summable_measureReal_mul_norm_of_integrable {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [MeasurableSingletonClass X] [NormedAddCommGroup E] {ν : Measure X} {f : X → E} (hf : Integrable f ν) : Summable fun (x : X) => ν.real {x} * ‖f x‖

Integrability with respect to a measure on a type with measurable singletons implies summability of the singleton masses weighted by the norms of the function values.

theorem MeasureTheory.isFiniteMeasure_of_integrable_of_one_le {X : Type u_1} {F : Type u_2} [MeasurableSpace X] [NormedAddCommGroup F] {f : X → F} {μ : Measure X} (hf : Integrable f μ) (h_one : ∀ᵐ (x : X) ∂μ, 1 ≤ ‖f x‖) : IsFiniteMeasure μ

An integrable function whose norm is almost everywhere at least one can only be carried by a finite measure.

theorem MeasureTheory.integrable_finset_sup' {X : Type u_1} {β : Type u_2} {κ : Type u_3} [MeasurableSpace X] [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] {μ : Measure X} {s : Finset κ} (hs : s.Nonempty) {f : κ → X → β} (hf : ∀ i ∈ s, Integrable (f i) μ) : Integrable (fun (x : X) => s.sup' hs fun (i : κ) => f i x) μ

The pointwise supremum over a nonempty finset of integrable functions with values in a normed lattice is integrable.

theorem MeasureTheory.MemLp.integrable_rpow {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {g : X → ℝ} {p : ℝ} (hp : 0 < p) (hg : MemLp g (ENNReal.ofReal p) μ) : Integrable (fun (y : X) => g y ^ p) μ

For a positive real order p, if g lies in Lᵖ then g ^ p is integrable.

theorem TauCeti.integrable_norm_rpow_of_memLp_id_ofReal {E : Type u_1} [SeminormedAddCommGroup E] [MeasurableSpace E] {p : ℝ} (hp : 0 ≤ p) {ν : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure ν] (hν : MeasureTheory.MemLp id (ENNReal.ofReal p) ν) : MeasureTheory.Integrable (fun (x : E) => ‖x‖ ^ p) ν

On a finite measure, Lᵖ membership of the identity gives integrability of its norm power, including for seminormed groups and order zero.

theorem TauCeti.memLp_id_ofReal_iff_integrable_abs_rpow {q : ℝ} (hq : 0 < q) (μ : MeasureTheory.Measure ℝ) : MeasureTheory.MemLp id (ENNReal.ofReal q) μ ↔ MeasureTheory.Integrable (fun (x : ℝ) => |x| ^ q) μ

For a positive real order, Lᵖ membership of the identity on the real line is equivalent to integrability of the absolute power.