awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = 0

Tactic:
lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.nonneg hf hf_zero

Premises used: ENNReal.lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero, Real.HolderTriple.nonneg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = 0

Tactic:
exact lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.nonneg hf hf_zero

Premises used: ENNReal.lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero, Real.HolderTriple.nonneg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
pos :
  ∀ (hg_zero : ∫⁻ (a : α), g a ^ q ∂μ = 0),
    ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
neg :
  ∀ (hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0),
    ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
by_cases hg_zero : ∫⁻ a, g a ^ q ∂μ = 0
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ∫⁻ (a : α), g a ^ q ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
Eq.trans_le ?_ zero_le

Premises used: zero_le, Eq.trans_le
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ∫⁻ (a : α), g a ^ q ∂μ = 0
pos : ∫⁻ (a : α), (f * g) a ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
refine Eq.trans_le ?_ zero_le

Premises used: zero_le, Eq.trans_le
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ∫⁻ (a : α), g a ^ q ∂μ = 0
pos : ∫⁻ (a : α), (g * f) a ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = 0

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ∫⁻ (a : α), g a ^ q ∂μ = 0
⊢ ∫⁻ (a : α), (g * f) a ∂μ = 0

Tactic:
lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.symm.nonneg hg hg_zero

Premises used: Real.HolderConjugate.symm, ENNReal.lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero, Real.HolderTriple.nonneg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ∫⁻ (a : α), g a ^ q ∂μ = 0
⊢ ∫⁻ (a : α), (g * f) a ∂μ = 0

Tactic:
exact lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.symm.nonneg hg hg_zero

Premises used: Real.HolderConjugate.symm, ENNReal.lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero, Real.HolderTriple.nonneg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
pos :
  ∀ (hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ∞),
    ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
neg :
  ∀ (hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞),
    ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
by_cases hf_top : ∫⁻ a, f a ^ p ∂μ = ⊤
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.pos hpq.symm.nonneg hf_top hg_zero

Premises used: Real.HolderConjugate.symm, Real.HolderTriple.pos, ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top, Real.HolderTriple.nonneg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
exact lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.pos hpq.symm.nonneg hf_top hg_zero

Premises used: Real.HolderConjugate.symm, Real.HolderTriple.pos, ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top, Real.HolderTriple.nonneg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
pos :
  ∀ (hg_top : ∫⁻ (a : α), g a ^ q ∂μ = ∞),
    ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
neg :
  ∀ (hg_top : ¬∫⁻ (a : α), g a ^ q ∂μ = ∞),
    ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
by_cases hg_top : ∫⁻ a, g a ^ q ∂μ = ⊤
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
hg_top : ∫⁻ (a : α), g a ^ q ∂μ = ∞
pos : ∫⁻ (a : α), (g * f) a ∂μ ≤ (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p)
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
rw [mul_comm, mul_comm ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p))]

Premises used: HDiv.hDiv, HPow.hPow, mul_comm, OfNat.ofNat, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
hg_top : ∫⁻ (a : α), g a ^ q ∂μ = ∞
⊢ ∫⁻ (a : α), (g * f) a ∂μ ≤ (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p)

Tactic:
lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.symm.pos hpq.nonneg hg_top hf_zero

Premises used: Real.HolderConjugate.symm, Real.HolderTriple.pos, ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top, Real.HolderTriple.nonneg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
hg_top : ∫⁻ (a : α), g a ^ q ∂μ = ∞
⊢ ∫⁻ (a : α), (g * f) a ∂μ ≤ (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p)

Tactic:
exact lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.symm.pos hpq.nonneg hg_top hf_zero

Premises used: Real.HolderConjugate.symm, Real.HolderTriple.pos, ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top, Real.HolderTriple.nonneg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
hg_top : ¬∫⁻ (a : α), g a ^ q ∂μ = ∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top hpq hf hf_top hg_top hf_zero hg_zero

Premises used: ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
hg_top : ¬∫⁻ (a : α), g a ^ q ∂μ = ∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
exact ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top hpq hf hf_top hg_top hf_zero hg_zero

Premises used: ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : 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
inl :
  ∀ (hp : LE.le (α := ℝ) 0 0) (hpq : 0 + q = 1),
    ∫⁻ (a : α), HPow.hPow (β := ℝ) (f a) 0 * g a ^ q ∂μ ≤
      HPow.hPow (β := ℝ) (∫⁻ (a : α), f a ∂μ) 0 * (∫⁻ (a : α), g a ∂μ) ^ q
inr : ∀ (hp : 0 < p), ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
rcases hp.eq_or_lt with rfl | hp

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
q : ℝ
hq : 0 ≤ q
hp : LE.le (α := ℝ) 0 0
hpq : 0 + q = 1
⊢ q = 1

Tactic:
rw [zero_add] at hpq

Premises used: zero_add
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
q : ℝ
hq : 0 ≤ q
hp : LE.le (α := ℝ) 0 0
hpq : q = 1
⊢ ∫⁻ (a : α), HPow.hPow (β := ℝ) (f a) 0 * g a ^ q ∂μ ≤
    HPow.hPow (β := ℝ) (∫⁻ (a : α), f a ∂μ) 0 * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
simp [hpq]
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp_1 : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
inr :
  ∀ (hq : LE.le (α := ℝ) 0 0) (hpq : p + 0 = 1),
    ∫⁻ (a : α), f a ^ p * HPow.hPow (β := ℝ) (g a) 0 ∂μ ≤
      (∫⁻ (a : α), f a ∂μ) ^ p * HPow.hPow (β := ℝ) (∫⁻ (a : α), g a ∂μ) 0
