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.

The extension step from integrable simple functions to L1 relies on a second_countable_topology assumption. Without it, we could only extend to ae_fin_strongly_measurable functions. (TODO: this might be worth doing?)

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.add {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} [add_comm_monoid β] {T T' : set α → β} (hT : measure_theory.fin_meas_additive μ T) (hT' : measure_theory.fin_meas_additive μ T') :
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.of_eq_top_imp_eq_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} [add_comm_monoid β] {T : set α → β} {μ' : measure_theory.measure α} (h : ∀ (s : set α), measurable_set sμ s = μ' s = ) (hT : measure_theory.fin_meas_additive μ T) :
theorem measure_theory.fin_meas_additive.of_smul_measure {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} [add_comm_monoid β] {T : set α → β} (c : ℝ≥0∞) (hc_ne_top : c ) (hT : measure_theory.fin_meas_additive (c μ) T) :
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 : ℝ≥0∞) (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 : ℝ≥0∞) (hc_ne_zero : c 0) (hc_ne_top : c ) :
theorem measure_theory.fin_meas_additive.map_empty_eq_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [add_cancel_monoid β] {T : set α → β} (hT : measure_theory.fin_meas_additive μ T) :
T = 0
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 jdisjoint (S i) (S j)) :
T (⋃ (i : ι) (H : i sι), S i) = ∑ (i : ι) in sι, T (S i)
def measure_theory.dominated_fin_meas_additive {α : Type u_1} {β : Type u_2} [semi_normed_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_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_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} [semi_normed_group β] {T : set α → β} {C : } [normed_field 𝕜] [normed_space 𝕜 β] (hT : measure_theory.dominated_fin_meas_additive μ T C) (c : 𝕜) :
theorem measure_theory.dominated_fin_meas_additive.of_measure_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} [semi_normed_group β] {T : set α → β} {C : } {μ' : measure_theory.measure α} (h : μ μ') (hT : measure_theory.dominated_fin_meas_additive μ T C) (hC : 0 C) :
theorem measure_theory.dominated_fin_meas_additive.of_smul_measure {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} [semi_normed_group β] {T : set α → β} {C : } (c : ℝ≥0∞) (hc_ne_top : c ) (hT : measure_theory.dominated_fin_meas_additive (c μ) T C) :
theorem measure_theory.dominated_fin_meas_additive.of_measure_le_smul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} [semi_normed_group β] {T : set α → β} {C : } {μ' : measure_theory.measure α} (c : ℝ≥0∞) (hc : c ) (h : μ c μ') (hT : measure_theory.dominated_fin_meas_additive μ T C) (hC : 0 C) :
noncomputable def measure_theory.simple_func.set_to_simple_func {α : Type u_1} {F : Type u_3} {F' : Type u_4} [normed_group F] [normed_space F] [normed_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_zero' {α : Type u_1} {E : Type u_2} {F' : Type u_4} [normed_group E] [measurable_space E] [normed_space E] [normed_group F'] [normed_space F'] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α(E →L[] F')} (h_zero : ∀ (s : set α), measurable_set sμ s < T s = 0) (f : measure_theory.simple_func α E) (hf : measure_theory.integrable f μ) :
@[simp]
theorem measure_theory.simple_func.set_to_simple_func_zero_apply {α : Type u_1} {F : Type u_3} {F' : Type u_4} [normed_group F] [normed_space F] [normed_group F'] [normed_space F'] {m : measurable_space α} (T : set α(F →L[] F')) :
theorem measure_theory.simple_func.set_to_simple_func_eq_sum_filter {α : Type u_1} {F : Type u_3} {F' : Type u_4} [normed_group F] [normed_space F] [normed_group F'] [normed_space F'] {m : measurable_space α} (T : set α(F →L[] F')) (f : measure_theory.simple_func α F) :
measure_theory.simple_func.set_to_simple_func T f = ∑ (x : F) in finset.filter (λ (x : F), x 0) f.range, (T (f ⁻¹' {x})) x
theorem measure_theory.simple_func.map_set_to_simple_func {α : Type u_1} {F : Type u_3} {F' : Type u_4} {G : Type u_5} [normed_group F] [normed_space F] [normed_group F'] [normed_space F'] [normed_group G] [measurable_space G] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α(F →L[] F')) (h_add : measure_theory.fin_meas_additive μ T) {f : measure_theory.simple_func α G} (hf : measure_theory.integrable f μ) {g : G → F} (hg : g 0 = 0) :
theorem measure_theory.simple_func.set_to_simple_func_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_6} [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_2} [measurable_space E] [normed_group E] [normed_field 𝕜] [normed_space 𝕜 E] [normed_space E] [normed_space 𝕜 F] (T : set α(E →L[] F)) (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.simple_func α E} (hf : measure_theory.integrable f μ) :
theorem measure_theory.simple_func.set_to_simple_func_mono_left {α : Type u_1} {F : Type u_3} [normed_group F] [normed_space F] {G'' : Type u_8} [normed_lattice_add_comm_group G''] [normed_space G''] {m : measurable_space α} (T T' : set α(F →L[] G'')) (hTT' : ∀ (s : set α) (x : F), (T s) x (T' s) x) (f : measure_theory.simple_func α F) :
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 x0 (T s) x) (f : measure_theory.simple_func α G') (hf : 0 f) :
theorem measure_theory.simple_func.set_to_simple_func_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'] [measurable_space G'] (T : set α(G' →L[] G'')) (hT_nonneg : ∀ (s : set α), measurable_set sμ s < ∀ (x : G'), 0 x0 (T s) x) (f : measure_theory.simple_func α G') (hf : 0 f) (hfi : measure_theory.integrable f μ) :
theorem measure_theory.simple_func.norm_set_to_simple_func_le_sum_mul_norm {α : Type u_1} {F : Type u_3} {F' : Type u_4} [normed_group F] [normed_space F] [normed_group F'] [normed_space F'] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α(F →L[] F')) {C : } (hT_norm : ∀ (s : set α), measurable_set sT s C * (μ s).to_real) (f : measure_theory.simple_func α F) :
theorem measure_theory.simple_func.norm_set_to_simple_func_le_sum_mul_norm_of_integrable {α : Type u_1} {E : Type u_2} {F' : Type u_4} [normed_group E] [measurable_space E] [normed_space E] [normed_group F'] [normed_space F'] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α(E →L[] F')) {C : } (hT_norm : ∀ (s : set α), measurable_set sμ s < T s C * (μ s).to_real) (f : measure_theory.simple_func α E) (hf : measure_theory.integrable f μ) :
theorem measure_theory.simple_func.set_to_simple_func_const {α : Type u_1} {F : Type u_3} {F' : Type u_4} [normed_group F] [normed_space F] [normed_group F'] [normed_space F'] (T : set α(F →L[] F')) (hT_empty : T = 0) (x : F) {m : measurable_space α} :

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_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [normed_field 𝕜] {E : Type u_2} [normed_group E] [measurable_space E] [normed_space E] [normed_space 𝕜 E] [topological_space.second_countable_topology E] [borel_space E] [normed_space 𝕜 F] [measurable_space 𝕜] [opens_measurable_space 𝕜] (T : set α(E →L[] F)) (h_zero : ∀ (s : set α), measurable_set sμ s = 0T 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_indicator_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] {T : set α(E →L[] F)} {s : set α} (h_zero : ∀ (s : set α), measurable_set sμ s = 0T s = 0) (h_add : measure_theory.fin_meas_additive μ T) (hs : measurable_set s) (hμs : μ s < ) (x : E) :
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')} [measurable_space G''] [borel_space G''] [topological_space.second_countable_topology G''] (h_zero : ∀ (s : set α), measurable_set sμ s = 0T s = 0) (h_add : measure_theory.fin_meas_additive μ T) (hT_nonneg : ∀ (s : set α), measurable_set sμ s < ∀ (x : G''), 0 x0 (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')} [measurable_space G''] [borel_space G''] [topological_space.second_countable_topology G''] (h_zero : ∀ (s : set α), measurable_set sμ s = 0T s = 0) (h_add : measure_theory.fin_meas_additive μ T) (hT_nonneg : ∀ (s : set α), measurable_set sμ s < ∀ (x : G''), 0 x0 (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_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} (μ : measure_theory.measure α) [topological_space.second_countable_topology E] [borel_space E] [normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [measurable_space 𝕜] [opens_measurable_space 𝕜] {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.simple_func.set_to_L1s_clm_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'] [measurable_space G'] [borel_space G'] [topological_space.second_countable_topology 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 x0 (T s) x) {f : (measure_theory.Lp.simple_func G' 1 μ)} (hf : 0 f) :
theorem measure_theory.L1.simple_func.set_to_L1s_clm_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'] [measurable_space G'] [borel_space G'] [topological_space.second_countable_topology 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 x0 (T s) x) {f g : (measure_theory.Lp.simple_func G' 1 μ)} (hfg : f g) :
noncomputable def measure_theory.L1.set_to_L1' {α : Type u_1} {E : Type u_2} {F : Type u_3} (𝕜 : Type u_6) [normed_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [nondiscrete_normed_field 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] [topological_space.second_countable_topology E] [borel_space E] [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_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [nondiscrete_normed_field 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] [topological_space.second_countable_topology E] [borel_space E] [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_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [complete_space F] {T : set α(E →L[] F)} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (h_zero : ∀ (s : set α), measurable_set sμ s < T s = 0) (f : (measure_theory.Lp E 1 μ)) :
theorem measure_theory.L1.set_to_L1_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [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 : (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_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [nondiscrete_normed_field 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] [topological_space.second_countable_topology E] [borel_space E] [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_mono_left' {α : Type u_1} {E : Type u_2} [normed_group E] [measurable_space E] [normed_space E] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] {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 : (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'] [measurable_space G'] [borel_space G'] [topological_space.second_countable_topology 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 x0 (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'] [measurable_space G'] [borel_space G'] [topological_space.second_countable_topology 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 x0 (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_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [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 (𝓝 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_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} (μ : measure_theory.measure α) [topological_space.second_countable_topology E] [borel_space E] [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_congr_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [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') (h : ∀ (s : set α), measurable_set sμ s < T s = T' s) (f : α → E) :
theorem measure_theory.set_to_fun_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [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_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [complete_space F] {T : set α(E →L[] F)} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) (c : ) (f : α → E) :
measure_theory.set_to_fun μ (λ (s : set α), c T s) _ f = c measure_theory.set_to_fun μ T hT f
theorem measure_theory.set_to_fun_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [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_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [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_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [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 smeasure_theory.integrable (f i) μ) :
measure_theory.set_to_fun μ T hT (∑ (i : ι) in s, f i) = ∑ (i : ι) in s, 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_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [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 smeasure_theory.integrable (f i) μ) :
measure_theory.set_to_fun μ T hT (λ (a : α), ∑ (i : ι) in s, f i a) = ∑ (i : ι) in s, 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_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [complete_space F] {T : set α(E →L[] F)} {C : } [nondiscrete_normed_field 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] [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_measure_zero {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [complete_space F] {T : set α(E →L[] F)} {C : } {f : α → E} (hT : measure_theory.dominated_fin_meas_additive μ T C) (h : μ = 0) :
theorem measure_theory.set_to_fun_measure_zero' {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [complete_space F] {T : set α(E →L[] F)} {C : } {f : α → E} (hT : measure_theory.dominated_fin_meas_additive μ T C) (h : ∀ (s : set α), measurable_set sμ s < μ s = 0) :
theorem measure_theory.set_to_fun_indicator_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [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_group E] [measurable_space E] [normed_space E] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] {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_group E] [measurable_space E] [normed_space E] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] {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'] [measurable_space G'] [borel_space G'] [topological_space.second_countable_topology 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 x0 (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'] [measurable_space G'] [borel_space G'] [topological_space.second_countable_topology 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 x0 (T s) x) {f g : α → G'} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) (hfg : f ≤ᵐ[μ] g) :

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_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [complete_space F] {T : set α(E →L[] F)} {C C' : } {μ' : measure_theory.measure α} (c c' : ℝ≥0∞) (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) :
theorem measure_theory.set_to_fun_congr_smul_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [complete_space F] {T : set α(E →L[] F)} {C C' : } (c : ℝ≥0∞) (hc_ne_top : c ) (hT : measure_theory.dominated_fin_meas_additive μ T C) (hT_smul : measure_theory.dominated_fin_meas_additive (c μ) T C') (f : α → E) :
theorem measure_theory.tendsto_set_to_fun_of_dominated_convergence {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [measurable_space E] [normed_space E] [normed_group F] [normed_space F] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] [borel_space E] [complete_space F] {T : set α(E →L[] F)} {C : } (hT : measure_theory.dominated_fin_meas_additive μ T C) {fs : α → E} {f : α → E} (bound : α → ) (fs_measurable : ∀ (n : ), ae_measurable (fs n) μ) (bound_integrable : measure_theory.integrable bound μ) (h_bound : ∀ (n : ), ∀ᵐ (a : α) ∂μ, fs n a bound a) (h_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ), fs n a) filter.at_top (𝓝 (f a))) :

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