Theorem: integrable_Lp_smul_Lq (ForML/LpHoelder.lean)

State before:
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ Integrable (f • g)
Tactic:
rw [← memℒp_one_iff_integrable]
State after:
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ Memℒp (f • g) 1

State before:
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ Memℒp (f • g) 1
Tactic:
exact memL1_Lp_smul_Lq hpq hf hg
State after:
no goals