case pos
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : Integrable f
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

case neg
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
by_cases hf : Integrable f μ
no goals
case pos
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : Integrable f
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
rw [setToFun_eq hT hf, setToFun_eq hT, Integrable.toL1_smul',
  L1.setToL1_smul hT h_smul c _]
case pos
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f
hr : c = 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

case neg
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f
hr : ¬c = 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
case neg
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
by_cases hr : c = 0
case pos
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f
hr : c = 0
⊢ setToFun μ T hT (0 • f) = 0 • setToFun μ T hT f
case pos
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f
hr : c = 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
rw [hr]
no goals
case pos
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f
hr : c = 0
⊢ setToFun μ T hT (0 • f) = 0 • setToFun μ T hT f
simp
case neg
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f
hr : ¬c = 0
hf' : ¬Integrable (c • f)
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
case neg
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f
hr : ¬c = 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have hf' : ¬Integrable (c • f) μ := by rwa [integrable_smul_iff hr f]
no goals
case neg
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f
hr : ¬c = 0
hf' : ¬Integrable (c • f)
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
rw [setToFun_undef hT hf, setToFun_undef hT hf', smul_zero]
no goals
α : Type u_4
E : Type u_2
F : Type u_3
F' : Type ?u.1468982
G : Type ?u.1468985
𝕜 : Type u_1
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
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), ↑(T s) (c • x) = c • ↑(T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f
hr : ¬c = 0
⊢ ¬Integrable (c • f)
rwa [integrable_smul_iff hr f]