Extension of a linear function from indicators to L1

Given T : Set α → E →L[ℝ] F with DominatedFinMeasAdditive μ T C, we construct an extension of T to integrable simple functions, which are finite sums of indicators of measurable sets with finite measure, then to integrable functions, which are limits of integrable simple functions.

The main result is a continuous linear map (α →₁[μ] E) →L[ℝ] F. This extension process is used to define the Bochner integral in the Mathlib/MeasureTheory/Integral/Bochner/Basic.lean file and the conditional expectation of an integrable function in Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean.

Main definitions

• setToL1 (hT : DominatedFinMeasAdditive μ T C) : (α →₁[μ] E) →L[ℝ] F: the extension of T from indicators to L1.
• setToFun μ T (hT : DominatedFinMeasAdditive μ T C) (f : α → E) : F: a version of the extension which applies to functions (with value 0 if the function is not integrable).

Properties

For most properties of setToFun, we provide two lemmas. One version uses hypotheses valid on all sets, like T = T', and a second version which uses a primed name uses hypotheses on measurable sets with finite measure, like ∀ s, MeasurableSet s → μ s < ∞ → T s = T' s.

The lemmas listed here don't show all hypotheses. Refer to the actual lemmas for details.

Linearity:

• setToFun_zero_left : setToFun μ 0 hT f = 0
• setToFun_add_left : setToFun μ (T + T') _ f = setToFun μ T hT f + setToFun μ T' hT' f
• setToFun_smul_left : setToFun μ (fun s ↦ c • (T s)) (hT.smul c) f = c • setToFun μ T hT f
• setToFun_zero : setToFun μ T hT (0 : α → E) = 0
• setToFun_neg : setToFun μ T hT (-f) = - setToFun μ T hT f If f and g are integrable:
• setToFun_add : setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g
• setToFun_sub : setToFun μ T hT (f - g) = setToFun μ T hT f - setToFun μ T hT g If T satisfies ∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x:
• setToFun_smul : setToFun μ T hT (c • f) = c • setToFun μ T hT f

Other:

• setToFun_congr_ae (h : f =ᵐ[μ] g) : setToFun μ T hT f = setToFun μ T hT g
• setToFun_measure_zero (h : μ = 0) : setToFun μ T hT f = 0

If the space is also an ordered additive group with an order closed topology and T is such that 0 ≤ T s x for 0 ≤ x, we also prove order-related properties:

• setToFun_mono_left (h : ∀ s x, T s x ≤ T' s x) : setToFun μ T hT f ≤ setToFun μ T' hT' f
• setToFun_nonneg (hf : 0 ≤ᵐ[μ] f) : 0 ≤ setToFun μ T hT f
• setToFun_mono (hfg : f ≤ᵐ[μ] g) : setToFun μ T hT f ≤ setToFun μ T hT g

theorem MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {μ : Measure α} (f : ↥(Lp.simpleFunc G 1 μ)) : ‖f‖ = ∑ x ∈ (Lp.simpleFunc.toSimpleFunc f).range, μ.real (⇑(Lp.simpleFunc.toSimpleFunc f) ⁻¹' {x}) * ‖x‖

def MeasureTheory.L1.SimpleFunc.setToL1S {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ] F) (f : ↥(Lp.simpleFunc E 1 μ)) : F

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

Equations

• MeasureTheory.L1.SimpleFunc.setToL1S T f = MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.Lp.simpleFunc.toSimpleFunc f)

theorem MeasureTheory.L1.SimpleFunc.setToL1S_eq_setToSimpleFunc {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ] F) (f : ↥(Lp.simpleFunc E 1 μ)) : setToL1S T f = SimpleFunc.setToSimpleFunc T (Lp.simpleFunc.toSimpleFunc f)

@[simp]

theorem MeasureTheory.L1.SimpleFunc.setToL1S_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (f : ↥(Lp.simpleFunc E 1 μ)) : setToL1S 0 f = 0

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

theorem MeasureTheory.L1.SimpleFunc.setToL1S_congr {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ] F) (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) {f g : ↥(Lp.simpleFunc E 1 μ)} (h : ⇑(Lp.simpleFunc.toSimpleFunc f) =ᶠ[ae μ] ⇑(Lp.simpleFunc.toSimpleFunc g)) : setToL1S T f = setToL1S T g

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

