awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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 * g =ᶠ[ae μ] 0 * g
have hf_eq_zero : f =ᶠ[ae μ] 0
Tactic: have hf_eq_zero : f =ᵐ[μ] 0 := ae_eq_zero_of_lintegral_rpow_eq_zero hp0 hf hf_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
have pos : ∀ (hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0),
  ∫⁻ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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)
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
have neg : ∀ (hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0),
  ∫⁻ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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)
have pos : ∫⁻ (a : α), (f * g) a ∂μ = 0
Tactic: refine Eq.trans_le ?_ zero_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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)
have pos : ∀ (hg_zero : ∫⁻ (a : α), g a ^ q ∂μ = 0),
  ∫⁻ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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)
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
have neg : ∀ (hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0),
  ∫⁻ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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)
have pos : ∫⁻ (a : α), (f * g) a ∂μ = 0
Tactic: refine Eq.trans_le ?_ zero_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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 ∂μ = 0
have pos : ∫⁻ (a : α), (g * f) a ∂μ = 0
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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)
have pos : ∀ (hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ∞),
  ∫⁻ (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 ∂μ = ⊤
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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)
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
have neg : ∀ (hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞),
  ∫⁻ (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 ∂μ = ⊤
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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)
have pos : ∀ (hg_top : ∫⁻ (a : α), g a ^ 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 ∂μ = ⊤
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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)
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
have neg : ∀ (hg_top : ¬∫⁻ (a : α), g a ^ 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 ∂μ = ⊤
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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)
have pos : ∫⁻ (a : α), (g * f) a ∂μ ≤ (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p)
Tactic: rw [mul_comm, mul_comm ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
have 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
Tactic: rcases hp.eq_or_lt with rfl | hp
Cleared hypotheses: p, hp, hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
have inr : ∀ (hp : 0 < p), ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
Tactic: rcases hp.eq_or_lt with rfl | hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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
⊢ ∫⁻ (a : α), HPow.hPow (β := ℝ) (f a) 0 * g a ^ q ∂μ ≤
    HPow.hPow (β := ℝ) (∫⁻ (a : α), f a ∂μ) 0 * (∫⁻ (a : α), g a ∂μ) ^ q
have hpq₁ : q = 1
Tactic: rw [zero_add] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
have 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
Tactic: rcases hq.eq_or_lt with rfl | hq
Cleared hypotheses: q, hq, hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
have inr₁ : ∀ (hq : 0 < 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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
⊢ ∫⁻ (a : α), f a ^ p * HPow.hPow (β := ℝ) (g a) 0 ∂μ ≤
    (∫⁻ (a : α), f a ∂μ) ^ p * HPow.hPow (β := ℝ) (∫⁻ (a : α), g a ∂μ) 0
have hpq₁ : p = 1
Tactic: rw [add_zero] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
have rw : p < 1
Tactic: rw [one_div, one_lt_inv₀ hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ p < 1
have linarith : 1 ≤ p → p + q - 1 + (0 - q) + (1 - p) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
have h2p : 1 < 1 / p
Tactic: have h2p : 1 < 1 / p := by
    rw [one_div, one_lt_inv₀ hp]
    linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
have h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1
Tactic: have h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1 := by simp [hpq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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 : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
have 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))
Tactic: have := ENNReal.lintegral_mul_le_Lp_mul_Lq μ (Real.holderConjugate_iff.mpr ⟨h2p, h2pq⟩)
    (hf.pow_const p) (hg.pow_const q)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
have insert : ∀ (h2i₀ : p i₀ = 1), ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
Tactic: rcases eq_or_ne (p i₀) 1 with h2i₀ | h2i₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ ∫⁻ (a : α), ∏ i ∈ Insert.insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ Insert.insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
have 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
Tactic: rcases eq_or_ne (p i₀) 1 with h2i₀ | h2i₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
have 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
Tactic: simp only [hi₀, not_false_eq_true, prod_insert]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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
⊢ ∫⁻ (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
have h2p₁ : ∀ 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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, f i a ^ p i ∂μ = ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ
have h : ∀ (x : α), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i x ^ p i) (∏ i ∈ s, 1)
Tactic: congr! 3 with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ f i x ^ p i = 1
have rw : HPow.hPow (β := ℝ) (f i x) 0 = 1
Tactic: rw [h2p i hi, ENNReal.rpow_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ f i x ^ p i = 1
have rw₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [h2p i hi, ENNReal.rpow_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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, (∫⁻ (a : α), f i a ∂μ) ^ p i
have e_a : Eq (α := ℝ≥0∞) (∏ i ∈ s, 1) (∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ 1 = (∫⁻ (a : α), f i a ∂μ) ^ p i
have rw : 1 = HPow.hPow (β := ℝ) (∫⁻ (a : α), f i a ∂μ) 0
Tactic: rw [h2p i hi, ENNReal.rpow_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ 1 = (∫⁻ (a : α), f i a ∂μ) ^ p i
have rw₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [h2p i hi, ENNReal.rpow_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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, f i a ^ p i ∂μ ≤
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
have calc : ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ = ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ
Tactic: calc ∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ
          = ∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ := by
            congr! 3 with x
            apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]
        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, 1 := by simp [h2i₀]
        _ = (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ p i := by
            congr 1
            apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
calc : ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ = ∫⁻ (a : α), f i₀ a ^ 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, (∫⁻ (a : α), f i a ∂μ) ^ p i
have calc₁ : ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ ≤ (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, 1
Tactic: calc ∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ
          = ∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ := by
            congr! 3 with x
            apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]
        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, 1 := by simp [h2i₀]
        _ = (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ p i := by
            congr 1
            apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]