awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
s t : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
f g : ((i : δ) → X i) → ℝ≥0∞
hst : s ⊆ t
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f = lmarginal (X := X) μ s g
rw : lmarginal (X := X) μ (s ∪ t \ s) f = lmarginal (X := X) μ (s ∪ t \ s) g
rw₁ : lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s f) = lmarginal (X := X) μ (s ∪ t \ s) g
rw₂ : lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s f) = lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s g)
⊢ lmarginal (X := X) μ t f = lmarginal (X := X) μ t g
have rw₃ : lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s g) = lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s g)
Tactic: rw [← union_sdiff_of_subset hst, lmarginal_union' μ f hf disjoint_sdiff,
    lmarginal_union' μ g hg disjoint_sdiff, hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
s t : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
f g : ((i : δ) → X i) → ℝ≥0∞
hst : s ⊆ t
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f ≤ lmarginal (X := X) μ s g
⊢ lmarginal (X := X) μ t f ≤ lmarginal (X := X) μ t g
have rw : lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s f) ≤ lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s g)
Tactic: rw [← union_sdiff_of_subset hst, lmarginal_union' μ f hf disjoint_sdiff,
    lmarginal_union' μ g hg disjoint_sdiff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f = lmarginal (X := X) μ s g
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
have inl : ∀ (h : IsEmpty ((i : δ) → X i)),
  ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
Tactic: rcases isEmpty_or_nonempty (∀ i, X i) with h | ⟨⟨x⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f = lmarginal (X := X) μ s g
inl :
  ∀ (h : IsEmpty ((i : δ) → X i)),
    ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
have inr : ∀ (x : (i : δ) → X i),
  ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
Tactic: rcases isEmpty_or_nonempty (∀ i, X i) with h | ⟨⟨x⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f = lmarginal (X := X) μ s g
x : (i : δ) → X i
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
have inr : lmarginal (X := X) μ Finset.univ f x = lmarginal (X := X) μ Finset.univ g x
Tactic: simp_rw [lintegral_eq_lmarginal_univ x, lmarginal_eq_of_subset (Finset.subset_univ s) hf hg hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f ≤ lmarginal (X := X) μ s g
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
have inl : ∀ (h : IsEmpty ((i : δ) → X i)),
  ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
Tactic: rcases isEmpty_or_nonempty (∀ i, X i) with h | ⟨⟨x⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f ≤ lmarginal (X := X) μ s g
inl :
  ∀ (h : IsEmpty ((i : δ) → X i)),
    ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
have inr : ∀ (x : (i : δ) → X i),
  ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
Tactic: rcases isEmpty_or_nonempty (∀ i, X i) with h | ⟨⟨x⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f ≤ lmarginal (X := X) μ s g
h : IsEmpty ((i : δ) → X i)
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
have inl : LE.le (α := ℝ≥0∞) 0 0
Tactic: simp_rw [lintegral_of_isEmpty, le_rfl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f ≤ lmarginal (X := X) μ s g
x : (i : δ) → X i
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
have inr : lmarginal (X := X) μ Finset.univ f x ≤ lmarginal (X := X) μ Finset.univ g x
Tactic: simp_rw [lintegral_eq_lmarginal_univ x, lmarginal_le_of_subset (Finset.subset_univ s) hf hg hfg x]
-- 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 μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ = 1
have simp : ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ + g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1
Tactic: simp only [div_eq_mul_inv]
-- 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 μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ + g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1
have rw : ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ ∂μ + ∫⁻ (a : α), g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1
Tactic: rw [lintegral_add_left']
-- 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 μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
rw : ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ ∂μ + ∫⁻ (a : α), g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ + g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1
have hf₁ : AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ f a ^ p * (ENNReal.ofReal p)⁻¹) μ
Tactic: rw [lintegral_add_left']
-- 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 μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ ∂μ + ∫⁻ (a : α), g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1
have hr : (ENNReal.ofReal q)⁻¹ ≠ ∞
Tactic: rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const', hf_norm, hg_norm,
          one_mul, one_mul, hpq.inv_add_inv_ennreal]
-- 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 μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ 1
have a : ∫⁻ (a : α), f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ = 1
Tactic: calc
    (∫⁻ a : α, (f * g) a ∂μ) ≤
        ∫⁻ a : α, f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ :=
      lintegral_mono fun a => young_inequality (f a) (g a) hpq
    _ = 1 := by
      simp only [div_eq_mul_inv]
      rw [lintegral_add_left']
      · rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const', hf_norm, hg_norm,
          one_mul, one_mul, hpq.inv_add_inv_ennreal]
        simp [hpq.symm.pos]
      · exact (hf.pow_const _).mul_const _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
⊢ funMulInvSnorm f p μ a ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
have rw : f a ^ p * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
Tactic: rw [funMulInvSnorm, mul_rpow_of_nonneg _ _ (le_of_lt hp0)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
h_inv_rpow : ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
⊢ f a ^ p * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
have rw : f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
Tactic: rw [h_inv_rpow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
⊢ f a ^ p * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
have suffices : ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
Tactic: suffices h_inv_rpow : ((∫⁻ c : α, f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ c : α, f c ^ p ∂μ)⁻¹ by
    rw [h_inv_rpow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
⊢ ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
have rw : (((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)) ^ p)⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
Tactic: rw [inv_rpow, ← rpow_mul, one_div_mul_cancel hp0.ne', rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
rw : (((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)) ^ p)⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
⊢ ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
have rw₁ : ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p * p))⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
Tactic: rw [inv_rpow, ← rpow_mul, one_div_mul_cancel hp0.ne', rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
rw : (((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)) ^ p)⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
rw₁ : ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p * p))⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
⊢ ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
have rw₂ : (HPow.hPow (β := ℝ) (∫⁻ (c : α), f c ^ p ∂μ) 1)⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
Tactic: rw [inv_rpow, ← rpow_mul, one_div_mul_cancel hp0.ne', rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
rw : (((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)) ^ p)⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
rw₁ : ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p * p))⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
rw₂ : (HPow.hPow (β := ℝ) (∫⁻ (c : α), f c ^ p ∂μ) 1)⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
⊢ ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
have rw₃ : (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
Tactic: rw [inv_rpow, ← rpow_mul, one_div_mul_cancel hp0.ne', rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
⊢ ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1
have simp_rw : ∫⁻ (c : α), f c ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ∂μ = 1
Tactic: simp_rw [funMulInvSnorm_rpow hp0_lt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
⊢ ∫⁻ (c : α), f c ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ∂μ = 1
have hr : (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ≠ ∞
Tactic: rw [lintegral_mul_const', ENNReal.mul_inv_cancel hf_nonzero hf_top]
-- 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 μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
⊢ ∫⁻ (a : α), (f * g) a ∂μ = ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ
have refine : ∀ (a : α), (f * g) a = (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg)
Tactic: refine lintegral_congr fun a => ?_
-- 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 μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
a : α
⊢ (f * g) a = (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg)
have rw : funMulInvSnorm f p μ a * (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p) *
    (funMulInvSnorm g q μ a * (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)) =
  funMulInvSnorm f p μ a * funMulInvSnorm g q μ a * (npf * nqg)
Tactic: rw [Pi.mul_apply, fun_eq_funMulInvSnorm_mul_eLpNorm f hf_nonzero hf_nontop,
        fun_eq_funMulInvSnorm_mul_eLpNorm g hg_nonzero hg_nontop, Pi.mul_apply]
-- 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 μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
⊢ ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ ≤ npf * nqg
have rw : (∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a ∂μ) * (npf * nqg) ≤ npf * nqg
Tactic: rw [lintegral_mul_const' (npf * nqg) _
          (by simp [npf, nqg, hf_nontop, hg_nontop, hf_nonzero, hg_nonzero, ENNReal.mul_eq_top])]
-- 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 μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
⊢ (∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a ∂μ) * (npf * nqg) ≤ npf * nqg
have refine : ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a ∂μ ≤ 1
Tactic: refine mul_le_of_le_one_left' ?_
-- 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 μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
⊢ ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a ∂μ ≤ 1
have hf1 : ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1
Tactic: have hf1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.pos hf_nonzero hf_nontop
-- 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 μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
hf1 : ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1
⊢ ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a ∂μ ≤ 1
have hg1 : ∫⁻ (c : α), funMulInvSnorm g q μ c ^ q ∂μ = 1
Tactic: have hg1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.symm.pos hg_nonzero hg_nontop
-- 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 μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
have a : ∫⁻ (a : α), (f * g) a ∂μ = ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ
Tactic: calc
    (∫⁻ a : α, (f * g) a ∂μ) =
        ∫⁻ a : α, (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ := by
      refine lintegral_congr fun a => ?_
      rw [Pi.mul_apply, fun_eq_funMulInvSnorm_mul_eLpNorm f hf_nonzero hf_nontop,
        fun_eq_funMulInvSnorm_mul_eLpNorm g hg_nonzero hg_nontop, Pi.mul_apply]
      ring
    _ ≤ npf * nqg := by
      rw [lintegral_mul_const' (npf * nqg) _
          (by simp [npf, nqg, hf_nontop, hg_nontop, hf_nonzero, hg_nonzero, ENNReal.mul_eq_top])]
      refine mul_le_of_le_one_left' ?_
      have hf1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.pos hf_nonzero hf_nontop
      have hg1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.symm.pos hg_nonzero hg_nontop
      exact lintegral_mul_le_one_of_lintegral_rpow_eq_one hpq (hf.mul_const _) hf1 hg1
-- 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 μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
a : ∫⁻ (a : α), (f * g) a ∂μ = ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
have a₁ : ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ ≤ npf * nqg
Tactic: calc
    (∫⁻ a : α, (f * g) a ∂μ) =
        ∫⁻ a : α, (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ := by
      refine lintegral_congr fun a => ?_
      rw [Pi.mul_apply, fun_eq_funMulInvSnorm_mul_eLpNorm f hf_nonzero hf_nontop,
        fun_eq_funMulInvSnorm_mul_eLpNorm g hg_nonzero hg_nontop, Pi.mul_apply]
      ring
    _ ≤ npf * nqg := by
      rw [lintegral_mul_const' (npf * nqg) _
          (by simp [npf, nqg, hf_nontop, hg_nontop, hf_nonzero, hg_nonzero, ENNReal.mul_eq_top])]
      refine mul_le_of_le_one_left' ?_
      have hf1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.pos hf_nonzero hf_nontop
      have hg1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.symm.pos hg_nonzero hg_nontop
      exact lintegral_mul_le_one_of_lintegral_rpow_eq_one hpq (hf.mul_const _) hf1 hg1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ f =ᶠ[ae μ] 0
have hf_zero₁ : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ f x ^ p) 0
Tactic: rw [lintegral_eq_zero_iff' (hf.pow_const p)] at hf_zero
Cleared hypotheses: hf_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ f x ^ p) 0
⊢ f =ᶠ[ae μ] 0
have h : ∀ (x : α), f x ^ p = 0 x → f x = 0 x
Tactic: filter_upwards [hf_zero] with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ f x ^ p) 0
x : α
⊢ f x ^ p = 0 x → f x = 0 x
have h : ¬f x = 0 → ¬f x ^ p = 0
Tactic: rw [Pi.zero_apply, ← not_imp_not]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = 0
have rw : ∫⁻ (a : α), (f * g) a ∂μ = lintegral μ 0
Tactic: rw [← @lintegral_zero_fun α _ μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = lintegral μ 0
have refine : f * g =ᶠ[ae μ] 0
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
h_mul_zero : f * g =ᶠ[ae μ] 0 * g
⊢ f * g =ᶠ[ae μ] 0
have rwa : ∀ (h_mul_zero : f * g =ᶠ[ae μ] 0), f * g =ᶠ[ae μ] 0
Tactic: rwa [zero_mul] at h_mul_zero
Cleared hypotheses: h_mul_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
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
have suffices : f * g =ᶠ[ae μ] 0 * g
Tactic: suffices h_mul_zero : f * g =ᵐ[μ] 0 * g by rwa [zero_mul] at h_mul_zero