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