inr₁ : ∀ (hq : 0 < q), ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
rcases hq.eq_or_lt with rfl | hq

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p : ℝ
hp_1 : 0 ≤ p
hp : 0 < p
hq : LE.le (α := ℝ) 0 0
hpq : p + 0 = 1
⊢ p = 1

Tactic:
rw [add_zero] at hpq

Premises used: add_zero
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p : ℝ
hp_1 : 0 ≤ p
hp : 0 < p
hq : LE.le (α := ℝ) 0 0
hpq : p = 1
⊢ ∫⁻ (a : α), f a ^ p * HPow.hPow (β := ℝ) (g a) 0 ∂μ ≤
    (∫⁻ (a : α), f a ∂μ) ^ p * HPow.hPow (β := ℝ) (∫⁻ (a : α), g a ∂μ) 0

Tactic:
simp [hpq]
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
rw : p < 1
⊢ 1 < 1 / p

Tactic:
rw [one_div, one_lt_inv₀ hp]

Premises used: one_div, one_lt_inv₀
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
linarith : 1 ≤ p → p + q - 1 + (0 - q) + (1 - p) = 0
⊢ p < 1

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
⊢ 1 < 1 / p

Tactic:
have h2p : 1 < 1 / p := by
    rw [one_div, one_lt_inv₀ hp]
    linarith
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
h2p : 1 < 1 / p
⊢ (1 / p)⁻¹ + (1 / q)⁻¹ = 1

Tactic:
simp [hpq]
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
h2p : 1 < 1 / p
⊢ (1 / p)⁻¹ + (1 / q)⁻¹ = 1

Tactic:
have h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1 := by simp [hpq]
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
h2p : 1 < 1 / p
h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1
⊢ ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (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))

Tactic:
have := ENNReal.lintegral_mul_le_Lp_mul_Lq μ (Real.holderConjugate_iff.mpr ⟨h2p, h2pq⟩)
    (hf.pow_const p) (hg.pow_const q)
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
h2p : 1 < 1 / p
h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1
this :
  ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (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

Premises used: ENNReal.rpow_mul, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ ∅, p i) 1
h2p : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ p i
⊢ ∫⁻ (a : α), ∏ i ∈ ∅, f i a ^ p i ∂μ ≤ ∏ i ∈ ∅, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
simp at hp
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ Insert.insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ Insert.insert i₀ s, p i) 1
h2p : ∀ i ∈ Insert.insert i₀ s, 0 ≤ p i
insert :
  ∀ (h2i₀ : p i₀ = 1),
    ∫⁻ (a : α), ∏ i ∈ Insert.insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ Insert.insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
insert₁ :
  ∀ (h2i₀ : p i₀ ≠ 1),
    ∫⁻ (a : α), ∏ i ∈ Insert.insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ Insert.insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
⊢ ∫⁻ (a : α), ∏ i ∈ Insert.insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ Insert.insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
rcases eq_or_ne (p i₀) 1 with h2i₀ | h2i₀

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ Insert.insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ Insert.insert i₀ s, p i) 1
h2p : ∀ i ∈ Insert.insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
insert :
  ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ ≤
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
⊢ ∫⁻ (a : α), ∏ i ∈ Insert.insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ Insert.insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
simp only [hi₀, not_false_eq_true, prod_insert]

Premises used: Finset.prod_insert, not_false_eq_true
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
⊢ ∀ i ∈ s, p i = 0

Tactic:
simpa [hi₀, h2i₀, sum_eq_zero_iff_of_nonneg (fun i hi ↦ h2p i <| mem_insert_of_mem hi)]
          using hp

Premises used: Finset.sum_eq_zero_iff_of_nonneg, Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
⊢ ∀ i ∈ s, p i = 0

Tactic:
have h2p : ∀ i ∈ s, p i = 0 := by
        simpa [hi₀, h2i₀, sum_eq_zero_iff_of_nonneg (fun i hi ↦ h2p i <| mem_insert_of_mem hi)]
          using hp
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p_1 : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
h2p : ∀ i ∈ s, p i = 0
h : ∀ (x : α), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i x ^ p i) (∏ i ∈ s, 1)
⊢ ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ = ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ

Tactic:
congr! 3 with x
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p_1 : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
h2p : ∀ i ∈ s, p i = 0
x : α
i : ι
hi : i ∈ s
rw : HPow.hPow (β := ℝ) (f i x) 0 = 1
rw₁ rw₂ : Eq (α := ℝ≥0∞) 1 1
⊢ f i x ^ p i = 1

Tactic:
rw [h2p i hi, ENNReal.rpow_zero]

Premises used: ENNReal.rpow_zero
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p_1 : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
h2p : ∀ i ∈ s, p i = 0
x : α
⊢ Eq (α := ℝ≥0∞) (∏ i ∈ s, f i x ^ p i) (∏ i ∈ s, 1)

Tactic:
apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p_1 : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
h2p : ∀ i ∈ s, p i = 0
⊢ ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ ≤ (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, 1

Tactic:
simp [h2i₀]
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p_1 : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
h2p : ∀ i ∈ s, p i = 0
e_a : Eq (α := ℝ≥0∞) (∏ i ∈ s, 1) (∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i)
⊢ (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, 1 = (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p_1 : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
h2p : ∀ i ∈ s, p i = 0
i : ι
hi : i ∈ s
rw : 1 = HPow.hPow (β := ℝ) (∫⁻ (a : α), f i a ∂μ) 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 1 1
⊢ 1 = (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
rw [h2p i hi, ENNReal.rpow_zero]

Premises used: ENNReal.rpow_zero