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))
:
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'.
Equations
Instances For
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))
:
@[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))
:
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))
:
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))
:
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))
:
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 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))
:
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))
:
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))
:
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))
:
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))
:
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))
:
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))
:
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))
:
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))
:
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))
:
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)
:
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)
:
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))
:
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))
:
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)
:
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)
:
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)
:
Extend Set α → E →L[ℝ] F to (α →₁ₛ[μ] E) →L[𝕜] F.
Equations
- MeasureTheory.L1.SimpleFunc.setToL1SCLM' α E 𝕜 μ hT h_smul = { toFun := MeasureTheory.L1.SimpleFunc.setToL1S T, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous C ⋯
Instances For
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)
:
Extend Set α → E →L[ℝ] F to (α →₁ₛ[μ] E) →L[ℝ] F.
Equations
- MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT = { toFun := MeasureTheory.L1.SimpleFunc.setToL1S T, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous C ⋯
Instances For
@[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))
:
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))
:
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))
:
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))
:
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')
:
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))
:
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))
:
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))
:
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))
:
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)
:
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)
:
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)
:
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))
:
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))
:
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)
:
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)
: