awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
calc : ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ = ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ
calc₁ :
  ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ =
    ∫⁻ (a : α), f i₀ a ^ p i₀ * HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i a ^ q i) (1 - p i₀) ∂μ
calc₂ :
  ∫⁻ (a : α), f i₀ a ^ p i₀ * HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i a ^ q i) (1 - p i₀) ∂μ ≤
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * (∫⁻ (a : α), ∏ i ∈ s, f i a ^ q i ∂μ) ^ (1 - p i₀)
calc₃ :
  (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * (∫⁻ (a : α), ∏ i ∈ s, f i a ^ q i ∂μ) ^ (1 - p i₀) ≤
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ q i) (1 - p i₀)
calc₄ :
  (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ q i) (1 - p i₀) =
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
calc₅ :
  (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i =
    ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
calc ∫⁻ a, ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ
          = ∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ := by simp [hi₀]
        _ = ∫⁻ a, f i₀ a ^ p i₀ * (∏ i ∈ s, f i a ^ q i) ^ (1 - p i₀) ∂μ := by
            simp [q, ← ENNReal.prod_rpow_of_nonneg hpi₀, ← ENNReal.rpow_mul,
              div_mul_cancel₀ (h := h2pi₀)]
        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * (∫⁻ a, ∏ i ∈ s, f i a ^ q i ∂μ) ^ (1 - p i₀) := by
            apply ENNReal.lintegral_mul_norm_pow_le
            · exact hf i₀ <| mem_insert_self ..
            · exact s.aemeasurable_fun_prod fun i hi ↦ (hf i <| mem_insert_of_mem hi).pow_const _
            · exact h2p i₀ <| mem_insert_self ..
            · exact hpi₀
            · apply add_sub_cancel
        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * (∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ q i) ^ (1 - p i₀) := by
            gcongr -- behavior of gcongr is heartbeat-dependent, which makes code really fragile...
            exact ih (fun i hi ↦ hf i <| mem_insert_of_mem hi) hq h2q
        _ = (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ p i := by
            simp [q, ← ENNReal.prod_rpow_of_nonneg hpi₀, ← ENNReal.rpow_mul,
              div_mul_cancel₀ (h := h2pi₀)]
        _ = ∏ i ∈ insert i₀ s, (∫⁻ a, f i a ∂μ) ^ p i := by simp [hi₀]

Premises used: HSub.hSub, Insert.insert, Finset.prod, HPow.hPow, OfNat.ofNat, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
this :
  ∫⁻ (t : α),
      ∏ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) s, (j.elim (g t) fun (j : ι) ↦ f j t) ^ j.elim q p ∂μ ≤
    ∏ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) s,
      (∫⁻ (t : α), j.elim (g t) fun (j : ι) ↦ f j t ∂μ) ^ j.elim q p
⊢ ∫⁻ (a : α), g a ^ q * ∏ i ∈ s, f i a ^ p i ∂μ ≤ (∫⁻ (a : α), g a ∂μ) ^ q * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
simpa using this
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
j :
  ∫⁻ (t : α),
      ∏ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) s, (j.elim (g t) fun (j : ι) ↦ f j t) ^ j.elim q p ∂μ ≤
    ∏ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) s,
      (∫⁻ (t : α), j.elim (g t) fun (j : ι) ↦ f j t ∂μ) ^ j.elim q p
⊢ ∫⁻ (a : α), g a ^ q * ∏ i ∈ s, f i a ^ p i ∂μ ≤ (∫⁻ (a : α), g a ∂μ) ^ q * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
suffices
    ∫⁻ t, ∏ j ∈ insertNone s, Option.elim j (g t) (fun j ↦ f j t) ^ Option.elim j q p ∂μ
    ≤ ∏ j ∈ insertNone s, (∫⁻ t, Option.elim j (g t) (fun j ↦ f j t) ∂μ) ^ Option.elim j q p by
    simpa using this
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
⊢ ∫⁻ (t : α),
      ∏ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) s, (j.elim (g t) fun (j : ι) ↦ f j t) ^ j.elim q p ∂μ ≤
    ∏ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) s,
      (∫⁻ (t : α), j.elim (g t) fun (j : ι) ↦ f j t ∂μ) ^ j.elim q p

Tactic:
ENNReal.lintegral_prod_norm_pow_le _ ?_ ?_ ?_

Premises used: ENNReal.lintegral_prod_norm_pow_le
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
refine_1 :
  ∀ (i : Option ι),
    Membership.mem (γ := Finset (Option ι)) ((insertNone : (a : Finset ι) → Finset (Option ι)) s : Finset (Option ι))
        i →
      AEMeasurable (β := ℝ≥0∞) (fun (t : α) ↦ i.elim (g t) fun (j : ι) ↦ f j t) μ
refine_2 : Eq (α := ℝ) (∑ i ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) s, i.elim q p) 1
refine_3 :
  ∀ (i : Option ι),
    Membership.mem (γ := Finset (Option ι)) ((insertNone : (a : Finset ι) → Finset (Option ι)) s : Finset (Option ι))
        i →
      0 ≤ i.elim q p
