Extension of a linear function from indicators to L1

Let T : Set α → E →L[ℝ] F be additive for measurable sets with finite measure, in the sense that for s, t two such sets, Disjoint s t → T (s ∪ t) = T s + T t. T is akin to a bilinear map on Set α × E, or a linear map on indicator functions.

This file constructs 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 file and the conditional expectation of an integrable function in Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1.

Main Definitions

• FinMeasAdditive μ T: the property that T is additive on measurable sets with finite measure. For two such sets, Disjoint s t → T (s ∪ t) = T s + T t.
• DominatedFinMeasAdditive μ T C: FinMeasAdditive μ T ∧ ∀ s, ‖T s‖ ≤ C * (μ s).toReal. This is the property needed to perform the extension from indicators to L1.
• 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 is verifies ∀ 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 a NormedLatticeAddCommGroup 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

Implementation notes

The starting object T : Set α → E →L[ℝ] F matters only through its restriction on measurable sets with finite measure. Its value on other sets is ignored.

def MeasureTheory.FinMeasAdditive {α : Type u_1} {β : Type u_7} [AddMonoid β] {x✝ : MeasurableSpace α} (μ : Measure α) (T : Set α → β) : Prop

A set function is FinMeasAdditive if its value on the union of two disjoint measurable sets with finite measure is the sum of its values on each set.

Equations

• MeasureTheory.FinMeasAdditive μ T = ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → μ s ≠ ⊤ → μ t ≠ ⊤ → Disjoint s t → T (s ∪ t) = T s + T t

theorem MeasureTheory.FinMeasAdditive.zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [AddCommMonoid β] : FinMeasAdditive μ 0

theorem MeasureTheory.FinMeasAdditive.add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [AddCommMonoid β] {T T' : Set α → β} (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive μ T') : FinMeasAdditive μ (T + T')

theorem MeasureTheory.FinMeasAdditive.smul {α : Type u_1} {𝕜 : Type u_6} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [AddCommMonoid β] {T : Set α → β} [Monoid 𝕜] [DistribMulAction 𝕜 β] (hT : FinMeasAdditive μ T) (c : 𝕜) : FinMeasAdditive μ fun (s : Set α) => c • T s

theorem MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [AddCommMonoid β] {T : Set α → β} {μ' : Measure α} (h : ∀ (s : Set α), MeasurableSet s → μ s = ⊤ → μ' s = ⊤) (hT : FinMeasAdditive μ T) : FinMeasAdditive μ' T

theorem MeasureTheory.FinMeasAdditive.of_smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [AddCommMonoid β] {T : Set α → β} {c : ENNReal} (hc_ne_top : c ≠ ⊤) (hT : FinMeasAdditive (c • μ) T) : FinMeasAdditive μ T

theorem MeasureTheory.FinMeasAdditive.smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [AddCommMonoid β] {T : Set α → β} (c : ENNReal) (hc_ne_zero : c ≠ 0) (hT : FinMeasAdditive μ T) : FinMeasAdditive (c • μ) T

theorem MeasureTheory.FinMeasAdditive.smul_measure_iff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [AddCommMonoid β] {T : Set α → β} (c : ENNReal) (hc_ne_zero : c ≠ 0) (hc_ne_top : c ≠ ⊤) : FinMeasAdditive (c • μ) T ↔ FinMeasAdditive μ T

theorem MeasureTheory.FinMeasAdditive.map_empty_eq_zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_8} [AddCancelMonoid β] {T : Set α → β} (hT : FinMeasAdditive μ T) : T ∅ = 0

theorem MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [AddCommMonoid β] (T : Set α → β) (T_empty : T ∅ = 0) (h_add : FinMeasAdditive μ T) {ι : Type u_8} (S : ι → Set α) (sι : Finset ι) (hS_meas : ∀ (i : ι), MeasurableSet (S i)) (hSp : ∀ i ∈ sι, μ (S i) ≠ ⊤) (h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)) : T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)

