# mathlib3documentation

measure_theory.integral.set_to_l1

# 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 that `T` is 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 of `T` from 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 = 0`
• `set_to_fun_add_left : set_to_fun μ (T + T') _ f = set_to_fun μ T hT f + set_to_fun μ T' hT' f`
• `set_to_fun_smul_left : set_to_fun μ (λ s, c • (T s)) (hT.smul c) f = c • set_to_fun μ T hT f`
• `set_to_fun_zero : set_to_fun μ T hT (0 : α → E) = 0`
• `set_to_fun_neg : set_to_fun μ T hT (-f) = - set_to_fun μ T hT f` If `f` and `g` are integrable:
• `set_to_fun_add : set_to_fun μ T hT (f + g) = set_to_fun μ T hT f + set_to_fun μ T hT g`
• `set_to_fun_sub : set_to_fun μ T hT (f - g) = set_to_fun μ T hT f - set_to_fun μ T hT g` If `T` is 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 g`
• `set_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' f`
• `set_to_fun_nonneg (hf : 0 ≤ᵐ[μ] f) : 0 ≤ set_to_fun μ T hT f`
• `set_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.

Equations
theorem measure_theory.fin_meas_additive.zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7}  :
theorem measure_theory.fin_meas_additive.add {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} {T T' : set α β} (hT : T) (hT' : T') :
(T + T')
theorem measure_theory.fin_meas_additive.smul {α : Type u_1} {𝕜 : Type u_6} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} {T : set α β} [monoid 𝕜] [ β] (hT : T) (c : 𝕜) :
(λ (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} {T : set α β} {μ' : measure_theory.measure α} (h : (s : set α), μ s = μ' s = ) (hT : T) :
theorem measure_theory.fin_meas_additive.of_smul_measure {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} {T : set α β} (c : ennreal) (hc_ne_top : c ) (hT : T) :
theorem measure_theory.fin_meas_additive.smul_measure {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} {T : set α β} (c : ennreal) (hc_ne_zero : c 0) (hT : T) :
theorem measure_theory.fin_meas_additive.smul_measure_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} {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} {T : set α β} (hT : T) :
T = 0
theorem measure_theory.fin_meas_additive.map_Union_fin_meas_set_eq_sum {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} (T : set α β) (T_empty : T = 0) (h_add : T) {ι : Type u_2} (S : ι set α) (sι : finset ι) (hS_meas : (i : ι), measurable_set (S i)) (hSp : (i : ι), i μ (S i) ) (h_disj : (i : ι), i (j : ι), j i j disjoint (S i) (S j)) :
T ( (i : ι) (H : i sι), S i) = sι.sum (λ (i : ι), T (S i))
def measure_theory.dominated_fin_meas_additive {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) (T : set α β) (C : ) :
Prop

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

Equations
theorem measure_theory.dominated_fin_meas_additive.zero {α : Type u_1} {β : Type u_7} {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} {T : set α β} {C : } (hT : 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} {T : set α β} {C : } {m : measurable_space α} (hT : 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} {T T' : set α β} {C C' : } (hT : C) (hT' : C') :
(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} {T : set α β} {C : } [normed_field 𝕜] [ β] (hT : C) (c : 𝕜) :
(λ (s : set α), c T s) (c * C)
theorem measure_theory.dominated_fin_meas_additive.of_measure_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} {T : set α β} {C : } {μ' : measure_theory.measure α} (h : μ μ') (hT : C) (hC : 0 C) :
theorem measure_theory.dominated_fin_meas_additive.add_measure_right {α : Type u_1} {β : Type u_7} {T : set α β} {C : } {m : measurable_space α} (μ ν : measure_theory.measure α) (hT : C) (hC : 0 C) :
theorem measure_theory.dominated_fin_meas_additive.add_measure_left {α : Type u_1} {β : Type u_7} {T : set α β} {C : } {m : measurable_space α} (μ ν : measure_theory.measure α) (hT : C) (hC : 0 C) :
theorem measure_theory.dominated_fin_meas_additive.of_smul_measure {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} {T : set α β} {C : } (c : ennreal) (hc_ne_top : c ) (hT : C) :
theorem measure_theory.dominated_fin_meas_additive.of_measure_le_smul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_7} {T : set α β} {C : } {μ' : measure_theory.measure α} (c : ennreal) (hc : c ) (h : μ c μ') (hT : C) (hC : 0 C) :
noncomputable def measure_theory.simple_func.set_to_simple_func {α : Type u_1} {F : Type u_3} {F' : Type u_4} [ F] [ F'] {m : measurable_space α} (T : set α (F →L[] F')) (f : F) :
F'

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

Equations
@[simp]
theorem measure_theory.simple_func.set_to_simple_func_zero {α : Type u_1} {F : Type u_3} {F' : Type u_4} [ F] [ F'] {m : measurable_space α} (f : F) :
theorem measure_theory.simple_func.set_to_simple_func_zero' {α : Type u_1} {E : Type u_2} {F' : Type u_4} [ E] [ F'] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F')} (h_zero : (s : set α), μ s < T s = 0) (f : E) (hf : μ) :
@[simp]
theorem measure_theory.simple_func.set_to_simple_func_zero_apply {α : Type u_1} {F : Type u_3} {F' : Type u_4} [ F] [ 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} [ F] [ F'] {m : measurable_space α} (T : set α (F →L[] F')) (f : 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} [ F] [ F'] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (F →L[] F')) (h_add : T) {f : G} (hf : μ) {g : G F} (hg : g 0 = 0) :
= 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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) (h_add : T) {f g : E} (hf : μ) (hg : μ) (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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) (h_zero : (s : set α), μ s = 0 T s = 0) (h_add : T) {f g : E} (hf : μ) (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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T T' : set α (E →L[] F)) (h : (s : set α), μ s < T s = T' s) (f : E) (hf : μ) :
theorem measure_theory.simple_func.set_to_simple_func_add_left {α : Type u_1} {F : Type u_3} {F' : Type u_4} [ F] [ F'] {m : measurable_space α} (T T' : set α (F →L[] F')) {f : F} :
theorem measure_theory.simple_func.set_to_simple_func_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T T' T'' : set α (E →L[] F)) (h_add : (s : set α), μ s < T'' s = T s + T' s) {f : E} (hf : μ) :
theorem measure_theory.simple_func.set_to_simple_func_smul_left {α : Type u_1} {F : Type u_3} {F' : Type u_4} [ F] [ F'] {m : measurable_space α} (T : set α (F →L[] F')) (c : ) (f : F) :
theorem measure_theory.simple_func.set_to_simple_func_smul_left' {α : Type u_1} {E : Type u_2} {F' : Type u_4} [ E] [ F'] {m : measurable_space α} {μ : measure_theory.measure α} (T T' : set α (E →L[] F')) (c : ) (h_smul : (s : set α), μ s < T' s = c T s) {f : E} (hf : μ) :
theorem measure_theory.simple_func.set_to_simple_func_add {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) (h_add : T) {f g : E} (hf : μ) (hg : μ) :
theorem measure_theory.simple_func.set_to_simple_func_neg {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) (h_add : T) {f : E} (hf : μ) :
theorem measure_theory.simple_func.set_to_simple_func_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) (h_add : T) {f g : E} (hf : μ) (hg : μ) :
theorem measure_theory.simple_func.set_to_simple_func_smul_real {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) (h_add : T) (c : ) {f : E} (hf : μ) :
theorem measure_theory.simple_func.set_to_simple_func_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_6} [ F] {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_2} [normed_field 𝕜] [ E] [ E] [ F] (T : set α (E →L[] F)) (h_add : T) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) {f : E} (hf : μ) :
theorem measure_theory.simple_func.set_to_simple_func_mono_left {α : Type u_1} {F : Type u_3} [ F] {G'' : Type u_8} [ G''] {m : measurable_space α} (T T' : set α (F →L[] G'')) (hTT' : (s : set α) (x : F), (T s) x (T' s) x) (f : F) :
theorem measure_theory.simple_func.set_to_simple_func_mono_left' {α : Type u_1} {E : Type u_2} [ E] {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_8} [ G''] (T T' : set α (E →L[] G'')) (hTT' : (s : set α), μ s < (x : E), (T s) x (T' s) x) (f : E) (hf : μ) :
theorem measure_theory.simple_func.set_to_simple_func_nonneg {α : Type u_1} {G' : Type u_7} {G'' : Type u_8} [ G''] [ G'] {m : measurable_space α} (T : set α (G' →L[] G'')) (hT_nonneg : (s : set α) (x : G'), 0 x 0 (T s) x) (f : 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} [ G''] [ G'] (T : set α (G' →L[] G'')) (hT_nonneg : (s : set α), μ s < (x : G'), 0 x 0 (T s) x) (f : G') (hf : 0 f) (hfi : μ) :
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} [ G''] [ G'] {T : set α (G' →L[] G'')} (h_add : T) (hT_nonneg : (s : set α), μ s < (x : G'), 0 x 0 (T s) x) {f g : G'} (hfi : μ) (hgi : μ) (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} [ F] [ F'] {m : measurable_space α} (T : set α (F' →L[] F)) (f : F') :
f.range.sum (λ (x : F'), T (f ⁻¹' {x}) * x)
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} [ F] [ F'] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (F →L[] F')) {C : } (hT_norm : (s : set α), T s C * (μ s).to_real) (f : F) :
C * f.range.sum (λ (x : F), (μ (f ⁻¹' {x})).to_real * x)
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} [ E] [ F'] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F')) {C : } (hT_norm : (s : set α), μ s < T s C * (μ s).to_real) (f : E) (hf : μ) :
C * f.range.sum (λ (x : E), (μ (f ⁻¹' {x})).to_real * x)
theorem measure_theory.simple_func.set_to_simple_func_indicator {α : Type u_1} {F : Type u_3} {F' : Type u_4} [ F] [ 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} [ F] [ 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} [ F] [ 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} {m : measurable_space α} {μ : measure_theory.measure α} (f : ) :
f = (λ (x : G), (μ .to_real * x)
noncomputable def measure_theory.L1.simple_func.set_to_L1s {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) (f : ) :
F

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

Equations
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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) (f : ) :
@[simp]
theorem measure_theory.L1.simple_func.set_to_L1s_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (f : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} (h_zero : (s : set α), μ s < T s = 0) (f : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_congr {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) (h_zero : (s : set α), μ s = 0 T s = 0) (h_add : T) {f g : }  :
theorem measure_theory.L1.simple_func.set_to_L1s_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T T' : set α (E →L[] F)) (h : (s : set α), μ s < T s = T' s) (f : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_congr_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ μ' : measure_theory.measure α} (T : set α (E →L[] F)) (h_zero : (s : set α), μ s = 0 T s = 0) (h_add : T) (hμ : μ.absolutely_continuous μ') (f : ) (f' : μ')) (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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T T' : set α (E →L[] F)) (f : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T T' T'' : set α (E →L[] F)) (h_add : (s : set α), μ s < T'' s = T s + T' s) (f : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_smul_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) (c : ) (f : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T T' : set α (E →L[] F)) (c : ) (h_smul : (s : set α), μ s < T' s = c T s) (f : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_add {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) (h_zero : (s : set α), μ s = 0 T s = 0) (h_add : T) (f g : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_neg {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} (h_zero : (s : set α), μ s = 0 T s = 0) (h_add : T) (f : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} (h_zero : (s : set α), μ s = 0 T s = 0) (h_add : T) (f g : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_smul_real {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) (h_zero : (s : set α), μ s = 0 T s = 0) (h_add : T) (c : ) (f : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_6} [ F] {m : measurable_space α} {μ : measure_theory.measure α} [normed_field 𝕜] {E : Type u_2} [ E] [ E] [ F] (T : set α (E →L[] F)) (h_zero : (s : set α), μ s = 0 T s = 0) (h_add : T) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) (f : ) :
theorem measure_theory.L1.simple_func.norm_set_to_L1s_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T : set α (E →L[] F)) {C : } (hT_norm : (s : set α), μ s < T s C * (μ s).to_real) (f : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_indicator_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {s : set α} (h_zero : (s : set α), μ s = 0 T s = 0) (h_add : T) (hs : measurable_set s) (hμs : μ s < ) (x : E) :
theorem measure_theory.L1.simple_func.set_to_L1s_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} (h_zero : (s : set α), μ s = 0 T s = 0) (h_add : T) (x : E) :
theorem measure_theory.L1.simple_func.set_to_L1s_mono_left {α : Type u_1} {E : Type u_2} [ E] {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_7} [ G''] {T T' : set α (E →L[] G'')} (hTT' : (s : set α) (x : E), (T s) x (T' s) x) (f : ) :
theorem measure_theory.L1.simple_func.set_to_L1s_mono_left' {α : Type u_1} {E : Type u_2} [ E] {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_7} [ G''] {T T' : set α (E →L[] G'')} (hTT' : (s : set α), μ s < (x : E), (T s) x (T' s) x) (f : ) :
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} [ G'] [ G''] {T : set α (G'' →L[] G')} (h_zero : (s : set α), μ s = 0 T s = 0) (h_add : T) (hT_nonneg : (s : set α), μ s < (x : G''), 0 x 0 (T s) x) {f : μ)} (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} [ G'] [ G''] {T : set α (G'' →L[] G')} (h_zero : (s : set α), μ s = 0 T s = 0) (h_add : T) (hT_nonneg : (s : set α), μ s < (x : G''), 0 x 0 (T s) x) {f g : μ)} (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) [ E] [ F] {m : measurable_space α} (μ : measure_theory.measure α) [normed_field 𝕜] [ E] [ F] {T : set α (E →L[] F)} {C : } (hT : C) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) :
→L[𝕜] F

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

Equations
noncomputable def measure_theory.L1.simple_func.set_to_L1s_clm (α : Type u_1) (E : Type u_2) {F : Type u_3} [ E] [ F] {m : measurable_space α} (μ : measure_theory.measure α) {T : set α (E →L[] F)} {C : } (hT : C) :

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

Equations
@[simp]
theorem measure_theory.L1.simple_func.set_to_L1s_clm_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {C : } (hT : C) (f : ) :
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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (h_zero : (s : set α), μ s < T s = 0) (f : ) :
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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' : set α (E →L[] F)} {C C' : } (hT : C) (hT' : C') (h : T = T') (f : ) :
f = 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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' : set α (E →L[] F)} {C C' : } (hT : C) (hT' : C') (h : (s : set α), μ s < T s = T' s) (f : ) :
f = 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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C C' : } {μ' : measure_theory.measure α} (hT : C) (hT' : C') (hμ : μ.absolutely_continuous μ') (f : ) (f' : μ')) (h : f =ᵐ[μ] f') :
f = 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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' : set α (E →L[] F)} {C C' : } (hT : C) (hT' : C') (f : ) :
= f + 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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' T'' : set α (E →L[] F)} {C C' C'' : } (hT : C) (hT' : C') (hT'' : C'') (h_add : (s : set α), μ s < T'' s = T s + T' s) (f : ) :
hT'') f = f + 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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (c : ) (hT : C) (f : ) :
= c f
theorem measure_theory.L1.simple_func.set_to_L1s_clm_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' : set α (E →L[] F)} {C C' : } (c : ) (hT : C) (hT' : C') (h_smul : (s : set α), μ s < T' s = c T s) (f : ) :
hT') f = c f
theorem measure_theory.L1.simple_func.norm_set_to_L1s_clm_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (hC : 0 C) :
theorem measure_theory.L1.simple_func.norm_set_to_L1s_clm_le' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) :
theorem measure_theory.L1.simple_func.set_to_L1s_clm_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (x : E) :
theorem measure_theory.L1.simple_func.set_to_L1s_clm_mono_left {α : Type u_1} {E : Type u_2} [ E] {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_8} [ G''] {T T' : set α (E →L[] G'')} {C C' : } (hT : C) (hT' : C') (hTT' : (s : set α) (x : E), (T s) x (T' s) x) (f : ) :
f hT') f
theorem measure_theory.L1.simple_func.set_to_L1s_clm_mono_left' {α : Type u_1} {E : Type u_2} [ E] {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_8} [ G''] {T T' : set α (E →L[] G'')} {C C' : } (hT : C) (hT' : C') (hTT' : (s : set α), μ s < (x : E), (T s) x (T' s) x) (f : ) :
f 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} [ G''] [ G'] {T : set α (G' →L[] G'')} {C : } (hT : C) (hT_nonneg : (s : set α), μ s < (x : G'), 0 x 0 (T s) x) {f : μ)} (hf : 0 f) :
0 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} [ G''] [ G'] {T : set α (G' →L[] G'')} {C : } (hT : C) (hT_nonneg : (s : set α), μ s < (x : G'), 0 x 0 (T s) x) {f g : μ)} (hfg : f g) :
hT) f hT) g
noncomputable def measure_theory.L1.set_to_L1' {α : Type u_1} {E : Type u_2} {F : Type u_3} (𝕜 : Type u_6) [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} [ E] [ F] {T : set α (E →L[] F)} {C : } (hT : C) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) :
μ) →L[𝕜] F

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

Equations
• h_smul = h_smul).extend 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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) :

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

Equations
• = 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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (f : ) :
= 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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} [ E] [ F] {T : set α (E →L[] F)} {C : } (hT : C) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) (f : μ)) :
= h_smul) f
@[simp]
theorem measure_theory.L1.set_to_L1_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {C : } (hT : C) (f : μ)) :
= 0
theorem measure_theory.L1.set_to_L1_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (h_zero : (s : set α), μ s < T s = 0) (f : μ)) :
= 0
theorem measure_theory.L1.set_to_L1_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T T' : set α (E →L[] F)) {C C' : } (hT : C) (hT' : C') (h : T = T') (f : μ)) :
= f
theorem measure_theory.L1.set_to_L1_congr_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (T T' : set α (E →L[] F)) {C C' : } (hT : C) (hT' : C') (h : (s : set α), μ s < T s = T' s) (f : μ)) :
= f
theorem measure_theory.L1.set_to_L1_add_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' : set α (E →L[] F)} {C C' : } (hT : C) (hT' : C') (f : μ)) :
= + f
theorem measure_theory.L1.set_to_L1_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' T'' : set α (E →L[] F)} {C C' C'' : } (hT : C) (hT' : C') (hT'' : C'') (h_add : (s : set α), μ s < T'' s = T s + T' s) (f : μ)) :
f = + f
theorem measure_theory.L1.set_to_L1_smul_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (c : ) (f : μ)) :
= c
theorem measure_theory.L1.set_to_L1_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' : set α (E →L[] F)} {C C' : } (hT : C) (hT' : C') (c : ) (h_smul : (s : set α), μ s < T' s = c T s) (f : μ)) :
f = c
theorem measure_theory.L1.set_to_L1_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} [ E] [ F] {T : set α (E →L[] F)} {C : } (hT : C) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) (f : μ)) :
(c f) = c
theorem measure_theory.L1.set_to_L1_simple_func_indicator_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) {s : set α} (hs : measurable_set s) (hμs : μ s < ) (x : E) :
= (T s) x
theorem measure_theory.L1.set_to_L1_indicator_const_Lp {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) {s : set α} (hs : measurable_set s) (hμs : μ s ) (x : E) :
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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (x : E) :
theorem measure_theory.L1.set_to_L1_mono_left' {α : Type u_1} {E : Type u_2} [ E] {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_8} [ G''] [complete_space G''] {T T' : set α (E →L[] G'')} {C C' : } (hT : C) (hT' : C') (hTT' : (s : set α), μ s < (x : E), (T s) x (T' s) x) (f : μ)) :
f
theorem measure_theory.L1.set_to_L1_mono_left {α : Type u_1} {E : Type u_2} [ E] {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_8} [ G''] [complete_space G''] {T T' : set α (E →L[] G'')} {C C' : } (hT : C) (hT' : C') (hTT' : (s : set α) (x : E), (T s) x (T' s) x) (f : μ)) :
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} [ G''] [complete_space G''] [ G'] {T : set α (G' →L[] G'')} {C : } (hT : C) (hT_nonneg : (s : set α), μ s < (x : G'), 0 x 0 (T s) x) {f : 1 μ)} (hf : 0 f) :
0
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} [ G''] [complete_space G''] [ G'] {T : set α (G' →L[] G'')} {C : } (hT : C) (hT_nonneg : (s : set α), μ s < (x : G'), 0 x 0 (T s) x) {f g : 1 μ)} (hfg : f 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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) :
theorem measure_theory.L1.norm_set_to_L1_le_mul_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (hC : 0 C) (f : μ)) :
theorem measure_theory.L1.norm_set_to_L1_le_mul_norm' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (f : μ)) :
theorem measure_theory.L1.norm_set_to_L1_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (hC : 0 C) :
theorem measure_theory.L1.norm_set_to_L1_le' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) :
theorem measure_theory.L1.set_to_L1_lipschitz {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) :
theorem measure_theory.L1.tendsto_set_to_L1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (f : μ)) {ι : Type u_4} (fs : ι μ)) {l : filter ι} (hfs : l (nhds f)) :
filter.tendsto (λ (i : ι), (fs i)) l (nhds f))

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

noncomputable def measure_theory.set_to_fun {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} (μ : measure_theory.measure α) (T : set α (E →L[] F)) {C : } (hT : 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
• f = (λ (hf : , (λ (hf : , 0)
theorem measure_theory.set_to_fun_eq {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } {f : α E} (hT : C) (hf : μ) :
f =
theorem measure_theory.L1.set_to_fun_eq_set_to_L1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (f : μ)) :
f =
theorem measure_theory.set_to_fun_undef {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } {f : α E} (hT : C) (hf : ¬) :
f = 0
theorem measure_theory.set_to_fun_non_ae_strongly_measurable {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } {f : α E} (hT : C) (hf : ¬) :
f = 0
theorem measure_theory.set_to_fun_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' : set α (E →L[] F)} {C C' : } (hT : C) (hT' : C') (h : T = T') (f : α E) :
f = hT' f
theorem measure_theory.set_to_fun_congr_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' : set α (E →L[] F)} {C C' : } (hT : C) (hT' : C') (h : (s : set α), μ s < T s = T' s) (f : α E) :
f = hT' f
theorem measure_theory.set_to_fun_add_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' : set α (E →L[] F)} {C C' : } (hT : C) (hT' : C') (f : α E) :
(T + T') _ f = f + hT' f
theorem measure_theory.set_to_fun_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' T'' : set α (E →L[] F)} {C C' C'' : } (hT : C) (hT' : C') (hT'' : C'') (h_add : (s : set α), μ s < T'' s = T s + T' s) (f : α E) :
hT'' f = f + hT' f
theorem measure_theory.set_to_fun_smul_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (c : ) (f : α E) :
(λ (s : set α), c T s) _ f = c f
theorem measure_theory.set_to_fun_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T T' : set α (E →L[] F)} {C C' : } (hT : C) (hT' : C') (c : ) (h_smul : (s : set α), μ s < T' s = c T s) (f : α E) :
hT' f = c f
@[simp]
theorem measure_theory.set_to_fun_zero {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) :
0 = 0
@[simp]
theorem measure_theory.set_to_fun_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {C : } {f : α E} {hT : C} :
f = 0
theorem measure_theory.set_to_fun_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } {f : α E} (hT : C) (h_zero : (s : set α), μ s < T s = 0) :
f = 0
theorem measure_theory.set_to_fun_add {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } {f g : α E} (hT : C) (hf : μ) (hg : μ) :
(f + g) = f + g
theorem measure_theory.set_to_fun_finset_sum' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) {ι : Type u_4} (s : finset ι) {f : ι α E} (hf : (i : ι), i s μ) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
theorem measure_theory.set_to_fun_finset_sum {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) {ι : Type u_4} (s : finset ι) {f : ι α E} (hf : (i : ι), i s μ) :
(λ (a : α), s.sum (λ (i : ι), f i a)) = s.sum (λ (i : ι), (f i))
theorem measure_theory.set_to_fun_neg {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (f : α E) :
(-f) = - f
theorem measure_theory.set_to_fun_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } {f g : α E} (hT : C) (hf : μ) (hg : μ) :
(f - g) = f - g
theorem measure_theory.set_to_fun_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } [ E] [ F] (hT : C) (h_smul : (c : 𝕜) (s : set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) (f : α E) :
(c f) = c f
theorem measure_theory.set_to_fun_congr_ae {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } {f g : α E} (hT : C) (h : f =ᵐ[μ] g) :
f = g
theorem measure_theory.set_to_fun_measure_zero {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } {f : α E} (hT : C) (h : μ = 0) :
f = 0
theorem measure_theory.set_to_fun_measure_zero' {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } {f : α E} (hT : C) (h : (s : set α), μ s < μ s = 0) :
f = 0
theorem measure_theory.set_to_fun_to_L1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } {f : α E} (hT : C) (hf : μ) :
= f
theorem measure_theory.set_to_fun_indicator_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) {s : set α} (hs : measurable_set s) (hμs : μ s ) (x : E) :
(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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) (x : E) :
(λ (_x : α), x) = (T set.univ) x
theorem measure_theory.set_to_fun_mono_left' {α : Type u_1} {E : Type u_2} [ E] {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_8} [ G''] [complete_space G''] {T T' : set α (E →L[] G'')} {C C' : } (hT : C) (hT' : C') (hTT' : (s : set α), μ s < (x : E), (T s) x (T' s) x) (f : α E) :
f hT' f
theorem measure_theory.set_to_fun_mono_left {α : Type u_1} {E : Type u_2} [ E] {m : measurable_space α} {μ : measure_theory.measure α} {G'' : Type u_8} [ G''] [complete_space G''] {T T' : set α (E →L[] G'')} {C C' : } (hT : C) (hT' : C') (hTT' : (s : set α) (x : E), (T s) x (T' s) x) (f : μ)) :
f 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} [ G''] [complete_space G''] [ G'] {T : set α (G' →L[] G'')} {C : } (hT : C) (hT_nonneg : (s : set α), μ s < (x : G'), 0 x 0 (T s) x) {f : α G'} (hf : 0 ≤ᵐ[μ] f) :
0 f
theorem measure_theory.set_to_fun_mono {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {G' : Type u_7} {G'' : Type u_8} [ G''] [complete_space G''] [ G'] {T : set α (G' →L[] G'')} {C : } (hT : C) (hT_nonneg : (s : set α), μ s < (x : G'), 0 x 0 (T s) x) {f g : α G'} (hf : μ) (hg : μ) (hfg : f ≤ᵐ[μ] g) :
f g
@[continuity]
theorem measure_theory.continuous_set_to_fun {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) :
continuous (λ (f : μ)), f)
theorem measure_theory.tendsto_set_to_fun_of_L1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) {ι : Type u_4} (f : α E) (hfi : μ) {fs : ι α E} {l : filter ι} (hfsi : ∀ᶠ (i : ι) in l, μ) (hfs : filter.tendsto (λ (i : ι), ∫⁻ (x : α), fs i x - f x‖₊ μ) l (nhds 0)) :
filter.tendsto (λ (i : ι), (fs i)) l (nhds 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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) [borel_space E] {f : α E} {s : set E} (hfi : μ) (hfm : measurable f) (hs : ∀ᵐ (x : α) μ, f x ) {y₀ : E} (h₀ : y₀ s) (h₀i : measure_theory.integrable (λ (x : α), y₀) μ) :
filter.tendsto (λ (n : ), y₀ h₀ n)) filter.at_top (nhds 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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C : } (hT : C) [borel_space E] {f : α E} (fmeas : measurable f) (hf : μ) (s : set E) (hs : {0} s) :
filter.tendsto (λ (n : ), s 0 _ n)) filter.at_top (nhds hT f))
theorem measure_theory.continuous_L1_to_L1 {α : Type u_1} {G : Type u_5} {m : measurable_space α} {μ μ' : measure_theory.measure α} (c' : ennreal) (hc' : c' ) (hμ'_le : μ' c' μ) :
continuous (λ (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} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C C' : } {μ' : measure_theory.measure α} (c' : ennreal) (hc' : c' ) (hμ'_le : μ' c' μ) (hT : C) (hT' : C') (f : α E) (hfμ : μ) :
f = hT' f
theorem measure_theory.set_to_fun_congr_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C C' : } {μ' : measure_theory.measure α} (c c' : ennreal) (hc : c ) (hc' : c' ) (hμ_le : μ c μ') (hμ'_le : μ' c' μ) (hT : C) (hT' : C') (f : α E) :
f = hT' f
theorem measure_theory.set_to_fun_congr_measure_of_add_right {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C C' : } {μ' : measure_theory.measure α} (hT_add : C') (hT : C) (f : α E) (hf : + μ')) :
measure_theory.set_to_fun + μ') T hT_add f = f
theorem measure_theory.set_to_fun_congr_measure_of_add_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {T : set α (E →L[] F)} {C C' : } {μ' : measure_theory.measure α} (hT_add : C') (hT : C) (f : α E) (hf : + μ')) :
measure_theory.set_to_fun + μ') T hT_add f =