mathlib documentation

measure_theory.integral.set_to_l1

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 measure_theory.integral.bochner file and the conditional expectation of an integrable function in measure_theory.function.conditional_expectation.

Main Definitions #

Properties #

For most properties of set_to_fun, 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, measurable_set s → μ s < ∞ → T s = T' s.

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

Linearity:

Other:

If the space is a normed_lattice_add_comm_group and T is such that 0 ≤ T s x for 0 ≤ x, we also prove order-related properties:

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 measure_theory.fin_meas_additive {α : Type u_1} {β : Type u_2} [add_monoid β] {m : measurable_space α} (μ : measure_theory.measure α) (T : set α β) :
Prop

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

Equations
theorem measure_theory.fin_meas_additive.smul {α : Type u_1} {𝕜 : Type u_6} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} [add_comm_monoid β] {T : set α β} [monoid 𝕜] [distrib_mul_action 𝕜 β] (hT : measure_theory.fin_meas_additive μ T) (c : 𝕜) :
measure_theory.fin_meas_additive μ (λ (s : set α), c T s)
theorem measure_theory.fin_meas_additive.smul_measure {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} [add_comm_monoid β] {T : set α β} (c : ennreal) (hc_ne_zero : c 0) (hT : measure_theory.fin_meas_additive μ T) :
theorem measure_theory.fin_meas_additive.smul_measure_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} [add_comm_monoid β] {T : set α β} (c : ennreal) (hc_ne_zero : c 0) (hc_ne_top : c ) :
theorem measure_theory.fin_meas_additive.map_Union_fin_meas_set_eq_sum {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} [add_comm_monoid β] (T : set α β) (T_empty : T = 0) (h_add : measure_theory.fin_meas_additive μ T) {ι : Type u_2} (S : ι set α) (sι : finset ι) (hS_meas : (i : ι), measurable_set (S i)) (hSp : (i : ι), i μ (S i) ) (h_disj : (i : ι), i (j : ι), j i j disjoint (S i) (S j)) :
T ( (i : ι) (H : i sι), S i) = sι.sum (λ (i : ι), T (S i))
def measure_theory.dominated_fin_meas_additive {α : Type u_1} {β : Type u_2} [seminormed_add_comm_group β] {m : measurable_space α} (μ : measure_theory.measure α) (T : set α β) (C : ) :
Prop

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

Equations
theorem measure_theory.dominated_fin_meas_additive.eq_zero_of_measure_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [normed_add_comm_group β] {T : set α β} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) {s : set α} (hs : measurable_set s) (hs_zero : μ s = 0) :
T s = 0
theorem measure_theory.dominated_fin_meas_additive.eq_zero {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {T : set α β} {C : } {m : measurable_space α} (hT : measure_theory.dominated_fin_meas_additive 0 T C) {s : set α} (hs : measurable_set s) :
T s = 0
theorem measure_theory.dominated_fin_meas_additive.smul {α : Type u_1} {𝕜 : Type u_6} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} [seminormed_add_comm_group β] {T : set α β} {C : } [normed_field 𝕜] [normed_space 𝕜 β] (hT : measure_theory.dominated_fin_meas_additive μ T C) (c : 𝕜) :
noncomputable def measure_theory.simple_func.set_to_simple_func {α : Type u_1} {F : Type u_3} {F' : Type u_4} [normed_add_comm_group F] [normed_space F] [normed_add_comm_group F'] [normed_space F'] {m : measurable_space α} (T : set α (F →L[] F')) (f : measure_theory.simple_func α F) :
F'

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