theorem MeasureTheory.L1.SimpleFunc.setToL1S_congr_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ μ' : Measure α} (T : Set α → E →L[ℝ] F) (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (hμ : μ.AbsolutelyContinuous μ') (f : ↥(Lp.simpleFunc E 1 μ)) (f' : ↥(Lp.simpleFunc E 1 μ')) (h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f') : setToL1S T f = setToL1S T f'

setToL1S does not change if we replace the measure μ by μ' with μ ≪ μ'. The statement uses two functions f and f' because they have to belong to different types, but morally these are the same function (we have f =ᵐ[μ] f').

theorem MeasureTheory.L1.SimpleFunc.setToL1S_add_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T T' : Set α → E →L[ℝ] F) (f : ↥(Lp.simpleFunc E 1 μ)) : setToL1S (T + T') f = setToL1S T f + setToL1S T' f

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

theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ] F) (c : ℝ) (f : ↥(Lp.simpleFunc E 1 μ)) : setToL1S (fun (s : Set α) => c • T s) f = c • setToL1S T f

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

theorem MeasureTheory.L1.SimpleFunc.setToL1S_add {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ] F) (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (f g : ↥(Lp.simpleFunc E 1 μ)) : setToL1S T (f + g) = setToL1S T f + setToL1S T g

theorem MeasureTheory.L1.SimpleFunc.setToL1S_neg {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (f : ↥(Lp.simpleFunc E 1 μ)) : setToL1S T (-f) = -setToL1S T f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (f g : ↥(Lp.simpleFunc E 1 μ)) : setToL1S T (f - g) = setToL1S T f - setToL1S T g

theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul_real {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ] F) (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (c : ℝ) (f : ↥(Lp.simpleFunc E 1 μ)) : setToL1S T (c • f) = c • setToL1S T f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [DistribSMul 𝕜 F] (T : Set α → E →L[ℝ] F) (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (c : 𝕜) (f : ↥(Lp.simpleFunc E 1 μ)) : setToL1S T (c • f) = c • setToL1S T f

theorem MeasureTheory.L1.SimpleFunc.norm_setToL1S_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ] F) {C : ℝ} (hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * μ.real s) (f : ↥(Lp.simpleFunc E 1 μ)) : ‖setToL1S T f‖ ≤ C * ‖f‖

theorem MeasureTheory.L1.SimpleFunc.setToL1S_indicatorConst {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {s : Set α} (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (hs : MeasurableSet s) (hμs : μ s < ⊤) (x : E) : setToL1S T (Lp.simpleFunc.indicatorConst 1 hs ⋯ x) = (T s) x

theorem MeasureTheory.L1.SimpleFunc.setToL1S_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {T : Set α → E →L[ℝ] F} (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (x : E) : setToL1S T (Lp.simpleFunc.indicatorConst 1 ⋯ ⋯ x) = (T Set.univ) x

theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono_left {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_7} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] {T T' : Set α → E →L[ℝ] G''} (hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x) (f : ↥(Lp.simpleFunc E 1 μ)) : setToL1S T f ≤ setToL1S T' f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_7} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] {T T' : Set α → E →L[ℝ] G''} (hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x) (f : ↥(Lp.simpleFunc E 1 μ)) : setToL1S T f ≤ setToL1S T' f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_7} {G' : Type u_8} [NormedAddCommGroup G'] [PartialOrder G'] [IsOrderedAddMonoid G'] [NormedSpace ℝ G'] [NormedAddCommGroup G''] [PartialOrder G''] [NormedSpace ℝ G''] {T : Set α → G'' →L[ℝ] G'} (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x) {f : ↥(Lp.simpleFunc G'' 1 μ)} (hf : 0 ≤ f) : 0 ≤ setToL1S T f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_7} {G' : Type u_8} [NormedAddCommGroup G'] [PartialOrder G'] [IsOrderedAddMonoid G'] [NormedSpace ℝ G'] [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] {T : Set α → G'' →L[ℝ] G'} (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x) {f g : ↥(Lp.simpleFunc G'' 1 μ)} (hfg : f ≤ g) : setToL1S T f ≤ setToL1S T g

def MeasureTheory.L1.SimpleFunc.setToL1SCLM' (α : Type u_1) (E : Type u_2) {F : Type u_3} (𝕜 : Type u_6) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} (μ : Measure α) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Module 𝕜 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.simpleFunc E 1 μ) →L[𝕜] F

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

Equations

• MeasureTheory.L1.SimpleFunc.setToL1SCLM' α E 𝕜 μ hT h_smul = { toFun := MeasureTheory.L1.SimpleFunc.setToL1S T, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous C ⋯

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

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

Equations

• MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT = { toFun := MeasureTheory.L1.SimpleFunc.setToL1S T, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous C ⋯

@[simp]

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

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

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

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {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.simpleFunc E 1 μ)) : (setToL1SCLM α E μ hT) f = (setToL1SCLM α E μ hT') f

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C C' : ℝ} {μ' : Measure α} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ' T C') (hμ : μ.AbsolutelyContinuous μ') (f : ↥(Lp.simpleFunc E 1 μ)) (f' : ↥(Lp.simpleFunc E 1 μ')) (h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f') : (setToL1SCLM α E μ hT) f = (setToL1SCLM α E μ' hT') f'

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

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {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.simpleFunc E 1 μ)) : (setToL1SCLM α E μ hT'') f = (setToL1SCLM α E μ hT) f + (setToL1SCLM α E μ hT') f

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

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

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

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

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (x : E) : (setToL1SCLM α E μ hT) (Lp.simpleFunc.indicatorConst 1 ⋯ ⋯ x) = (T Set.univ) x

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ 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.simpleFunc E 1 μ)) : (setToL1SCLM α E μ hT) f ≤ (setToL1SCLM α E μ hT') f

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ 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.simpleFunc E 1 μ)) : (setToL1SCLM α E μ hT) f ≤ (setToL1SCLM α E μ hT') f

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ 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.simpleFunc G' 1 μ)} (hf : 0 ≤ f) : 0 ≤ (setToL1SCLM α G' μ hT) f

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [NormedAddCommGroup G'] [PartialOrder G'] [IsOrderedAddMonoid G'] [NormedSpace ℝ 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.simpleFunc G' 1 μ)} (hfg : f ≤ g) : (setToL1SCLM α G' μ hT) f ≤ (setToL1SCLM α G' μ hT) g

