Extension of a linear function from indicators to L1 #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
fin_meas_additive μ T: the property thatTis additive on measurable sets with finite measure. For two such sets,s ∩ t = ∅ → T (s ∪ t) = T s + T t.dominated_fin_meas_additive μ T C:fin_meas_additive μ T ∧ ∀ s, ‖T s‖ ≤ C * (μ s).to_real. This is the property needed to perform the extension from indicators to L1.set_to_L1 (hT : dominated_fin_meas_additive μ T C) : (α →₁[μ] E) →L[ℝ] F: the extension ofTfrom indicators to L1.set_to_fun μ T (hT : dominated_fin_meas_additive μ 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 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:
set_to_fun_zero_left : set_to_fun μ 0 hT f = 0set_to_fun_add_left : set_to_fun μ (T + T') _ f = set_to_fun μ T hT f + set_to_fun μ T' hT' fset_to_fun_smul_left : set_to_fun μ (λ s, c • (T s)) (hT.smul c) f = c • set_to_fun μ T hT fset_to_fun_zero : set_to_fun μ T hT (0 : α → E) = 0set_to_fun_neg : set_to_fun μ T hT (-f) = - set_to_fun μ T hT fIffandgare integrable:set_to_fun_add : set_to_fun μ T hT (f + g) = set_to_fun μ T hT f + set_to_fun μ T hT gset_to_fun_sub : set_to_fun μ T hT (f - g) = set_to_fun μ T hT f - set_to_fun μ T hT gIfTis verifies∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x:set_to_fun_smul : set_to_fun μ T hT (c • f) = c • set_to_fun μ T hT f
Other:
set_to_fun_congr_ae (h : f =ᵐ[μ] g) : set_to_fun μ T hT f = set_to_fun μ T hT gset_to_fun_measure_zero (h : μ = 0) : set_to_fun μ T hT f = 0
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:
set_to_fun_mono_left (h : ∀ s x, T s x ≤ T' s x) : set_to_fun μ T hT f ≤ set_to_fun μ T' hT' fset_to_fun_nonneg (hf : 0 ≤ᵐ[μ] f) : 0 ≤ set_to_fun μ T hT fset_to_fun_mono (hfg : f ≤ᵐ[μ] g) : set_to_fun μ T hT f ≤ set_to_fun μ 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
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.
theorem
measure_theory.fin_meas_additive.zero
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_7}
[add_comm_monoid β] :
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') :
measure_theory.fin_meas_additive μ (T + 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 : ennreal)
(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 : ennreal)
(hc_ne_zero : c ≠ 0)
(hT : measure_theory.fin_meas_additive μ T) :
measure_theory.fin_meas_additive (c • μ) 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_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) :
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ι → ⇑μ (S i) ≠ ⊤)
(h_disj : ∀ (i : ι), i ∈ sι → ∀ (j : ι), j ∈ sι → i ≠ j → disjoint (S i) (S j)) :
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).
theorem
measure_theory.dominated_fin_meas_additive.zero
{α : Type u_1}
{β : Type u_7}
[seminormed_add_comm_group β]
{C : ℝ}
{m : measurable_space α}
(μ : measure_theory.measure α)
(hC : 0 ≤ C) :
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.add
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_7}
[seminormed_add_comm_group β]
{T T' : set α → β}
{C C' : ℝ}
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(hT' : measure_theory.dominated_fin_meas_additive μ T' C') :
measure_theory.dominated_fin_meas_additive μ (T + T') (C + C')
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 : 𝕜) :
theorem
measure_theory.dominated_fin_meas_additive.of_measure_le
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_7}
[seminormed_add_comm_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.add_measure_right
{α : Type u_1}
{β : Type u_7}
[seminormed_add_comm_group β]
{T : set α → β}
{C : ℝ}
{m : measurable_space α}
(μ ν : measure_theory.measure α)
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(hC : 0 ≤ C) :
measure_theory.dominated_fin_meas_additive (μ + ν) T C
theorem
measure_theory.dominated_fin_meas_additive.add_measure_left
{α : Type u_1}
{β : Type u_7}
[seminormed_add_comm_group β]
{T : set α → β}
{C : ℝ}
{m : measurable_space α}
(μ ν : measure_theory.measure α)
(hT : measure_theory.dominated_fin_meas_additive ν T C)
(hC : 0 ≤ C) :
measure_theory.dominated_fin_meas_additive (μ + ν) T C
theorem
measure_theory.dominated_fin_meas_additive.of_smul_measure
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_7}
[seminormed_add_comm_group β]
{T : set α → β}
{C : ℝ}
(c : ennreal)
(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}
[seminormed_add_comm_group β]
{T : set α → β}
{C : ℝ}
{μ' : measure_theory.measure α}
(c : ennreal)
(hc : c ≠ ⊤)
(h : μ ≤ c • μ')
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(hC : 0 ≤ C) :
measure_theory.dominated_fin_meas_additive μ' T (c.to_real * 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'.
@[simp]
theorem
measure_theory.simple_func.set_to_simple_func_zero
{α : 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 α}
(f : measure_theory.simple_func α F) :
theorem
measure_theory.simple_func.set_to_simple_func_zero'
{α : Type u_1}
{E : Type u_2}
{F' : Type u_4}
[normed_add_comm_group E]
[normed_space ℝ E]
[normed_add_comm_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_add_comm_group F]
[normed_space ℝ F]
[normed_add_comm_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_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) :
measure_theory.simple_func.set_to_simple_func T f = (finset.filter (λ (x : F), x ≠ 0) f.range).sum (λ (x : F), ⇑(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_add_comm_group F]
[normed_space ℝ F]
[normed_add_comm_group F']
[normed_space ℝ F']
[normed_add_comm_group 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) :
measure_theory.simple_func.set_to_simple_func T (measure_theory.simple_func.map g f) = f.range.sum (λ (x : G), ⇑(T (⇑f ⁻¹' {x})) (g x))
theorem
measure_theory.simple_func.set_to_simple_func_congr'
{α : 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 α}
(T : set α → (E →L[ℝ] F))
(h_add : measure_theory.fin_meas_additive μ T)
{f g : measure_theory.simple_func α E}
(hf : measure_theory.integrable ⇑f μ)
(hg : measure_theory.integrable ⇑g μ)
(h : ∀ (x y : E), x ≠ y → T (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0) :
theorem
measure_theory.simple_func.set_to_simple_func_congr
{α : 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 α}
(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)
{f g : measure_theory.simple_func α E}
(hf : measure_theory.integrable ⇑f μ)
(h : ⇑f =ᵐ[μ] ⇑g) :
theorem
measure_theory.simple_func.set_to_simple_func_congr_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 α}
(T T' : set α → (E →L[ℝ] F))
(h : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → T s = T' s)
(f : measure_theory.simple_func α E)
(hf : measure_theory.integrable ⇑f μ) :
theorem
measure_theory.simple_func.set_to_simple_func_add_left
{α : 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 T' : set α → (F →L[ℝ] F'))
{f : measure_theory.simple_func α F} :
theorem
measure_theory.simple_func.set_to_simple_func_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 α}
(T T' T'' : set α → (E →L[ℝ] F))
(h_add : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → T'' s = T s + T' s)
{f : measure_theory.simple_func α E}
(hf : measure_theory.integrable ⇑f μ) :
theorem
measure_theory.simple_func.set_to_simple_func_smul_left
{α : 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'))
(c : ℝ)
(f : measure_theory.simple_func α F) :
measure_theory.simple_func.set_to_simple_func (λ (s : set α), c • T s) f = c • measure_theory.simple_func.set_to_simple_func T f
theorem
measure_theory.simple_func.set_to_simple_func_smul_left'
{α : Type u_1}
{E : Type u_2}
{F' : Type u_4}
[normed_add_comm_group E]
[normed_space ℝ E]
[normed_add_comm_group F']
[normed_space ℝ F']
{m : measurable_space α}
{μ : measure_theory.measure α}
(T T' : set α → (E →L[ℝ] F'))
(c : ℝ)
(h_smul : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → T' s = c • T s)
{f : measure_theory.simple_func α E}
(hf : measure_theory.integrable ⇑f μ) :
theorem
measure_theory.simple_func.set_to_simple_func_add
{α : 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 α}
(T : set α → (E →L[ℝ] F))
(h_add : measure_theory.fin_meas_additive μ T)
{f g : measure_theory.simple_func α E}
(hf : measure_theory.integrable ⇑f μ)
(hg : measure_theory.integrable ⇑g μ) :
theorem
measure_theory.simple_func.set_to_simple_func_neg
{α : 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 α}
(T : set α → (E →L[ℝ] F))
(h_add : measure_theory.fin_meas_additive μ T)
{f : measure_theory.simple_func α E}
(hf : measure_theory.integrable ⇑f μ) :
theorem
measure_theory.simple_func.set_to_simple_func_sub
{α : 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 α}
(T : set α → (E →L[ℝ] F))
(h_add : measure_theory.fin_meas_additive μ T)
{f g : measure_theory.simple_func α E}
(hf : measure_theory.integrable ⇑f μ)
(hg : measure_theory.integrable ⇑g μ) :
theorem
measure_theory.simple_func.set_to_simple_func_smul_real
{α : 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 α}
(T : set α → (E →L[ℝ] F))
(h_add : measure_theory.fin_meas_additive μ T)
(c : ℝ)
{f : measure_theory.simple_func α E}
(hf : measure_theory.integrable ⇑f μ) :
theorem
measure_theory.simple_func.set_to_simple_func_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 α}
{E : Type u_2}
[normed_add_comm_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_add_comm_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_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'']
(T T' : set α → (E →L[ℝ] G''))
(hTT' : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∀ (x : E), ⇑(T s) x ≤ ⇑(T' s) x)
(f : measure_theory.simple_func α E)
(hf : measure_theory.integrable ⇑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 ≤ x → 0 ≤ ⇑(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']
(T : set α → (G' →L[ℝ] G''))
(hT_nonneg : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ⇑(T s) x)
(f : measure_theory.simple_func α G')
(hf : 0 ≤ f)
(hfi : measure_theory.integrable ⇑f μ) :
theorem
measure_theory.simple_func.set_to_simple_func_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_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.simple_func α G'}
(hfi : measure_theory.integrable ⇑f μ)
(hgi : measure_theory.integrable ⇑g μ)
(hfg : f ≤ g) :
theorem
measure_theory.simple_func.norm_set_to_simple_func_le_sum_op_norm
{α : 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') :
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_add_comm_group F]
[normed_space ℝ F]
[normed_add_comm_group F']
[normed_space ℝ F']
{m : measurable_space α}
{μ : measure_theory.measure α}
(T : set α → (F →L[ℝ] F'))
{C : ℝ}
(hT_norm : ∀ (s : set α), measurable_set s → ‖T 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_add_comm_group E]
[normed_space ℝ E]
[normed_add_comm_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_indicator
{α : 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']
(T : set α → (F →L[ℝ] F'))
(hT_empty : T ∅ = 0)
{m : measurable_space α}
{s : set α}
(hs : measurable_set s)
(x : F) :
theorem
measure_theory.simple_func.set_to_simple_func_const'
{α : 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']
[nonempty α]
(T : set α → (F →L[ℝ] F'))
(x : F)
{m : measurable_space α} :
theorem
measure_theory.simple_func.set_to_simple_func_const
{α : 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']
(T : set α → (F →L[ℝ] F'))
(hT_empty : T ∅ = 0)
(x : F)
{m : measurable_space α} :
theorem
measure_theory.L1.simple_func.norm_eq_sum_mul
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m : measurable_space α}
{μ : measure_theory.measure α}
(f : ↥(measure_theory.Lp.simple_func G 1 μ)) :
noncomputable
def
measure_theory.L1.simple_func.set_to_L1s
{α : 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 α}
(T : set α → (E →L[ℝ] F))
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
F
Extend set α → (E →L[ℝ] F') to (α →₁ₛ[μ] E) → F'.
theorem
measure_theory.L1.simple_func.set_to_L1s_eq_set_to_simple_func
{α : 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 α}
(T : set α → (E →L[ℝ] F))
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
@[simp]
theorem
measure_theory.L1.simple_func.set_to_L1s_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 α}
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
theorem
measure_theory.L1.simple_func.set_to_L1s_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 α}
{T : set α → (E →L[ℝ] F)}
(h_zero : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → T s = 0)
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
theorem
measure_theory.L1.simple_func.set_to_L1s_congr
{α : 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 α}
(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)
{f g : ↥(measure_theory.Lp.simple_func E 1 μ)}
(h : ⇑(measure_theory.Lp.simple_func.to_simple_func f) =ᵐ[μ] ⇑(measure_theory.Lp.simple_func.to_simple_func g)) :
theorem
measure_theory.L1.simple_func.set_to_L1s_congr_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 α}
(T T' : set α → (E →L[ℝ] F))
(h : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → T s = T' s)
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
theorem
measure_theory.L1.simple_func.set_to_L1s_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 α}
(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μ : μ.absolutely_continuous μ')
(f : ↥(measure_theory.Lp.simple_func E 1 μ))
(f' : ↥(measure_theory.Lp.simple_func E 1 μ'))
(h : ⇑f =ᵐ[μ] ⇑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_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 α}
(T T' : set α → (E →L[ℝ] F))
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
theorem
measure_theory.L1.simple_func.set_to_L1s_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 α}
(T T' T'' : set α → (E →L[ℝ] F))
(h_add : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → T'' s = T s + T' s)
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
theorem
measure_theory.L1.simple_func.set_to_L1s_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 α}
(T : set α → (E →L[ℝ] F))
(c : ℝ)
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
measure_theory.L1.simple_func.set_to_L1s (λ (s : set α), c • T s) f = c • measure_theory.L1.simple_func.set_to_L1s T f
theorem
measure_theory.L1.simple_func.set_to_L1s_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 α}
(T T' : set α → (E →L[ℝ] F))
(c : ℝ)
(h_smul : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → T' s = c • T s)
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
theorem
measure_theory.L1.simple_func.set_to_L1s_add
{α : 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 α}
(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)
(f g : ↥(measure_theory.Lp.simple_func E 1 μ)) :
theorem
measure_theory.L1.simple_func.set_to_L1s_neg
{α : 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 α}
{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)
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
theorem
measure_theory.L1.simple_func.set_to_L1s_sub
{α : 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 α}
{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)
(f g : ↥(measure_theory.Lp.simple_func E 1 μ)) :
theorem
measure_theory.L1.simple_func.set_to_L1s_smul_real
{α : 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 α}
(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)
(c : ℝ)
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
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.norm_set_to_L1s_le
{α : 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 α}
(T : set α → (E →L[ℝ] F))
{C : ℝ}
(hT_norm : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ‖T s‖ ≤ C * (⇑μ s).to_real)
(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_add_comm_group E]
[normed_space ℝ E]
[normed_add_comm_group F]
[normed_space ℝ F]
{m : measurable_space α}
{μ : measure_theory.measure α}
{T : set α → (E →L[ℝ] F)}
{s : set α}
(h_zero : ∀ (s : set α), measurable_set s → ⇑μ s = 0 → T s = 0)
(h_add : measure_theory.fin_meas_additive μ T)
(hs : measurable_set s)
(hμs : ⇑μ s < ⊤)
(x : E) :
measure_theory.L1.simple_func.set_to_L1s T (measure_theory.Lp.simple_func.indicator_const 1 hs _ x) = ⇑(T s) x
theorem
measure_theory.L1.simple_func.set_to_L1s_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 α}
[measure_theory.is_finite_measure μ]
{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)
(x : E) :
theorem
measure_theory.L1.simple_func.set_to_L1s_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_7}
[normed_lattice_add_comm_group G'']
[normed_space ℝ G'']
{T T' : set α → (E →L[ℝ] G'')}
(hTT' : ∀ (s : set α) (x : E), ⇑(T s) x ≤ ⇑(T' s) x)
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
theorem
measure_theory.L1.simple_func.set_to_L1s_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_7}
[normed_lattice_add_comm_group G'']
[normed_space ℝ G'']
{T T' : set α → (E →L[ℝ] G'')}
(hTT' : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∀ (x : E), ⇑(T s) x ≤ ⇑(T' s) x)
(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) :
↥(measure_theory.Lp.simple_func E 1 μ) →L[𝕜] F
Extend set α → E →L[ℝ] F to (α →₁ₛ[μ] E) →L[𝕜] F.
Equations
- measure_theory.L1.simple_func.set_to_L1s_clm' α E 𝕜 μ hT h_smul = {to_fun := measure_theory.L1.simple_func.set_to_L1s T, map_add' := _, map_smul' := _}.mk_continuous C _
noncomputable
def
measure_theory.L1.simple_func.set_to_L1s_clm
(α : 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 α)
{T : set α → (E →L[ℝ] F)}
{C : ℝ}
(hT : measure_theory.dominated_fin_meas_additive μ T C) :
↥(measure_theory.Lp.simple_func E 1 μ) →L[ℝ] F
Extend set α → E →L[ℝ] F to (α →₁ₛ[μ] E) →L[ℝ] F.
Equations
- measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT = {to_fun := measure_theory.L1.simple_func.set_to_L1s T, map_add' := _, map_smul' := _}.mk_continuous C _
@[simp]
theorem
measure_theory.L1.simple_func.set_to_L1s_clm_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 α}
{C : ℝ}
(hT : measure_theory.dominated_fin_meas_additive μ 0 C)
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT) f = 0
theorem
measure_theory.L1.simple_func.set_to_L1s_clm_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 α}
{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.simple_func E 1 μ)) :
⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT) f = 0
theorem
measure_theory.L1.simple_func.set_to_L1s_clm_congr_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 α}
{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 : T = T')
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT) f = ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT') f
theorem
measure_theory.L1.simple_func.set_to_L1s_clm_congr_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 α}
{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 : ↥(measure_theory.Lp.simple_func E 1 μ)) :
⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT) f = ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT') f
theorem
measure_theory.L1.simple_func.set_to_L1s_clm_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 α}
{T : set α → (E →L[ℝ] F)}
{C C' : ℝ}
{μ' : measure_theory.measure α}
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(hT' : measure_theory.dominated_fin_meas_additive μ' T C')
(hμ : μ.absolutely_continuous μ')
(f : ↥(measure_theory.Lp.simple_func E 1 μ))
(f' : ↥(measure_theory.Lp.simple_func E 1 μ'))
(h : ⇑f =ᵐ[μ] ⇑f') :
⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT) f = ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ' hT') f'
theorem
measure_theory.L1.simple_func.set_to_L1s_clm_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 α}
{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')
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ _) f = ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT) f + ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT') f
theorem
measure_theory.L1.simple_func.set_to_L1s_clm_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 α}
{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 : ↥(measure_theory.Lp.simple_func E 1 μ)) :
⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT'') f = ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT) f + ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT') f
theorem
measure_theory.L1.simple_func.set_to_L1s_clm_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 α}
{T : set α → (E →L[ℝ] F)}
{C : ℝ}
(c : ℝ)
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ _) f = c • ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT) f
theorem
measure_theory.L1.simple_func.set_to_L1s_clm_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 α}
{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')
(h_smul : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → T' s = c • T s)
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT') f = c • ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT) f
theorem
measure_theory.L1.simple_func.norm_set_to_L1s_clm_le
{α : 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 α}
{T : set α → (E →L[ℝ] F)}
{C : ℝ}
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(hC : 0 ≤ C) :
‖measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT‖ ≤ C
theorem
measure_theory.L1.simple_func.norm_set_to_L1s_clm_le'
{α : 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 α}
{T : set α → (E →L[ℝ] F)}
{C : ℝ}
(hT : measure_theory.dominated_fin_meas_additive μ T C) :
theorem
measure_theory.L1.simple_func.set_to_L1s_clm_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 α}
[measure_theory.is_finite_measure μ]
{T : set α → (E →L[ℝ] F)}
{C : ℝ}
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(x : E) :
theorem
measure_theory.L1.simple_func.set_to_L1s_clm_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'']
{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.simple_func E 1 μ)) :
⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT) f ≤ ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT') f
theorem
measure_theory.L1.simple_func.set_to_L1s_clm_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'']
{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.simple_func E 1 μ)) :
⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT) f ≤ ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT') f
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']
{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.simple_func G' 1 μ)}
(hf : 0 ≤ f) :
0 ≤ ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α G' μ hT) 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']
{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.simple_func G' 1 μ)}
(hfg : f ≤ g) :
⇑(measure_theory.L1.simple_func.set_to_L1s_clm α G' μ hT) f ≤ ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α G' μ hT) g
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) :
↥(measure_theory.Lp E 1 μ) →L[𝕜] F
Extend set α → (E →L[ℝ] F) to (α →₁[μ] E) →L[𝕜] F.
Equations
- measure_theory.L1.set_to_L1' 𝕜 hT h_smul = (measure_theory.L1.simple_func.set_to_L1s_clm' α E 𝕜 μ hT h_smul).extend (measure_theory.Lp.simple_func.coe_to_Lp α E 𝕜) measure_theory.L1.set_to_L1'._proof_6 measure_theory.L1.set_to_L1'._proof_7
noncomputable
def
measure_theory.L1.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) :
↥(measure_theory.Lp E 1 μ) →L[ℝ] F
Extend set α → E →L[ℝ] F to (α →₁[μ] E) →L[ℝ] F.
Equations
- measure_theory.L1.set_to_L1 hT = (measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT).extend (measure_theory.Lp.simple_func.coe_to_Lp α E ℝ) measure_theory.L1.set_to_L1._proof_6 measure_theory.L1.set_to_L1._proof_7
theorem
measure_theory.L1.set_to_L1_eq_set_to_L1s_clm
{α : 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.simple_func E 1 μ)) :
⇑(measure_theory.L1.set_to_L1 hT) ↑f = ⇑(measure_theory.L1.simple_func.set_to_L1s_clm α E μ hT) f
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 μ)) :
⇑(measure_theory.L1.set_to_L1 hT) f = ⇑(measure_theory.L1.set_to_L1' 𝕜 hT h_smul) f
@[simp]
theorem
measure_theory.L1.set_to_L1_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]
{C : ℝ}
(hT : measure_theory.dominated_fin_meas_additive μ 0 C)
(f : ↥(measure_theory.Lp E 1 μ)) :
⇑(measure_theory.L1.set_to_L1 hT) f = 0
theorem
measure_theory.L1.set_to_L1_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 : ℝ}
(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 μ)) :
⇑(measure_theory.L1.set_to_L1 hT) f = 0
theorem
measure_theory.L1.set_to_L1_congr_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')
(h : T = T')
(f : ↥(measure_theory.Lp E 1 μ)) :
⇑(measure_theory.L1.set_to_L1 hT) f = ⇑(measure_theory.L1.set_to_L1 hT') f
theorem
measure_theory.L1.set_to_L1_congr_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')
(h : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → T s = T' s)
(f : ↥(measure_theory.Lp E 1 μ)) :
⇑(measure_theory.L1.set_to_L1 hT) f = ⇑(measure_theory.L1.set_to_L1 hT') f
theorem
measure_theory.L1.set_to_L1_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' : set α → (E →L[ℝ] F)}
{C C' : ℝ}
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(hT' : measure_theory.dominated_fin_meas_additive μ T' C')
(f : ↥(measure_theory.Lp E 1 μ)) :
⇑(measure_theory.L1.set_to_L1 _) f = ⇑(measure_theory.L1.set_to_L1 hT) f + ⇑(measure_theory.L1.set_to_L1 hT') f
theorem
measure_theory.L1.set_to_L1_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 : ↥(measure_theory.Lp E 1 μ)) :
⇑(measure_theory.L1.set_to_L1 hT'') f = ⇑(measure_theory.L1.set_to_L1 hT) f + ⇑(measure_theory.L1.set_to_L1 hT') f
theorem
measure_theory.L1.set_to_L1_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 : set α → (E →L[ℝ] F)}
{C : ℝ}
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(c : ℝ)
(f : ↥(measure_theory.Lp E 1 μ)) :
⇑(measure_theory.L1.set_to_L1 _) f = c • ⇑(measure_theory.L1.set_to_L1 hT) f
theorem
measure_theory.L1.set_to_L1_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 : ↥(measure_theory.Lp E 1 μ)) :
⇑(measure_theory.L1.set_to_L1 hT') f = c • ⇑(measure_theory.L1.set_to_L1 hT) f
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 μ)) :
⇑(measure_theory.L1.set_to_L1 hT) (c • f) = c • ⇑(measure_theory.L1.set_to_L1 hT) f
theorem
measure_theory.L1.set_to_L1_simple_func_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.L1.set_to_L1 hT) ↑(measure_theory.Lp.simple_func.indicator_const 1 hs _ x) = ⇑(T s) x
theorem
measure_theory.L1.set_to_L1_indicator_const_Lp
{α : 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.L1.set_to_L1 hT) (measure_theory.indicator_const_Lp 1 hs hμs x) = ⇑(T s) x
theorem
measure_theory.L1.set_to_L1_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 : ℝ}
[measure_theory.is_finite_measure μ]
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(x : E) :
⇑(measure_theory.L1.set_to_L1 hT) (measure_theory.indicator_const_Lp 1 measurable_set.univ _ x) = ⇑(T set.univ) x
theorem
measure_theory.L1.set_to_L1_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 : ↥(measure_theory.Lp E 1 μ)) :
⇑(measure_theory.L1.set_to_L1 hT) f ≤ ⇑(measure_theory.L1.set_to_L1 hT') f
theorem
measure_theory.L1.set_to_L1_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 μ)) :
⇑(measure_theory.L1.set_to_L1 hT) f ≤ ⇑(measure_theory.L1.set_to_L1 hT') f
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) :
0 ≤ ⇑(measure_theory.L1.set_to_L1 hT) 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) :
⇑(measure_theory.L1.set_to_L1 hT) f ≤ ⇑(measure_theory.L1.set_to_L1 hT) g
theorem
measure_theory.L1.norm_set_to_L1_le_norm_set_to_L1s_clm
{α : 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) :
theorem
measure_theory.L1.norm_set_to_L1_le_mul_norm
{α : 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)
(hC : 0 ≤ C)
(f : ↥(measure_theory.Lp E 1 μ)) :
theorem
measure_theory.L1.norm_set_to_L1_le_mul_norm'
{α : 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 μ)) :
‖⇑(measure_theory.L1.set_to_L1 hT) f‖ ≤ linear_order.max C 0 * ‖f‖
theorem
measure_theory.L1.norm_set_to_L1_le
{α : 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)
(hC : 0 ≤ C) :
theorem
measure_theory.L1.norm_set_to_L1_le'
{α : 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) :
theorem
measure_theory.L1.set_to_L1_lipschitz
{α : 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) :
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)) :
filter.tendsto (λ (i : ι), ⇑(measure_theory.L1.set_to_L1 hT) (fs i)) l (nhds (⇑(measure_theory.L1.set_to_L1 hT) 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
- measure_theory.set_to_fun μ T hT f = dite (measure_theory.integrable f μ) (λ (hf : measure_theory.integrable f μ), ⇑(measure_theory.L1.set_to_L1 hT) (measure_theory.integrable.to_L1 f hf)) (λ (hf : ¬measure_theory.integrable f μ), 0)
theorem
measure_theory.set_to_fun_eq
{α : 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)
(hf : measure_theory.integrable f μ) :
measure_theory.set_to_fun μ T hT f = ⇑(measure_theory.L1.set_to_L1 hT) (measure_theory.integrable.to_L1 f hf)
theorem
measure_theory.L1.set_to_fun_eq_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 μ)) :
measure_theory.set_to_fun μ T hT ⇑f = ⇑(measure_theory.L1.set_to_L1 hT) f
theorem
measure_theory.set_to_fun_undef
{α : 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)
(hf : ¬measure_theory.integrable f μ) :
measure_theory.set_to_fun μ T hT f = 0
theorem
measure_theory.set_to_fun_non_ae_strongly_measurable
{α : 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)
(hf : ¬measure_theory.ae_strongly_measurable f μ) :
measure_theory.set_to_fun μ T hT f = 0
theorem
measure_theory.set_to_fun_congr_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')
(h : T = T')
(f : α → E) :
measure_theory.set_to_fun μ T hT f = measure_theory.set_to_fun μ T' hT' f
theorem
measure_theory.set_to_fun_congr_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')
(h : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → T s = T' s)
(f : α → E) :
measure_theory.set_to_fun μ T hT f = measure_theory.set_to_fun μ T' hT' f
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' : set α → (E →L[ℝ] F)}
{C C' : ℝ}
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(hT' : measure_theory.dominated_fin_meas_additive μ T' C')
(f : α → E) :
measure_theory.set_to_fun μ (T + T') _ f = measure_theory.set_to_fun μ T hT f + measure_theory.set_to_fun μ T' hT' f
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) :
measure_theory.set_to_fun μ T'' hT'' f = measure_theory.set_to_fun μ T hT f + 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_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)
(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_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) :
measure_theory.set_to_fun μ T' hT' f = c • measure_theory.set_to_fun μ T hT f
@[simp]
theorem
measure_theory.set_to_fun_zero
{α : 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) :
measure_theory.set_to_fun μ T hT 0 = 0
@[simp]
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]
{C : ℝ}
{f : α → E}
{hT : measure_theory.dominated_fin_meas_additive μ 0 C} :
measure_theory.set_to_fun μ 0 hT f = 0
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) :
measure_theory.set_to_fun μ T hT f = 0
theorem
measure_theory.set_to_fun_add
{α : 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 g : α → E}
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.set_to_fun μ T hT (f + g) = measure_theory.set_to_fun μ T hT f + measure_theory.set_to_fun μ T hT g
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_neg
{α : 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) :
measure_theory.set_to_fun μ T hT (-f) = -measure_theory.set_to_fun μ T hT f
theorem
measure_theory.set_to_fun_sub
{α : 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 g : α → E}
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.set_to_fun μ T hT (f - g) = measure_theory.set_to_fun μ T hT f - measure_theory.set_to_fun μ T hT g
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) :
measure_theory.set_to_fun μ T hT (c • f) = c • measure_theory.set_to_fun μ T hT f
theorem
measure_theory.set_to_fun_congr_ae
{α : 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 g : α → E}
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(h : f =ᵐ[μ] g) :
measure_theory.set_to_fun μ T hT f = measure_theory.set_to_fun μ T hT g
theorem
measure_theory.set_to_fun_measure_zero
{α : 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 : μ = 0) :
measure_theory.set_to_fun μ T hT f = 0
theorem
measure_theory.set_to_fun_measure_zero'
{α : 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 : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ⇑μ s = 0) :
measure_theory.set_to_fun μ T hT f = 0
theorem
measure_theory.set_to_fun_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 : ℝ}
{f : α → E}
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(hf : measure_theory.integrable f μ) :
measure_theory.set_to_fun μ T hT ⇑(measure_theory.integrable.to_L1 f hf) = measure_theory.set_to_fun μ T hT f
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_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 : ℝ}
[measure_theory.is_finite_measure μ]
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(x : E) :
measure_theory.set_to_fun μ T hT (λ (_x : α), x) = ⇑(T set.univ) 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) :
measure_theory.set_to_fun μ T hT f ≤ measure_theory.set_to_fun μ T' hT' f
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 μ)) :
measure_theory.set_to_fun μ T hT ⇑f ≤ measure_theory.set_to_fun μ T' hT' ⇑f
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) :
0 ≤ measure_theory.set_to_fun μ T hT 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) :
measure_theory.set_to_fun μ T hT f ≤ measure_theory.set_to_fun μ T hT g
@[continuity]
theorem
measure_theory.continuous_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) :
continuous (λ (f : ↥(measure_theory.Lp E 1 μ)), measure_theory.set_to_fun μ T hT ⇑f)
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.tendsto_set_to_fun_approx_on_of_measurable
{α : 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)
[measurable_space E]
[borel_space E]
{f : α → E}
{s : set E}
[topological_space.separable_space ↥s]
(hfi : measure_theory.integrable f μ)
(hfm : measurable f)
(hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s)
{y₀ : E}
(h₀ : y₀ ∈ s)
(h₀i : measure_theory.integrable (λ (x : α), y₀) μ) :
filter.tendsto (λ (n : ℕ), measure_theory.set_to_fun μ T hT ⇑(measure_theory.simple_func.approx_on f hfm s y₀ h₀ n)) filter.at_top (nhds (measure_theory.set_to_fun μ T hT f))
theorem
measure_theory.tendsto_set_to_fun_approx_on_of_measurable_of_range_subset
{α : 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)
[measurable_space E]
[borel_space E]
{f : α → E}
(fmeas : measurable f)
(hf : measure_theory.integrable f μ)
(s : set E)
[topological_space.separable_space ↥s]
(hs : set.range f ∪ {0} ⊆ s) :
filter.tendsto (λ (n : ℕ), measure_theory.set_to_fun μ T hT ⇑(measure_theory.simple_func.approx_on f fmeas s 0 _ n)) filter.at_top (nhds (measure_theory.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' • μ) :
continuous (λ (f : ↥(measure_theory.Lp G 1 μ)), measure_theory.integrable.to_L1 ⇑f _)
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_of_integrable
{α : 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' : ennreal)
(hc' : c' ≠ ⊤)
(hμ'_le : μ' ≤ c' • μ)
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(hT' : measure_theory.dominated_fin_meas_additive μ' T C')
(f : α → E)
(hfμ : measure_theory.integrable f μ) :
measure_theory.set_to_fun μ T hT f = measure_theory.set_to_fun μ' T hT' f
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) :
measure_theory.set_to_fun μ T hT f = measure_theory.set_to_fun μ' T hT' f
theorem
measure_theory.set_to_fun_congr_measure_of_add_right
{α : 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 α}
(hT_add : measure_theory.dominated_fin_meas_additive (μ + μ') T C')
(hT : measure_theory.dominated_fin_meas_additive μ T C)
(f : α → E)
(hf : measure_theory.integrable f (μ + μ')) :
measure_theory.set_to_fun (μ + μ') T hT_add f = measure_theory.set_to_fun μ T hT f
theorem
measure_theory.set_to_fun_congr_measure_of_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 : set α → (E →L[ℝ] F)}
{C C' : ℝ}
{μ' : measure_theory.measure α}
(hT_add : measure_theory.dominated_fin_meas_additive (μ + μ') T C')
(hT : measure_theory.dominated_fin_meas_additive μ' T C)
(f : α → E)
(hf : measure_theory.integrable f (μ + μ')) :
measure_theory.set_to_fun (μ + μ') T hT_add f = measure_theory.set_to_fun μ' T hT f
theorem
measure_theory.set_to_fun_top_smul_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 : ℝ}
(hT : measure_theory.dominated_fin_meas_additive (⊤ • μ) T C)
(f : α → E) :
measure_theory.set_to_fun (⊤ • μ) T hT f = 0
theorem
measure_theory.set_to_fun_congr_smul_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' : ℝ}
(c : ennreal)
(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) :
measure_theory.set_to_fun μ T hT f = measure_theory.set_to_fun (c • μ) T hT_smul f
theorem
measure_theory.norm_set_to_fun_le_mul_norm
{α : 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 μ))
(hC : 0 ≤ C) :
theorem
measure_theory.norm_set_to_fun_le_mul_norm'
{α : 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 μ)) :
‖measure_theory.set_to_fun μ T hT ⇑f‖ ≤ linear_order.max C 0 * ‖f‖
theorem
measure_theory.norm_set_to_fun_le
{α : 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)
(hf : measure_theory.integrable f μ)
(hC : 0 ≤ C) :
‖measure_theory.set_to_fun μ T hT f‖ ≤ C * ‖measure_theory.integrable.to_L1 f hf‖
theorem
measure_theory.norm_set_to_fun_le'
{α : 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)
(hf : measure_theory.integrable f μ) :
‖measure_theory.set_to_fun μ T hT f‖ ≤ linear_order.max C 0 * ‖measure_theory.integrable.to_L1 f hf‖
theorem
measure_theory.tendsto_set_to_fun_of_dominated_convergence
{α : 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)
{fs : ℕ → α → E}
{f : α → E}
(bound : α → ℝ)
(fs_measurable : ∀ (n : ℕ), measure_theory.ae_strongly_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 (nhds (f a))) :
filter.tendsto (λ (n : ℕ), measure_theory.set_to_fun μ T hT (fs n)) filter.at_top (nhds (measure_theory.set_to_fun μ T hT f))
Lebesgue dominated convergence theorem provides sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their image by
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.
theorem
measure_theory.tendsto_set_to_fun_filter_of_dominated_convergence
{α : 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}
{l : filter ι}
[l.is_countably_generated]
{fs : ι → α → E}
{f : α → E}
(bound : α → ℝ)
(hfs_meas : ∀ᶠ (n : ι) in l, measure_theory.ae_strongly_measurable (fs n) μ)
(h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a)
(bound_integrable : measure_theory.integrable bound μ)
(h_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ι), fs n a) l (nhds (f a))) :
filter.tendsto (λ (n : ι), measure_theory.set_to_fun μ T hT (fs n)) l (nhds (measure_theory.set_to_fun μ T hT f))
Lebesgue dominated convergence theorem for filters with a countable basis
theorem
measure_theory.continuous_within_at_set_to_fun_of_dominated
{α : 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 : ℝ}
{X : Type u_7}
[topological_space X]
[topological_space.first_countable_topology X]
(hT : measure_theory.dominated_fin_meas_additive μ T C)
{fs : X → α → E}
{x₀ : X}
{bound : α → ℝ}
{s : set X}
(hfs_meas : ∀ᶠ (x : X) in nhds_within x₀ s, measure_theory.ae_strongly_measurable (fs x) μ)
(h_bound : ∀ᶠ (x : X) in nhds_within x₀ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : measure_theory.integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, continuous_within_at (λ (x : X), fs x a) s x₀) :
continuous_within_at (λ (x : X), measure_theory.set_to_fun μ T hT (fs x)) s x₀
theorem
measure_theory.continuous_at_set_to_fun_of_dominated
{α : 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 : ℝ}
{X : Type u_7}
[topological_space X]
[topological_space.first_countable_topology X]
(hT : measure_theory.dominated_fin_meas_additive μ T C)
{fs : X → α → E}
{x₀ : X}
{bound : α → ℝ}
(hfs_meas : ∀ᶠ (x : X) in nhds x₀, measure_theory.ae_strongly_measurable (fs x) μ)
(h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : measure_theory.integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, continuous_at (λ (x : X), fs x a) x₀) :
continuous_at (λ (x : X), measure_theory.set_to_fun μ T hT (fs x)) x₀
theorem
measure_theory.continuous_on_set_to_fun_of_dominated
{α : 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 : ℝ}
{X : Type u_7}
[topological_space X]
[topological_space.first_countable_topology X]
(hT : measure_theory.dominated_fin_meas_additive μ T C)
{fs : X → α → E}
{bound : α → ℝ}
{s : set X}
(hfs_meas : ∀ (x : X), x ∈ s → measure_theory.ae_strongly_measurable (fs x) μ)
(h_bound : ∀ (x : X), x ∈ s → (∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a))
(bound_integrable : measure_theory.integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, continuous_on (λ (x : X), fs x a) s) :
continuous_on (λ (x : X), measure_theory.set_to_fun μ T hT (fs x)) s
theorem
measure_theory.continuous_set_to_fun_of_dominated
{α : 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 : ℝ}
{X : Type u_7}
[topological_space X]
[topological_space.first_countable_topology X]
(hT : measure_theory.dominated_fin_meas_additive μ T C)
{fs : X → α → E}
{bound : α → ℝ}
(hfs_meas : ∀ (x : X), measure_theory.ae_strongly_measurable (fs x) μ)
(h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : measure_theory.integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, continuous (λ (x : X), fs x a)) :
continuous (λ (x : X), measure_theory.set_to_fun μ T hT (fs x))