Equations
theorem measure_theory.simple_func.set_to_simple_func_nonneg {α : Type u_1} {G' : Type u_7} {G'' : Type u_8} [normed_lattice_add_comm_group G''] [normed_space G''] [normed_lattice_add_comm_group G'] [normed_space G'] {m : measurable_space α} (T : set α (G' →L[] G'')) (hT_nonneg : (s : set α) (x : G'), 0 x 0 (T s) x) (f : measure_theory.simple_func α G') (hf : 0 f) :

set_to_L1s 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 measure_theory.L1.simple_func.set_to_L1s_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_6} [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space E] [normed_space 𝕜 E] [normed_space 𝕜 F] (T : set α (E →L[] F)) (h_zero : (s : set α), measurable_set s μ s = 0 T s = 0) (h_add : measure_theory.fin_meas_additive μ T) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) (f : (measure_theory.Lp.simple_func E 1 μ)) :
theorem measure_theory.L1.simple_func.set_to_L1s_nonneg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_7} {G' : Type u_8} [normed_lattice_add_comm_group G'] [normed_space G'] [normed_lattice_add_comm_group G''] [normed_space G''] {T : set α (G'' →L[] G')} (h_zero : (s : set α), measurable_set s μ s = 0 T s = 0) (h_add : measure_theory.fin_meas_additive μ T) (hT_nonneg : (s : set α), measurable_set s μ s < (x : G''), 0 x 0 (T s) x) {f : (measure_theory.Lp.simple_func G'' 1 μ)} (hf : 0 f) :
theorem measure_theory.L1.simple_func.set_to_L1s_mono {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_7} {G' : Type u_8} [normed_lattice_add_comm_group G'] [normed_space G'] [normed_lattice_add_comm_group G''] [normed_space G''] {T : set α (G'' →L[] G')} (h_zero : (s : set α), measurable_set s μ s = 0 T s = 0) (h_add : measure_theory.fin_meas_additive μ T) (hT_nonneg : (s : set α), measurable_set s μ s < (x : G''), 0 x 0 (T s) x) {f g : (measure_theory.Lp.simple_func G'' 1 μ)} (hfg : f g) :
noncomputable def measure_theory.L1.simple_func.set_to_L1s_clm' (α : Type u_1) (E : Type u_2) {F : Type u_3} (𝕜 : Type u_6) [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} (μ : measure_theory.measure α) [normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] {T : set α (E →L[] F)} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) :

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

Equations

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

Equations
noncomputable def measure_theory.L1.set_to_L1' {α : Type u_1} {E : Type u_2} {F : Type u_3} (𝕜 : Type u_6) [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [complete_space F] {T : set α (E →L[] F)} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) :

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

Equations

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

Equations
theorem measure_theory.L1.set_to_L1_eq_set_to_L1' {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [complete_space F] {T : set α (E →L[] F)} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) (f : (measure_theory.Lp E 1 μ)) :
theorem measure_theory.L1.set_to_L1_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [complete_space F] {T : set α (E →L[] F)} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) (f : (measure_theory.Lp E 1 μ)) :
theorem measure_theory.L1.set_to_L1_nonneg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {G' : Type u_7} {G'' : Type u_8} [normed_lattice_add_comm_group G''] [normed_space G''] [complete_space G''] [normed_lattice_add_comm_group G'] [normed_space G'] {T : set α (G' →L[] G'')} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (hT_nonneg : (s : set α), measurable_set s μ s < (x : G'), 0 x 0 (T s) x) {f : (measure_theory.Lp G' 1 μ)} (hf : 0 f) :
theorem measure_theory.L1.set_to_L1_mono {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {G' : Type u_7} {G'' : Type u_8} [normed_lattice_add_comm_group G''] [normed_space G''] [complete_space G''] [normed_lattice_add_comm_group G'] [normed_space G'] {T : set α (G' →L[] G'')} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (hT_nonneg : (s : set α), measurable_set s μ s < (x : G'), 0 x 0 (T s) x) {f g : (measure_theory.Lp G' 1 μ)} (hfg : f g) :
theorem measure_theory.L1.tendsto_set_to_L1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [complete_space F] {T : set α (E →L[] F)} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (f : (measure_theory.Lp E 1 μ)) {ι : Type u_4} (fs : ι (measure_theory.Lp E 1 μ)) {l : filter ι} (hfs : filter.tendsto fs l (nhds f)) :

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

