α : Type u_2
E : Type ?u.6078231
F : Type ?u.6078234
G : Type ?u.6078237
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Memℒp f p
this : ∀ (x : α), ‖↑IsROrC.re (f x)‖ ≤ 1 * ‖f x‖
⊢ Memℒp (fun x => ↑IsROrC.re (f x)) p
α : Type u_2
E : Type ?u.6078231
F : Type ?u.6078234
G : Type ?u.6078237
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Memℒp f p
⊢ Memℒp (fun x => ↑IsROrC.re (f x)) p
have : ∀ x, ‖IsROrC.re (f x)‖ ≤ 1 * ‖f x‖ := by
  intro x
  rw [one_mul]
  exact IsROrC.norm_re_le_norm (f x)
α : Type u_2
E : Type ?u.6078231
F : Type ?u.6078234
G : Type ?u.6078237
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Memℒp f p
this : ∀ (x : α), ‖↑IsROrC.re (f x)‖ ≤ 1 * ‖f x‖
⊢ AEStronglyMeasurable (fun x => ↑IsROrC.re (f x)) μ
α : Type u_2
E : Type ?u.6078231
F : Type ?u.6078234
G : Type ?u.6078237
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Memℒp f p
this : ∀ (x : α), ‖↑IsROrC.re (f x)‖ ≤ 1 * ‖f x‖
⊢ Memℒp (fun x => ↑IsROrC.re (f x)) p
refine' hf.of_le_mul _ (eventually_of_forall this)
no goals
α : Type u_2
E : Type ?u.6078231
F : Type ?u.6078234
G : Type ?u.6078237
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Memℒp f p
this : ∀ (x : α), ‖↑IsROrC.re (f x)‖ ≤ 1 * ‖f x‖
⊢ AEStronglyMeasurable (fun x => ↑IsROrC.re (f x)) μ
exact IsROrC.continuous_re.comp_aestronglyMeasurable hf.1
α : Type u_2
E : Type ?u.6078231
F : Type ?u.6078234
G : Type ?u.6078237
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Memℒp f p
x : α
⊢ ‖↑IsROrC.re (f x)‖ ≤ 1 * ‖f x‖
α : Type u_2
E : Type ?u.6078231
F : Type ?u.6078234
G : Type ?u.6078237
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Memℒp f p
⊢ ∀ (x : α), ‖↑IsROrC.re (f x)‖ ≤ 1 * ‖f x‖
intro x
α : Type u_2
E : Type ?u.6078231
F : Type ?u.6078234
G : Type ?u.6078237
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Memℒp f p
x : α
⊢ ‖↑IsROrC.re (f x)‖ ≤ ‖f x‖
α : Type u_2
E : Type ?u.6078231
F : Type ?u.6078234
G : Type ?u.6078237
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Memℒp f p
x : α
⊢ ‖↑IsROrC.re (f x)‖ ≤ 1 * ‖f x‖
rw [one_mul]
no goals
α : Type u_2
E : Type ?u.6078231
F : Type ?u.6078234
G : Type ?u.6078237
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Memℒp f p
x : α
⊢ ‖↑IsROrC.re (f x)‖ ≤ ‖f x‖
exact IsROrC.norm_re_le_norm (f x)