Restriction and set integration on finite-measure sets

This file provides the continuous map from Lᵖ to L¹ obtained by restricting to a finite-measure set, together with the corresponding set-integral map. These constructions are useful whenever an Lᵖ identity is tested against integrals on finite-measure sets.

Main declarations

• MeasureTheory.Measure.LpToL1CLM: the continuous inclusion from Lᵖ to L¹ on a finite-measure space.
• MeasureTheory.Measure.LpToL1CLM_coeFn: the inclusion has the original representative almost everywhere.
• Set.LpToL1RestrictCLM: restriction from Lᵖ to L¹ on a finite-measure set.
• Set.LpToL1RestrictCLM_coeFn: the restricted class has the original representative almost everywhere.
• Set.setIntegralLp: integration on a finite-measure set as a continuous linear map on Lᵖ.
• Set.setIntegralLp_apply: the pointwise formula for this map.

noncomputable def MeasureTheory.Measure.LpToL1CLM {E : Type u_1} {F : Type u_2} {𝕜 : Type u_3} [MeasurableSpace E] [NormedAddCommGroup F] [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] (μ : Measure E) (p : ENNReal) [IsFiniteMeasure μ] [Fact (1 ≤ p)] : ↥(Lp F p μ) →L[𝕜] ↥(Lp F 1 μ)

The continuous inclusion from Lᵖ to L¹ on a finite-measure space.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Measure.LpToL1CLM_coeFn {E : Type u_1} {F : Type u_2} {𝕜 : Type u_3} [MeasurableSpace E] [NormedAddCommGroup F] [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] (μ : Measure E) (p : ENNReal) [IsFiniteMeasure μ] [Fact (1 ≤ p)] (f : ↥(Lp F p μ)) : ↑↑((μ.LpToL1CLM p) f) =ᵐ[μ] ↑↑f

The finite-measure Lᵖ to L¹ inclusion has the original representative almost everywhere.

noncomputable def Set.LpToL1RestrictCLM {E : Type u_1} {F : Type u_2} {𝕜 : Type u_3} [MeasurableSpace E] [NormedAddCommGroup F] [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {mu : MeasureTheory.Measure E} {p : ENNReal} [Fact (1 ≤ p)] (s : Set E) (hμs : mu s < ⊤) : ↥(MeasureTheory.Lp F p mu) →L[𝕜] ↥(MeasureTheory.Lp F 1 (mu.restrict s))

Restrict an Lᵖ class to a finite-measure set and view it as an L¹ class.

Equations

• s.LpToL1RestrictCLM hμs = (mu.restrict s).LpToL1CLM p ∘SL MeasureTheory.LpToLpRestrictCLM E F 𝕜 mu p s

theorem Set.LpToL1RestrictCLM_coeFn {E : Type u_1} {F : Type u_2} {𝕜 : Type u_3} [MeasurableSpace E] [NormedAddCommGroup F] [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {mu : MeasureTheory.Measure E} {p : ENNReal} [Fact (1 ≤ p)] (s : Set E) (hμs : mu s < ⊤) (f : ↥(MeasureTheory.Lp F p mu)) : ↑↑((s.LpToL1RestrictCLM hμs) f) =ᵐ[mu.restrict s] ↑↑f

The restricted L¹ class agrees almost everywhere with the original Lᵖ class.

noncomputable def Set.setIntegralLp {E : Type u_1} {F : Type u_2} {𝕜 : Type u_3} [MeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] [SMulCommClass ℝ 𝕜 F] [CompleteSpace F] {mu : MeasureTheory.Measure E} {p : ENNReal} [Fact (1 ≤ p)] (s : Set E) (hμs : mu s < ⊤) : ↥(MeasureTheory.Lp F p mu) →L[𝕜] F

Integrate an Lᵖ class over a finite-measure set as a continuous linear map.

Equations

• s.setIntegralLp hμs = MeasureTheory.L1.integralCLM' 𝕜 ∘SL s.LpToL1RestrictCLM hμs

@[simp]

theorem Set.setIntegralLp_apply {E : Type u_1} {F : Type u_2} {𝕜 : Type u_3} [MeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] [SMulCommClass ℝ 𝕜 F] [CompleteSpace F] {mu : MeasureTheory.Measure E} {p : ENNReal} [Fact (1 ≤ p)] (s : Set E) (hμs : mu s < ⊤) (f : ↥(MeasureTheory.Lp F p mu)) : (s.setIntegralLp hμs) f = ∫ (x : E) in s, ↑↑f x ∂mu

The set integral of an Lᵖ class agrees with the integral of its representative.