α : Type u_1
E : Type ?u.748247
F : Type ?u.748250
F' : Type ?u.748253
G : Type ?u.748256
𝕜 : Type ?u.748259
p : ℝ≥0∞
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup F'
inst✝⁷ : NormedSpace ℝ F'
inst✝⁶ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
G'' : Type u_2
G' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : 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 : { x // x ∈ simpleFunc G'' 1 μ }
hfg✝ : f ≤ g
hfg : 0 ≤ g - f
⊢ 0 ≤ setToL1S T g - setToL1S T f
α : Type u_1
E : Type ?u.748247
F : Type ?u.748250
F' : Type ?u.748253
G : Type ?u.748256
𝕜 : Type ?u.748259
p : ℝ≥0∞
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup F'
inst✝⁷ : NormedSpace ℝ F'
inst✝⁶ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
G'' : Type u_2
G' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : 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 : { x // x ∈ simpleFunc G'' 1 μ }
hfg : f ≤ g
⊢ setToL1S T f ≤ setToL1S T g
rw [← sub_nonneg] at hfg ⊢
α : Type u_1
E : Type ?u.748247
F : Type ?u.748250
F' : Type ?u.748253
G : Type ?u.748256
𝕜 : Type ?u.748259
p : ℝ≥0∞
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup F'
inst✝⁷ : NormedSpace ℝ F'
inst✝⁶ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
G'' : Type u_2
G' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : 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 : { x // x ∈ simpleFunc G'' 1 μ }
hfg✝ : f ≤ g
hfg : 0 ≤ g - f
⊢ 0 ≤ setToL1S (fun s => T s) (g - f)
α : Type u_1
E : Type ?u.748247
F : Type ?u.748250
F' : Type ?u.748253
G : Type ?u.748256
𝕜 : Type ?u.748259
p : ℝ≥0∞
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup F'
inst✝⁷ : NormedSpace ℝ F'
inst✝⁶ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
G'' : Type u_2
G' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : 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 : { x // x ∈ simpleFunc G'' 1 μ }
hfg✝ : f ≤ g
hfg : 0 ≤ g - f
⊢ 0 ≤ setToL1S T g - setToL1S T f
rw [← setToL1S_sub h_zero h_add]
no goals
α : Type u_1
E : Type ?u.748247
F : Type ?u.748250
F' : Type ?u.748253
G : Type ?u.748256
𝕜 : Type ?u.748259
p : ℝ≥0∞
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup F'
inst✝⁷ : NormedSpace ℝ F'
inst✝⁶ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
G'' : Type u_2
G' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : 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 : { x // x ∈ simpleFunc G'' 1 μ }
hfg✝ : f ≤ g
hfg : 0 ≤ g - f
⊢ 0 ≤ setToL1S (fun s => T s) (g - f)
exact setToL1S_nonneg h_zero h_add hT_nonneg hfg