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 μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
rw : ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ ∂μ + ∫⁻ (a : α), g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1
hf₁ : AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ f a ^ p * (ENNReal.ofReal p)⁻¹) μ
⊢ ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ + g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1

Tactic:
rw [lintegral_add_left']

Premises used: MeasureTheory.lintegral_add_left'
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
hr : (ENNReal.ofReal q)⁻¹ ≠ ∞
⊢ ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ ∂μ + ∫⁻ (a : α), g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1

Tactic:
rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const', hf_norm, hg_norm,
          one_mul, one_mul, hpq.inv_add_inv_ennreal]

Premises used: AEMeasurable.pow_const, MeasureTheory.lintegral_mul_const'', Real.HolderConjugate.inv_add_inv_ennreal, MeasureTheory.lintegral_mul_const', one_mul
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ (ENNReal.ofReal q)⁻¹ ≠ ∞

Tactic:
simp [hpq.symm.pos]

Premises used: Real.HolderConjugate.symm, Real.HolderTriple.pos
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ f a ^ p * (ENNReal.ofReal p)⁻¹) μ

Tactic:
(hf.pow_const _).mul_const _

Premises used: AEMeasurable.pow_const, AEMeasurable.mul_const
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ f a ^ p * (ENNReal.ofReal p)⁻¹) μ

Tactic:
exact (hf.pow_const _).mul_const _

Premises used: AEMeasurable.pow_const, AEMeasurable.mul_const
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
a : ∫⁻ (a : α), f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ = 1
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ 1

Tactic:
calc
    (∫⁻ a : α, (f * g) a ∂μ) ≤
        ∫⁻ a : α, f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ :=
      lintegral_mono fun a => young_inequality (f a) (g a) hpq
    _ = 1 := by
      simp only [div_eq_mul_inv]
      rw [lintegral_add_left']
      · rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const', hf_norm, hg_norm,
          one_mul, one_mul, hpq.inv_add_inv_ennreal]
        simp [hpq.symm.pos]
      · exact (hf.pow_const _).mul_const _

Premises used: HMul.hMul, ENNReal.ofReal, MeasureTheory.lintegral_mono, ENNReal.young_inequality, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
a : α
⊢ f a = funMulInvSnorm f p μ a * (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)

Tactic:
simp [funMulInvSnorm, mul_assoc, ENNReal.inv_mul_cancel, hf_nonzero, hf_top]

Premises used: mul_assoc, ENNReal.inv_mul_cancel, ENNReal.funMulInvSnorm
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
rw : f a ^ p * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
⊢ funMulInvSnorm f p μ a ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

Tactic:
rw [funMulInvSnorm, mul_rpow_of_nonneg _ _ (le_of_lt hp0)]

Premises used: ENNReal.mul_rpow_of_nonneg, le_of_lt, ENNReal.funMulInvSnorm
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
h_inv_rpow : ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
rw rw₁ : f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
⊢ f a ^ p * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

Tactic:
rw [h_inv_rpow]
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
suffices : ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
⊢ f a ^ p * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

