case pos
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1394453
G : Type ?u.1394456
𝕜 : Type ?u.1394459
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
hT : DominatedFinMeasAdditive μ 0 C
hf : Integrable f
⊢ setToFun μ 0 hT f = 0

case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1394453
G : Type ?u.1394456
𝕜 : Type ?u.1394459
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
hT : DominatedFinMeasAdditive μ 0 C
hf : ¬Integrable f
⊢ setToFun μ 0 hT f = 0
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1394453
G : Type ?u.1394456
𝕜 : Type ?u.1394459
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
hT : DominatedFinMeasAdditive μ 0 C
⊢ setToFun μ 0 hT f = 0
by_cases hf : Integrable f μ
case pos
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1394453
G : Type ?u.1394456
𝕜 : Type ?u.1394459
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
hT : DominatedFinMeasAdditive μ 0 C
hf : Integrable f
⊢ ↑(L1.setToL1 hT) (Integrable.toL1 f hf) = 0
case pos
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1394453
G : Type ?u.1394456
𝕜 : Type ?u.1394459
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
hT : DominatedFinMeasAdditive μ 0 C
hf : Integrable f
⊢ setToFun μ 0 hT f = 0
rw [setToFun_eq hT hf]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1394453
G : Type ?u.1394456
𝕜 : Type ?u.1394459
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
hT : DominatedFinMeasAdditive μ 0 C
hf : Integrable f
⊢ ↑(L1.setToL1 hT) (Integrable.toL1 f hf) = 0
exact L1.setToL1_zero_left hT _
no goals
case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1394453
G : Type ?u.1394456
𝕜 : Type ?u.1394459
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
hT : DominatedFinMeasAdditive μ 0 C
hf : ¬Integrable f
⊢ setToFun μ 0 hT f = 0
exact setToFun_undef hT hf