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

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
𝕜 : Type u_6
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
f : α → β
hf : MemLp f 1 μ
g : α → 𝕜
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤
⊢ eLpNorm (fun x => g x • f 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✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
f : α → β
hf : MemLp f 1 μ
g : α → 𝕜
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤
hg' : eLpNorm g ⊤ μ ≠ ⊤
⊢ eLpNorm (fun x => g x • f x) 1 μ < ⊤

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

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

Result:
no goals

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

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

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

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

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

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
𝕜 : Type u_6
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
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✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
f : α → β
hf : Integrable f μ
g : α → 𝕜
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤
⊢ Integrable (fun x => g x • f x) μ

Tactic:
rw [← memLp_one_iff_integrable] at *

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