awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm' f p μ * eLpNorm' g q μ
have simp : ‖(↑c : ℝ)‖ₑ * eLpNorm' (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm' f p μ * eLpNorm' g q μ
Tactic: simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm'_const_smul _ hro_lt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ ‖(↑c : ℝ)‖ₑ * eLpNorm' (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm' f p μ * eLpNorm' g q μ
have rw : (↑c : ℝ≥0∞) * eLpNorm' (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) r μ ≤ (↑c : ℝ≥0∞) * (eLpNorm' f p μ * eLpNorm' g q μ)
Tactic: rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ (↑c : ℝ≥0∞) * eLpNorm' (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) r μ ≤ (↑c : ℝ≥0∞) * (eLpNorm' f p μ * eLpNorm' g q μ)
have bc : eLpNorm' (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) r μ ≤ eLpNorm' f p μ * eLpNorm' g q μ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm' f p μ * eLpNorm' g q μ
have eLpNorm' : eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤
  eLpNorm' (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) r μ
Tactic: calc
    eLpNorm' (fun x => b (f x) (g x)) r μ
      ≤ eLpNorm' (fun x ↦ (c : ℝ) • ‖f x‖ * ‖g x‖) r μ := by
      simp only [eLpNorm']
      gcongr ?_ ^ _
      refine lintegral_mono_ae <| h.mono fun a ha ↦ ?_
      gcongr
      simp only [enorm_eq_nnnorm, ENNReal.coe_le_coe]
      simpa using ha
    _ ≤ c * eLpNorm' f p μ * eLpNorm' g q μ := by
      simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm'_const_smul _ hro_lt]
      rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]
      gcongr
      simpa only [eLpNorm', enorm_mul, enorm_norm] using
        ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hro_lt hrp hpqr μ hf.enorm hg.enorm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
eLpNorm' :
  MeasureTheory.eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤
    MeasureTheory.eLpNorm' (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) r μ
⊢ MeasureTheory.eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤
    (↑c : ℝ≥0∞) * MeasureTheory.eLpNorm' f p μ * MeasureTheory.eLpNorm' g q μ
have eLpNorm'₁ : MeasureTheory.eLpNorm' (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) r μ ≤
  (↑c : ℝ≥0∞) * MeasureTheory.eLpNorm' f p μ * MeasureTheory.eLpNorm' g q μ
Tactic: calc
    eLpNorm' (fun x => b (f x) (g x)) r μ
      ≤ eLpNorm' (fun x ↦ (c : ℝ) • ‖f x‖ * ‖g x‖) r μ := by
      simp only [eLpNorm']
      gcongr ?_ ^ _
      refine lintegral_mono_ae <| h.mono fun a ha ↦ ?_
      gcongr
      simp only [enorm_eq_nnnorm, ENNReal.coe_le_coe]
      simpa using ha
    _ ≤ c * eLpNorm' f p μ * eLpNorm' g q μ := by
      simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm'_const_smul _ hro_lt]
      rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]
      gcongr
      simpa only [eLpNorm', enorm_mul, enorm_norm] using
        ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hro_lt hrp hpqr μ hf.enorm hg.enorm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr : p.HolderTriple q r
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have hpqr₁ : 1 / r = 1 / p + 1 / q
Tactic: have hpqr := hpqr.one_div_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inl : ∀ [hpqr : ENNReal.HolderTriple 0 q r] (hpqr : 1 / r = 1 / 0 + 1 / q),
  eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f 0 μ * eLpNorm g q μ
Tactic: obtain (rfl | rfl | hp) := ENNReal.trichotomy p
Cleared hypotheses: p, hpqr_1, hpqr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
inl :
  ∀ [hpqr : ENNReal.HolderTriple 0 q r] (hpqr : 1 / r = 1 / 0 + 1 / q),
    eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f 0 μ * eLpNorm g q μ
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inr : ∀ [hpqr : ENNReal.HolderTriple ∞ q r] (hpqr : 1 / r = HDiv.hDiv (α := ℝ≥0∞) 1 ∞ + 1 / q),
  eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g q μ
Tactic: obtain (rfl | rfl | hp) := ENNReal.trichotomy p
Cleared hypotheses: p, hpqr_1, hpqr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
inl :
  ∀ [hpqr : ENNReal.HolderTriple 0 q r] (hpqr : 1 / r = 1 / 0 + 1 / q),
    eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f 0 μ * eLpNorm g q μ
inr :
  ∀ [hpqr : ENNReal.HolderTriple ∞ q r] (hpqr : 1 / r = HDiv.hDiv (α := ℝ≥0∞) 1 ∞ + 1 / q),
    eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g q μ
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inr₁ : ∀ (hp : 0 < p.toReal),
  eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
Tactic: obtain (rfl | rfl | hp) := ENNReal.trichotomy p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : ENNReal.HolderTriple ∞ q r
hpqr : 1 / r = HDiv.hDiv (α := ℝ≥0∞) 1 ∞ + 1 / q
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g q μ
have this : r = q
Tactic: have : r = q := by simpa using hpqr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inr : ∀ [hpqr : p.HolderTriple 0 r] (hpqr : 1 / r = 1 / p + 1 / 0),
  eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g 0 μ
Tactic: obtain (rfl | rfl | hq) := ENNReal.trichotomy q
Cleared hypotheses: q, hpqr_1, hpqr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
inr :
  ∀ [hpqr : p.HolderTriple 0 r] (hpqr : 1 / r = 1 / p + 1 / 0),
    eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g 0 μ
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inr₁ : ∀ [hpqr : p.HolderTriple ∞ r] (hpqr : 1 / r = 1 / p + HDiv.hDiv (α := ℝ≥0∞) 1 ∞),
  eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g ∞ μ
Tactic: obtain (rfl | rfl | hq) := ENNReal.trichotomy q
Cleared hypotheses: q, hpqr_1, hpqr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
inr :
  ∀ [hpqr : p.HolderTriple 0 r] (hpqr : 1 / r = 1 / p + 1 / 0),
    eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g 0 μ
inr₁ :
  ∀ [hpqr : p.HolderTriple ∞ r] (hpqr : 1 / r = 1 / p + HDiv.hDiv (α := ℝ≥0∞) 1 ∞),
    eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g ∞ μ
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inr₂ : ∀ (hq : 0 < q.toReal),
  eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
Tactic: obtain (rfl | rfl | hq) := ENNReal.trichotomy q
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hpqr_1 : p.HolderTriple ∞ r
hpqr : 1 / r = 1 / p + HDiv.hDiv (α := ℝ≥0∞) 1 ∞
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g ∞ μ
have this : r = p
Tactic: have : r = p := by simpa using hpqr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have hp₁ : 0 < p
Tactic: obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have hp₂ : p < ∞
Tactic: obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have hq₁ : 0 < q
Tactic: obtain ⟨hq₁, hq₂⟩ := ENNReal.toReal_pos_iff.mp hq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have hq₂ : q < ∞
Tactic: obtain ⟨hq₁, hq₂⟩ := ENNReal.toReal_pos_iff.mp hq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
⊢ 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
have this : (1 / r).toReal = (1 / p + 1 / q).toReal
Tactic: have := congr(ENNReal.toReal $(hpqr))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
this : (1 / r).toReal = (1 / p + 1 / q).toReal
⊢ 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
have this₁ : (1 / r).toReal = (1 / p).toReal + (1 / q).toReal
Tactic: rw [ENNReal.toReal_add (by simpa using hp₁.ne') (by simpa using hq₁.ne')] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
Tactic: have hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal := by
    have := congr(ENNReal.toReal $(hpqr))
    rw [ENNReal.toReal_add (by simpa using hp₁.ne') (by simpa using hq₁.ne')] at this
    simpa
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
⊢ 0 < 1 / r.toReal
have rw : 0 < 1 / p.toReal + 1 / q.toReal
Tactic: rw [hpqr']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have hr : 0 < r.toReal
Tactic: have hr : 0 < r.toReal := one_div_pos.mp <| by rw [hpqr']; positivity
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have hr₁ : 0 < r
Tactic: obtain ⟨hr₁, hr₂⟩ := ENNReal.toReal_pos_iff.mp hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
hr₁ : 0 < r
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have hr₂ : r < ∞
Tactic: obtain ⟨hr₁, hr₂⟩ := ENNReal.toReal_pos_iff.mp hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
hr₁ : 0 < r
hr₂ : r < ∞
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have hrp : r.toReal < p.toReal
Tactic: have hrp : r.toReal < p.toReal := lt_of_one_div_lt_one_div hp <|
    hpqr' ▸ lt_add_of_pos_right _ (by positivity)