awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
inr :
  eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r.toReal μ ≤
    (↑c : ℝ≥0∞) * eLpNorm' f p.toReal μ * eLpNorm' g q.toReal μ
inr₁ : q ≠ 0
inr₂ : q ≠ ∞
inr₃ : p ≠ 0
inr₄ : p ≠ ∞
inr₅ : r ≠ 0
inr₆ : r ≠ ∞
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ

Tactic:
rw [eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm']

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r.toReal μ ≤
    (↑c : ℝ≥0∞) * eLpNorm' f p.toReal μ * eLpNorm' g q.toReal μ

Tactic:
eLpNorm'_le_eLpNorm'_mul_eLpNorm' hf hg b c h hr hrp hpqr'

Premises used: MeasureTheory.eLpNorm'_le_eLpNorm'_mul_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r.toReal μ ≤
    (↑c : ℝ≥0∞) * eLpNorm' f p.toReal μ * eLpNorm' g q.toReal μ

Tactic:
exact eLpNorm'_le_eLpNorm'_mul_eLpNorm' hf hg b c h hr hrp hpqr'

Premises used: MeasureTheory.eLpNorm'_le_eLpNorm'_mul_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ q ≠ 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ q ≠ 0

Tactic:
first | positivity | finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ q ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ q ≠ ∞

Tactic:
first | positivity | finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ p ≠ 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ p ≠ 0

Tactic:
first | positivity | finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ p ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ p ≠ ∞

Tactic:
first | positivity | finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ r ≠ 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ r ≠ 0

Tactic:
first | positivity | finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ r ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 < ∞
hrp : r.toReal < p.toReal
⊢ r ≠ ∞

Tactic:
first | positivity | finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 μ

Tactic:
eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm hf hg b c h

Premises used: MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 α
p q r : ℝ≥0∞
f : α → E
g : α → F
b : E → F → G
c : ℝ≥0
hf : MemLp f p μ
hg : MemLp g q μ
h : AEStronglyMeasurable.{u_1, u_4} (β := G) (fun (x : α) ↦ b (f x) (g x)) μ
hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr : p.HolderTriple q r
⊢ MemLp.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ

Tactic:
⟨h, ?_⟩

Premises used: MeasureTheory.MemLp, And.intro
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 α
p q r : ℝ≥0∞
f : α → E
g : α → F
b : E → F → G
c : ℝ≥0
hf : MemLp f p μ
hg : MemLp g q μ
h : AEStronglyMeasurable.{u_1, u_4} (β := G) (fun (x : α) ↦ b (f x) (g x)) μ
hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr : p.HolderTriple q r
refine : eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ < ∞
⊢ MemLp.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ

Tactic:
refine ⟨h, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 α
p q r : ℝ≥0∞
f : α → E
g : α → F
b : E → F → G
c : ℝ≥0
hf : MemLp f p μ
hg : MemLp g q μ
h : AEStronglyMeasurable.{u_1, u_4} (β := G) (fun (x : α) ↦ b (f x) (g x)) μ
hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr : p.HolderTriple q r
apply : (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ < ∞
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ < ∞

Tactic:
apply (eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm hf.1 hg.1 b c hb (hpqr := hpqr)).trans_lt

Premises used: And.left, MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : α → E
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
φ : α → 𝕜
x : α
⊢ nnnorm.{u_3} (E := E) ((fun (x1 : 𝕜) (x2 : E) ↦ x1 • x2) (φ x) (f x)) ≤ 1 * ‖φ x‖₊ * ‖f x‖₊

Tactic:
simpa using nnnorm_smul_le _ _

Premises used: nnnorm_smul_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : α → E
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
φ : α → 𝕜
⊢ eLpNorm (φ • f) p μ ≤ eLpNorm φ ∞ μ * eLpNorm f p μ

Tactic:
simpa using (eLpNorm_le_eLpNorm_top_mul_eLpNorm p φ hf (· • ·) 1
    (.of_forall fun _ => by simpa using nnnorm_smul_le _ _) :)

Premises used: MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm, Filter.Eventually.of_forall, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
p : ℝ≥0∞
f : α → E
φ : α → 𝕜
hφ : AEStronglyMeasurable φ μ
x : α
⊢ nnnorm.{u_3} (E := E) ((fun (x1 : 𝕜) (x2 : E) ↦ x1 • x2) (φ x) (f x)) ≤ 1 * ‖φ x‖₊ * ‖f x‖₊

Tactic:
simpa using nnnorm_smul_le _ _

Premises used: nnnorm_smul_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
p : ℝ≥0∞
f : α → E
φ : α → 𝕜
hφ : AEStronglyMeasurable φ μ
⊢ eLpNorm (φ • f) p μ ≤ eLpNorm φ p μ * eLpNorm f ∞ μ

Tactic:
simpa using (eLpNorm_le_eLpNorm_mul_eLpNorm_top p hφ f (· • ·) 1
    (.of_forall fun _ => by simpa using nnnorm_smul_le _ _) :)

Premises used: MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_top, Filter.Eventually.of_forall, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
p q r : ℝ
f : α → E
hf : AEStronglyMeasurable f μ
φ : α → 𝕜
hφ : AEStronglyMeasurable φ μ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
x : α
⊢ nnnorm.{u_3} (E := E) ((fun (x1 : 𝕜) (x2 : E) ↦ x1 • x2) (φ x) (f x)) ≤ 1 * ‖φ x‖₊ * ‖f x‖₊

Tactic:
simpa using nnnorm_smul_le _ _

Premises used: nnnorm_smul_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
p q r : ℝ
f : α → E
hf : AEStronglyMeasurable f μ
φ : α → 𝕜
hφ : AEStronglyMeasurable φ μ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
⊢ eLpNorm' (φ • f) p μ ≤ eLpNorm' φ q μ * eLpNorm' f r μ

Tactic:
simpa using eLpNorm'_le_eLpNorm'_mul_eLpNorm' hφ hf (· • ·) 1
    (.of_forall fun _ => by simpa using nnnorm_smul_le _ _)
    hp0_lt hpq hpqr

Premises used: Filter.Eventually.of_forall, MeasureTheory.eLpNorm'_le_eLpNorm'_mul_eLpNorm', HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
p q r : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
φ : α → 𝕜
hφ : AEStronglyMeasurable φ μ
hpqr : p.HolderTriple q r
x : α
⊢ nnnorm.{u_3} (E := E) ((fun (x1 : 𝕜) (x2 : E) ↦ x1 • x2) (φ x) (f x)) ≤ 1 * ‖φ x‖₊ * ‖f x‖₊

Tactic:
simpa using nnnorm_smul_le _ _

Premises used: nnnorm_smul_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
p q r : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
φ : α → 𝕜
hφ : AEStronglyMeasurable φ μ
hpqr : p.HolderTriple q r
⊢ eLpNorm (φ • f) r μ ≤ eLpNorm φ p μ * eLpNorm f q μ

Tactic:
simpa using (eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm hφ hf (· • ·) 1
      (.of_forall fun _ => by simpa using nnnorm_smul_le _ _) : _)

Premises used: Filter.Eventually.of_forall, HSMul.hSMul, OfNat.ofNat, MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
p q r : ℝ≥0∞
f : α → E
φ : α → 𝕜
hf : MemLp f q μ
hφ : MemLp φ p μ
hpqr : p.HolderTriple q r
⊢ MemLp (φ • f) r μ

Tactic:
⟨hφ.1.smul hf.1,
    eLpNorm_smul_le_mul_eLpNorm hf.1 hφ.1 |>.trans_lt <|
      ENNReal.mul_lt_top hφ.eLpNorm_lt_top hf.eLpNorm_lt_top⟩

Premises used: MeasureTheory.eLpNorm_smul_le_mul_eLpNorm, MeasureTheory.MemLp, ENNReal.mul_lt_top, And.left, And.intro, MeasureTheory.MemLp.eLpNorm_lt_top, LE.le.trans_lt, MeasureTheory.AEStronglyMeasurable.smul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
x : MeasurableSpace α
𝕜 : Type u_2
inst : NormedRing 𝕜
μ : Measure α
p q r : ℝ≥0∞
f φ : α → 𝕜
hf : MemLp f q μ
hφ : MemLp φ p μ
hpqr : p.HolderTriple q r
⊢ MemLp (φ * f) r μ

Tactic:
MemLp.smul hf hφ

Premises used: MeasureTheory.MemLp.smul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
x : MeasurableSpace α
𝕜 : Type u_2
inst : NormedRing 𝕜
μ : Measure α
p q r : ℝ≥0∞
f φ : α → 𝕜
hf : MemLp f q μ
hφ : MemLp φ p μ
hpqr : p.HolderTriple q r
⊢ MemLp.{u_1, u_2} (ε := 𝕜) (fun (x : α) ↦ φ x * f x) r μ

Tactic:
MemLp.smul hf hφ

Premises used: MeasureTheory.MemLp.smul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) (p i) μ
pos : ∀ (hμ : μ = 0), MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ
neg : ∀ (hμ : ¬μ = 0), MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ
⊢ MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) (p i) μ
hμ : μ = 0
⊢ MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ

