# 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, 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 MeasureTheory.Integral.Bochner file and the conditional expectation of an integrable function in MeasureTheory.Function.ConditionalExpectation.

## Main Definitions #

• FinMeasAdditive μ T: the property that T is additive on measurable sets with finite measure. For two such sets, 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} [] :
{x : } → (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
Instances For
theorem MeasureTheory.FinMeasAdditive.zero {α : Type u_1} {m : } {μ : } {β : Type u_7} [] :
theorem MeasureTheory.FinMeasAdditive.add {α : Type u_1} {m : } {μ : } {β : Type u_7} [] {T : Set αβ} {T' : Set αβ} (hT : ) (hT' : ) :
theorem MeasureTheory.FinMeasAdditive.smul {α : Type u_1} {𝕜 : Type u_6} {m : } {μ : } {β : Type u_7} [] {T : Set αβ} [] [] (hT : ) (c : 𝕜) :
MeasureTheory.FinMeasAdditive μ fun (s : Set α) => c T s
theorem MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top {α : Type u_1} {m : } {μ : } {β : Type u_7} [] {T : Set αβ} {μ' : } (h : ∀ (s : Set α), μ s = μ' s = ) (hT : ) :
theorem MeasureTheory.FinMeasAdditive.of_smul_measure {α : Type u_1} {m : } {μ : } {β : Type u_7} [] {T : Set αβ} (c : ENNReal) (hc_ne_top : c ) (hT : ) :
theorem MeasureTheory.FinMeasAdditive.smul_measure {α : Type u_1} {m : } {μ : } {β : Type u_7} [] {T : Set αβ} (c : ENNReal) (hc_ne_zero : c 0) (hT : ) :
theorem MeasureTheory.FinMeasAdditive.smul_measure_iff {α : Type u_1} {m : } {μ : } {β : Type u_7} [] {T : Set αβ} (c : ENNReal) (hc_ne_zero : c 0) (hc_ne_top : c ) :
theorem MeasureTheory.FinMeasAdditive.map_empty_eq_zero {α : Type u_1} {m : } {μ : } {β : Type u_8} [] {T : Set αβ} (hT : ) :
T = 0
theorem MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum {α : Type u_1} {m : } {μ : } {β : Type u_7} [] (T : Set αβ) (T_empty : T = 0) (h_add : ) {ι : Type u_8} (S : ιSet α) (sι : ) (hS_meas : ∀ (i : ι), MeasurableSet (S i)) (hSp : i, μ (S i) ) (h_disj : i, j, i jDisjoint (S i) (S j)) :
T (i, S i) = .sum fun (i : ι) => T (S i)
def MeasureTheory.DominatedFinMeasAdditive {α : Type u_1} {β : Type u_7} :
{x : } → (Set αβ)

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

Equations
Instances For
theorem MeasureTheory.DominatedFinMeasAdditive.zero {α : Type u_1} {β : Type u_7} {C : } {m : } (μ : ) (hC : 0 C) :
theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero {α : Type u_1} {m : } {μ : } {β : Type u_8} {T : Set αβ} {C : } (hT : ) {s : Set α} (hs : ) (hs_zero : μ s = 0) :
T s = 0
theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero {α : Type u_1} {β : Type u_8} {T : Set αβ} {C : } {m : } (hT : ) {s : Set α} (hs : ) :
T s = 0
theorem MeasureTheory.DominatedFinMeasAdditive.add {α : Type u_1} {m : } {μ : } {β : Type u_7} {T : Set αβ} {T' : Set αβ} {C : } {C' : } (hT : ) (hT' : ) :
theorem MeasureTheory.DominatedFinMeasAdditive.smul {α : Type u_1} {𝕜 : Type u_6} {m : } {μ : } {β : Type u_7} {T : Set αβ} {C : } [] [] (hT : ) (c : 𝕜) :
MeasureTheory.DominatedFinMeasAdditive μ (fun (s : Set α) => c T s) (c * C)
theorem MeasureTheory.DominatedFinMeasAdditive.of_measure_le {α : Type u_1} {m : } {μ : } {β : Type u_7} {T : Set αβ} {C : } {μ' : } (h : μ μ') (hT : ) (hC : 0 C) :
theorem MeasureTheory.DominatedFinMeasAdditive.add_measure_right {α : Type u_1} {β : Type u_7} {T : Set αβ} {C : } :
∀ {x : } (μ ν : ), 0 C
theorem MeasureTheory.DominatedFinMeasAdditive.add_measure_left {α : Type u_1} {β : Type u_7} {T : Set αβ} {C : } :
∀ {x : } (μ ν : ), 0 C
theorem MeasureTheory.DominatedFinMeasAdditive.of_smul_measure {α : Type u_1} {m : } {μ : } {β : Type u_7} {T : Set αβ} {C : } (c : ENNReal) (hc_ne_top : c ) (hT : ) :
theorem MeasureTheory.DominatedFinMeasAdditive.of_measure_le_smul {α : Type u_1} {m : } {μ : } {β : Type u_7} {T : Set αβ} {C : } {μ' : } (c : ENNReal) (hc : c ) (h : μ c μ') (hT : ) (hC : 0 C) :
def MeasureTheory.SimpleFunc.setToSimpleFunc {α : Type u_1} {F : Type u_3} {F' : Type u_4} [] [] [] :
{x : } → (Set αF →L[] F')F'

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

Equations
• = f.range.sum fun (x_1 : F) => (T (f ⁻¹' {x_1})) x_1
Instances For
@[simp]
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero {α : Type u_1} {F : Type u_3} {F' : Type u_4} [] [] [] {m : } (f : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero' {α : Type u_1} {E : Type u_2} {F' : Type u_4} [] [] [] {m : } {μ : } {T : Set αE →L[] F'} (h_zero : ∀ (s : Set α), μ s < T s = 0) (f : ) (hf : ) :
@[simp]
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero_apply {α : Type u_1} {F : Type u_3} {F' : Type u_4} [] [] [] {m : } (T : Set αF →L[] F') :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter {α : Type u_1} {F : Type u_3} {F' : Type u_4} [] [] [] {m : } (T : Set αF →L[] F') (f : ) :
= (Finset.filter (fun (x : F) => x 0) f.range).sum fun (x : F) => (T (f ⁻¹' {x})) x
theorem MeasureTheory.SimpleFunc.map_setToSimpleFunc {α : Type u_1} {F : Type u_3} {F' : Type u_4} {G : Type u_5} [] [] [] {m : } {μ : } (T : Set αF →L[] F') (h_add : ) {f : } (hf : ) {g : GF} (hg : g 0 = 0) :
= f.range.sum fun (x : G) => (T (f ⁻¹' {x})) (g x)
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (h_add : ) {f : } {g : } (hf : ) (hg : ) (h : Pairwise fun (x y : E) => T (f ⁻¹' {x} g ⁻¹' {y}) = 0) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (h_zero : ∀ (s : Set α), μ s = 0T s = 0) (h_add : ) {f : } {g : } (hf : ) (h : f =ᶠ[μ.ae] g) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (T' : Set αE →L[] F) (h : ∀ (s : Set α), μ s < T s = T' s) (f : ) (hf : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add_left {α : Type u_1} {F : Type u_3} {F' : Type u_4} [] [] [] {m : } (T : Set αF →L[] F') (T' : Set αF →L[] F') {f : } :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (T' : Set αE →L[] F) (T'' : Set αE →L[] F) (h_add : ∀ (s : Set α), μ s < T'' s = T s + T' s) {f : } (hf : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left {α : Type u_1} {F : Type u_3} {F' : Type u_4} [] [] [] {m : } (T : Set αF →L[] F') (c : ) (f : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left' {α : Type u_1} {E : Type u_2} {F' : Type u_4} [] [] [] {m : } {μ : } (T : Set αE →L[] F') (T' : Set αE →L[] F') (c : ) (h_smul : ∀ (s : Set α), μ s < T' s = c T s) {f : } (hf : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (h_add : ) {f : } {g : } (hf : ) (hg : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_neg {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (h_add : ) {f : } (hf : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (h_add : ) {f : } {g : } (hf : ) (hg : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_real {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (h_add : ) (c : ) {f : } (hf : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_6} [] {m : } {μ : } {E : Type u_7} [] [] [] [] (T : Set αE →L[] F) (h_add : ) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) {f : } (hf : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left {α : Type u_1} {F : Type u_3} [] {G'' : Type u_8} [NormedSpace G''] {m : } (T : Set αF →L[] G'') (T' : Set αF →L[] G'') (hTT' : ∀ (s : Set α) (x : F), (T s) x (T' s) x) (f : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left' {α : Type u_1} {E : Type u_2} [] {m : } {μ : } {G'' : Type u_8} [NormedSpace G''] (T : Set αE →L[] G'') (T' : Set αE →L[] G'') (hTT' : ∀ (s : Set α), μ s < ∀ (x : E), (T s) x (T' s) x) (f : ) (hf : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg {α : Type u_1} {G' : Type u_7} {G'' : Type u_8} [NormedSpace G''] [] {m : } (T : Set αG' →L[] G'') (hT_nonneg : ∀ (s : Set α) (x : G'), 0 x0 (T s) x) (f : ) (hf : 0 f) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg' {α : Type u_1} {m : } {μ : } {G' : Type u_7} {G'' : Type u_8} [NormedSpace G''] [] (T : Set αG' →L[] G'') (hT_nonneg : ∀ (s : Set α), μ s < ∀ (x : G'), 0 x0 (T s) x) (f : ) (hf : 0 f) (hfi : ) :
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono {α : Type u_1} {m : } {μ : } {G' : Type u_7} {G'' : Type u_8} [NormedSpace G''] [] {T : Set αG' →L[] G''} (h_add : ) (hT_nonneg : ∀ (s : Set α), μ s < ∀ (x : G'), 0 x0 (T s) x) {f : } {g : } (hfi : ) (hgi : ) (hfg : f g) :
theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm {α : Type u_1} {F : Type u_3} {F' : Type u_4} [] [] [] {m : } (T : Set αF' →L[] F) (f : ) :
f.range.sum fun (x : F') => T (f ⁻¹' {x}) * x
@[deprecated MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm]
theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_op_norm {α : Type u_1} {F : Type u_3} {F' : Type u_4} [] [] [] {m : } (T : Set αF' →L[] F) (f : ) :
f.range.sum fun (x : F') => T (f ⁻¹' {x}) * x

Alias of MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm.

theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm {α : Type u_1} {F : Type u_3} {F' : Type u_4} [] [] [] {m : } {μ : } (T : Set αF →L[] F') {C : } (hT_norm : ∀ (s : Set α), T s C * (μ s).toReal) (f : ) :
C * f.range.sum fun (x : F) => (μ (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} [] [] [] {m : } {μ : } (T : Set αE →L[] F') {C : } (hT_norm : ∀ (s : Set α), μ s < T s C * (μ s).toReal) (f : ) (hf : ) :
C * f.range.sum fun (x : E) => (μ (f ⁻¹' {x})).toReal * x
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_indicator {α : Type u_1} {F : Type u_3} {F' : Type u_4} [] [] [] (T : Set αF →L[] F') (hT_empty : T = 0) {m : } {s : Set α} (hs : ) (x : F) :
= (T s) x
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_const' {α : Type u_1} {F : Type u_3} {F' : Type u_4} [] [] [] [] (T : Set αF →L[] F') (x : F) {m : } :
= (T Set.univ) x
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_const {α : Type u_1} {F : Type u_3} {F' : Type u_4} [] [] [] (T : Set αF →L[] F') (hT_empty : T = 0) (x : F) {m : } :
= (T Set.univ) x
theorem MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul {α : Type u_1} {G : Type u_5} {m : } {μ : } (f : ()) :
f = .range.sum fun (x : G) => (μ ()).toReal * x
def MeasureTheory.L1.SimpleFunc.setToL1S {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (f : ()) :
F

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

Equations
Instances For
theorem MeasureTheory.L1.SimpleFunc.setToL1S_eq_setToSimpleFunc {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (f : ()) :
@[simp]
theorem MeasureTheory.L1.SimpleFunc.setToL1S_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (f : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} (h_zero : ∀ (s : Set α), μ s < T s = 0) (f : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_congr {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (h_zero : ∀ (s : Set α), μ s = 0T s = 0) (h_add : ) {f : ()} {g : ()} (h : ) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (T' : Set αE →L[] F) (h : ∀ (s : Set α), μ s < T s = T' s) (f : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_congr_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {μ' : } (T : Set αE →L[] F) (h_zero : ∀ (s : Set α), μ s = 0T s = 0) (h_add : ) (hμ : μ.AbsolutelyContinuous μ') (f : ()) (f' : ()) (h : f =ᶠ[μ.ae] 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} [] [] {m : } {μ : } (T : Set αE →L[] F) (T' : Set αE →L[] F) (f : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (T' : Set αE →L[] F) (T'' : Set αE →L[] F) (h_add : ∀ (s : Set α), μ s < T'' s = T s + T' s) (f : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (c : ) (f : ()) :
MeasureTheory.L1.SimpleFunc.setToL1S (fun (s : Set α) => c T s) f =
theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (T' : Set αE →L[] F) (c : ) (h_smul : ∀ (s : Set α), μ s < T' s = c T s) (f : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_add {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (h_zero : ∀ (s : Set α), μ s = 0T s = 0) (h_add : ) (f : ()) (g : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_neg {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} (h_zero : ∀ (s : Set α), μ s = 0T s = 0) (h_add : ) (f : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} (h_zero : ∀ (s : Set α), μ s = 0T s = 0) (h_add : ) (f : ()) (g : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul_real {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) (h_zero : ∀ (s : Set α), μ s = 0T s = 0) (h_add : ) (c : ) (f : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_6} [] {m : } {μ : } [] {E : Type u_7} [] [] [] (T : Set αE →L[] F) (h_zero : ∀ (s : Set α), μ s = 0T s = 0) (h_add : ) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) (f : ()) :
theorem MeasureTheory.L1.SimpleFunc.norm_setToL1S_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } (T : Set αE →L[] F) {C : } (hT_norm : ∀ (s : Set α), μ s < T s C * (μ s).toReal) (f : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_indicatorConst {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} {s : Set α} (h_zero : ∀ (s : Set α), μ s = 0T s = 0) (h_add : ) (hs : ) (hμs : μ s < ) (x : E) :
= (T s) x
theorem MeasureTheory.L1.SimpleFunc.setToL1S_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} (h_zero : ∀ (s : Set α), μ s = 0T s = 0) (h_add : ) (x : E) :
= (T Set.univ) x
theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono_left {α : Type u_1} {E : Type u_2} [] {m : } {μ : } {G'' : Type u_7} [NormedSpace G''] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} (hTT' : ∀ (s : Set α) (x : E), (T s) x (T' s) x) (f : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono_left' {α : Type u_1} {E : Type u_2} [] {m : } {μ : } {G'' : Type u_7} [NormedSpace G''] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} (hTT' : ∀ (s : Set α), μ s < ∀ (x : E), (T s) x (T' s) x) (f : ()) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_nonneg {α : Type u_1} {m : } {μ : } {G'' : Type u_7} {G' : Type u_8} [] [NormedSpace G''] {T : Set αG'' →L[] G'} (h_zero : ∀ (s : Set α), μ s = 0T s = 0) (h_add : ) (hT_nonneg : ∀ (s : Set α), μ s < ∀ (x : G''), 0 x0 (T s) x) {f : ()} (hf : 0 f) :
theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono {α : Type u_1} {m : } {μ : } {G'' : Type u_7} {G' : Type u_8} [] [NormedSpace G''] {T : Set αG'' →L[] G'} (h_zero : ∀ (s : Set α), μ s = 0T s = 0) (h_add : ) (hT_nonneg : ∀ (s : Set α), μ s < ∀ (x : G''), 0 x0 (T s) x) {f : ()} {g : ()} (hfg : f g) :
def MeasureTheory.L1.SimpleFunc.setToL1SCLM' (α : Type u_1) (E : Type u_2) {F : Type u_3} (𝕜 : Type u_6) [] [] {m : } (μ : ) [] [] [] {T : Set αE →L[] F} {C : } (hT : ) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) :
() →L[𝕜] F

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

Equations
Instances For
def MeasureTheory.L1.SimpleFunc.setToL1SCLM (α : Type u_1) (E : Type u_2) {F : Type u_3} [] [] {m : } (μ : ) {T : Set αE →L[] F} {C : } (hT : ) :
() →L[] F

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

Equations
• = { toFun := , map_add' := , map_smul' := }.mkContinuous C
Instances For
@[simp]
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {C : } (hT : ) (f : ()) :
() f = 0
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} {C : } (hT : ) (h_zero : ∀ (s : Set α), μ s < T s = 0) (f : ()) :
() f = 0
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : ) (hT' : ) (h : T = T') (f : ()) :
() f = () f
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : ) (hT' : ) (h : ∀ (s : Set α), μ s < T s = T' s) (f : ()) :
() f = () f
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} {C : } {C' : } {μ' : } (hT : ) (hT' : ) (hμ : μ.AbsolutelyContinuous μ') (f : ()) (f' : ()) (h : f =ᶠ[μ.ae] f') :
() f = () f'
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : ) (hT' : ) (f : ()) :
() f = () f + () f
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} {T' : Set αE →L[] F} {T'' : Set αE →L[] F} {C : } {C' : } {C'' : } (hT : ) (hT' : ) (hT'' : ) (h_add : ∀ (s : Set α), μ s < T'' s = T s + T' s) (f : ()) :
() f = () f + () f
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} {C : } (c : ) (hT : ) (f : ()) :
() f = c () f
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (c : ) (hT : ) (hT' : ) (h_smul : ∀ (s : Set α), μ s < T' s = c T s) (f : ()) :
() f = c () f
theorem MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} {C : } (hT : ) (hC : 0 C) :
theorem MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} {C : } (hT : ) :
max C 0
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } {T : Set αE →L[] F} {C : } (hT : ) (x : E) :
() = (T Set.univ) x
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left {α : Type u_1} {E : Type u_2} [] {m : } {μ : } {G'' : Type u_8} [NormedSpace G''] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} {C : } {C' : } (hT : ) (hT' : ) (hTT' : ∀ (s : Set α) (x : E), (T s) x (T' s) x) (f : ()) :
() f () f
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left' {α : Type u_1} {E : Type u_2} [] {m : } {μ : } {G'' : Type u_8} [NormedSpace G''] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} {C : } {C' : } (hT : ) (hT' : ) (hTT' : ∀ (s : Set α), μ s < ∀ (x : E), (T s) x (T' s) x) (f : ()) :
() f () f
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg {α : Type u_1} {m : } {μ : } {G' : Type u_7} {G'' : Type u_8} [NormedSpace G''] [] {T : Set αG' →L[] G''} {C : } (hT : ) (hT_nonneg : ∀ (s : Set α), μ s < ∀ (x : G'), 0 x0 (T s) x) {f : ()} (hf : 0 f) :
0 () f
theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono {α : Type u_1} {m : } {μ : } {G' : Type u_7} {G'' : Type u_8} [NormedSpace G''] [] {T : Set αG' →L[] G''} {C : } (hT : ) (hT_nonneg : ∀ (s : Set α), μ s < ∀ (x : G'), 0 x0 (T s) x) {f : ()} {g : ()} (hfg : f g) :
() f () g
def MeasureTheory.L1.setToL1' {α : Type u_1} {E : Type u_2} {F : Type u_3} (𝕜 : Type u_6) [] [] {m : } {μ : } [] [] [] {T : Set αE →L[] F} {C : } (hT : ) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) :
() →L[𝕜] F

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

Equations
Instances For
def MeasureTheory.L1.setToL1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) :
() →L[] F

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

Equations
• = ().extend
Instances For
theorem MeasureTheory.L1.setToL1_eq_setToL1SCLM {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (f : ()) :
f = () f
theorem MeasureTheory.L1.setToL1_eq_setToL1' {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [] [] {m : } {μ : } [] [] [] {T : Set αE →L[] F} {C : } (hT : ) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) (f : ()) :
f = (MeasureTheory.L1.setToL1' 𝕜 hT h_smul) f
@[simp]
theorem MeasureTheory.L1.setToL1_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {C : } (hT : ) (f : ()) :
f = 0
theorem MeasureTheory.L1.setToL1_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (h_zero : ∀ (s : Set α), μ s < T s = 0) (f : ()) :
f = 0
theorem MeasureTheory.L1.setToL1_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] (T : Set αE →L[] F) (T' : Set αE →L[] F) {C : } {C' : } (hT : ) (hT' : ) (h : T = T') (f : ()) :
f = () f
theorem MeasureTheory.L1.setToL1_congr_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] (T : Set αE →L[] F) (T' : Set αE →L[] F) {C : } {C' : } (hT : ) (hT' : ) (h : ∀ (s : Set α), μ s < T s = T' s) (f : ()) :
f = () f
theorem MeasureTheory.L1.setToL1_add_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : ) (hT' : ) (f : ()) :
= f + () f
theorem MeasureTheory.L1.setToL1_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {T' : Set αE →L[] F} {T'' : Set αE →L[] F} {C : } {C' : } {C'' : } (hT : ) (hT' : ) (hT'' : ) (h_add : ∀ (s : Set α), μ s < T'' s = T s + T' s) (f : ()) :
() f = f + () f
theorem MeasureTheory.L1.setToL1_smul_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (c : ) (f : ()) :
= c f
theorem MeasureTheory.L1.setToL1_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : ) (hT' : ) (c : ) (h_smul : ∀ (s : Set α), μ s < T' s = c T s) (f : ()) :
() f = c f
theorem MeasureTheory.L1.setToL1_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [] [] {m : } {μ : } [] [] [] {T : Set αE →L[] F} {C : } (hT : ) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) (f : ()) :
(c f) = c f
theorem MeasureTheory.L1.setToL1_simpleFunc_indicatorConst {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) {s : Set α} (hs : ) (hμs : μ s < ) (x : E) :
() = (T s) x
theorem MeasureTheory.L1.setToL1_indicatorConstLp {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) {s : Set α} (hs : ) (hμs : μ s ) (x : E) :
() = (T s) x
theorem MeasureTheory.L1.setToL1_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (x : E) :
() = (T Set.univ) x
theorem MeasureTheory.L1.setToL1_mono_left' {α : Type u_1} {E : Type u_2} [] {m : } {μ : } {G'' : Type u_8} [NormedSpace G''] [] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} {C : } {C' : } (hT : ) (hT' : ) (hTT' : ∀ (s : Set α), μ s < ∀ (x : E), (T s) x (T' s) x) (f : ()) :
f () f
theorem MeasureTheory.L1.setToL1_mono_left {α : Type u_1} {E : Type u_2} [] {m : } {μ : } {G'' : Type u_8} [NormedSpace G''] [] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} {C : } {C' : } (hT : ) (hT' : ) (hTT' : ∀ (s : Set α) (x : E), (T s) x (T' s) x) (f : ()) :
f () f
theorem MeasureTheory.L1.setToL1_nonneg {α : Type u_1} {m : } {μ : } {G' : Type u_7} {G'' : Type u_8} [NormedSpace G''] [] [] {T : Set αG' →L[] G''} {C : } (hT : ) (hT_nonneg : ∀ (s : Set α), μ s < ∀ (x : G'), 0 x0 (T s) x) {f : (MeasureTheory.Lp G' 1 μ)} (hf : 0 f) :
0 f
theorem MeasureTheory.L1.setToL1_mono {α : Type u_1} {m : } {μ : } {G' : Type u_7} {G'' : Type u_8} [NormedSpace G''] [] [] {T : Set αG' →L[] G''} {C : } (hT : ) (hT_nonneg : ∀ (s : Set α), μ s < ∀ (x : G'), 0 x0 (T s) x) {f : (MeasureTheory.Lp G' 1 μ)} {g : (MeasureTheory.Lp G' 1 μ)} (hfg : f g) :
f g
theorem MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) :
theorem MeasureTheory.L1.norm_setToL1_le_mul_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (hC : 0 C) (f : ()) :
theorem MeasureTheory.L1.norm_setToL1_le_mul_norm' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (f : ()) :
theorem MeasureTheory.L1.norm_setToL1_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (hC : 0 C) :
theorem MeasureTheory.L1.norm_setToL1_le' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) :
theorem MeasureTheory.L1.setToL1_lipschitz {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) :
LipschitzWith C.toNNReal
theorem MeasureTheory.L1.tendsto_setToL1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (f : ()) {ι : Type u_7} (fs : ι()) {l : } (hfs : Filter.Tendsto fs l (nhds f)) :
Filter.Tendsto (fun (i : ι) => (fs i)) l (nhds ( 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} [] [] {m : } (μ : ) [] (T : Set αE →L[] F) {C : } (hT : ) (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
• = if hf : then else 0
Instances For
theorem MeasureTheory.setToFun_eq {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {f : αE} (hT : ) (hf : ) :
=
theorem MeasureTheory.L1.setToFun_eq_setToL1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (f : ()) :
MeasureTheory.setToFun μ T hT f = f
theorem MeasureTheory.setToFun_undef {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {f : αE} (hT : ) (hf : ) :
= 0
theorem MeasureTheory.setToFun_non_aEStronglyMeasurable {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {f : αE} (hT : ) (hf : ) :
= 0
theorem MeasureTheory.setToFun_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : ) (hT' : ) (h : T = T') (f : αE) :
theorem MeasureTheory.setToFun_congr_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : ) (hT' : ) (h : ∀ (s : Set α), μ s < T s = T' s) (f : αE) :
theorem MeasureTheory.setToFun_add_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : ) (hT' : ) (f : αE) :
MeasureTheory.setToFun μ (T + T') f = + MeasureTheory.setToFun μ T' hT' f
theorem MeasureTheory.setToFun_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {T' : Set αE →L[] F} {T'' : Set αE →L[] F} {C : } {C' : } {C'' : } (hT : ) (hT' : ) (hT'' : ) (h_add : ∀ (s : Set α), μ s < T'' s = T s + T' s) (f : αE) :
theorem MeasureTheory.setToFun_smul_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (c : ) (f : αE) :
MeasureTheory.setToFun μ (fun (s : Set α) => c T s) f = c
theorem MeasureTheory.setToFun_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : ) (hT' : ) (c : ) (h_smul : ∀ (s : Set α), μ s < T' s = c T s) (f : αE) :
@[simp]
theorem MeasureTheory.setToFun_zero {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) :
= 0
@[simp]
theorem MeasureTheory.setToFun_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {C : } {f : αE} {hT : } :
= 0
theorem MeasureTheory.setToFun_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {f : αE} (hT : ) (h_zero : ∀ (s : Set α), μ s < T s = 0) :
= 0
theorem MeasureTheory.setToFun_add {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {f : αE} {g : αE} (hT : ) (hf : ) (hg : ) :
MeasureTheory.setToFun μ T hT (f + g) = +
theorem MeasureTheory.setToFun_finset_sum' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) {ι : Type u_7} (s : ) {f : ιαE} (hf : is, MeasureTheory.Integrable (f i) μ) :
MeasureTheory.setToFun μ T hT (s.sum fun (i : ι) => f i) = s.sum fun (i : ι) => MeasureTheory.setToFun μ T hT (f i)
theorem MeasureTheory.setToFun_finset_sum {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) {ι : Type u_7} (s : ) {f : ιαE} (hf : is, MeasureTheory.Integrable (f i) μ) :
(MeasureTheory.setToFun μ T hT fun (a : α) => s.sum fun (i : ι) => f i a) = s.sum fun (i : ι) => MeasureTheory.setToFun μ T hT (f i)
theorem MeasureTheory.setToFun_neg {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (f : αE) :
theorem MeasureTheory.setToFun_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {f : αE} {g : αE} (hT : ) (hf : ) (hg : ) :
MeasureTheory.setToFun μ T hT (f - g) = -
theorem MeasureTheory.setToFun_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } [] [] (hT : ) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) (f : αE) :
MeasureTheory.setToFun μ T hT (c f) = c
theorem MeasureTheory.setToFun_congr_ae {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {f : αE} {g : αE} (hT : ) (h : f =ᶠ[μ.ae] g) :
=
theorem MeasureTheory.setToFun_measure_zero {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {f : αE} (hT : ) (h : μ = 0) :
= 0
theorem MeasureTheory.setToFun_measure_zero' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {f : αE} (hT : ) (h : ∀ (s : Set α), μ s < μ s = 0) :
= 0
theorem MeasureTheory.setToFun_toL1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {f : αE} (hT : ) (hf : ) :
MeasureTheory.setToFun μ T hT =
theorem MeasureTheory.setToFun_indicator_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) {s : Set α} (hs : ) (hμs : μ s ) (x : E) :
MeasureTheory.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} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (x : E) :
(MeasureTheory.setToFun μ T hT fun (x_1 : α) => x) = (T Set.univ) x
theorem MeasureTheory.setToFun_mono_left' {α : Type u_1} {E : Type u_2} [] {m : } {μ : } {G'' : Type u_8} [NormedSpace G''] [] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} {C : } {C' : } (hT : ) (hT' : ) (hTT' : ∀ (s : Set α), μ s < ∀ (x : E), (T s) x (T' s) x) (f : αE) :
theorem MeasureTheory.setToFun_mono_left {α : Type u_1} {E : Type u_2} [] {m : } {μ : } {G'' : Type u_8} [NormedSpace G''] [] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} {C : } {C' : } (hT : ) (hT' : ) (hTT' : ∀ (s : Set α) (x : E), (T s) x (T' s) x) (f : ()) :
MeasureTheory.setToFun μ T hT f MeasureTheory.setToFun μ T' hT' f
theorem MeasureTheory.setToFun_nonneg {α : Type u_1} {m : } {μ : } {G' : Type u_7} {G'' : Type u_8} [NormedSpace G''] [] [] {T : Set αG' →L[] G''} {C : } (hT : ) (hT_nonneg : ∀ (s : Set α), μ s < ∀ (x : G'), 0 x0 (T s) x) {f : αG'} (hf : 0 ≤ᶠ[μ.ae] f) :
0
theorem MeasureTheory.setToFun_mono {α : Type u_1} {m : } {μ : } {G' : Type u_7} {G'' : Type u_8} [NormedSpace G''] [] [] {T : Set αG' →L[] G''} {C : } (hT : ) (hT_nonneg : ∀ (s : Set α), μ s < ∀ (x : G'), 0 x0 (T s) x) {f : αG'} {g : αG'} (hf : ) (hg : ) (hfg : f ≤ᶠ[μ.ae] g) :
theorem MeasureTheory.continuous_setToFun {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) :
Continuous fun (f : ()) => MeasureTheory.setToFun μ T hT f
theorem MeasureTheory.tendsto_setToFun_of_L1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) {ι : Type u_7} (f : αE) (hfi : ) {fs : ιαE} {l : } (hfsi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (fs i) μ) (hfs : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α), fs i x - f x‖₊μ) l (nhds 0)) :
Filter.Tendsto (fun (i : ι) => MeasureTheory.setToFun μ T hT (fs i)) l (nhds ())

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} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) [] [] {f : αE} {s : Set E} (hfi : ) (hfm : ) (hs : ∀ᵐ (x : α) ∂μ, f x ) {y₀ : E} (h₀ : y₀ s) (h₀i : MeasureTheory.Integrable (fun (x : α) => y₀) μ) :
Filter.Tendsto (fun (n : ) => MeasureTheory.setToFun μ T hT (MeasureTheory.SimpleFunc.approxOn f hfm s y₀ h₀ n)) Filter.atTop (nhds ())
theorem MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) [] [] {f : αE} (fmeas : ) (hf : ) (s : Set E) (hs : {0} s) :
Filter.Tendsto (fun (n : ) => MeasureTheory.setToFun μ T hT (MeasureTheory.SimpleFunc.approxOn f fmeas s 0 n)) Filter.atTop (nhds ())
theorem MeasureTheory.continuous_L1_toL1 {α : Type u_1} {G : Type u_5} {m : } {μ : } {μ' : } (c' : ENNReal) (hc' : c' ) (hμ'_le : μ' c' μ) :
Continuous fun (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} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {C' : } {μ' : } (c' : ENNReal) (hc' : c' ) (hμ'_le : μ' c' μ) (hT : ) (hT' : ) (f : αE) (hfμ : ) :
theorem MeasureTheory.setToFun_congr_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {C' : } {μ' : } (c : ENNReal) (c' : ENNReal) (hc : c ) (hc' : c' ) (hμ_le : μ c μ') (hμ'_le : μ' c' μ) (hT : ) (hT' : ) (f : αE) :
theorem MeasureTheory.setToFun_congr_measure_of_add_right {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {C' : } {μ' : } (hT_add : MeasureTheory.DominatedFinMeasAdditive (μ + μ') T C') (hT : ) (f : αE) (hf : MeasureTheory.Integrable f (μ + μ')) :
MeasureTheory.setToFun (μ + μ') T hT_add f =
theorem MeasureTheory.setToFun_congr_measure_of_add_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {C' : } {μ' : } (hT_add : MeasureTheory.DominatedFinMeasAdditive (μ + μ') T C') (hT : ) (f : αE) (hf : MeasureTheory.Integrable f (μ + μ')) :
MeasureTheory.setToFun (μ + μ') T hT_add f = MeasureTheory.setToFun μ' T hT f
theorem MeasureTheory.setToFun_top_smul_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (f : αE) :
theorem MeasureTheory.setToFun_congr_smul_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {C' : } (c : ENNReal) (hc_ne_top : c ) (hT : ) (hT_smul : ) (f : αE) :
= MeasureTheory.setToFun (c μ) T hT_smul f
theorem MeasureTheory.norm_setToFun_le_mul_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (f : ()) (hC : 0 C) :
theorem MeasureTheory.norm_setToFun_le_mul_norm' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) (f : ()) :
theorem MeasureTheory.norm_setToFun_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {f : αE} (hT : ) (hf : ) (hC : 0 C) :
theorem MeasureTheory.norm_setToFun_le' {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {f : αE} (hT : ) (hf : ) :
theorem MeasureTheory.tendsto_setToFun_of_dominated_convergence {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } (hT : ) {fs : αE} {f : αE} (bound : α) (fs_measurable : ∀ (n : ), ) (bound_integrable : MeasureTheory.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 : ) => MeasureTheory.setToFun μ T hT (fs n)) Filter.atTop (nhds ())

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

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} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {X : Type u_7} [] (hT : ) {fs : XαE} {x₀ : X} {bound : α} {s : Set X} (hfs_meas : ∀ᶠ (x : X) in nhdsWithin x₀ s, ) (h_bound : ∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (a : α) ∂μ, fs x a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun (x : X) => fs x a) s x₀) :
ContinuousWithinAt (fun (x : X) => MeasureTheory.setToFun μ T hT (fs x)) s x₀
theorem MeasureTheory.continuousAt_setToFun_of_dominated {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {X : Type u_7} [] (hT : ) {fs : XαE} {x₀ : X} {bound : α} (hfs_meas : ∀ᶠ (x : X) in nhds x₀, ) (h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (a : α) ∂μ, fs x a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun (x : X) => fs x a) x₀) :
ContinuousAt (fun (x : X) => MeasureTheory.setToFun μ T hT (fs x)) x₀
theorem MeasureTheory.continuousOn_setToFun_of_dominated {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {X : Type u_7} [] (hT : ) {fs : XαE} {bound : α} {s : Set X} (hfs_meas : xs, ) (h_bound : xs, ∀ᵐ (a : α) ∂μ, fs x a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun (x : X) => fs x a) s) :
ContinuousOn (fun (x : X) => MeasureTheory.setToFun μ T hT (fs x)) s
theorem MeasureTheory.continuous_setToFun_of_dominated {α : Type u_1} {E : Type u_2} {F : Type u_3} [] [] {m : } {μ : } [] {T : Set αE →L[] F} {C : } {X : Type u_7} [] (hT : ) {fs : XαE} {bound : α} (hfs_meas : ∀ (x : X), ) (h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, fs x a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, Continuous fun (x : X) => fs x a) :
Continuous fun (x : X) => MeasureTheory.setToFun μ T hT (fs x)