α : Type u_1
E : Type ?u.5158781
F : Type ?u.5158784
G : Type ?u.5158787
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
𝕜 : Type ?u.5387273
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
K : Type u_2
inst✝ : IsROrC K
f : α → K
⊢ Memℒp (fun x => ↑IsROrC.re (f x)) p ∧ Memℒp (fun x => ↑IsROrC.im (f x)) p → Memℒp f p
α : Type u_1
E : Type ?u.5158781
F : Type ?u.5158784
G : Type ?u.5158787
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
𝕜 : Type ?u.5387273
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
K : Type u_2
inst✝ : IsROrC K
f : α → K
⊢ Memℒp (fun x => ↑IsROrC.re (f x)) p ∧ Memℒp (fun x => ↑IsROrC.im (f x)) p ↔ Memℒp f p
refine' ⟨_, fun hf => ⟨hf.re, hf.im⟩⟩
case intro
α : Type u_1
E : Type ?u.5158781
F : Type ?u.5158784
G : Type ?u.5158787
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
𝕜 : Type ?u.5387273
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
K : Type u_2
inst✝ : IsROrC K
f : α → K
hre : Memℒp (fun x => ↑IsROrC.re (f x)) p
him : Memℒp (fun x => ↑IsROrC.im (f x)) p
⊢ Memℒp f p
α : Type u_1
E : Type ?u.5158781
F : Type ?u.5158784
G : Type ?u.5158787
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
𝕜 : Type ?u.5387273
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
K : Type u_2
inst✝ : IsROrC K
f : α → K
⊢ Memℒp (fun x => ↑IsROrC.re (f x)) p ∧ Memℒp (fun x => ↑IsROrC.im (f x)) p → Memℒp f p
rintro ⟨hre, him⟩
case h.e'_5
α : Type u_1
E : Type ?u.5158781
F : Type ?u.5158784
G : Type ?u.5158787
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
𝕜 : Type ?u.5387273
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
K : Type u_2
inst✝ : IsROrC K
f : α → K
hre : Memℒp (fun x => ↑IsROrC.re (f x)) p
him : Memℒp (fun x => ↑IsROrC.im (f x)) p
⊢ f = (fun x => ↑(↑IsROrC.re (f x))) + fun x => IsROrC.I * ↑(↑IsROrC.im (f x))
case intro
α : Type u_1
E : Type ?u.5158781
F : Type ?u.5158784
G : Type ?u.5158787
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
𝕜 : Type ?u.5387273
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
K : Type u_2
inst✝ : IsROrC K
f : α → K
hre : Memℒp (fun x => ↑IsROrC.re (f x)) p
him : Memℒp (fun x => ↑IsROrC.im (f x)) p
⊢ Memℒp f p
convert MeasureTheory.Memℒp.add (E := K) hre.ofReal (him.ofReal.const_mul IsROrC.I)
case h.e'_5.h
α : Type u_1
E : Type ?u.5158781
F : Type ?u.5158784
G : Type ?u.5158787
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
𝕜 : Type ?u.5387273
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
K : Type u_2
inst✝ : IsROrC K
f : α → K
hre : Memℒp (fun x => ↑IsROrC.re (f x)) p
him : Memℒp (fun x => ↑IsROrC.im (f x)) p
x : α
⊢ f x = ((fun x => ↑(↑IsROrC.re (f x))) + fun x => IsROrC.I * ↑(↑IsROrC.im (f x))) x
case h.e'_5
α : Type u_1
E : Type ?u.5158781
F : Type ?u.5158784
G : Type ?u.5158787
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
𝕜 : Type ?u.5387273
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
K : Type u_2
inst✝ : IsROrC K
f : α → K
hre : Memℒp (fun x => ↑IsROrC.re (f x)) p
him : Memℒp (fun x => ↑IsROrC.im (f x)) p
⊢ f = (fun x => ↑(↑IsROrC.re (f x))) + fun x => IsROrC.I * ↑(↑IsROrC.im (f x))
ext1 x
no goals
case h.e'_5.h
α : Type u_1
E : Type ?u.5158781
F : Type ?u.5158784
G : Type ?u.5158787
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
𝕜 : Type ?u.5387273
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
K : Type u_2
inst✝ : IsROrC K
f : α → K
hre : Memℒp (fun x => ↑IsROrC.re (f x)) p
him : Memℒp (fun x => ↑IsROrC.im (f x)) p
x : α
⊢ f x = ((fun x => ↑(↑IsROrC.re (f x))) + fun x => IsROrC.I * ↑(↑IsROrC.im (f x))) x
rw [Pi.add_apply, mul_comm, IsROrC.re_add_im]