Tactic:
simp [MemLp, eLpNormEssSup_const, hμ, aestronglyMeasurable_const, Pi.one_def]

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.eLpNormEssSup_const, MeasureTheory.MemLp, Pi.one_def
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) (p i) μ
hμ : ¬μ = 0
⊢ MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ

Tactic:
simp [MemLp, eLpNormEssSup_const, hμ, aestronglyMeasurable_const, Pi.one_def]

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.eLpNormEssSup_const, MeasureTheory.MemLp, Pi.one_def
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, MemLp (f i) (p i) μ), MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
hf : ∀ i_1 ∈ Finset.cons i s hi, MemLp (f i_1) (p i_1) μ
cons : MemLp (f i * ∏ x ∈ s, f x) (∑ i ∈ Finset.cons i s hi, (p i)⁻¹)⁻¹ μ
⊢ MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ Finset.cons i s hi, f i) (∑ i ∈ Finset.cons i s hi, (p i)⁻¹)⁻¹ μ

Tactic:
rw [prod_cons]

Premises used: Finset.prod_cons
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, MemLp (f i) (p i) μ), MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
hf : ∀ i_1 ∈ cons i s hi, MemLp (f i_1) (p i_1) μ
⊢ (p i)⁻¹ + (∑ i ∈ s, (p i)⁻¹)⁻¹⁻¹ = (∑ i ∈ cons i s hi, (p i)⁻¹)⁻¹⁻¹

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, MemLp (f i) (p i) μ), MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
hf : ∀ i_1 ∈ cons i s hi, MemLp (f i_1) (p i_1) μ
⊢ MemLp (f i * ∏ x ∈ s, f x) (∑ i ∈ cons i s hi, (p i)⁻¹)⁻¹ μ

Tactic:
exact (ih <| forall_of_forall_cons hf).mul (hf i <| mem_cons_self ..) (hpqr := ⟨by simp⟩)

Premises used: Finset.forall_of_forall_cons, MeasureTheory.MemLp.mul, Finset.mem_cons_self