awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
inst_3 : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst_4 : Decidable (a ∈ s)
pos : a ∈ s → (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f x) = f a
⊢ (@integral _ _ _ _ inst_2 (if a ∈ s then Measure.dirac a else 0) fun (x : α) ↦ f x) = if a ∈ s then f a else 0
have neg : a ∉ s → Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ inst_2 0 fun (x : α) ↦ f x) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
⊢ ε * μ.real {x : α | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ
have inl : ∀ (hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ε * μ.real {x : α | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ
Tactic: rcases eq_top_or_lt_top (μ {x | ε ≤ f x}) with hμ | hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
inl :
  ∀ (hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ε * μ.real {x : α | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ
⊢ ε * μ.real {x : α | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ
have inr : ∀ (hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ε * μ.real {x : α | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ
Tactic: rcases eq_top_or_lt_top (μ {x | ε ≤ f x}) with hμ | hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ε * μ.real {x : α | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have := Fact.mk hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ ε * μ.real {x : α | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ
have ε₁ : ε * μ.real {x : α | ε ≤ f x} = ∫ (x : α) in {x : α | ε ≤ f x}, ε ∂μ
Tactic: calc
      ε * μ.real { x | ε ≤ f x } = ∫ _ in {x | ε ≤ f x}, ε ∂μ := by simp [mul_comm]
      _ ≤ ∫ x in {x | ε ≤ f x}, f x ∂μ :=
        integral_mono_ae (integrable_const _) (hf_int.mono_measure μ.restrict_le_self) <|
          ae_restrict_mem₀ <| hf_int.aemeasurable.nullMeasurable measurableSet_Ici
      _ ≤ _ := integral_mono_measure μ.restrict_le_self hf_nonneg hf_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤
    HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), ‖g a‖ ^ q ∂μ) (1 / q)
have rw : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
  (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
    (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae,
    integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
rw :
  (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤
    HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), ‖g a‖ ^ q ∂μ) (1 / q)
have hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖g a‖ ^ q
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae,
    integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
rw :
  (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)
hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖g a‖ ^ q
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤
    HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), ‖g a‖ ^ q ∂μ) (1 / q)
have hfm : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖g a‖ ^ q) μ
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae,
    integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
rw :
  (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)
hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖g a‖ ^ q
hfm : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖g a‖ ^ q) μ
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤
    HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), ‖g a‖ ^ q ∂μ) (1 / q)
have hf₂ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ ^ p
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae,
    integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
rw :
  (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)
hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖g a‖ ^ q
hfm : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖g a‖ ^ q) μ
hf₂ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ ^ p
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤
    HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), ‖g a‖ ^ q ∂μ) (1 / q)
have hfm₁ : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ ^ p) μ
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae,
    integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
rw :
  (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)
hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖g a‖ ^ q
hfm : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖g a‖ ^ q) μ
hf₂ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ ^ p
hfm₁ : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ ^ p) μ
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤
    HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), ‖g a‖ ^ q ∂μ) (1 / q)
have hf₃ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ * ‖g a‖
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae,
    integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
rw :
  (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)
hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖g a‖ ^ q
hfm : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖g a‖ ^ q) μ
hf₂ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ ^ p
hfm₁ : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ ^ p) μ
hf₃ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ * ‖g a‖
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤
    HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), ‖g a‖ ^ q ∂μ) (1 / q)
have hfm₂ : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ * ‖g a‖) μ
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae,
    integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)
have rw : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
  ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) * (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
Tactic: rw [ENNReal.toReal_rpow, ENNReal.toReal_rpow, ← ENNReal.toReal_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
have simp_rw : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ * ‖g a‖ₑ ∂μ
Tactic: simp_rw [Pi.mul_apply, ← ofReal_norm, ENNReal.ofReal_mul (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
simp_rw : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ * ‖g a‖ₑ ∂μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
have simp_rw₁ : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ * ENNReal.ofReal ‖g a‖ ∂μ
Tactic: simp_rw [Pi.mul_apply, ← ofReal_norm, ENNReal.ofReal_mul (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) *
        (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
have h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
  ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
Tactic: have h_left : ∫⁻ a, ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
      ∫⁻ a, ((‖f ·‖ₑ) * (‖g ·‖ₑ)) a ∂μ := by
    simp_rw [Pi.mul_apply, ← ofReal_norm, ENNReal.ofReal_mul (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
have refine : ∀ (x : α), ENNReal.ofReal (‖f x‖ ^ p) = ‖f x‖ₑ ^ p
Tactic: refine lintegral_congr fun x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
x : α
⊢ ENNReal.ofReal (‖f x‖ ^ p) = ‖f x‖ₑ ^ p
have rw : ENNReal.ofReal (‖f x‖ ^ p) = ENNReal.ofReal ‖f x‖ ^ p
Tactic: rw [← ofReal_norm, ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hpq.nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
x : α
rw : ENNReal.ofReal (‖f x‖ ^ p) = ENNReal.ofReal ‖f x‖ ^ p
⊢ ENNReal.ofReal (‖f x‖ ^ p) = ‖f x‖ₑ ^ p
have rw₁ : ENNReal.ofReal (‖f x‖ ^ p) = ENNReal.ofReal (‖f x‖ ^ p)
Tactic: rw [← ofReal_norm, ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hpq.nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) *
        (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
have h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
Tactic: have h_right_f : ∫⁻ a, .ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ a, ‖f a‖ₑ ^ p ∂μ := by
    refine lintegral_congr fun x => ?_
    rw [← ofReal_norm, ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hpq.nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
have refine : ∀ (x : α), ENNReal.ofReal (‖g x‖ ^ q) = ‖g x‖ₑ ^ q
Tactic: refine lintegral_congr fun x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
x : α
⊢ ENNReal.ofReal (‖g x‖ ^ q) = ‖g x‖ₑ ^ q
have rw : ENNReal.ofReal (‖g x‖ ^ q) = ENNReal.ofReal ‖g x‖ ^ q
Tactic: rw [← ofReal_norm, ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hpq.symm.nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
x : α
rw : ENNReal.ofReal (‖g x‖ ^ q) = ENNReal.ofReal ‖g x‖ ^ q
⊢ ENNReal.ofReal (‖g x‖ ^ q) = ‖g x‖ₑ ^ q
have rw₁ : ENNReal.ofReal (‖g x‖ ^ q) = ENNReal.ofReal (‖g x‖ ^ q)
Tactic: rw [← ofReal_norm, ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hpq.symm.nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) *
        (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
have h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
Tactic: have h_right_g : ∫⁻ a, .ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ a, ‖g a‖ₑ ^ q ∂μ := by
    refine lintegral_congr fun x => ?_
    rw [← ofReal_norm, ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hpq.symm.nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) *
        (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
have rw : (∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ).toReal ≤
  ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q)).toReal
Tactic: rw [h_left, h_right_f, h_right_g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ).toReal ≤
    ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q)).toReal
have refine_1 : (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) ≠ ∞
Tactic: refine ENNReal.toReal_mono ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
refine_1 : (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) ≠ ∞
⊢ (∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ).toReal ≤
    ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q)).toReal
have refine_2 : ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ ≤
  (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q)
Tactic: refine ENNReal.toReal_mono ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) ≠ ∞
have refine_1 : (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≠ ∞
Tactic: refine ENNReal.mul_ne_top ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
refine_1 : (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≠ ∞
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) ≠ ∞
have refine_1₁ : (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) ≠ ∞
Tactic: refine ENNReal.mul_ne_top ?_ ?_