-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_mul_norm_le_Lp_mul_Lq {E} [NormedAddCommGroup E] {f g : α → E} {p q : ℝ}
    (hpq : p.IsConjExponent q) (hf : MemLp f (ENNReal.ofReal p) μ)
    (hg : MemLp g (ENNReal.ofReal q) μ) :
    ∫ a, ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ a, ‖f a‖ ^ p ∂μ) ^ (1 / p) * (∫ a, ‖g a‖ ^ q ∂μ) ^ (1 / q)

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x => ‖f x‖ₑ) * fun x => ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) ≠ ⊤

Tactic:
refine ENNReal.mul_ne_top ?_ ?_

Result:
case refine_1.refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x => ‖f x‖ₑ) * fun x => ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≠ ⊤

case refine_1.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x => ‖f x‖ₑ) * fun x => ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) ≠ ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ 0 ≤ᶠ[ae μ] fun a => ‖g a‖ ^ q

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (fun a => ‖g a‖ ^ q) μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ 0 ≤ᶠ[ae μ] fun a => ‖f a‖ ^ p

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (fun a => ‖f a‖ ^ p) μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ 0 ≤ᶠ[ae μ] fun a => ‖f a‖ * ‖g a‖

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (fun a => ‖f a‖ * ‖g a‖) μ

Tactic:
rotate_left

Result:
case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ 0 ≤ᶠ[ae μ] fun a => ‖g a‖ ^ q

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (fun a => ‖g a‖ ^ q) μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ 0 ≤ᶠ[ae μ] fun a => ‖f a‖ ^ p

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (fun a => ‖f a‖ ^ p) μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ 0 ≤ᶠ[ae μ] fun a => ‖f a‖ * ‖g a‖

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (fun a => ‖f a‖ * ‖g a‖) μ

α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x => ‖f x‖ₑ) * fun x => ‖g x‖ₑ) a ∂μ

Tactic:
simp_rw [Pi.mul_apply, ← ofReal_norm_eq_enorm, ENNReal.ofReal_mul (norm_nonneg _)]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x => ‖f x‖ₑ) * fun x => ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) *
        (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal

Tactic:
have h_right_g : ∫⁻ a, .ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ a, ‖g a‖ₑ ^ q ∂μ := by
  refine lintegral_congr fun x => ?_
  rw [← ofReal_norm_eq_enorm, ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hpq.symm.nonneg]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.IsConjExponent q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x => ‖f x‖ₑ) * fun x => ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) *
        (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal