Extension of set functions to L¹

Starting from the continuous linear map on integrable simple functions constructed in Mathlib.MeasureTheory.Integral.SetToL1.SimpleFunc, this file extends a dominated finitely-measure-additive set function to all of L¹. The main definition is MeasureTheory.L1.setToL1, together with its uniqueness, algebraic and order properties, norm bounds, and continuity.

noncomputable def MeasureTheory.L1.setToL1' {α : Type u_1} {E : Type u_2} {F : Type u_3} (𝕜 : Type u_4) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [Module 𝕜 F] [IsBoundedSMul 𝕜 E] [IsBoundedSMul 𝕜 F] [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) : ↥(Lp E 1 μ) →L[𝕜] F

Extend Set α → (E →L[ℝ] F) to (α →₁[μ] E) →L[𝕜] F.

Equations

• MeasureTheory.L1.setToL1' 𝕜 hT h_smul = (MeasureTheory.L1.SimpleFunc.setToL1SCLM' α E 𝕜 μ hT h_smul).extend (MeasureTheory.Lp.simpleFunc.coeToLp α E 𝕜)

theorem MeasureTheory.L1.setToL1'_eq_setToL1SCLM {α : Type u_1} {E : Type u_2} {F : Type u_3} (𝕜 : Type u_4) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [Module 𝕜 F] [IsBoundedSMul 𝕜 E] [IsBoundedSMul 𝕜 F] [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (f : ↥(α →₁ₛ[μ] E)) : (setToL1' 𝕜 hT h_smul) ↑f = (SimpleFunc.setToL1SCLM α E μ hT) f

@[simp]

theorem MeasureTheory.L1.setToL1'_apply_coeToLp {α : Type u_1} {E : Type u_2} {F : Type u_3} (𝕜 : Type u_4) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [Module 𝕜 F] [IsBoundedSMul 𝕜 E] [IsBoundedSMul 𝕜 F] [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (f : ↥(α →₁ₛ[μ] E)) : (setToL1' 𝕜 hT h_smul) ((Lp.simpleFunc.coeToLp α E ℝ) f) = (SimpleFunc.setToL1SCLM α E μ hT) f

noncomputable def MeasureTheory.L1.setToL1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) : ↥(Lp E 1 μ) →L[ℝ] F

Extend Set α → E →L[ℝ] F to (α →₁[μ] E) →L[ℝ] F.

Equations

• MeasureTheory.L1.setToL1 hT = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT).extend (MeasureTheory.Lp.simpleFunc.coeToLp α E ℝ)

theorem MeasureTheory.L1.setToL1_eq_setToL1SCLM {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (f : ↥(α →₁ₛ[μ] E)) : (setToL1 hT) ↑f = (SimpleFunc.setToL1SCLM α E μ hT) f

@[simp]

theorem MeasureTheory.L1.setToL1_apply_coeToLp {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (f : ↥(α →₁ₛ[μ] E)) : (setToL1 hT) ((Lp.simpleFunc.coeToLp α E ℝ) f) = (SimpleFunc.setToL1SCLM α E μ hT) f

theorem MeasureTheory.L1.setToL1_unique {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) {A : ↥(Lp E 1 μ) →L[ℝ] F} (hA : ∀ (f : ↥(α →₁ₛ[μ] E)), (SimpleFunc.setToL1SCLM α E μ hT) f = A ↑f) (f : ↥(Lp E 1 μ)) : (setToL1 hT) f = A f

theorem MeasureTheory.L1.setToL1_eq_setToL1' {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [Module 𝕜 F] [IsBoundedSMul 𝕜 E] [IsBoundedSMul 𝕜 F] [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (f : ↥(Lp E 1 μ)) : (setToL1 hT) f = (setToL1' 𝕜 hT h_smul) f

@[simp]

theorem MeasureTheory.L1.setToL1_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {C : ℝ} (hT : DominatedFinMeasAdditive μ 0 C) (f : ↥(Lp E 1 μ)) : (setToL1 hT) f = 0

theorem MeasureTheory.L1.setToL1_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0) (f : ↥(Lp E 1 μ)) : (setToL1 hT) f = 0

theorem MeasureTheory.L1.setToL1_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] (T T' : Set α → E →L[ℝ] F) {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (h : T = T') (f : ↥(Lp E 1 μ)) : (setToL1 hT) f = (setToL1 hT') f

theorem MeasureTheory.L1.setToL1_congr_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] (T T' : Set α → E →L[ℝ] F) {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s) (f : ↥(Lp E 1 μ)) : (setToL1 hT) f = (setToL1 hT') f

