awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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₀)
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
have 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₀)
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₀]
-- 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
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₀)
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
have 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
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₀]
-- 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
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
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
have 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
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₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ ∫⁻ (a : α), g a ^ q * ∏ i ∈ s, f i a ^ p i ∂μ ≤ (∫⁻ (a : α), g a ∂μ) ^ q * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
have 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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
have 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) μ
Tactic: refine ENNReal.lintegral_prod_norm_pow_le _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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) μ
⊢ ∫⁻ (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
have refine_2 : Eq (α := ℝ) (∑ i ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) s, i.elim q p) 1
Tactic: refine ENNReal.lintegral_prod_norm_pow_le _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
⊢ ∫⁻ (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
have refine_3 : ∀ (i : Option ι),
  Membership.mem (γ := Finset (Option ι)) ((insertNone : (a : Finset ι) → Finset (Option ι)) s : Finset (Option ι)) i →
    0 ≤ i.elim q p
Tactic: refine ENNReal.lintegral_prod_norm_pow_le _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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) μ
have refine_1 : i ∈ s
Tactic: refine hf i ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
have refine_3 : i ∈ s
Tactic: refine hp i ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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 ∂μ
have 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
Tactic: refine lintegral_mono fun a => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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 : α), HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p + HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * g a ^ p ∂μ < ∞
have rw : HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), f a ^ p ∂μ < ∞ ∧
  HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), g a ^ p ∂μ < ∞
Tactic: rw [lintegral_add_left', lintegral_const_mul'' _ (hf.pow_const p),
        lintegral_const_mul' _ _ (by finiteness), ENNReal.add_lt_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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 ∂μ < ∞
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p + HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * g a ^ p ∂μ < ∞
have hf₁ : AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p) μ
Tactic: rw [lintegral_add_left', lintegral_const_mul'' _ (hf.pow_const p),
        lintegral_const_mul' _ _ (by finiteness), ENNReal.add_lt_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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 ∂μ < ∞ ∧
    HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), g a ^ p ∂μ < ∞
have left : HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), f a ^ p ∂μ < ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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 ∂μ < ∞
⊢ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), f a ^ p ∂μ < ∞ ∧
    HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), g a ^ p ∂μ < ∞
have right : HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * ∫⁻ (a : α), g a ^ p ∂μ < ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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 + g) a ^ p ∂μ < ∞
have 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 ∂μ
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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 : α), (f + g) a ^ p ∂μ < ∞
have a₁ : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * f a ^ p + HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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 μ
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have hp0_ne : p ≠ 0
Tactic: have hp0_ne : p ≠ 0 := (ne_of_lt hp0_lt).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have hp0 : 0 ≤ p
Tactic: have hp0 : 0 ≤ p := le_of_lt hp0_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have hq0_lt : 0 < q
Tactic: have hq0_lt : 0 < q := lt_of_le_of_lt hp0 hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have hq0_ne : q ≠ 0
Tactic: have hq0_ne : q ≠ 0 := (ne_of_lt hq0_lt).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
have rw : 1 / r = 1 / q + 1 / r - 1 / q
Tactic: rw [hpqr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have h_one_div_r : 1 / r = 1 / p - 1 / q
Tactic: have h_one_div_r : 1 / r = 1 / p - 1 / q := by rw [hpqr]; simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
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
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have hp2q2 : p2.HolderConjugate q2
Tactic: have hp2q2 : p2.HolderConjugate q2 :=
    .conjExponent (by simp [p2, _root_.lt_div_iff₀, hpq, hp0_lt])
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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 ∂μ) ^ (1 / p) ≤
    ((∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p)
have h₁ : ∫⁻ (a : α), f a ^ p * g a ^ p ∂μ ≤
  (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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)
have h₁ : ∫⁻ (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]