awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ≠ ∞
have h : (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) = eLpNorm f (ENNReal.ofReal p) μ
Tactic: convert! hf.eLpNorm_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 ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) = eLpNorm f (ENNReal.ofReal p) μ
have h : (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) =
  (∫⁻ (x : α), ‖f x‖ₑ ^ (ENNReal.ofReal p).toReal ∂μ) ^ (1 / (ENNReal.ofReal p).toReal)
Tactic: rw [eLpNorm_eq_lintegral_rpow_enorm_toReal]
-- 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 ∂μ
h :
  (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) =
    (∫⁻ (x : α), ‖f x‖ₑ ^ (ENNReal.ofReal p).toReal ∂μ) ^ (1 / (ENNReal.ofReal p).toReal)
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) = eLpNorm f (ENNReal.ofReal p) μ
have h₁ : ENNReal.ofReal p ≠ 0
Tactic: rw [eLpNorm_eq_lintegral_rpow_enorm_toReal]
-- 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 ∂μ
h :
  (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) =
    (∫⁻ (x : α), ‖f x‖ₑ ^ (ENNReal.ofReal p).toReal ∂μ) ^ (1 / (ENNReal.ofReal p).toReal)
h₁ : ENNReal.ofReal p ≠ 0
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) = eLpNorm f (ENNReal.ofReal p) μ
have h₂ : ENNReal.ofReal p ≠ ∞
Tactic: rw [eLpNorm_eq_lintegral_rpow_enorm_toReal]
-- 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) =
    (∫⁻ (x : α), ‖f x‖ₑ ^ (ENNReal.ofReal p).toReal ∂μ) ^ (1 / (ENNReal.ofReal p).toReal)
have h : (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (x : α), ‖f x‖ₑ ^ p ∂μ) ^ (1 / p)
Tactic: rw [ENNReal.toReal_ofReal 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 ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ ENNReal.ofReal p ≠ 0
have h : 0 < p
Tactic: rw [Ne, ENNReal.ofReal_eq_zero, not_le]
-- 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 : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) ≠ ∞
have h : (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) = eLpNorm g (ENNReal.ofReal q) μ
Tactic: convert! hg.eLpNorm_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 ∂μ
⊢ (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) = eLpNorm g (ENNReal.ofReal q) μ
have h : (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) =
  (∫⁻ (x : α), ‖g x‖ₑ ^ (ENNReal.ofReal q).toReal ∂μ) ^ (1 / (ENNReal.ofReal q).toReal)
Tactic: rw [eLpNorm_eq_lintegral_rpow_enorm_toReal]
-- 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 ∂μ
h :
  (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) =
    (∫⁻ (x : α), ‖g x‖ₑ ^ (ENNReal.ofReal q).toReal ∂μ) ^ (1 / (ENNReal.ofReal q).toReal)
⊢ (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) = eLpNorm g (ENNReal.ofReal q) μ
have h₁ : ENNReal.ofReal q ≠ 0
Tactic: rw [eLpNorm_eq_lintegral_rpow_enorm_toReal]
-- 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 ∂μ
h :
  (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) =
    (∫⁻ (x : α), ‖g x‖ₑ ^ (ENNReal.ofReal q).toReal ∂μ) ^ (1 / (ENNReal.ofReal q).toReal)
h₁ : ENNReal.ofReal q ≠ 0
⊢ (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) = eLpNorm g (ENNReal.ofReal q) μ
have h₂ : ENNReal.ofReal q ≠ ∞
Tactic: rw [eLpNorm_eq_lintegral_rpow_enorm_toReal]
-- 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 : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) =
    (∫⁻ (x : α), ‖g x‖ₑ ^ (ENNReal.ofReal q).toReal ∂μ) ^ (1 / (ENNReal.ofReal q).toReal)
