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 bochner file. It will also be used to define the conditional expectation of an integrable function (TODO).

Main Definitions #

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.map_empty_eq_zero_of_map_union {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [add_cancel_monoid β] (T : set α → β) (h_add : measure_theory.fin_meas_additive μ T) :
T = 0
theorem measure_theory.map_Union_fin_meas_set_eq_sum {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [add_comm_monoid β] (T : set α → β) (T_empty : T = 0) (h_add : measure_theory.fin_meas_additive μ T) {ι : Type u_3} (S : ι → set α) (sι : finset ι) (hS_meas : ∀ (i : ι), measurable_set (S i)) (hSp : ∀ (i : ι), i μ (S i) ) (h_disj : ∀ (i j : ι), i 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} [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
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
@[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.set_to_simple_func_mono {α : Type u_1} {F : Type u_3} [normed_group F] [normed_space F] {G : Type u_2} [normed_linear_ordered_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.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.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 α), T s C * (μ s).to_real) (f : measure_theory.simple_func α 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 μ)) :
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
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_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 μ)) :
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_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_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 hT (s.indicator (λ (_x : α), x)) = (T s) x