Documentation

Mathlib.MeasureTheory.Integral.FinMeasAdditive

Additivity on measurable sets with finite measure #

Let T : Set α → E →L[ℝ] F be additive for measurable sets with finite measure, in the sense that for s, t two such sets, Disjoint 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 property is named FinMeasAdditive in this file. We also define DominatedFinMeasAdditive, which requires in addition that the norm on every set is less than the measure of the set (up to a multiplicative constant); in Mathlib/MeasureTheory/Integral/SetToL1.lean we extend set functions with this stronger property to integrable (L1) functions.

Main definitions #

FinMeasAdditive μ T: the property that T is additive on measurable sets with finite measure. For two such sets, Disjoint s t → T (s ∪ t) = T s + T t.
DominatedFinMeasAdditive μ T C: FinMeasAdditive μ T ∧ ∀ s, ‖T s‖ ≤ C * μ.real s. This is the property needed to perform the extension from indicators to L1.

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 MeasureTheory.FinMeasAdditive {α : Type u_1} {β : Type u_7} [AddMonoid β] {x✝ : MeasurableSpace α} (μ : Measure α) (T : Set α → β) :

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

Equations

MeasureTheory.FinMeasAdditive μ T = ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → μ s ≠ ⊤ → μ t ≠ ⊤ → Disjoint s t → T (s ∪ t) = T s + T t

Instances For

theorem MeasureTheory.FinMeasAdditive.zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [AddMonoid β] :

FinMeasAdditive μ 0

theorem MeasureTheory.FinMeasAdditive.smul {α : Type u_1} {𝕜 : Type u_6} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} {T : Set α → β} [AddMonoid β] [DistribSMul 𝕜 β] (hT : FinMeasAdditive μ T) (c : 𝕜) :

FinMeasAdditive μ fun (s : Set α) => c • T s

theorem MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} {T : Set α → β} [AddMonoid β] {μ' : Measure α} (h : ∀ (s : Set α), MeasurableSet s → μ s = ⊤ → μ' s = ⊤) (hT : FinMeasAdditive μ T) :

FinMeasAdditive μ' T

theorem MeasureTheory.FinMeasAdditive.add_right_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} {T : Set α → β} [AddMonoid β] {ν : Measure α} (hT : FinMeasAdditive μ T) :

FinMeasAdditive (μ + ν) T

theorem MeasureTheory.FinMeasAdditive.add_left_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} {T : Set α → β} [AddMonoid β] {ν : Measure α} (hT : FinMeasAdditive μ T) :

FinMeasAdditive (ν + μ) T

theorem MeasureTheory.FinMeasAdditive.of_smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} {T : Set α → β} [AddMonoid β] {c : ENNReal} (hc_ne_top : c ≠ ⊤) (hT : FinMeasAdditive (c • μ) T) :

FinMeasAdditive μ T

theorem MeasureTheory.FinMeasAdditive.smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} {T : Set α → β} [AddMonoid β] (c : ENNReal) (hc_ne_zero : c ≠ 0) (hT : FinMeasAdditive μ T) :

FinMeasAdditive (c • μ) T

theorem MeasureTheory.FinMeasAdditive.smul_measure_iff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} {T : Set α → β} [AddMonoid β] (c : ENNReal) (hc_ne_zero : c ≠ 0) (hc_ne_top : c ≠ ⊤) :

FinMeasAdditive (c • μ) T ↔ FinMeasAdditive μ T

theorem MeasureTheory.FinMeasAdditive.map_empty_eq_zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_8} [AddCancelMonoid β] {T : Set α → β} (hT : FinMeasAdditive μ T) :

T ∅ = 0

theorem MeasureTheory.FinMeasAdditive.add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} {T T' : Set α → β} [AddCommMonoid β] (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive μ T') :

FinMeasAdditive μ (T + T')

theorem MeasureTheory.FinMeasAdditive.add_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} {T T' : Set α → β} [AddCommMonoid β] {ν : Measure α} (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive ν T') :

FinMeasAdditive (μ + ν) (T + T')

theorem MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [AddCommMonoid β] (T : Set α → β) (T_empty : T ∅ = 0) (h_add : FinMeasAdditive μ T) {ι : Type u_8} (S : ι → Set α) (sι : Finset ι) (hS_meas : ∀ (i : ι), MeasurableSet (S i)) (hSp : ∀ i ∈ sι, μ (S i) ≠ ⊤) (h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)) :

