-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem lintegral_mul_norm_pow_le {α} [MeasurableSpace α] {μ : Measure α}
    {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
    {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) (hpq : p + q = 1) :
    ∫⁻ a, f a ^ p * g a ^ q ∂μ ≤ (∫⁻ a, f a ∂μ) ^ p * (∫⁻ a, g a ∂μ) ^ q

Proof state:
case inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
q : ℝ
hq : 0 ≤ q
hp : 0 ≤ 0
hpq : q = 1
⊢ ∫⁻ (a : α), f a ^ 0 * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ 0 * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
simp [hpq]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
⊢ p < 1

Tactic:
linarith

Result:
no goals

Proof state:
case inr.inr
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
have h2p : 1 < 1 / p := by
  rw [one_div, one_lt_inv₀ hp]
  linarith

Result:
case inr.inr
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
h2p : 1 < 1 / p
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Proof state:
case inr
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
rcases hq.eq_or_lt with rfl|hq

Result:
case inr.inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p : ℝ
hp✝ : 0 ≤ p
hp : 0 < p
hq : 0 ≤ 0
hpq : p + 0 = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ 0 ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ 0

case inr.inr
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Proof state:
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
⊢ 1 < 1 / p

Tactic:
rw [one_div, one_lt_inv₀ hp]

Result:
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
⊢ p < 1

Proof state:
case inr.inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p : ℝ
hp✝ : 0 ≤ p
hp : 0 < p
hq : 0 ≤ 0
hpq : p = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ 0 ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ 0

Tactic:
simp [hpq]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
h2p : 1 < 1 / p
⊢ (1 / p)⁻¹ + (1 / q)⁻¹ = 1

Tactic:
simp [hp.ne', hq.ne', hpq]

Result:
no goals

Proof state:
case inr.inr
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
h2p : 1 < 1 / p
h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1
this :
  ∫⁻ (a : α), ((fun x => f x ^ p) * fun x => g x ^ q) a ∂μ ≤
    (∫⁻ (a : α), (f a ^ p) ^ (1 / p) ∂μ) ^ (1 / (1 / p)) * (∫⁻ (a : α), (g a ^ q) ^ (1 / q) ∂μ) ^ (1 / (1 / q))
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
simpa [← ENNReal.rpow_mul, hp.ne', hq.ne'] using this

Result:
no goals

Proof state:
case inr.inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p : ℝ
hp✝ : 0 ≤ p
hp : 0 < p
hq : 0 ≤ 0
hpq : p + 0 = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ 0 ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ 0

Tactic:
rw [add_zero] at hpq

Result:
case inr.inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p : ℝ
hp✝ : 0 ≤ p
hp : 0 < p
hq : 0 ≤ 0
hpq : p = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ 0 ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ 0

Proof state:
case inr.inr
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
h2p : 1 < 1 / p
h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
have := ENNReal.lintegral_mul_le_Lp_mul_Lq μ ⟨h2p, h2pq⟩ (hf.pow_const p) (hg.pow_const q)

Result:
case inr.inr
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
h2p : 1 < 1 / p
h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1
this :
  ∫⁻ (a : α), ((fun x => f x ^ p) * fun x => g x ^ q) a ∂μ ≤
    (∫⁻ (a : α), (f a ^ p) ^ (1 / p) ∂μ) ^ (1 / (1 / p)) * (∫⁻ (a : α), (g a ^ q) ^ (1 / q) ∂μ) ^ (1 / (1 / q))
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Proof state:
case inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
q : ℝ
hq : 0 ≤ q
hp : 0 ≤ 0
hpq : 0 + q = 1
⊢ ∫⁻ (a : α), f a ^ 0 * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ 0 * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
rw [zero_add] at hpq

Result:
case inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
q : ℝ
hq : 0 ≤ q
hp : 0 ≤ 0
hpq : q = 1
⊢ ∫⁻ (a : α), f a ^ 0 * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ 0 * (∫⁻ (a : α), g a ∂μ) ^ q

Proof state:
case inr.inr
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
h2p : 1 < 1 / p
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
have h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1 := by simp [hp.ne', hq.ne', hpq]

Result:
case inr.inr
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
h2p : 1 < 1 / p
h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Proof state:
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
rcases hp.eq_or_lt with rfl|hp

Result:
case inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
q : ℝ
hq : 0 ≤ q
hp : 0 ≤ 0
hpq : 0 + q = 1
⊢ ∫⁻ (a : α), f a ^ 0 * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ 0 * (∫⁻ (a : α), g a ∂μ) ^ q

case inr
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q