case pos
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hf : Integrable f
⊢ (∫ (x : α), f x • c ∂μ) = (∫ (x : α), f x ∂μ) • c

case neg
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hf : ¬Integrable f
⊢ (∫ (x : α), f x • c ∂μ) = (∫ (x : α), f x ∂μ) • c
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
⊢ (∫ (x : α), f x • c ∂μ) = (∫ (x : α), f x ∂μ) • c
by_cases hf : Integrable f μ
no goals
case pos
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hf : Integrable f
⊢ (∫ (x : α), f x • c ∂μ) = (∫ (x : α), f x ∂μ) • c
exact ((1 : 𝕜 →L[𝕜] 𝕜).smulRight c).integral_comp_comm hf
case pos
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hf : ¬Integrable f
hc : c = 0
⊢ (∫ (x : α), f x • c ∂μ) = (∫ (x : α), f x ∂μ) • c

case neg
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hf : ¬Integrable f
hc : ¬c = 0
⊢ (∫ (x : α), f x • c ∂μ) = (∫ (x : α), f x ∂μ) • c
case neg
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hf : ¬Integrable f
⊢ (∫ (x : α), f x • c ∂μ) = (∫ (x : α), f x ∂μ) • c
by_cases hc : c = 0
case neg
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hf : ¬Integrable f
hc : ¬c = 0
⊢ ¬Integrable fun x => f x • c
case neg
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hf : ¬Integrable f
hc : ¬c = 0
⊢ (∫ (x : α), f x • c ∂μ) = (∫ (x : α), f x ∂μ) • c
rw [integral_undef hf, integral_undef, zero_smul]
case neg
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hf : ¬Integrable f
hc : ¬c = 0
⊢ ¬Integrable fun x => f x
case neg
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hf : ¬Integrable f
hc : ¬c = 0
⊢ ¬Integrable fun x => f x • c
rw [integrable_smul_const hc]
no goals
case neg
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hf : ¬Integrable f
hc : ¬c = 0
⊢ ¬Integrable fun x => f x
simp_rw [hf]
no goals
case pos
α : Type u_3
β : Type ?u.4211708
E : Type u_2
F : Type ?u.4211714
inst✝¹¹ : MeasurableSpace α
ι : Type ?u.4211720
inst✝¹⁰ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜✝ : Type ?u.4326528
inst✝⁹ : IsROrC 𝕜✝
inst✝⁸ : NormedSpace 𝕜✝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜✝ F
p : ℝ≥0∞
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace F
inst✝² : NormedSpace ℝ F
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hf : ¬Integrable f
hc : c = 0
⊢ (∫ (x : α), f x • c ∂μ) = (∫ (x : α), f x ∂μ) • c
simp only [hc, integral_zero, smul_zero]