T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)

theorem MeasureTheory.FinMeasAdditive.neg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} {T : Set α → β} [AddGroup β] (hT : FinMeasAdditive μ T) :

FinMeasAdditive μ (-T)

theorem MeasureTheory.FinMeasAdditive.sub {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} {T T' : Set α → β} [AddCommGroup β] (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive μ T') :

FinMeasAdditive μ (T - T')

def MeasureTheory.DominatedFinMeasAdditive {α : Type u_1} {β : Type u_7} [SeminormedAddCommGroup β] {x✝ : MeasurableSpace α} (μ : Measure α) (T : Set α → β) (C : ℝ) :

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

Equations

MeasureTheory.DominatedFinMeasAdditive μ T C = (MeasureTheory.FinMeasAdditive μ T ∧ ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * μ.real s)

Instances For

theorem MeasureTheory.DominatedFinMeasAdditive.zero {α : Type u_1} {β : Type u_7} [SeminormedAddCommGroup β] {C : ℝ} {m : MeasurableSpace α} (μ : Measure α) (hC : 0 ≤ C) :

DominatedFinMeasAdditive μ 0 C

theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_8} [NormedAddCommGroup β] {T : Set α → β} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s) (hs_zero : μ s = 0) :

T s = 0

theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero {α : Type u_1} {β : Type u_8} [NormedAddCommGroup β] {T : Set α → β} {C : ℝ} {x✝ : MeasurableSpace α} (hT : DominatedFinMeasAdditive 0 T C) {s : Set α} (hs : MeasurableSet s) :

T s = 0

theorem MeasureTheory.DominatedFinMeasAdditive.of_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hC : C ≤ C') :

DominatedFinMeasAdditive μ T C'

theorem MeasureTheory.DominatedFinMeasAdditive.add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T T' : Set α → β} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') :

DominatedFinMeasAdditive μ (T + T') (C + C')

theorem MeasureTheory.DominatedFinMeasAdditive.neg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) :

DominatedFinMeasAdditive μ (-T) C

theorem MeasureTheory.DominatedFinMeasAdditive.smul {α : Type u_1} {𝕜 : Type u_6} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} [SeminormedAddGroup 𝕜] [DistribSMul 𝕜 β] [IsBoundedSMul 𝕜 β] (hT : DominatedFinMeasAdditive μ T C) (c : 𝕜) :

DominatedFinMeasAdditive μ (fun (s : Set α) => c • T s) (‖c‖ * C)

theorem MeasureTheory.DominatedFinMeasAdditive.of_measure_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {μ' : Measure α} (h : μ ≤ μ') (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) :

DominatedFinMeasAdditive μ' T C

theorem MeasureTheory.DominatedFinMeasAdditive.add_measure {α : Type u_1} {m : MeasurableSpace α} {β : Type u_7} [SeminormedAddCommGroup β] {T T' : Set α → β} {C C' : ℝ} (μ ν : Measure α) (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive ν T' C') :

DominatedFinMeasAdditive (μ + ν) (T + T') (max C C')

theorem MeasureTheory.DominatedFinMeasAdditive.sub_measure {α : Type u_1} {m : MeasurableSpace α} {β : Type u_7} [SeminormedAddCommGroup β] {T T' : Set α → β} {C C' : ℝ} (μ ν : Measure α) (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive ν T' C') :

DominatedFinMeasAdditive (μ + ν) (T - T') (max C C')

theorem MeasureTheory.DominatedFinMeasAdditive.add_measure_right {α : Type u_1} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {x✝ : MeasurableSpace α} (μ ν : Measure α) (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) :

DominatedFinMeasAdditive (μ + ν) T C

theorem MeasureTheory.DominatedFinMeasAdditive.add_measure_left {α : Type u_1} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {x✝ : MeasurableSpace α} (μ ν : Measure α) (hT : DominatedFinMeasAdditive ν T C) (hC : 0 ≤ C) :

DominatedFinMeasAdditive (μ + ν) T C

theorem MeasureTheory.DominatedFinMeasAdditive.finsetSum_measure {α : Type u_1} {m : MeasurableSpace α} {β : Type u_7} [SeminormedAddCommGroup β] {ι : Type u_8} {s : Finset ι} (hs : s.Nonempty) (μ : ι → Measure α) (T : ι → Set α → β) (C : ι → ℝ) (hT : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)) :

