case pos
α : Type u_1
E : Type u_2
F : Type ?u.1515415
F' : Type ?u.1515418
G : Type ?u.1515421
𝕜 : Type ?u.1515424
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✝⁵ : CompleteSpace F
T✝ T'✝ T'' : Set α → E →L[ℝ] F
C✝ C'✝ C'' : ℝ
f✝ g : α → E
G' : Type ?u.1517653
G'' : Type u_3
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : 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
hf : Integrable f
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f

case neg
α : Type u_1
E : Type u_2
F : Type ?u.1515415
F' : Type ?u.1515418
G : Type ?u.1515421
𝕜 : Type ?u.1515424
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✝⁵ : CompleteSpace F
T✝ T'✝ T'' : Set α → E →L[ℝ] F
C✝ C'✝ C'' : ℝ
f✝ g : α → E
G' : Type ?u.1517653
G'' : Type u_3
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : 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
hf : ¬Integrable f
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f
α : Type u_1
E : Type u_2
F : Type ?u.1515415
F' : Type ?u.1515418
G : Type ?u.1515421
𝕜 : Type ?u.1515424
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✝⁵ : CompleteSpace F
T✝ T'✝ T'' : Set α → E →L[ℝ] F
C✝ C'✝ C'' : ℝ
f✝ g : α → E
G' : Type ?u.1517653
G'' : Type u_3
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : 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
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f
by_cases hf : Integrable f μ
case pos
α : Type u_1
E : Type u_2
F : Type ?u.1515415
F' : Type ?u.1515418
G : Type ?u.1515421
𝕜 : Type ?u.1515424
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✝⁵ : CompleteSpace F
T✝ T'✝ T'' : Set α → E →L[ℝ] F
C✝ C'✝ C'' : ℝ
f✝ g : α → E
G' : Type ?u.1517653
G'' : Type u_3
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : 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
hf : Integrable f
⊢ ↑(L1.setToL1 hT) (Integrable.toL1 f hf) ≤ ↑(L1.setToL1 hT') (Integrable.toL1 f hf)
case pos
α : Type u_1
E : Type u_2
F : Type ?u.1515415
F' : Type ?u.1515418
G : Type ?u.1515421
𝕜 : Type ?u.1515424
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✝⁵ : CompleteSpace F
T✝ T'✝ T'' : Set α → E →L[ℝ] F
C✝ C'✝ C'' : ℝ
f✝ g : α → E
G' : Type ?u.1517653
G'' : Type u_3
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : 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
hf : Integrable f
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f
simp_rw [setToFun_eq _ hf]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.1515415
F' : Type ?u.1515418
G : Type ?u.1515421
𝕜 : Type ?u.1515424
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✝⁵ : CompleteSpace F
T✝ T'✝ T'' : Set α → E →L[ℝ] F
C✝ C'✝ C'' : ℝ
f✝ g : α → E
G' : Type ?u.1517653
G'' : Type u_3
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : 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
hf : Integrable f
⊢ ↑(L1.setToL1 hT) (Integrable.toL1 f hf) ≤ ↑(L1.setToL1 hT') (Integrable.toL1 f hf)
exact L1.setToL1_mono_left' hT hT' hTT' _
case neg
α : Type u_1
E : Type u_2
F : Type ?u.1515415
F' : Type ?u.1515418
G : Type ?u.1515421
𝕜 : Type ?u.1515424
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✝⁵ : CompleteSpace F
T✝ T'✝ T'' : Set α → E →L[ℝ] F
C✝ C'✝ C'' : ℝ
f✝ g : α → E
G' : Type ?u.1517653
G'' : Type u_3
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : 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
hf : ¬Integrable f
⊢ 0 ≤ 0
case neg
α : Type u_1
E : Type u_2
F : Type ?u.1515415
F' : Type ?u.1515418
G : Type ?u.1515421
𝕜 : Type ?u.1515424
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✝⁵ : CompleteSpace F
T✝ T'✝ T'' : Set α → E →L[ℝ] F
C✝ C'✝ C'' : ℝ
f✝ g : α → E
G' : Type ?u.1517653
G'' : Type u_3
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : 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
hf : ¬Integrable f
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f
simp_rw [setToFun_undef _ hf]
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.1515415
F' : Type ?u.1515418
G : Type ?u.1515421
𝕜 : Type ?u.1515424
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✝⁵ : CompleteSpace F
T✝ T'✝ T'' : Set α → E →L[ℝ] F
C✝ C'✝ C'' : ℝ
f✝ g : α → E
G' : Type ?u.1517653
G'' : Type u_3
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : 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
hf : ¬Integrable f
⊢ 0 ≤ 0
rfl