-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_mul_le_Lp_mul_Lq_of_nonneg {p q : ℝ} (hpq : p.IsConjExponent q) {f g : α → ℝ}
    (hf_nonneg : 0 ≤ᵐ[μ] f) (hg_nonneg : 0 ≤ᵐ[μ] g) (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:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ
⊢ (fun a => g a ^ q) =ᶠ[ae μ] fun a => ‖g a‖ ^ q

Tactic:
filter_upwards [hg_nonneg] with x hxg

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ
x : α
hxg : 0 x ≤ g x
⊢ g x ^ q = ‖g x‖ ^ q

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
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)

Tactic:
have h_left : ∫ a, f a * g a ∂μ = ∫ a, ‖f a‖ * ‖g a‖ ∂μ := by
  refine integral_congr_ae ?_
  filter_upwards [hf_nonneg, hg_nonneg] with x hxf hxg
  rw [Real.norm_of_nonneg hxf, Real.norm_of_nonneg hxg]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
⊢ ∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
⊢ ∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
have h_right_f : ∫ a, f a ^ p ∂μ = ∫ a, ‖f a‖ ^ p ∂μ := by
  refine integral_congr_ae ?_
  filter_upwards [hf_nonneg] with x hxf
  rw [Real.norm_of_nonneg hxf]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ
⊢ ∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
x : α
hxf : 0 x ≤ f x
hxg : 0 x ≤ g x
⊢ f x * g x = ‖f x‖ * ‖g x‖

Tactic:
rw [Real.norm_of_nonneg hxf, Real.norm_of_nonneg hxg]

Result:
no goals