def MeasureTheory.L1.setToL1' {α : Type u_1} {E : Type u_2} {F : Type u_3} (𝕜 : Type u_6) [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 𝕜) ⋯ ⋯

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 : ↥(Lp.simpleFunc E 1 μ)) : (setToL1 hT) ↑f = (SimpleFunc.setToL1SCLM α E μ hT) f

theorem MeasureTheory.L1.setToL1_eq_setToL1' {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [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_6} [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_8} [NormedAddCommGroup G''] [PartialOrder G''] [OrderClosedTopology G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [CompleteSpace 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_8} [NormedAddCommGroup G''] [PartialOrder G''] [OrderClosedTopology G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [CompleteSpace 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_7} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [OrderClosedTopology G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [CompleteSpace G''] [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ 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_7} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [OrderClosedTopology G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [CompleteSpace G''] [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ 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_7} (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.

def MeasureTheory.setToFun {α : 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) : F

Extend T : Set α → E →L[ℝ] F to (α → E) → F (for integrable functions α → E). We set it to 0 if the function is not integrable.

Equations

• MeasureTheory.setToFun μ T hT f = if hf : MeasureTheory.Integrable f μ then (MeasureTheory.L1.setToL1 hT) (MeasureTheory.Integrable.toL1 f hf) else 0

theorem MeasureTheory.setToFun_eq {α : 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 : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) : setToFun μ T hT f = (L1.setToL1 hT) (Integrable.toL1 f hf)

theorem MeasureTheory.L1.setToFun_eq_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 μ)) : setToFun μ T hT ↑↑f = (setToL1 hT) f

theorem MeasureTheory.setToFun_undef {α : 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 : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : ¬Integrable f μ) : setToFun μ T hT f = 0

theorem MeasureTheory.setToFun_non_aestronglyMeasurable {α : 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 : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : ¬AEStronglyMeasurable f μ) : setToFun μ T hT f = 0

@[deprecated MeasureTheory.setToFun_non_aestronglyMeasurable (since := "2025-04-09")]

theorem MeasureTheory.setToFun_non_aEStronglyMeasurable {α : 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 : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : ¬AEStronglyMeasurable f μ) : setToFun μ T hT f = 0

Alias of MeasureTheory.setToFun_non_aestronglyMeasurable.

theorem MeasureTheory.setToFun_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 : α → E) : setToFun μ T hT f = setToFun μ T' hT' f

theorem MeasureTheory.setToFun_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 : α → E) : setToFun μ T hT f = setToFun μ T' hT' f

theorem MeasureTheory.setToFun_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 : α → E) : setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

theorem MeasureTheory.setToFun_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 : α → E) : setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f

theorem MeasureTheory.setToFun_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 : α → E) : setToFun μ (fun (s : Set α) => c • T s) ⋯ f = c • setToFun μ T hT f

theorem MeasureTheory.setToFun_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 : α → E) : setToFun μ T' hT' f = c • setToFun μ T hT f

@[simp]

theorem MeasureTheory.setToFun_zero {α : 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) : setToFun μ T hT 0 = 0

@[simp]

theorem MeasureTheory.setToFun_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 : ℝ} {f : α → E} {hT : DominatedFinMeasAdditive μ 0 C} : setToFun μ 0 hT f = 0

theorem MeasureTheory.setToFun_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 : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0) : setToFun μ T hT f = 0

theorem MeasureTheory.setToFun_add {α : 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 : ℝ} {f g : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) (hg : Integrable g μ) : setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g

theorem MeasureTheory.setToFun_finset_sum' {α : 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) {ι : Type u_7} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, Integrable (f i) μ) : setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)

theorem MeasureTheory.setToFun_finset_sum {α : 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) {ι : Type u_7} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, Integrable (f i) μ) : (setToFun μ T hT fun (a : α) => ∑ i ∈ s, f i a) = ∑ i ∈ s, setToFun μ T hT (f i)

theorem MeasureTheory.setToFun_neg {α : 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) : setToFun μ T hT (-f) = -setToFun μ T hT f

theorem MeasureTheory.setToFun_sub {α : 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 : ℝ} {f g : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) (hg : Integrable g μ) : setToFun μ T hT (f - g) = setToFun μ T hT f - setToFun μ T hT g

