L¹ space

In this file we establish an API between Integrable and the space L¹ of equivalence classes of integrable functions, already defined as a special case of L^p spaces for p = 1.

Notation

• α →₁[μ] β is the type of L¹ space, where α is a MeasureSpace and β is a NormedAddCommGroup. f : α →ₘ β is a "function" in L¹. In comments, [f] is also used to denote an L¹ function.

  ₁ can be typed as \1.

Tags

function space, l1

def MeasureTheory.AEEqFun.Integrable {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] (f : α →ₘ[μ] ε) : Prop

A class of almost everywhere equal functions is Integrable if its function representative is integrable.

theorem MeasureTheory.AEEqFun.integrable_mk {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) : (mk f hf).Integrable ↔ MeasureTheory.Integrable f μ

theorem MeasureTheory.AEEqFun.integrable_coeFn {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α →ₘ[μ] ε} : MeasureTheory.Integrable (↑f) μ ↔ f.Integrable

theorem MeasureTheory.AEEqFun.integrable_zero {α : Type u_1} {ε' : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε'] [ENormedAddMonoid ε'] : Integrable 0

theorem MeasureTheory.AEEqFun.Integrable.neg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α →ₘ[μ] β} : f.Integrable → (-f).Integrable

theorem MeasureTheory.AEEqFun.integrable_iff_mem_L1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α →ₘ[μ] β} : f.Integrable ↔ f ∈ Lp β 1 μ

theorem MeasureTheory.AEEqFun.Integrable.add {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f g : α →ₘ[μ] β} : f.Integrable → g.Integrable → (f + g).Integrable

theorem MeasureTheory.AEEqFun.Integrable.sub {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f g : α →ₘ[μ] β} (hf : f.Integrable) (hg : g.Integrable) : (f - g).Integrable

theorem MeasureTheory.AEEqFun.Integrable.smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜} {f : α →ₘ[μ] β} : f.Integrable → (c • f).Integrable

theorem MeasureTheory.L1.integrable_coeFn {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : ↥(Lp β 1 μ)) : Integrable (↑↑f) μ

theorem MeasureTheory.L1.hasFiniteIntegral_coeFn {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : ↥(Lp β 1 μ)) : HasFiniteIntegral (↑↑f) μ

theorem MeasureTheory.L1.stronglyMeasurable_coeFn {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : ↥(Lp β 1 μ)) : StronglyMeasurable ↑↑f

theorem MeasureTheory.L1.measurable_coeFn {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [MeasurableSpace β] [BorelSpace β] (f : ↥(Lp β 1 μ)) : Measurable ↑↑f

theorem MeasureTheory.L1.aestronglyMeasurable_coeFn {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : ↥(Lp β 1 μ)) : AEStronglyMeasurable (↑↑f) μ

theorem MeasureTheory.L1.aemeasurable_coeFn {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [MeasurableSpace β] [BorelSpace β] (f : ↥(Lp β 1 μ)) : AEMeasurable (↑↑f) μ

theorem MeasureTheory.L1.edist_def {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f g : ↥(Lp β 1 μ)) : edist f g = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ

theorem MeasureTheory.L1.dist_def {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f g : ↥(Lp β 1 μ)) : dist f g = (∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ).toReal

theorem MeasureTheory.L1.norm_def {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : ↥(Lp β 1 μ)) : ‖f‖ = (∫⁻ (a : α), ‖↑↑f a‖ₑ ∂μ).toReal

theorem MeasureTheory.L1.norm_sub_eq_lintegral {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f g : ↥(Lp β 1 μ)) : ‖f - g‖ = (∫⁻ (x : α), ‖↑↑f x - ↑↑g x‖ₑ ∂μ).toReal

Computing the norm of a difference between two L¹-functions. Note that this is not a special case of norm_def since (f - g) x and f x - g x are not equal (but only a.e.-equal).

theorem MeasureTheory.L1.ofReal_norm_eq_lintegral {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : ↥(Lp β 1 μ)) : ENNReal.ofReal ‖f‖ = ∫⁻ (x : α), ‖↑↑f x‖ₑ ∂μ

theorem MeasureTheory.L1.ofReal_norm_sub_eq_lintegral {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f g : ↥(Lp β 1 μ)) : ENNReal.ofReal ‖f - g‖ = ∫⁻ (x : α), ‖↑↑f x - ↑↑g x‖ₑ ∂μ

Computing the norm of a difference between two L¹-functions. Note that this is not a special case of ofReal_norm_eq_lintegral since (f - g) x and f x - g x are not equal (but only a.e.-equal).

def MeasureTheory.Integrable.toL1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : α → β) (hf : Integrable f μ) : ↥(Lp β 1 μ)

Construct the equivalence class [f] of an integrable function f, as a member of the space Lp β 1 μ.

@[simp]

theorem MeasureTheory.Integrable.toL1_coeFn {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : ↥(Lp β 1 μ)) (hf : Integrable (↑↑f) μ) : toL1 (↑↑f) hf = f

theorem MeasureTheory.Integrable.coeFn_toL1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} (hf : Integrable f μ) : ↑↑(toL1 f hf) =ᶠ[ae μ] f

