α : Type u_2
β : Type ?u.3318321
E : Type ?u.3318324
F : Type ?u.3318327
inst✝⁹ : MeasurableSpace α
ι : Type ?u.3318333
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
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
f : α → 𝕜
hf : Integrable f
⊢ (∫ (a : α), ↑(↑IsROrC.re (f a)) + IsROrC.I • ↑(↑IsROrC.im (f a)) ∂μ) = ∫ (x : α), f x ∂μ

case hf
α : Type u_2
β : Type ?u.3318321
E : Type ?u.3318324
F : Type ?u.3318327
inst✝⁹ : MeasurableSpace α
ι : Type ?u.3318333
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
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
f : α → 𝕜
hf : Integrable f
⊢ Integrable fun x => ↑(↑IsROrC.re (f x))

case hg
α : Type u_2
β : Type ?u.3318321
E : Type ?u.3318324
F : Type ?u.3318327
inst✝⁹ : MeasurableSpace α
ι : Type ?u.3318333
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
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
f : α → 𝕜
hf : Integrable f
⊢ Integrable fun a => IsROrC.I • ↑(↑IsROrC.im (f a))
α : Type u_2
β : Type ?u.3318321
E : Type ?u.3318324
F : Type ?u.3318327
inst✝⁹ : MeasurableSpace α
ι : Type ?u.3318333
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
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
f : α → 𝕜
hf : Integrable f
⊢ (∫ (x : α), ↑(↑IsROrC.re (f x)) ∂μ) + (∫ (x : α), ↑(↑IsROrC.im (f x)) ∂μ) * IsROrC.I = ∫ (x : α), f x ∂μ
rw [mul_comm, ← smul_eq_mul, ← integral_smul, ← integral_add]
case e_f
α : Type u_2
β : Type ?u.3318321
E : Type ?u.3318324
F : Type ?u.3318327
inst✝⁹ : MeasurableSpace α
ι : Type ?u.3318333
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
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
f : α → 𝕜
hf : Integrable f
⊢ (fun a => ↑(↑IsROrC.re (f a)) + IsROrC.I • ↑(↑IsROrC.im (f a))) = fun x => f x
α : Type u_2
β : Type ?u.3318321
E : Type ?u.3318324
F : Type ?u.3318327
inst✝⁹ : MeasurableSpace α
ι : Type ?u.3318333
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
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
f : α → 𝕜
hf : Integrable f
⊢ (∫ (a : α), ↑(↑IsROrC.re (f a)) + IsROrC.I • ↑(↑IsROrC.im (f a)) ∂μ) = ∫ (x : α), f x ∂μ
congr
case e_f.h
α : Type u_2
β : Type ?u.3318321
E : Type ?u.3318324
F : Type ?u.3318327
inst✝⁹ : MeasurableSpace α
ι : Type ?u.3318333
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
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
f : α → 𝕜
hf : Integrable f
x : α
⊢ ↑(↑IsROrC.re (f x)) + IsROrC.I • ↑(↑IsROrC.im (f x)) = f x
case e_f
α : Type u_2
β : Type ?u.3318321
E : Type ?u.3318324
F : Type ?u.3318327
inst✝⁹ : MeasurableSpace α
ι : Type ?u.3318333
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
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
f : α → 𝕜
hf : Integrable f
⊢ (fun a => ↑(↑IsROrC.re (f a)) + IsROrC.I • ↑(↑IsROrC.im (f a))) = fun x => f x
ext1 x
no goals
case e_f.h
α : Type u_2
β : Type ?u.3318321
E : Type ?u.3318324
F : Type ?u.3318327
inst✝⁹ : MeasurableSpace α
ι : Type ?u.3318333
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
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
f : α → 𝕜
hf : Integrable f
x : α
⊢ ↑(↑IsROrC.re (f x)) + IsROrC.I • ↑(↑IsROrC.im (f x)) = f x
rw [smul_eq_mul, mul_comm, IsROrC.re_add_im]
no goals
case hf
α : Type u_2
β : Type ?u.3318321
E : Type ?u.3318324
F : Type ?u.3318327
inst✝⁹ : MeasurableSpace α
ι : Type ?u.3318333
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
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
f : α → 𝕜
hf : Integrable f
⊢ Integrable fun x => ↑(↑IsROrC.re (f x))
exact hf.re.ofReal
no goals
case hg
α : Type u_2
β : Type ?u.3318321
E : Type ?u.3318324
F : Type ?u.3318327
inst✝⁹ : MeasurableSpace α
ι : Type ?u.3318333
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
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
f : α → 𝕜
hf : Integrable f
⊢ Integrable fun a => IsROrC.I • ↑(↑IsROrC.im (f a))
exact hf.im.ofReal.smul (𝕜 := 𝕜) (β := 𝕜) IsROrC.I