noncomputable def measure_theory.set_to_fun {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} (μ : measure_theory.measure α) [complete_space F] (T : set α (E →L[] F)) {C : } (hT : measure_theory.dominated_fin_meas_additive μ 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
theorem measure_theory.set_to_fun_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [complete_space F] {T T' T'' : set α (E →L[] F)} {C C' C'' : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (hT' : measure_theory.dominated_fin_meas_additive μ T' C') (hT'' : measure_theory.dominated_fin_meas_additive μ T'' C'') (h_add : (s : set α), measurable_set s μ s < T'' s = T s + T' s) (f : α E) :
theorem measure_theory.set_to_fun_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [complete_space F] {T T' : set α (E →L[] F)} {C C' : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (hT' : measure_theory.dominated_fin_meas_additive μ T' C') (c : ) (h_smul : (s : set α), measurable_set s μ s < T' s = c T s) (f : α E) :
theorem measure_theory.set_to_fun_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [complete_space F] {T : set α (E →L[] F)} {C : } {f : α E} (hT : measure_theory.dominated_fin_meas_additive μ T C) (h_zero : (s : set α), measurable_set s μ s < T s = 0) :
theorem measure_theory.set_to_fun_finset_sum' {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [complete_space F] {T : set α (E →L[] F)} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) {ι : Type u_4} (s : finset ι) {f : ι α E} (hf : (i : ι), i s measure_theory.integrable (f i) μ) :
measure_theory.set_to_fun μ T hT (s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), measure_theory.set_to_fun μ T hT (f i))
theorem measure_theory.set_to_fun_finset_sum {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [complete_space F] {T : set α (E →L[] F)} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) {ι : Type u_4} (s : finset ι) {f : ι α E} (hf : (i : ι), i s measure_theory.integrable (f i) μ) :
measure_theory.set_to_fun μ T hT (λ (a : α), s.sum (λ (i : ι), f i a)) = s.sum (λ (i : ι), measure_theory.set_to_fun μ T hT (f i))
theorem measure_theory.set_to_fun_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [complete_space F] {T : set α (E →L[] F)} {C : } [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (hT : measure_theory.dominated_fin_meas_additive μ T C) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) (f : α E) :
theorem measure_theory.set_to_fun_indicator_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [complete_space F] {T : set α (E →L[] F)} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) {s : set α} (hs : measurable_set s) (hμs : μ s ) (x : E) :
measure_theory.set_to_fun μ T hT (s.indicator (λ (_x : α), x)) = (T s) x
theorem measure_theory.set_to_fun_mono_left' {α : Type u_1} {E : Type u_2} [normed_add_comm_group E] [normed_space E] {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_8} [normed_lattice_add_comm_group G''] [normed_space G''] [complete_space G''] {T T' : set α (E →L[] G'')} {C C' : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (hT' : measure_theory.dominated_fin_meas_additive μ T' C') (hTT' : (s : set α), measurable_set s μ s < (x : E), (T s) x (T' s) x) (f : α E) :
theorem measure_theory.set_to_fun_mono_left {α : Type u_1} {E : Type u_2} [normed_add_comm_group E] [normed_space E] {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_8} [normed_lattice_add_comm_group G''] [normed_space G''] [complete_space G''] {T T' : set α (E →L[] G'')} {C C' : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (hT' : measure_theory.dominated_fin_meas_additive μ T' C') (hTT' : (s : set α) (x : E), (T s) x (T' s) x) (f : (measure_theory.Lp E 1 μ)) :
theorem measure_theory.set_to_fun_nonneg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {G' : Type u_7} {G'' : Type u_8} [normed_lattice_add_comm_group G''] [normed_space G''] [complete_space G''] [normed_lattice_add_comm_group G'] [normed_space G'] {T : set α (G' →L[] G'')} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (hT_nonneg : (s : set α), measurable_set s μ s < (x : G'), 0 x 0 (T s) x) {f : α G'} (hf : 0 ≤ᵐ[μ] f) :
theorem measure_theory.set_to_fun_mono {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {G' : Type u_7} {G'' : Type u_8} [normed_lattice_add_comm_group G''] [normed_space G''] [complete_space G''] [normed_lattice_add_comm_group G'] [normed_space G'] {T : set α (G' →L[] G'')} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (hT_nonneg : (s : set α), measurable_set s μ s < (x : G'), 0 x 0 (T s) x) {f g : α G'} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) (hfg : f ≤ᵐ[μ] g) :
theorem measure_theory.tendsto_set_to_fun_of_L1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [complete_space F] {T : set α (E →L[] F)} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) {ι : Type u_4} (f : α E) (hfi : measure_theory.integrable f μ) {fs : ι α E} {l : filter ι} (hfsi : ∀ᶠ (i : ι) in l, measure_theory.integrable (fs i) μ) (hfs : filter.tendsto (λ (i : ι), ∫⁻ (x : α), fs i x - f x‖₊ μ) l (nhds 0)) :
filter.tendsto (λ (i : ι), measure_theory.set_to_fun μ T hT (fs i)) l (nhds (measure_theory.set_to_fun μ T hT f))

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

theorem measure_theory.continuous_L1_to_L1 {α : Type u_1} {G : Type u_5} [normed_add_comm_group G] {m : measurable_space α} {μ μ' : measure_theory.measure α} (c' : ennreal) (hc' : c' ) (hμ'_le : μ' c' μ) :

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

theorem measure_theory.set_to_fun_congr_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [complete_space F] {T : set α (E →L[] F)} {C C' : } {μ' : measure_theory.measure α} (c c' : ennreal) (hc : c ) (hc' : c' ) (hμ_le : μ c μ') (hμ'_le : μ' c' μ) (hT : measure_theory.dominated_fin_meas_additive μ T C) (hT' : measure_theory.dominated_fin_meas_additive μ' T C') (f : α E) :