def MeasureTheory.DominatedFinMeasAdditive {α : Type u_1} {β : Type u_7} [SeminormedAddCommGroup β] {x✝ : MeasurableSpace α} (μ : Measure α) (T : Set α → β) (C : ℝ) : Prop

A FinMeasAdditive set function whose norm on every set is less than the measure of the set (up to a multiplicative constant).

Equations

• MeasureTheory.DominatedFinMeasAdditive μ T C = (MeasureTheory.FinMeasAdditive μ T ∧ ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal)

theorem MeasureTheory.DominatedFinMeasAdditive.zero {α : Type u_1} {β : Type u_7} [SeminormedAddCommGroup β] {C : ℝ} {m : MeasurableSpace α} (μ : Measure α) (hC : 0 ≤ C) : DominatedFinMeasAdditive μ 0 C

theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_8} [NormedAddCommGroup β] {T : Set α → β} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s) (hs_zero : μ s = 0) : T s = 0

theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero {α : Type u_1} {β : Type u_8} [NormedAddCommGroup β] {T : Set α → β} {C : ℝ} {x✝ : MeasurableSpace α} (hT : DominatedFinMeasAdditive 0 T C) {s : Set α} (hs : MeasurableSet s) : T s = 0

theorem MeasureTheory.DominatedFinMeasAdditive.add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T T' : Set α → β} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') : DominatedFinMeasAdditive μ (T + T') (C + C')

theorem MeasureTheory.DominatedFinMeasAdditive.smul {α : Type u_1} {𝕜 : Type u_6} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} [NormedField 𝕜] [NormedSpace 𝕜 β] (hT : DominatedFinMeasAdditive μ T C) (c : 𝕜) : DominatedFinMeasAdditive μ (fun (s : Set α) => c • T s) (‖c‖ * C)

theorem MeasureTheory.DominatedFinMeasAdditive.of_measure_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {μ' : Measure α} (h : μ ≤ μ') (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) : DominatedFinMeasAdditive μ' T C

theorem MeasureTheory.DominatedFinMeasAdditive.add_measure_right {α : Type u_1} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {x✝ : MeasurableSpace α} (μ ν : Measure α) (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) : DominatedFinMeasAdditive (μ + ν) T C

theorem MeasureTheory.DominatedFinMeasAdditive.add_measure_left {α : Type u_1} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {x✝ : MeasurableSpace α} (μ ν : Measure α) (hT : DominatedFinMeasAdditive ν T C) (hC : 0 ≤ C) : DominatedFinMeasAdditive (μ + ν) T C

theorem MeasureTheory.DominatedFinMeasAdditive.of_smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {c : ENNReal} (hc_ne_top : c ≠ ⊤) (hT : DominatedFinMeasAdditive (c • μ) T C) : DominatedFinMeasAdditive μ T (c.toReal * C)

theorem MeasureTheory.DominatedFinMeasAdditive.of_measure_le_smul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {μ' : Measure α} {c : ENNReal} (hc : c ≠ ⊤) (h : μ ≤ c • μ') (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) : DominatedFinMeasAdditive μ' T (c.toReal * C)

def MeasureTheory.SimpleFunc.setToSimpleFunc {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {x✝ : MeasurableSpace α} (T : Set α → F →L[ℝ] F') (f : SimpleFunc α F) : F'

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

Equations

• MeasureTheory.SimpleFunc.setToSimpleFunc T f = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x

@[simp]

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} (f : SimpleFunc α F) : setToSimpleFunc 0 f = 0

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero' {α : Type u_1} {E : Type u_2} {F' : Type u_4} [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 : SimpleFunc α E) (hf : Integrable (⇑f) μ) : setToSimpleFunc T f = 0

@[simp]

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero_apply {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') : setToSimpleFunc T 0 = 0

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] [DecidablePred fun (x : F) => x ≠ 0] {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') (f : SimpleFunc α F) : setToSimpleFunc T f = ∑ x ∈ {x ∈ f.range | x ≠ 0}, (T (⇑f ⁻¹' {x})) x

