awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h :
  1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
rwa :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) *
          ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
            ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)))),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rwa₁ :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
          ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rwa₂ :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p + -(1 / p)) *
          ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rwa₃ :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p - 1 / p) *
          ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rwa₄ :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        HPow.hPow (β := ℝ) (∫⁻ (a : α), (f + g) a ^ p ∂μ) 0 *
          ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rwa₅ :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        1 * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have rwa₆ : ∀
  (h :
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
      (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)),
  (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Tactic: rwa [← ENNReal.mul_le_mul_iff_right h0_rpow (by finiteness),
      ← mul_assoc, ← rpow_add _ _ h_add_zero h_add_top, ←
      sub_eq_add_neg, _root_.sub_self, rpow_zero, one_mul, mul_one] at h
Cleared hypotheses: h
-- 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 μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have suffices : 1 ≤
  (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
Tactic: suffices h :
    1 ≤
      (∫⁻ a : α, (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
        ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a : α, g a ^ p ∂μ) ^ (1 / p)) by
    rwa [← ENNReal.mul_le_mul_iff_right h0_rpow (by finiteness),
      ← mul_assoc, ← rpow_add _ _ h_add_zero h_add_top, ←
      sub_eq_add_neg, _root_.sub_self, rpow_zero, one_mul, mul_one] at h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
have h : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
  ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / q)
Tactic: have h :
    (∫⁻ a : α, (f + g) a ^ p ∂μ) ≤
      ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a : α, g a ^ p ∂μ) ^ (1 / p)) *
        (∫⁻ a : α, (f + g) a ^ p ∂μ) ^ (1 / q) :=
    lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add hpq hf hg
-- 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 μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / q)
⊢ 1 / q = 1 - 1 / p
have nth_rw : 1 / q = p⁻¹ + q⁻¹ - 1 / p
Tactic: nth_rw 2 [← hpq.inv_add_inv_eq_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / q)
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
have h_one_div_q : 1 / q = 1 - 1 / p
Tactic: have h_one_div_q : 1 / q = 1 - 1 / p := by
    nth_rw 2 [← hpq.inv_add_inv_eq_one]
    ring
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / q)
h_one_div_q : 1 / q = 1 - 1 / p
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
have h₁ : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
  ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
    ((∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)))
Tactic: simp_rw [h_one_div_q, sub_eq_add_neg 1 (1 / p), ENNReal.rpow_add _ _ h_add_zero h_add_top,
    rpow_one] at h
Cleared hypotheses: h
-- 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 μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)))
| ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
    ((∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)))
have enter : (∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p))
Tactic: enter [2]
-- 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 μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)))
| (∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p))
have rw : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ
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 μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)))
| ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
    ((∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)))
have enter : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ
Tactic: enter [2]; rw [mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)))
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
have h₁ : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
  ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
    ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ)
Tactic: conv_rhs at h => enter [2]; rw [mul_comm]
Cleared hypotheses: h
-- 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 μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ)
| ∫⁻ (a : α), (f + g) a ^ p ∂μ
have rw : 1 * ∫⁻ (a : α), (f + g) a ^ p ∂μ
Tactic: rw [← one_mul (∫⁻ a : α, (f + g) a ^ p ∂μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ)
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
have h₁ : 1 * ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
  ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
    ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ)
Tactic: conv_lhs at h => rw [← one_mul (∫⁻ a : α, (f + g) a ^ p ∂μ)]
Cleared hypotheses: h
-- 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 μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  1 * ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ)
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
have rwa : ∀
  (h :
    1 * ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
          (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
        ∫⁻ (a : α), (f + g) a ^ p ∂μ),
  1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
Tactic: rwa [← mul_assoc, ENNReal.mul_le_mul_iff_left h_add_zero h_add_top, mul_comm] at h
Cleared hypotheses: h
-- 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 μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  1 * ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ)
rwa :
  ∀
    (h :
      1 * ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
        ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
            (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
          ∫⁻ (a : α), (f + g) a ^ p ∂μ),
    1 ≤
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
        ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
have rwa₁ : ∀
  (h :
    1 ≤
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
        (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p))),
  1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
Tactic: rwa [← mul_assoc, ENNReal.mul_le_mul_iff_left h_add_zero h_add_top, mul_comm] at h
Cleared hypotheses: h
-- 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 μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  1 * ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ)
rwa :
  ∀
    (h :
      1 * ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
        ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
            (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
          ∫⁻ (a : α), (f + g) a ^ p ∂μ),
    1 ≤
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
        ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
rwa₁ :
  ∀
    (h :
      1 ≤
        ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
          (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p))),
    1 ≤
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
        ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
have rwa₂ : ∀
  (h :
    1 ≤
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
        ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))),
  1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
Tactic: rwa [← mul_assoc, ENNReal.mul_le_mul_iff_left h_add_zero h_add_top, mul_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have hp_pos : 0 < p
Tactic: have hp_pos : 0 < p := lt_of_lt_of_le zero_lt_one hp1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have inl : ∀ (hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ∞),
  (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Tactic: obtain hf_top | hf_top := eq_top_or_lt_top (∫⁻ a, f a ^ p ∂μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
inl :
  ∀ (hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ∞),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have inr : ∀ (hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞),
  (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Tactic: obtain hf_top | hf_top := eq_top_or_lt_top (∫⁻ a, f a ^ p ∂μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have inr : ∀ (hg_top : ∫⁻ (a : α), g a ^ p ∂μ = ∞),
  (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Tactic: obtain hg_top | hg_top := eq_top_or_lt_top (∫⁻ a, g a ^ p ∂μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
inr :
  ∀ (hg_top : ∫⁻ (a : α), g a ^ p ∂μ = ∞),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have inr₁ : ∀ (hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞),
  (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Tactic: obtain hg_top | hg_top := eq_top_or_lt_top (∫⁻ a, g a ^ p ∂μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have pos : ∀ (h1 : p = 1),
  (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Tactic: by_cases h1 : p = 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
pos :
  ∀ (h1 : p = 1),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have neg : ∀ (h1 : ¬p = 1),
  (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Tactic: by_cases h1 : p = 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : p = 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have pos : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Tactic: refine le_of_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : p = 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have pos : ∫⁻ (a : α), (f + g) a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
Tactic: simp_rw [h1, one_div_one, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : ¬p = 1
⊢ 1 < p
have refine : 1 ≠ p
Tactic: refine lt_of_le_of_ne hp1 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : ¬p = 1
⊢ 1 ≠ p
have symm : p ≠ 1
Tactic: symm