@[simp]

theorem MeasureTheory.Integrable.toL1_zero {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (h : Integrable 0 μ) : toL1 0 h = 0

@[simp]

theorem MeasureTheory.Integrable.toL1_eq_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : α → β) (hf : Integrable f μ) : ↑(toL1 f hf) = AEEqFun.mk f ⋯

@[simp]

theorem MeasureTheory.Integrable.toL1_eq_toL1_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f g : α → β) (hf : Integrable f μ) (hg : Integrable g μ) : toL1 f hf = toL1 g hg ↔ f =ᶠ[ae μ] g

theorem MeasureTheory.Integrable.toL1_add {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f g : α → β) (hf : Integrable f μ) (hg : Integrable g μ) : toL1 (f + g) ⋯ = toL1 f hf + toL1 g hg

theorem MeasureTheory.Integrable.toL1_neg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : α → β) (hf : Integrable f μ) : toL1 (-f) ⋯ = -toL1 f hf

theorem MeasureTheory.Integrable.toL1_sub {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f g : α → β) (hf : Integrable f μ) (hg : Integrable g μ) : toL1 (f - g) ⋯ = toL1 f hf - toL1 g hg

theorem MeasureTheory.Integrable.norm_toL1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : α → β) (hf : Integrable f μ) : ‖toL1 f hf‖ = (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal

theorem MeasureTheory.Integrable.enorm_toL1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} (hf : Integrable f μ) : ‖toL1 f hf‖ₑ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

@[deprecated MeasureTheory.Integrable.enorm_toL1 (since := "2025-01-20")]

theorem MeasureTheory.Integrable.nnnorm_toL1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} (hf : Integrable f μ) : ‖toL1 f hf‖ₑ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Alias of MeasureTheory.Integrable.enorm_toL1.

theorem MeasureTheory.Integrable.norm_toL1_eq_lintegral_norm {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : α → β) (hf : Integrable f μ) : ‖toL1 f hf‖ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

@[simp]

theorem MeasureTheory.Integrable.edist_toL1_toL1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f g : α → β) (hf : Integrable f μ) (hg : Integrable g μ) : edist (toL1 f hf) (toL1 g hg) = ∫⁻ (a : α), edist (f a) (g a) ∂μ

theorem MeasureTheory.Integrable.edist_toL1_zero {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : α → β) (hf : Integrable f μ) : edist (toL1 f hf) 0 = ∫⁻ (a : α), edist (f a) 0 ∂μ

theorem MeasureTheory.Integrable.toL1_smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 β] [IsBoundedSMul 𝕜 β] (f : α → β) (hf : Integrable f μ) (k : 𝕜) : toL1 (fun (a : α) => k • f a) ⋯ = k • toL1 f hf

theorem MeasureTheory.Integrable.toL1_smul' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 β] [IsBoundedSMul 𝕜 β] (f : α → β) (hf : Integrable f μ) (k : 𝕜) : toL1 (k • f) ⋯ = k • toL1 f hf