⊢ ∫⁻ (t : α),
      ∏ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) s, (j.elim (g t) fun (j : ι) ↦ f j t) ^ j.elim q p ∂μ ≤
    ∏ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) s,
      (∫⁻ (t : α), j.elim (g t) fun (j : ι) ↦ f j t ∂μ) ^ j.elim q p

Tactic:
refine ENNReal.lintegral_prod_norm_pow_le _ ?_ ?_ ?_

Premises used: ENNReal.lintegral_prod_norm_pow_le
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
hi :
  Membership.mem (γ := Finset (Option ι)) ((insertNone : (a : Finset ι) → Finset (Option ι)) s : Finset (Option ι)) none
⊢ AEMeasurable (β := ℝ≥0∞) (fun (t : α) ↦ Option.elim none (g t) fun (j : ι) ↦ f j t) μ

Tactic:
hg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
hi :
  Membership.mem (γ := Finset (Option ι)) ((insertNone : (a : Finset ι) → Finset (Option ι)) s : Finset (Option ι)) none
⊢ AEMeasurable (β := ℝ≥0∞) (fun (t : α) ↦ Option.elim none (g t) fun (j : ι) ↦ f j t) μ

Tactic:
exact hg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
i : ι
hi :
  Membership.mem (γ := Finset (Option ι)) ((insertNone : (a : Finset ι) → Finset (Option ι)) s : Finset (Option ι))
    (some i)
⊢ AEMeasurable (β := ℝ≥0∞) (fun (t : α) ↦ (some i).elim (g t) fun (j : ι) ↦ f j t) μ

Tactic:
hf i ?_
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
i : ι
hi :
  Membership.mem (γ := Finset (Option ι)) ((insertNone : (a : Finset ι) → Finset (Option ι)) s : Finset (Option ι))
    (some i)
refine_1 : i ∈ s
⊢ AEMeasurable (β := ℝ≥0∞) (fun (t : α) ↦ (some i).elim (g t) fun (j : ι) ↦ f j t) μ

Tactic:
refine hf i ?_
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
i : ι
hi :
  Membership.mem (γ := Finset (Option ι)) ((insertNone : (a : Finset ι) → Finset (Option ι)) s : Finset (Option ι))
    (some i)
⊢ i ∈ s

Tactic:
simpa using hi
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
refine_2 : q + ∑ x ∈ s, p x = 1
⊢ Eq (α := ℝ) (∑ i ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) s, i.elim q p) 1

Tactic:
simp_rw [sum_insertNone, Option.elim]

Premises used: Finset.sum_insertNone, Option.elim
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
⊢ q + ∑ x ∈ s, p x = 1

Tactic:
hpq
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
⊢ q + ∑ x ∈ s, p x = 1

Tactic:
exact hpq
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
hi :
  Membership.mem (γ := Finset (Option ι)) ((insertNone : (a : Finset ι) → Finset (Option ι)) s : Finset (Option ι)) none
⊢ 0 ≤ Option.elim none q p

Tactic:
hq
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
hi :
  Membership.mem (γ := Finset (Option ι)) ((insertNone : (a : Finset ι) → Finset (Option ι)) s : Finset (Option ι)) none
⊢ 0 ≤ Option.elim none q p

Tactic:
exact hq
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
i : ι
hi :
  Membership.mem (γ := Finset (Option ι)) ((insertNone : (a : Finset ι) → Finset (Option ι)) s : Finset (Option ι))
    (some i)
⊢ 0 ≤ (some i).elim q p

Tactic:
hp i ?_
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
i : ι
hi :
  Membership.mem (γ := Finset (Option ι)) ((insertNone : (a : Finset ι) → Finset (Option ι)) s : Finset (Option ι))
    (some i)
refine_3 : i ∈ s
⊢ 0 ≤ (some i).elim q p

Tactic:
refine hp i ?_
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ ∫⁻ (a : α), (f a + g a) ^ p ∂μ ≤
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p + HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * g a ^ p ∂μ

Tactic:
lintegral_mono fun a => ?_

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
refine :
  ∀ (a : α), (f a + g a) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p + HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * g a ^ p
⊢ ∫⁻ (a : α), (f a + g a) ^ p ∂μ ≤
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p + HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * g a ^ p ∂μ

Tactic:
refine lintegral_mono fun a => ?_

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
a : α
⊢ (f a + g a) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p + HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * g a ^ p

Tactic:
simpa [mul_add] using ENNReal.rpow_add_le_mul_rpow_add_rpow (f a) (g a) hp1

Premises used: ENNReal.rpow_add_le_mul_rpow_add_rpow, mul_add
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
rw :
  HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), f a ^ p ∂μ < ∞ ∧
    HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), g a ^ p ∂μ < ∞
hf₁ : AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p) μ
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p + HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * g a ^ p ∂μ < ∞