theorem MeasureTheory.L1.setToL1_add_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (f : ↥(Lp E 1 μ)) : (setToL1 ⋯) f = (setToL1 hT) f + (setToL1 hT') f

theorem MeasureTheory.L1.setToL1_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T T' T'' : Set α → E →L[ℝ] F} {C C' C'' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (hT'' : DominatedFinMeasAdditive μ T'' C'') (h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s) (f : ↥(Lp E 1 μ)) : (setToL1 hT'') f = (setToL1 hT) f + (setToL1 hT') f

theorem MeasureTheory.L1.setToL1_smul_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (c : ℝ) (f : ↥(Lp E 1 μ)) : (setToL1 ⋯) f = c • (setToL1 hT) f

theorem MeasureTheory.L1.setToL1_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (c : ℝ) (h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s) (f : ↥(Lp E 1 μ)) : (setToL1 hT') f = c • (setToL1 hT) f

theorem MeasureTheory.L1.setToL1_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [Module 𝕜 F] [IsBoundedSMul 𝕜 E] [IsBoundedSMul 𝕜 F] [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (c : 𝕜) (f : ↥(Lp E 1 μ)) : (setToL1 hT) (c • f) = c • (setToL1 hT) f

theorem MeasureTheory.L1.setToL1_simpleFunc_indicatorConst {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤) (x : E) : (setToL1 hT) ↑(Lp.simpleFunc.indicatorConst 1 hs ⋯ x) = (T s) x

theorem MeasureTheory.L1.setToL1_indicatorConstLp {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E) : (setToL1 hT) (indicatorConstLp 1 hs hμs x) = (T s) x

theorem MeasureTheory.L1.setToL1_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} [IsFiniteMeasure μ] (hT : DominatedFinMeasAdditive μ T C) (x : E) : (setToL1 hT) (indicatorConstLp 1 ⋯ ⋯ x) = (T Set.univ) x

theorem MeasureTheory.L1.setToL1_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_6} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [CompleteSpace G''] [OrderClosedTopology G''] {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x) (f : ↥(Lp E 1 μ)) : (setToL1 hT) f ≤ (setToL1 hT') f

theorem MeasureTheory.L1.setToL1_mono_left {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_6} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [CompleteSpace G''] [OrderClosedTopology G''] {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x) (f : ↥(Lp E 1 μ)) : (setToL1 hT) f ≤ (setToL1 hT') f

theorem MeasureTheory.L1.setToL1_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_5} {G'' : Type u_6} [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ G'] [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [CompleteSpace G''] [ClosedIciTopology G''] {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) {f : ↥(Lp G' 1 μ)} (hf : 0 ≤ f) : 0 ≤ (setToL1 hT) f

theorem MeasureTheory.L1.setToL1_mono {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_5} {G'' : Type u_6} [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ G'] [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [CompleteSpace G''] [ClosedIciTopology G''] [IsOrderedAddMonoid G'] {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) {f g : ↥(Lp G' 1 μ)} (hfg : f ≤ g) : (setToL1 hT) f ≤ (setToL1 hT) g

theorem MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) : ‖setToL1 hT‖ ≤ ‖SimpleFunc.setToL1SCLM α E μ hT‖

theorem MeasureTheory.L1.norm_setToL1_le_mul_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) (f : ↥(Lp E 1 μ)) : ‖(setToL1 hT) f‖ ≤ C * ‖f‖

theorem MeasureTheory.L1.norm_setToL1_le_mul_norm' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (f : ↥(Lp E 1 μ)) : ‖(setToL1 hT) f‖ ≤ max C 0 * ‖f‖

theorem MeasureTheory.L1.norm_setToL1_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) : ‖setToL1 hT‖ ≤ C

theorem MeasureTheory.L1.norm_setToL1_le' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) : ‖setToL1 hT‖ ≤ max C 0

theorem MeasureTheory.L1.setToL1_lipschitz {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) : LipschitzWith C.toNNReal ⇑(setToL1 hT)

theorem MeasureTheory.L1.tendsto_setToL1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (f : ↥(Lp E 1 μ)) {ι : Type u_5} (fs : ι → ↥(Lp E 1 μ)) {l : Filter ι} (hfs : Filter.Tendsto fs l (nhds f)) : Filter.Tendsto (fun (i : ι) => (setToL1 hT) (fs i)) l (nhds ((setToL1 hT) f))

If fs i → f in L1, then setToL1 hT (fs i) → setToL1 hT f.