Extension from set functions to integrable simple functions

This file is the first stage in extending a dominated finitely-measure-additive set function T : Set α → E →L[ℝ] F to integrable functions. It defines L1.SimpleFunc.setToL1S on integrable simple functions, proves its algebraic, norm, and order properties, and packages it as the continuous linear map L1.SimpleFunc.setToL1SCLM.

theorem MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m : MeasurableSpace α} {μ : Measure α} (f : ↥(α →₁ₛ[μ] G)) : ‖f‖ = ∑ x ∈ (Lp.simpleFunc.toSimpleFunc f).range, μ.real (⇑(Lp.simpleFunc.toSimpleFunc f) ⁻¹' {x}) * ‖x‖

noncomputable def MeasureTheory.L1.SimpleFunc.setToL1S {α : 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) (f : ↥(α →₁ₛ[μ] E)) : F

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

theorem MeasureTheory.L1.SimpleFunc.setToL1S_eq_setToSimpleFunc {α : 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) (f : ↥(α →₁ₛ[μ] E)) : setToL1S T f = SimpleFunc.setToSimpleFunc T (Lp.simpleFunc.toSimpleFunc f)

@[simp]

theorem MeasureTheory.L1.SimpleFunc.setToL1S_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (f : ↥(α →₁ₛ[μ] E)) : setToL1S 0 f = 0

theorem MeasureTheory.L1.SimpleFunc.setToL1S_zero_left' {α : 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 < ⊤ → T s = 0) (f : ↥(α →₁ₛ[μ] E)) : setToL1S T f = 0

theorem MeasureTheory.L1.SimpleFunc.setToL1S_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 : ↥(α →₁ₛ[μ] E)} (h : ⇑(Lp.simpleFunc.toSimpleFunc f) =ᵐ[μ] ⇑(Lp.simpleFunc.toSimpleFunc g)) : setToL1S T f = setToL1S T g

theorem MeasureTheory.L1.SimpleFunc.setToL1S_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 : ↥(α →₁ₛ[μ] E)) : setToL1S T f = setToL1S T' f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_congr_measure {α : 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) (hμ : μ.AbsolutelyContinuous μ') (f : ↥(α →₁ₛ[μ] E)) (f' : ↥(α →₁ₛ[μ'] E)) (h : ↑↑↑f =ᵐ[μ] ↑↑↑f') : setToL1S T f = setToL1S T f'

setToL1S 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 MeasureTheory.L1.SimpleFunc.setToL1S_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' : Set α → E →L[ℝ] F) (f : ↥(α →₁ₛ[μ] E)) : setToL1S (T + T') f = setToL1S T f + setToL1S T' f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_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 : ↥(α →₁ₛ[μ] E)) : setToL1S T'' f = setToL1S T f + setToL1S T' f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul_left {α : 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) (c : ℝ) (f : ↥(α →₁ₛ[μ] E)) : setToL1S (fun (s : Set α) => c • T s) f = c • setToL1S T f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul_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) (c : ℝ) (h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s) (f : ↥(α →₁ₛ[μ] E)) : setToL1S T' f = c • setToL1S T f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_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_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (f g : ↥(α →₁ₛ[μ] E)) : setToL1S T (f + g) = setToL1S T f + setToL1S T g

theorem MeasureTheory.L1.SimpleFunc.setToL1S_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_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (f : ↥(α →₁ₛ[μ] E)) : setToL1S T (-f) = -setToL1S T f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_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_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (f g : ↥(α →₁ₛ[μ] E)) : setToL1S T (f - g) = setToL1S T f - setToL1S T g