Tactic:
rw [lintegral_add_left', lintegral_const_mul'' _ (hf.pow_const p),
        lintegral_const_mul' _ _ (by finiteness), ENNReal.add_lt_top]

Premises used: MeasureTheory.lintegral_add_left', AEMeasurable.pow_const, MeasureTheory.lintegral_const_mul', MeasureTheory.lintegral_const_mul'', ENNReal.add_lt_top
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
left : HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), f a ^ p ∂μ < ∞
right : HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), g a ^ p ∂μ < ∞
⊢ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), f a ^ p ∂μ < ∞ ∧
    HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), g a ^ p ∂μ < ∞

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), f a ^ p ∂μ < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), g a ^ p ∂μ < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
a :
  ∫⁻ (a : α), (f a + g a) ^ p ∂μ ≤
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p + HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * g a ^ p ∂μ
a₁ : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p + HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * g a ^ p ∂μ < ∞
⊢ ∫⁻ (a : α), (f + g) a ^ p ∂μ < ∞

Tactic:
calc
    (∫⁻ a : α, (f a + g a) ^ p ∂μ) ≤
        ∫⁻ a, (2 : ℝ≥0∞) ^ (p - 1) * f a ^ p + (2 : ℝ≥0∞) ^ (p - 1) * g a ^ p ∂μ := by
      refine lintegral_mono fun a => ?_
      simpa [mul_add] using ENNReal.rpow_add_le_mul_rpow_add_rpow (f a) (g a) hp1
    _ < ⊤ := by
      rw [lintegral_add_left', lintegral_const_mul'' _ (hf.pow_const p),
        lintegral_const_mul' _ _ (by finiteness), ENNReal.add_lt_top]
      · constructor <;> finiteness
      · fun_prop

Premises used: HSub.hSub, HPow.hPow, HAdd.hAdd, OfNat.ofNat, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ p ≠ 0

Tactic:
have hp0_ne : p ≠ 0 := (ne_of_lt hp0_lt).symm
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
⊢ 0 ≤ p

Tactic:
have hp0 : 0 ≤ p := le_of_lt hp0_lt
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
⊢ 0 < q

Tactic:
have hq0_lt : 0 < q := lt_of_le_of_lt hp0 hpq
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
⊢ q ≠ 0

Tactic:
have hq0_ne : q ≠ 0 := (ne_of_lt hq0_lt).symm
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
rw : 1 / r = 1 / q + 1 / r - 1 / q
⊢ 1 / r = 1 / p - 1 / q

Tactic:
rw [hpqr]
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
⊢ 1 / r = 1 / q + 1 / r - 1 / q

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
⊢ 1 / r = 1 / p - 1 / q

Tactic:
have h_one_div_r : 1 / r = 1 / p - 1 / q := by rw [hpqr]; simp
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
⊢ 1 < p2

Tactic:
simp [p2, _root_.lt_div_iff₀, hpq, hp0_lt]

Premises used: lt_div_iff₀
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
⊢ p2.HolderConjugate q2

Tactic:
have hp2q2 : p2.HolderConjugate q2 :=
    .conjExponent (by simp [p2, _root_.lt_div_iff₀, hpq, hp0_lt])
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
h₁ :
  ∫⁻ (a : α), f a ^ p * g a ^ p ∂μ ≤
    (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)
⊢ (∫⁻ (a : α), f a ^ p * g a ^ p ∂μ) ^ (1 / p) ≤
    ((∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
h₁ :
  ∫⁻ (a : α), f a ^ p * g a ^ p ∂μ ≤
    (∫⁻ (a : α), (f a ^ p) ^ p2 ∂μ) ^ (1 / p2) * (∫⁻ (a : α), (g a ^ p) ^ q2 ∂μ) ^ (1 / q2)
⊢ ∫⁻ (a : α), f a ^ p * g a ^ p ∂μ ≤
    (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)

Tactic:
simp_rw [ENNReal.rpow_mul]

Premises used: ENNReal.rpow_mul
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
⊢ ∫⁻ (a : α), f a ^ p * g a ^ p ∂μ ≤
    (∫⁻ (a : α), (f a ^ p) ^ p2 ∂μ) ^ (1 / p2) * (∫⁻ (a : α), (g a ^ p) ^ q2 ∂μ) ^ (1 / q2)

Tactic:
ENNReal.lintegral_mul_le_Lp_mul_Lq μ hp2q2 (hf.pow_const _) (hg.pow_const _)

Premises used: AEMeasurable.pow_const, ENNReal.lintegral_mul_le_Lp_mul_Lq
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
inst : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
⊢ ∫⁻ (a : α), f a ^ p * g a ^ p ∂μ ≤
    (∫⁻ (a : α), (f a ^ p) ^ p2 ∂μ) ^ (1 / p2) * (∫⁻ (a : α), (g a ^ p) ^ q2 ∂μ) ^ (1 / q2)

Tactic:
exact ENNReal.lintegral_mul_le_Lp_mul_Lq μ hp2q2 (hf.pow_const _) (hg.pow_const _)

Premises used: AEMeasurable.pow_const, ENNReal.lintegral_mul_le_Lp_mul_Lq