DominatedFinMeasAdditive (∑ i ∈ s, μ i) (∑ i ∈ s, T i) (s.sup' hs C)

theorem MeasureTheory.DominatedFinMeasAdditive.of_smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {c : ENNReal} (hc_ne_top : c ≠ ⊤) (hT : DominatedFinMeasAdditive (c • μ) T C) :

DominatedFinMeasAdditive μ T (c.toReal * C)

theorem MeasureTheory.DominatedFinMeasAdditive.of_measure_le_smul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {μ' : Measure α} {c : ENNReal} (hc : c ≠ ⊤) (h : μ ≤ c • μ') (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) :

DominatedFinMeasAdditive μ' T (c.toReal * C)

noncomputable def MeasureTheory.SimpleFunc.setToSimpleFunc {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {x✝ : MeasurableSpace α} (T : Set α → F →L[ℝ ] F') (f : SimpleFunc α F) :

F'

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

Equations

MeasureTheory.SimpleFunc.setToSimpleFunc T f = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x

Instances For

@[simp]

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} (f : SimpleFunc α F) :

setToSimpleFunc 0 f = 0

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero' {α : Type u_1} {E : Type u_2} {F' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ ] F'} (h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0) (f : SimpleFunc α E) (hf : Integrable (⇑f) μ) :

setToSimpleFunc T f = 0

@[simp]

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero_apply {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} (T : Set α → F →L[ℝ ] F') :

setToSimpleFunc T 0 = 0

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] [DecidablePred fun (x : F) => x ≠ 0] {m : MeasurableSpace α} (T : Set α → F →L[ℝ ] F') (f : SimpleFunc α F) :

setToSimpleFunc T f = ∑ x ∈ f.range with x ≠ 0, (T (⇑f ⁻¹' {x})) x

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_of_subset {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} [DecidablePred fun (x : F) => x ≠ 0] (T : Set α → F →L[ℝ ] F') (hT : T ∅ = 0) {f : SimpleFunc α F} {s : Finset F} (hs : {x ∈ f.range | x ≠ 0} ⊆ s) :

setToSimpleFunc T f = ∑ x ∈ s, (T (⇑f ⁻¹' {x})) x

The setToSimpleFunc is equal to a sum over any set that includes f.range (except 0).

theorem MeasureTheory.SimpleFunc.map_setToSimpleFunc {α : Type u_1} {F : Type u_3} {F' : Type u_4} {G : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] [NormedAddCommGroup G] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → F →L[ℝ ] F') (h_add : FinMeasAdditive μ T) {f : SimpleFunc α G} (hf : Integrable (⇑f) μ) {g : G → F} (hg : g 0 = 0) :

setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (g x)

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ ] F) (h_add : FinMeasAdditive μ T) {f g : SimpleFunc α E} (hf : Integrable (⇑f) μ) (hg : Integrable (⇑g) μ) (h : Pairwise fun (x y : E) => T (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0) :

setToSimpleFunc T f = setToSimpleFunc T g

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ ] F) (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) {f g : SimpleFunc α E} (hf : Integrable (⇑f) μ) (h : ⇑f =ᵐ[μ] ⇑g) :

setToSimpleFunc T f = setToSimpleFunc T g

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T T' : Set α → E →L[ℝ ] F) (h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s) (f : SimpleFunc α E) (hf : Integrable (⇑f) μ) :

setToSimpleFunc T f = setToSimpleFunc T' f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add_left {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} (T T' : Set α → F →L[ℝ ] F') {f : SimpleFunc α F} :

setToSimpleFunc (T + T') f = setToSimpleFunc T f + setToSimpleFunc T' f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T T' T'' : Set α → E →L[ℝ ] F) (h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s) {f : SimpleFunc α E} (hf : Integrable (⇑f) μ) :

setToSimpleFunc T'' f = setToSimpleFunc T f + setToSimpleFunc T' f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} (T : Set α → F →L[ℝ ] F') (c : ℝ) (f : SimpleFunc α F) :

setToSimpleFunc (fun (s : Set α) => c • T s) f = c • setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left' {α : Type u_1} {E : Type u_2} {F' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} {μ : Measure α} (T T' : Set α → E →L[ℝ ] F') (c : ℝ) (h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s) {f : SimpleFunc α E} (hf : Integrable (⇑f) μ) :

setToSimpleFunc T' f = c • setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ ] F) (h_add : FinMeasAdditive μ T) {f g : SimpleFunc α E} (hf : Integrable (⇑f) μ) (hg : Integrable (⇑g) μ) :

setToSimpleFunc T (f + g) = setToSimpleFunc T f + setToSimpleFunc T g

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_neg {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ ] F) (h_add : FinMeasAdditive μ T) {f : SimpleFunc α E} (hf : Integrable (⇑f) μ) :

setToSimpleFunc T (-f) = -setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ ] F) (h_add : FinMeasAdditive μ T) {f g : SimpleFunc α E} (hf : Integrable (⇑f) μ) (hg : Integrable (⇑g) μ) :