have h : (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) = (∫⁻ (x : α), ‖g x‖ₑ ^ q ∂μ) ^ (1 / q)
Tactic: rw [ENNReal.toReal_ofReal 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 ∂μ
⊢ ENNReal.ofReal q ≠ 0
have h : 0 < q
Tactic: rw [Ne, ENNReal.ofReal_eq_zero, not_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
have refine : (ae μ).EventuallyEq (β := ℝ) (fun (a : α) ↦ f a * g a) fun (a : α) ↦ ‖f a‖ * ‖g a‖
Tactic: refine integral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (a : α) ↦ f a * g a) fun (a : α) ↦ ‖f a‖ * ‖g a‖
have h : ∀ (x : α) (hxf : 0 x ≤ f x) (hxg : 0 x ≤ g x), f x * g x = ‖f x‖ * ‖g x‖
Tactic: filter_upwards [hf_nonneg, hg_nonneg] with x hxf hxg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
x : α
hxf : 0 x ≤ f x
hxg : 0 x ≤ g x
⊢ f x * g x = ‖f x‖ * ‖g x‖
have h : f x * g x = f x * ‖g x‖
Tactic: rw [Real.norm_of_nonneg hxf, Real.norm_of_nonneg hxg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
x : α
hxf : 0 x ≤ f x
hxg : 0 x ≤ g x
h : f x * g x = f x * ‖g x‖
⊢ f x * g x = ‖f x‖ * ‖g x‖
have h₁ : f x * g x = f x * g x
Tactic: rw [Real.norm_of_nonneg hxf, Real.norm_of_nonneg hxg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
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 h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
Tactic: have h_left : ∫ a, f a * g a ∂μ = ∫ a, ‖f a‖ * ‖g a‖ ∂μ := by
    refine integral_congr_ae ?_
    filter_upwards [hf_nonneg, hg_nonneg] with x hxf hxg
    rw [Real.norm_of_nonneg hxf, Real.norm_of_nonneg hxg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
⊢ Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
have refine : (ae μ).EventuallyEq (β := ℝ) (fun (a : α) ↦ f a ^ p) fun (a : α) ↦ ‖f a‖ ^ p
Tactic: refine integral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (a : α) ↦ f a ^ p) fun (a : α) ↦ ‖f a‖ ^ p
have h : ∀ (x : α) (hxf : 0 x ≤ f x), f x ^ p = ‖f x‖ ^ p
Tactic: filter_upwards [hf_nonneg] with x hxf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
x : α
hxf : 0 x ≤ f x
⊢ f x ^ p = ‖f x‖ ^ p
have h : f x ^ p = f x ^ p
Tactic: rw [Real.norm_of_nonneg hxf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (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 h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
Tactic: have h_right_f : ∫ a, f a ^ p ∂μ = ∫ a, ‖f a‖ ^ p ∂μ := by
    refine integral_congr_ae ?_
    filter_upwards [hf_nonneg] with x hxf
    rw [Real.norm_of_nonneg hxf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
⊢ Eq (α := ℝ) (∫ (a : α), g a ^ q ∂μ) (∫ (a : α), ‖g a‖ ^ q ∂μ)
have refine : (ae μ).EventuallyEq (β := ℝ) (fun (a : α) ↦ g a ^ q) fun (a : α) ↦ ‖g a‖ ^ q
Tactic: refine integral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (a : α) ↦ g a ^ q) fun (a : α) ↦ ‖g a‖ ^ q
have h : ∀ (x : α) (hxg : 0 x ≤ g x), g x ^ q = ‖g x‖ ^ q
Tactic: filter_upwards [hg_nonneg] with x hxg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
x : α
hxg : 0 x ≤ g x
⊢ g x ^ q = ‖g x‖ ^ q
have h : g x ^ q = g x ^ q
Tactic: rw [Real.norm_of_nonneg hxg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (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 h_right_g : Eq (α := ℝ) (∫ (a : α), g a ^ q ∂μ) (∫ (a : α), ‖g a‖ ^ q ∂μ)
Tactic: have h_right_g : ∫ a, g a ^ q ∂μ = ∫ a, ‖g a‖ ^ q ∂μ := by
    refine integral_congr_ae ?_
    filter_upwards [hg_nonneg] with x hxg
    rw [Real.norm_of_nonneg hxg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
h_right_g : Eq (α := ℝ) (∫ (a : α), g a ^ q ∂μ) (∫ (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 rw : ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤
  HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), ‖g a‖ ^ q ∂μ) (1 / q)
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
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
inst_2 : Unique α
f : α → E
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) (∫ (x : α), f default ∂μ)
have e_f : ∀ (x : α), f x = f default
Tactic: congr with x
-- 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
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
inst_2 : Unique α
f : α → E
x : α
⊢ f x = f default
have e_f : x = default
Tactic: congr
-- 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
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
inst_2 : Unique α
f : α → E
⊢ ∫ (x : α), f default ∂μ = μ.real univ • f default
have rw : μ.real univ • f default = μ.real univ • f default
Tactic: rw [integral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
⊢ Eq (α := F) (∫ (x : β), (f : (a : β) → F) x ∂μ) (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x)
have simp_rw : Eq (α := F) (∫ (x : β), (SimpleFunc.toLargerSpace hm f : (a : β) → F) x ∂μ)
  (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑(SimpleFunc.toLargerSpace hm f) : (a : β) → F) {x}) • x)
Tactic: simp_rw [← f.coe_toLargerSpace_eq hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
⊢ Eq (α := F) (∫ (x : β), (SimpleFunc.toLargerSpace hm f : (a : β) → F) x ∂μ)
    (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑(SimpleFunc.toLargerSpace hm f) : (a : β) → F) {x}) • x)
have rw : Eq (α := F)
  (∑ x ∈ (SimpleFunc.toLargerSpace hm f).range,
    μ.real (preimage (β := F) (⇑(SimpleFunc.toLargerSpace hm f) : (a : β) → F) {x}) • x)
  (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑(SimpleFunc.toLargerSpace hm f) : (a : β) → F) {x}) • x)
Tactic: rw [SimpleFunc.integral_eq_sum _ hf_int]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : β), (f : (a : β) → F) x ∂μ) (∫ (x : β), (f : (a : β) → F) x ∂μ.trim hm)
have hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
Tactic: have hf : StronglyMeasurable[m] f := @SimpleFunc.stronglyMeasurable β F m _ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : β), (f : (a : β) → F) x ∂μ) (∫ (x : β), (f : (a : β) → F) x ∂μ.trim hm)
have hf_int_m : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) (μ.trim hm)
Tactic: have hf_int_m := hf_int.trim hm hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
hf_int_m : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) (μ.trim hm)
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : β), (f : (a : β) → F) x ∂μ) (∫ (x : β), (f : (a : β) → F) x ∂μ.trim hm)
have rw : Eq (α := F) (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x)
  (∑ x ∈ f.range, (μ.trim hm).real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x)
Tactic: rw [integral_simpleFunc_larger_space (le_refl m) f hf_int_m,
    integral_simpleFunc_larger_space hm f hf_int]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
hf_int_m : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) (μ.trim hm)
⊢ Eq (α := F) (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x)
    (∑ x ∈ f.range, (μ.trim hm).real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x)
have e_f : ∀ (x : F),
  μ.real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x =
    (μ.trim hm).real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x
Tactic: congr with x