theorem MeasureTheory.SimpleFunc.map_setToSimpleFunc {α : Type u_1} {F : Type u_3} {F' : Type u_4} {G : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] [NormedAddCommGroup G] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → F →L[ℝ] F') (h_add : FinMeasAdditive μ T) {f : SimpleFunc α G} (hf : Integrable (⇑f) μ) {g : G → F} (hg : g 0 = 0) : setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (g x)

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_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_add : FinMeasAdditive μ T) {f g : SimpleFunc α E} (hf : Integrable (⇑f) μ) (hg : Integrable (⇑g) μ) (h : Pairwise fun (x y : E) => T (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0) : setToSimpleFunc T f = setToSimpleFunc T g

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_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 : SimpleFunc α E} (hf : Integrable (⇑f) μ) (h : ⇑f =ᶠ[ae μ] ⇑g) : setToSimpleFunc T f = setToSimpleFunc T g

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_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 : SimpleFunc α E) (hf : Integrable (⇑f) μ) : setToSimpleFunc T f = setToSimpleFunc T' f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add_left {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} (T T' : Set α → F →L[ℝ] F') {f : SimpleFunc α F} : setToSimpleFunc (T + T') f = setToSimpleFunc T f + setToSimpleFunc T' f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_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 : SimpleFunc α E} (hf : Integrable (⇑f) μ) : setToSimpleFunc T'' f = setToSimpleFunc T f + setToSimpleFunc T' f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') (c : ℝ) (f : SimpleFunc α F) : setToSimpleFunc (fun (s : Set α) => c • T s) f = c • setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left' {α : Type u_1} {E : Type u_2} {F' : Type u_4} [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 : SimpleFunc α E} (hf : Integrable (⇑f) μ) : setToSimpleFunc T' f = c • setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_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_add : FinMeasAdditive μ T) {f g : SimpleFunc α E} (hf : Integrable (⇑f) μ) (hg : Integrable (⇑g) μ) : setToSimpleFunc T (f + g) = setToSimpleFunc T f + setToSimpleFunc T g

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_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_add : FinMeasAdditive μ T) {f : SimpleFunc α E} (hf : Integrable (⇑f) μ) : setToSimpleFunc T (-f) = -setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_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_add : FinMeasAdditive μ T) {f g : SimpleFunc α E} (hf : Integrable (⇑f) μ) (hg : Integrable (⇑g) μ) : setToSimpleFunc T (f - g) = setToSimpleFunc T f - setToSimpleFunc T g

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_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_add : FinMeasAdditive μ T) (c : ℝ) {f : SimpleFunc α E} (hf : Integrable (⇑f) μ) : setToSimpleFunc T (c • f) = c • setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {E : Type u_7} [NormedAddCommGroup E] [NormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [NormedSpace 𝕜 F] (T : Set α → E →L[ℝ] F) (h_add : FinMeasAdditive μ T) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (c : 𝕜) {f : SimpleFunc α E} (hf : Integrable (⇑f) μ) : setToSimpleFunc T (c • f) = c • setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace ℝ G''] {m : MeasurableSpace α} (T T' : Set α → F →L[ℝ] G'') (hTT' : ∀ (s : Set α) (x : F), (T s) x ≤ (T' s) x) (f : SimpleFunc α F) : setToSimpleFunc T f ≤ setToSimpleFunc T' f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace ℝ G''] (T T' : Set α → E →L[ℝ] G'') (hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x) (f : SimpleFunc α E) (hf : Integrable (⇑f) μ) : setToSimpleFunc T f ≤ setToSimpleFunc T' f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg {α : Type u_1} {G' : Type u_7} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace ℝ G''] [NormedLatticeAddCommGroup G'] [NormedSpace ℝ G'] {m : MeasurableSpace α} (T : Set α → G' →L[ℝ] G'') (hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x) (f : SimpleFunc α G') (hf : 0 ≤ f) : 0 ≤ setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace ℝ G''] [NormedLatticeAddCommGroup G'] [NormedSpace ℝ G'] (T : Set α → G' →L[ℝ] G'') (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) (f : SimpleFunc α G') (hf : 0 ≤ f) (hfi : Integrable (⇑f) μ) : 0 ≤ setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace ℝ G''] [NormedLatticeAddCommGroup G'] [NormedSpace ℝ G'] {T : Set α → G' →L[ℝ] G''} (h_add : FinMeasAdditive μ T) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) {f g : SimpleFunc α G'} (hfi : Integrable (⇑f) μ) (hgi : Integrable (⇑g) μ) (hfg : f ≤ g) : setToSimpleFunc T f ≤ setToSimpleFunc T g

theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} (T : Set α → F' →L[ℝ] F) (f : SimpleFunc α F') : ‖setToSimpleFunc T f‖ ≤ ∑ x ∈ f.range, ‖T (⇑f ⁻¹' {x})‖ * ‖x‖

theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → F →L[ℝ] F') {C : ℝ} (hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal) (f : SimpleFunc α F) : ‖setToSimpleFunc T f‖ ≤ C * ∑ x ∈ f.range, (μ (⇑f ⁻¹' {x})).toReal * ‖x‖

theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable {α : Type u_1} {E : Type u_2} {F' : Type u_4} [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 * (μ s).toReal) (f : SimpleFunc α E) (hf : Integrable (⇑f) μ) : ‖setToSimpleFunc T f‖ ≤ C * ∑ x ∈ f.range, (μ (⇑f ⁻¹' {x})).toReal * ‖x‖

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_indicator {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] (T : Set α → F →L[ℝ] F') (hT_empty : T ∅ = 0) {m : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) (x : F) : setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s) x

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_const' {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] [Nonempty α] (T : Set α → F →L[ℝ] F') (x : F) {m : MeasurableSpace α} : setToSimpleFunc T (const α x) = (T Set.univ) x

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_const {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] (T : Set α → F →L[ℝ] F') (hT_empty : T ∅ = 0) (x : F) {m : MeasurableSpace α} : setToSimpleFunc T (const α x) = (T Set.univ) x

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, (μ (⇑(Lp.simpleFunc.toSimpleFunc f) ⁻¹' {x})).toReal * ‖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} {F : Type u_3} {𝕜 : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [NormedField 𝕜] {E : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] [NormedSpace 𝕜 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 * (μ s).toReal) (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} [NormedLatticeAddCommGroup 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} [NormedLatticeAddCommGroup 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} [NormedLatticeAddCommGroup G'] [NormedSpace ℝ G'] [NormedLatticeAddCommGroup 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} [NormedLatticeAddCommGroup G'] [NormedSpace ℝ G'] [NormedLatticeAddCommGroup 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 α) [NormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 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‖ ≤ 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} [NormedLatticeAddCommGroup 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} [NormedLatticeAddCommGroup 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} [NormedLatticeAddCommGroup G''] [NormedSpace ℝ G''] [NormedLatticeAddCommGroup 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} [NormedLatticeAddCommGroup G''] [NormedSpace ℝ G''] [NormedLatticeAddCommGroup 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 α} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 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 α} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 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 α} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 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} [NormedLatticeAddCommGroup 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} [NormedLatticeAddCommGroup 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} [NormedLatticeAddCommGroup G''] [NormedSpace ℝ G''] [CompleteSpace G''] [NormedLatticeAddCommGroup 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} [NormedLatticeAddCommGroup G''] [NormedSpace ℝ G''] [CompleteSpace G''] [NormedLatticeAddCommGroup 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 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‖ ≤ (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‖ ≤ 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

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 : ℝ} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 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} [NormedLatticeAddCommGroup 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} [NormedLatticeAddCommGroup 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} [NormedLatticeAddCommGroup G''] [NormedSpace ℝ G''] [CompleteSpace G''] [NormedLatticeAddCommGroup 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} [NormedLatticeAddCommGroup G''] [NormedSpace ℝ G''] [CompleteSpace G''] [NormedLatticeAddCommGroup 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 : α → 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‖ ≤ (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‖ ≤ (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)