setToSimpleFunc T (f - g) = setToSimpleFunc T f - setToSimpleFunc T g

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_real {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ ] F) (h_add : FinMeasAdditive μ T) (c : ℝ) {f : SimpleFunc α E} (hf : Integrable (⇑f) μ) :

setToSimpleFunc T (c • f) = c • setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {E : Type u_7} [NormedAddCommGroup E] [SMulZeroClass 𝕜 E] [NormedSpace ℝ E] [DistribSMul 𝕜 F] (T : Set α → E →L[ℝ ] F) (h_add : FinMeasAdditive μ T) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (c : 𝕜) {f : SimpleFunc α E} (hf : Integrable (⇑f) μ) :

setToSimpleFunc T (c • f) = c • setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] {m : MeasurableSpace α} (T T' : Set α → F →L[ℝ ] G'') (hTT' : ∀ (s : Set α) (x : F), (T s) x ≤ (T' s) x) (f : SimpleFunc α F) :

setToSimpleFunc T f ≤ setToSimpleFunc T' f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] (T T' : Set α → E →L[ℝ ] G'') (hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x) (f : SimpleFunc α E) (hf : Integrable (⇑f) μ) :

setToSimpleFunc T f ≤ setToSimpleFunc T' f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg {α : Type u_1} {G' : Type u_7} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ G'] {m : MeasurableSpace α} (T : Set α → G' →L[ℝ ] G'') (hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x) (f : SimpleFunc α G') (hf : 0 ≤ f) :

0 ≤ setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ G'] (T : Set α → G' →L[ℝ ] G'') (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) (f : SimpleFunc α G') (hf : 0 ≤ f) (hfi : Integrable (⇑f) μ) :

0 ≤ setToSimpleFunc T f

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ G'] [IsOrderedAddMonoid G'] {T : Set α → G' →L[ℝ ] G''} (h_add : FinMeasAdditive μ T) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) {f g : SimpleFunc α G'} (hfi : Integrable (⇑f) μ) (hgi : Integrable (⇑g) μ) (hfg : f ≤ g) :

setToSimpleFunc T f ≤ setToSimpleFunc T g

theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} (T : Set α → F' →L[ℝ ] F) (f : SimpleFunc α F') :

‖setToSimpleFunc T f‖ ≤ ∑ x ∈ f.range, ‖T (⇑f ⁻¹' {x})‖ * ‖x‖

theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → F →L[ℝ ] F') {C : ℝ} (hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * μ.real s) (f : SimpleFunc α F) :

‖setToSimpleFunc T f‖ ≤ C * ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) * ‖x‖

theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable {α : Type u_1} {E : Type u_2} {F' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F'] [NormedSpace ℝ F'] {m : MeasurableSpace α} {μ : Measure α} (T : Set α → E →L[ℝ ] F') {C : ℝ} (hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * μ.real s) (f : SimpleFunc α E) (hf : Integrable (⇑f) μ) :

‖setToSimpleFunc T f‖ ≤ C * ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) * ‖x‖

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_indicator {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] (T : Set α → F →L[ℝ ] F') (hT_empty : T ∅ = 0) {m : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) (x : F) :

setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s) x

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_const' {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] [Nonempty α] (T : Set α → F →L[ℝ ] F') (x : F) {m : MeasurableSpace α} :

setToSimpleFunc T (const α x) = (T Set.univ) x

theorem MeasureTheory.SimpleFunc.setToSimpleFunc_const {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] (T : Set α → F →L[ℝ ] F') (hT_empty : T ∅ = 0) (x : F) {m : MeasurableSpace α} :

setToSimpleFunc T (const α x) = (T Set.univ) x