-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.smul_essSup {𝕜 : Type*} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β]
    {f : α → 𝕜} (hf : Integrable f μ) {g : α → β}
    (g_aestronglyMeasurable : AEStronglyMeasurable g μ) (ess_sup_g : essSup (‖g ·‖ₑ) μ ≠ ∞) :
    Integrable (fun x : α => f x • g x) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤
⊢ eLpNorm g ⊤ μ ≠ ⊤

Tactic:
rwa [eLpNorm_exponent_top]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤
hg' : eLpNorm g ⊤ μ ≠ ⊤
⊢ eLpNorm (fun x => f x • g x) 1 μ < ⊤

Tactic:
calc
  eLpNorm (fun x : α => f x • g x) 1 μ ≤ _ := by
    simpa using MeasureTheory.eLpNorm_smul_le_mul_eLpNorm g_aestronglyMeasurable hf.1
      (p := 1) (q := ∞)
  _ < ∞ := ENNReal.mul_lt_top hf.2 hg'.lt_top

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤
⊢ eLpNorm (fun x => f x • g x) 1 μ < ⊤

Tactic:
have hg' : eLpNorm g ∞ μ ≠ ∞ := by rwa [eLpNorm_exponent_top]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤
hg' : eLpNorm g ⊤ μ ≠ ⊤
⊢ eLpNorm (fun x => f x • g x) 1 μ < ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤
hg' : eLpNorm g ⊤ μ ≠ ⊤
⊢ eLpNorm (fun x => f x • g x) 1 μ ≤ eLpNorm f 1 μ * eLpNorm g ⊤ μ

Tactic:
simpa using MeasureTheory.eLpNorm_smul_le_mul_eLpNorm g_aestronglyMeasurable hf.1
  (p := 1) (q := ∞)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤
⊢ MemLp (fun x => f x • g x) 1 μ

Tactic:
refine ⟨hf.1.smul g_aestronglyMeasurable, ?_⟩

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤
⊢ eLpNorm (fun x => f x • g x) 1 μ < ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Integrable f μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤
⊢ Integrable (fun x => f x • g x) μ

Tactic:
rw [← memLp_one_iff_integrable] at *

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤
⊢ MemLp (fun x => f x • g x) 1 μ