theorem MeasureTheory.L1.SimpleFunc.setToL1S_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_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (c : ℝ) (f : ↥(α →₁ₛ[μ] E)) : setToL1S T (c • f) = c • setToL1S T f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [DistribSMul 𝕜 F] (T : Set α → E →L[ℝ] F) (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (c : 𝕜) (f : ↥(α →₁ₛ[μ] E)) : setToL1S T (c • f) = c • setToL1S T f

theorem MeasureTheory.L1.SimpleFunc.norm_setToL1S_le {α : 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) {C : ℝ} (hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * μ.real s) (f : ↥(α →₁ₛ[μ] E)) : ‖setToL1S T f‖ ≤ C * ‖f‖

theorem MeasureTheory.L1.SimpleFunc.setToL1S_indicatorConst {α : 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} {s : Set α} (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (hs : MeasurableSet s) (hμs : μ s < ⊤) (x : E) : setToL1S T (Lp.simpleFunc.indicatorConst 1 hs ⋯ x) = (T s) x

theorem MeasureTheory.L1.SimpleFunc.setToL1S_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {T : Set α → E →L[ℝ] F} (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (x : E) : setToL1S T (Lp.simpleFunc.indicatorConst 1 ⋯ ⋯ x) = (T Set.univ) x

theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono_left {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_7} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] {T T' : Set α → E →L[ℝ] G''} (hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x) (f : ↥(α →₁ₛ[μ] E)) : setToL1S T f ≤ setToL1S T' f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_7} [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 : ↥(α →₁ₛ[μ] E)) : setToL1S T f ≤ setToL1S T' f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_6} {G'' : Type u_7} [NormedAddCommGroup G'] [PartialOrder G'] [IsOrderedAddMonoid G'] [NormedSpace ℝ G'] [NormedAddCommGroup G''] [PartialOrder G''] [NormedSpace ℝ G''] {T : Set α → G'' →L[ℝ] G'} (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x) {f : ↥(α →₁ₛ[μ] G'')} (hf : 0 ≤ f) : 0 ≤ setToL1S T f

theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_6} {G'' : Type u_7} [NormedAddCommGroup G'] [PartialOrder G'] [IsOrderedAddMonoid G'] [NormedSpace ℝ G'] [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] {T : Set α → G'' →L[ℝ] G'} (h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x) {f g : ↥(α →₁ₛ[μ] G'')} (hfg : f ≤ g) : setToL1S T f ≤ setToL1S T g

noncomputable def MeasureTheory.L1.SimpleFunc.setToL1SCLM' (α : Type u_1) (E : Type u_2) {F : Type u_3} (𝕜 : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} (μ : Measure α) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Module 𝕜 F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) : ↥(α →₁ₛ[μ] E) →L[𝕜] F

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

noncomputable def MeasureTheory.L1.SimpleFunc.setToL1SCLM (α : 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} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) : ↥(α →₁ₛ[μ] E) →L[ℝ] F

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

@[simp]

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {C : ℝ} (hT : DominatedFinMeasAdditive μ 0 C) (f : ↥(α →₁ₛ[μ] E)) : (setToL1SCLM α E μ hT) f = 0

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left' {α : 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} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0) (f : ↥(α →₁ₛ[μ] E)) : (setToL1SCLM α E μ hT) f = 0

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_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} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (h : T = T') (f : ↥(α →₁ₛ[μ] E)) : (setToL1SCLM α E μ hT) f = (setToL1SCLM α E μ hT') f

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_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} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s) (f : ↥(α →₁ₛ[μ] E)) : (setToL1SCLM α E μ hT) f = (setToL1SCLM α E μ hT') f

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_measure {α : 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} {C C' : ℝ} {μ' : Measure α} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ' T C') (hμ : μ.AbsolutelyContinuous μ') (f : ↥(α →₁ₛ[μ] E)) (f' : ↥(α →₁ₛ[μ'] E)) (h : ↑↑↑f =ᵐ[μ] ↑↑↑f') : (setToL1SCLM α E μ hT) f = (setToL1SCLM α E μ' hT') f'

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_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' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (f : ↥(α →₁ₛ[μ] E)) : (setToL1SCLM α E μ ⋯) f = (setToL1SCLM α E μ hT) f + (setToL1SCLM α E μ hT') f

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_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} {C C' C'' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (hT'' : DominatedFinMeasAdditive μ T'' C'') (h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s) (f : ↥(α →₁ₛ[μ] E)) : (setToL1SCLM α E μ hT'') f = (setToL1SCLM α E μ hT) f + (setToL1SCLM α E μ hT') f

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left {α : 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} {C : ℝ} (c : ℝ) (hT : DominatedFinMeasAdditive μ T C) (f : ↥(α →₁ₛ[μ] E)) : (setToL1SCLM α E μ ⋯) f = c • (setToL1SCLM α E μ hT) f

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_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} {C C' : ℝ} (c : ℝ) (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s) (f : ↥(α →₁ₛ[μ] E)) : (setToL1SCLM α E μ hT') f = c • (setToL1SCLM α E μ hT) f

theorem MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le {α : 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} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) : ‖setToL1SCLM α E μ hT‖ ≤ C

theorem MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le' {α : 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} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) : ‖setToL1SCLM α E μ hT‖ ≤ max C 0

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (x : E) : (setToL1SCLM α E μ hT) (Lp.simpleFunc.indicatorConst 1 ⋯ ⋯ x) = (T Set.univ) x

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_7} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x) (f : ↥(α →₁ₛ[μ] E)) : (setToL1SCLM α E μ hT) f ≤ (setToL1SCLM α E μ hT') f

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_7} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x) (f : ↥(α →₁ₛ[μ] E)) : (setToL1SCLM α E μ hT) f ≤ (setToL1SCLM α E μ hT') f

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_6} {G'' : Type u_7} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ G'] {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) {f : ↥(α →₁ₛ[μ] G')} (hf : 0 ≤ f) : 0 ≤ (setToL1SCLM α G' μ hT) f

theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_6} {G'' : Type u_7} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [NormedAddCommGroup G'] [PartialOrder G'] [IsOrderedAddMonoid G'] [NormedSpace ℝ G'] {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) {f g : ↥(α →₁ₛ[μ] G')} (hfg : f ≤ g) : (setToL1SCLM α G' μ hT) f ≤ (setToL1SCLM α G' μ hT) g