Tactic:
suffices h_inv_rpow : ((∫⁻ c : α, f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ c : α, f c ^ p ∂μ)⁻¹ by
    rw [h_inv_rpow]
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
rw : (((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)) ^ p)⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
rw₁ : ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p * p))⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
rw₂ : (HPow.hPow (β := ℝ) (∫⁻ (c : α), f c ^ p ∂μ) 1)⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
rw₃ rw₄ : (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
⊢ ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

Tactic:
rw [inv_rpow, ← rpow_mul, one_div_mul_cancel hp0.ne', rpow_one]

Premises used: ENNReal.rpow_mul, ENNReal.inv_rpow, ENNReal.rpow_one, LT.lt.ne', one_div_mul_cancel
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
simp_rw : ∫⁻ (c : α), f c ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ∂μ = 1
⊢ ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1

Tactic:
simp_rw [funMulInvSnorm_rpow hp0_lt]

Premises used: ENNReal.funMulInvSnorm_rpow
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hr : (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ≠ ∞
⊢ ∫⁻ (c : α), f c ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ∂μ = 1

Tactic:
rw [lintegral_mul_const', ENNReal.mul_inv_cancel hf_nonzero hf_top]

Premises used: ENNReal.mul_inv_cancel, MeasureTheory.lintegral_mul_const'
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hr hr₁ hr₂ hr₃ : ∫⁻ (c : α), f c ^ p ∂μ ≠ 0
⊢ (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ≠ ∞

Tactic:
rwa [inv_ne_top]

Premises used: ENNReal.inv_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 μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
⊢ ∫⁻ (a : α), (f * g) a ∂μ = ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ

Tactic:
lintegral_congr fun a => ?_

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
refine : ∀ (a : α), (f * g) a = (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg)
⊢ ∫⁻ (a : α), (f * g) a ∂μ = ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ

Tactic:
refine lintegral_congr fun a => ?_

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
a : α
rw :
  funMulInvSnorm f p μ a * (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p) *
      (funMulInvSnorm g q μ a * (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)) =
    funMulInvSnorm f p μ a * funMulInvSnorm g q μ a * (npf * nqg)
⊢ (f * g) a = (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg)

Tactic:
rw [Pi.mul_apply, fun_eq_funMulInvSnorm_mul_eLpNorm f hf_nonzero hf_nontop,
        fun_eq_funMulInvSnorm_mul_eLpNorm g hg_nonzero hg_nontop, Pi.mul_apply]

Premises used: Pi.mul_apply, ENNReal.fun_eq_funMulInvSnorm_mul_eLpNorm
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
a : α
⊢ funMulInvSnorm f p μ a * (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p) *
      (funMulInvSnorm g q μ a * (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)) =
    funMulInvSnorm f p μ a * funMulInvSnorm g q μ a * (npf * nqg)

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
⊢ npf * nqg ≠ ∞

Tactic:
simp [npf, nqg, hf_nontop, hg_nontop, hf_nonzero, hg_nonzero, ENNReal.mul_eq_top]

Premises used: ENNReal.mul_eq_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 μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
rw : (∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a ∂μ) * (npf * nqg) ≤ npf * nqg
⊢ ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ ≤ npf * nqg

Tactic:
rw [lintegral_mul_const' (npf * nqg) _
          (by simp [npf, nqg, hf_nontop, hg_nontop, hf_nonzero, hg_nonzero, ENNReal.mul_eq_top])]

Premises used: HMul.hMul, MeasureTheory.lintegral_mul_const'
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
⊢ (∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a ∂μ) * (npf * nqg) ≤ npf * nqg

Tactic:
mul_le_of_le_one_left' ?_

Premises used: mul_le_of_le_one_left'
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
refine : ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a ∂μ ≤ 1
⊢ (∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a ∂μ) * (npf * nqg) ≤ npf * nqg

Tactic:
refine mul_le_of_le_one_left' ?_

Premises used: mul_le_of_le_one_left'
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
⊢ ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1

Tactic:
have hf1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.pos hf_nonzero hf_nontop
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
hf1 : ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1
⊢ ∫⁻ (c : α), funMulInvSnorm g q μ c ^ q ∂μ = 1

Tactic:
have hg1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.symm.pos hg_nonzero hg_nontop
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
hf1 : ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1
hg1 : ∫⁻ (c : α), funMulInvSnorm g q μ c ^ q ∂μ = 1
⊢ ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a ∂μ ≤ 1

Tactic:
lintegral_mul_le_one_of_lintegral_rpow_eq_one hpq (hf.mul_const _) hf1 hg1

Premises used: ENNReal.lintegral_mul_le_one_of_lintegral_rpow_eq_one, AEMeasurable.mul_const
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
hf1 : ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1
hg1 : ∫⁻ (c : α), funMulInvSnorm g q μ c ^ q ∂μ = 1
⊢ ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a ∂μ ≤ 1

Tactic:
exact lintegral_mul_le_one_of_lintegral_rpow_eq_one hpq (hf.mul_const _) hf1 hg1

Premises used: ENNReal.lintegral_mul_le_one_of_lintegral_rpow_eq_one, AEMeasurable.mul_const
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
a : ∫⁻ (a : α), (f * g) a ∂μ = ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ
a₁ : ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ ≤ npf * nqg
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
calc
    (∫⁻ a : α, (f * g) a ∂μ) =
        ∫⁻ a : α, (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ := by
      refine lintegral_congr fun a => ?_
      rw [Pi.mul_apply, fun_eq_funMulInvSnorm_mul_eLpNorm f hf_nonzero hf_nontop,
        fun_eq_funMulInvSnorm_mul_eLpNorm g hg_nonzero hg_nontop, Pi.mul_apply]
      ring
    _ ≤ npf * nqg := by
      rw [lintegral_mul_const' (npf * nqg) _
          (by simp [npf, nqg, hf_nontop, hg_nontop, hf_nonzero, hg_nonzero, ENNReal.mul_eq_top])]
      refine mul_le_of_le_one_left' ?_
      have hf1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.pos hf_nonzero hf_nontop
      have hg1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.symm.pos hg_nonzero hg_nontop
      exact lintegral_mul_le_one_of_lintegral_rpow_eq_one hpq (hf.mul_const _) hf1 hg1

Premises used: HMul.hMul, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ f x ^ p) 0

Tactic:
rw [lintegral_eq_zero_iff' (hf.pow_const p)] at hf_zero

Premises used: AEMeasurable.pow_const, MeasureTheory.lintegral_eq_zero_iff'
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ f x ^ p) 0
h : ∀ (x : α), f x ^ p = 0 x → f x = 0 x
⊢ f =ᶠ[ae μ] 0

Tactic:
filter_upwards [hf_zero] with x
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ f x ^ p) 0
x : α
h : ¬f x = 0 → ¬f x ^ p = 0
⊢ f x ^ p = 0 x → f x = 0 x

Tactic:
rw [Pi.zero_apply, ← not_imp_not]

Premises used: Pi.zero_apply, not_imp_not
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ f x ^ p) 0
x : α
⊢ ¬f x = 0 → ¬f x ^ p = 0

Tactic:
fun hx => (rpow_pos_of_nonneg (pos_iff_ne_zero.2 hx) hp0).ne'

Premises used: Iff.mpr, LT.lt.ne', ENNReal.rpow_pos_of_nonneg, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ f x ^ p) 0
x : α
⊢ ¬f x = 0 → ¬f x ^ p = 0

Tactic:
exact fun hx => (rpow_pos_of_nonneg (pos_iff_ne_zero.2 hx) hp0).ne'

Premises used: Iff.mpr, LT.lt.ne', ENNReal.rpow_pos_of_nonneg, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
rw : ∫⁻ (a : α), (f * g) a ∂μ = lintegral μ 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = 0

Tactic:
rw [← @lintegral_zero_fun α _ μ]

Premises used: MeasureTheory.lintegral_zero_fun
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = lintegral μ 0

Tactic:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
refine : f * g =ᶠ[ae μ] 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = lintegral μ 0

Tactic:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
h_mul_zero : f * g =ᶠ[ae μ] 0 * g
rwa rwa₁ rwa₂ rwa₃ : ∀ (h_mul_zero : f * g =ᶠ[ae μ] 0), f * g =ᶠ[ae μ] 0
⊢ f * g =ᶠ[ae μ] 0

Tactic:
rwa [zero_mul] at h_mul_zero

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
suffices : f * g =ᶠ[ae μ] 0 * g
⊢ f * g =ᶠ[ae μ] 0

Tactic:
suffices h_mul_zero : f * g =ᵐ[μ] 0 * g by rwa [zero_mul] at h_mul_zero
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ f =ᶠ[ae μ] 0

Tactic:
have hf_eq_zero : f =ᵐ[μ] 0 := ae_eq_zero_of_lintegral_rpow_eq_zero hp0 hf hf_zero
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
hf_eq_zero : f =ᶠ[ae μ] 0
⊢ f * g =ᶠ[ae μ] 0 * g

Tactic:
hf_eq_zero.mul (ae_eq_refl g)

Premises used: Filter.EventuallyEq.mul, MeasureTheory.ae_eq_refl
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
hf_eq_zero : f =ᶠ[ae μ] 0
⊢ f * g =ᶠ[ae μ] 0 * g

Tactic:
exact hf_eq_zero.mul (ae_eq_refl g)

Premises used: Filter.EventuallyEq.mul, MeasureTheory.ae_eq_refl
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ∞
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
simp [*]
-- 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 μ
pos :
  ∀ (hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0),
    ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
neg :
  ∀ (hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 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 hf_zero : ∫⁻ a, f a ^ p ∂μ = 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
⊢ ∫⁻ (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
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