α : Type u_3
β : Type u_2
γ : Type ?u.969961
δ : Type ?u.969964
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ Memℒp (fun x => f x • g x) 1
α : Type u_3
β : Type u_2
γ : Type ?u.969961
δ : Type ?u.969964
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Integrable f
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ Integrable fun x => f x • g x
rw [← memℒp_one_iff_integrable] at *
α : Type u_3
β : Type u_2
γ : Type ?u.969961
δ : Type ?u.969964
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ snorm (fun x => f x • g x) 1 μ < ⊤
α : Type u_3
β : Type u_2
γ : Type ?u.969961
δ : Type ?u.969964
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ Memℒp (fun x => f x • g x) 1
refine' ⟨hf.1.smul g_ae_strongly_measurable, _⟩
α : Type u_3
β : Type u_2
γ : Type ?u.969961
δ : Type ?u.969964
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
h : 1 / 1 = 1 / 1 + 1 / ⊤
⊢ snorm (fun x => f x • g x) 1 μ < ⊤
α : Type u_3
β : Type u_2
γ : Type ?u.969961
δ : Type ?u.969964
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ snorm (fun x => f x • g x) 1 μ < ⊤
have h : (1 : ℝ≥0∞) / 1 = 1 / 1 + 1 / ∞ := by norm_num
α : Type u_3
β : Type u_2
γ : Type ?u.969961
δ : Type ?u.969964
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
h : 1 / 1 = 1 / 1 + 1 / ⊤
hg' : snorm g ⊤ μ ≠ ⊤
⊢ snorm (fun x => f x • g x) 1 μ < ⊤
α : Type u_3
β : Type u_2
γ : Type ?u.969961
δ : Type ?u.969964
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
h : 1 / 1 = 1 / 1 + 1 / ⊤
⊢ snorm (fun x => f x • g x) 1 μ < ⊤
have hg' : snorm g ∞ μ ≠ ∞ := by rwa [snorm_exponent_top]
no goals
α : Type u_3
β : Type u_2
γ : Type ?u.969961
δ : Type ?u.969964
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
h : 1 / 1 = 1 / 1 + 1 / ⊤
hg' : snorm g ⊤ μ ≠ ⊤
⊢ snorm (fun x => f x • g x) 1 μ < ⊤
calc
  snorm (fun x : α => f x • g x) 1 μ ≤ _ :=
    MeasureTheory.snorm_smul_le_mul_snorm g_ae_strongly_measurable hf.1 h
  _ < ∞ := ENNReal.mul_lt_top hf.2.ne hg'
no goals
α : Type u_3
β : Type u_2
γ : Type ?u.969961
δ : Type ?u.969964
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ 1 / 1 = 1 / 1 + 1 / ⊤
norm_num
no goals
α : Type u_3
β : Type u_2
γ : Type ?u.969961
δ : Type ?u.969964
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
h : 1 / 1 = 1 / 1 + 1 / ⊤
⊢ snorm g ⊤ μ ≠ ⊤
rwa [snorm_exponent_top]