theorem MeasureTheory.setToFun_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} [NormedDivisionRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [Module 𝕜 F] [NormSMulClass 𝕜 F] (hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (c : 𝕜) (f : α → E) : setToFun μ T hT (c • f) = c • setToFun μ T hT f

theorem MeasureTheory.setToFun_congr_ae {α : 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 : ℝ} {f g : α → E} (hT : DominatedFinMeasAdditive μ T C) (h : f =ᶠ[ae μ] g) : setToFun μ T hT f = setToFun μ T hT g

theorem MeasureTheory.setToFun_measure_zero {α : 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 : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (h : μ = 0) : setToFun μ T hT f = 0

theorem MeasureTheory.setToFun_measure_zero' {α : 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 : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → μ s = 0) : setToFun μ T hT f = 0

theorem MeasureTheory.setToFun_toL1 {α : 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 : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) : setToFun μ T hT ↑↑(Integrable.toL1 f hf) = setToFun μ T hT f

theorem MeasureTheory.setToFun_indicator_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 : ℝ} (hT : DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E) : setToFun μ T hT (s.indicator fun (x_1 : α) => x) = (T s) x

theorem MeasureTheory.setToFun_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) : (setToFun μ T hT fun (x_1 : α) => x) = (T Set.univ) x

theorem MeasureTheory.setToFun_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [OrderClosedTopology G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [CompleteSpace 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 : α → E) : setToFun μ T hT f ≤ setToFun μ T' hT' f

theorem MeasureTheory.setToFun_mono_left {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [OrderClosedTopology G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [CompleteSpace 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 μ)) : setToFun μ T hT ↑↑f ≤ setToFun μ T' hT' ↑↑f

theorem MeasureTheory.setToFun_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [OrderClosedTopology G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [CompleteSpace G''] [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ 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'} (hf : 0 ≤ᶠ[ae μ] f) : 0 ≤ setToFun μ T hT f

theorem MeasureTheory.setToFun_mono {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [OrderClosedTopology G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [CompleteSpace G''] [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ 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 : α → G'} (hf : Integrable f μ) (hg : Integrable g μ) (hfg : f ≤ᶠ[ae μ] g) : setToFun μ T hT f ≤ setToFun μ T hT g

theorem MeasureTheory.continuous_setToFun {α : 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) : Continuous fun (f : ↥(Lp E 1 μ)) => setToFun μ T hT ↑↑f

theorem MeasureTheory.tendsto_setToFun_of_L1 {α : 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) {ι : Type u_7} (f : α → E) (hfi : Integrable f μ) {fs : ι → α → E} {l : Filter ι} (hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ) (hfs : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => setToFun μ T hT (fs i)) l (nhds (setToFun μ T hT f))

If F i → f in L1, then setToFun μ T hT (F i) → setToFun μ T hT f.

theorem MeasureTheory.tendsto_setToFun_approxOn_of_measurable {α : 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) [MeasurableSpace E] [BorelSpace E] {f : α → E} {s : Set E} [TopologicalSpace.SeparableSpace ↑s] (hfi : Integrable f μ) (hfm : Measurable f) (hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s) {y₀ : E} (h₀ : y₀ ∈ s) (h₀i : Integrable (fun (x : α) => y₀) μ) : Filter.Tendsto (fun (n : ℕ) => setToFun μ T hT ⇑(SimpleFunc.approxOn f hfm s y₀ h₀ n)) Filter.atTop (nhds (setToFun μ T hT f))

theorem MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset {α : 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) [MeasurableSpace E] [BorelSpace E] {f : α → E} (fmeas : Measurable f) (hf : Integrable f μ) (s : Set E) [TopologicalSpace.SeparableSpace ↑s] (hs : Set.range f ∪ {0} ⊆ s) : Filter.Tendsto (fun (n : ℕ) => setToFun μ T hT ⇑(SimpleFunc.approxOn f fmeas s 0 ⋯ n)) Filter.atTop (nhds (setToFun μ T hT f))

theorem MeasureTheory.continuous_L1_toL1 {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {μ μ' : Measure α} (c' : ENNReal) (hc' : c' ≠ ⊤) (hμ'_le : μ' ≤ c' • μ) : Continuous fun (f : ↥(Lp G 1 μ)) => Integrable.toL1 ↑↑f ⋯

Auxiliary lemma for setToFun_congr_measure: the function sending f : α →₁[μ] G to f : α →₁[μ'] G is continuous when μ' ≤ c' • μ for c' ≠ ∞.

theorem MeasureTheory.setToFun_congr_measure_of_integrable {α : 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 C' : ℝ} {μ' : Measure α} (c' : ENNReal) (hc' : c' ≠ ⊤) (hμ'_le : μ' ≤ c' • μ) (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ' T C') (f : α → E) (hfμ : Integrable f μ) : setToFun μ T hT f = setToFun μ' T hT' f

theorem MeasureTheory.setToFun_congr_measure {α : 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 C' : ℝ} {μ' : Measure α} (c c' : ENNReal) (hc : c ≠ ⊤) (hc' : c' ≠ ⊤) (hμ_le : μ ≤ c • μ') (hμ'_le : μ' ≤ c' • μ) (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ' T C') (f : α → E) : setToFun μ T hT f = setToFun μ' T hT' f

theorem MeasureTheory.setToFun_congr_measure_of_add_right {α : 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 C' : ℝ} {μ' : Measure α} (hT_add : DominatedFinMeasAdditive (μ + μ') T C') (hT : DominatedFinMeasAdditive μ T C) (f : α → E) (hf : Integrable f (μ + μ')) : setToFun (μ + μ') T hT_add f = setToFun μ T hT f

theorem MeasureTheory.setToFun_congr_measure_of_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 : Set α → E →L[ℝ] F} {C C' : ℝ} {μ' : Measure α} (hT_add : DominatedFinMeasAdditive (μ + μ') T C') (hT : DominatedFinMeasAdditive μ' T C) (f : α → E) (hf : Integrable f (μ + μ')) : setToFun (μ + μ') T hT_add f = setToFun μ' T hT f

theorem MeasureTheory.setToFun_top_smul_measure {α : 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) : setToFun (⊤ • μ) T hT f = 0

theorem MeasureTheory.setToFun_congr_smul_measure {α : 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 C' : ℝ} (c : ENNReal) (hc_ne_top : c ≠ ⊤) (hT : DominatedFinMeasAdditive μ T C) (hT_smul : DominatedFinMeasAdditive (c • μ) T C') (f : α → E) : setToFun μ T hT f = setToFun (c • μ) T hT_smul f

theorem MeasureTheory.norm_setToFun_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 μ)) (hC : 0 ≤ C) : ‖setToFun μ T hT ↑↑f‖ ≤ C * ‖f‖

theorem MeasureTheory.norm_setToFun_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 μ)) : ‖setToFun μ T hT ↑↑f‖ ≤ max C 0 * ‖f‖

theorem MeasureTheory.norm_setToFun_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 : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) (hC : 0 ≤ C) : ‖setToFun μ T hT f‖ ≤ C * ‖Integrable.toL1 f hf‖

theorem MeasureTheory.norm_setToFun_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 : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) : ‖setToFun μ T hT f‖ ≤ max C 0 * ‖Integrable.toL1 f hf‖

theorem MeasureTheory.tendsto_setToFun_of_dominated_convergence {α : 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) {fs : ℕ → α → E} {f : α → E} (bound : α → ℝ) (fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ) (bound_integrable : Integrable bound μ) (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => fs n a) Filter.atTop (nhds (f a))) : Filter.Tendsto (fun (n : ℕ) => setToFun μ T hT (fs n)) Filter.atTop (nhds (setToFun μ T hT f))

Lebesgue dominated convergence theorem provides sufficient conditions under which almost everywhere convergence of a sequence of functions implies the convergence of their image by setToFun. We could weaken the condition bound_integrable to require HasFiniteIntegral bound μ instead (i.e. not requiring that bound is measurable), but in all applications proving integrability is easier.

theorem MeasureTheory.tendsto_setToFun_filter_of_dominated_convergence {α : 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) {ι : Type u_7} {l : Filter ι} [l.IsCountablyGenerated] {fs : ι → α → E} {f : α → E} (bound : α → ℝ) (hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ) (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) (bound_integrable : Integrable bound μ) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ι) => fs n a) l (nhds (f a))) : Filter.Tendsto (fun (n : ι) => setToFun μ T hT (fs n)) l (nhds (setToFun μ T hT f))

Lebesgue dominated convergence theorem for filters with a countable basis

theorem MeasureTheory.continuousWithinAt_setToFun_of_dominated {α : 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 : ℝ} {X : Type u_7} [TopologicalSpace X] [FirstCountableTopology X] (hT : DominatedFinMeasAdditive μ T C) {fs : X → α → E} {x₀ : X} {bound : α → ℝ} {s : Set X} (hfs_meas : ∀ᶠ (x : X) in nhdsWithin x₀ s, AEStronglyMeasurable (fs x) μ) (h_bound : ∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a) (bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun (x : X) => fs x a) s x₀) : ContinuousWithinAt (fun (x : X) => setToFun μ T hT (fs x)) s x₀

theorem MeasureTheory.continuousAt_setToFun_of_dominated {α : 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 : ℝ} {X : Type u_7} [TopologicalSpace X] [FirstCountableTopology X] (hT : DominatedFinMeasAdditive μ T C) {fs : X → α → E} {x₀ : X} {bound : α → ℝ} (hfs_meas : ∀ᶠ (x : X) in nhds x₀, AEStronglyMeasurable (fs x) μ) (h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a) (bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun (x : X) => fs x a) x₀) : ContinuousAt (fun (x : X) => setToFun μ T hT (fs x)) x₀

theorem MeasureTheory.continuousOn_setToFun_of_dominated {α : 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 : ℝ} {X : Type u_7} [TopologicalSpace X] [FirstCountableTopology X] (hT : DominatedFinMeasAdditive μ T C) {fs : X → α → E} {bound : α → ℝ} {s : Set X} (hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ) (h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a) (bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun (x : X) => fs x a) s) : ContinuousOn (fun (x : X) => setToFun μ T hT (fs x)) s

theorem MeasureTheory.continuous_setToFun_of_dominated {α : 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 : ℝ} {X : Type u_7} [TopologicalSpace X] [FirstCountableTopology X] (hT : DominatedFinMeasAdditive μ T C) {fs : X → α → E} {bound : α → ℝ} (hfs_meas : ∀ (x : X), AEStronglyMeasurable (fs x) μ) (h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a) (bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, Continuous fun (x : X) => fs x a) : Continuous fun (x : X) => setToFun μ T hT (fs x)