mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : ∑ i ∈ s, g i ^ q = 0
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

pp: case inr.inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
·

Goal state after:
case inr.inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : ∑ i ∈ s, g i ^ q = 0
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.inr.refine_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ ∑ i ∈ s, f' i ^ p = 1

pp: case inr.inr.refine_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ ∑ i ∈ s, g' i ^ q = 1

Tactic:
·

Goal state after:
case inr.inr.refine_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ ∑ i ∈ s, f' i ^ p = 1
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case h₁
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) ∂μ ≤
    (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q)

pp: case h₂
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ ≤
    (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q)

Tactic:
·

Goal state after:
case h₁
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) ∂μ ≤
    (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case h₂
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ ≤
    (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q)

Tactic:
·

Goal state after:
case h₂
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ ≤
    (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.inr.refine_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ ∑ i ∈ s, g' i ^ q = 1

Tactic:
·

Goal state after:
case inr.inr.refine_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ ∑ i ∈ s, g' i ^ q = 1
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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✝ : ENNReal.HolderTriple 0 q r
hpqr : 1 / r = 1 / 0 + 1 / q
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f 0 μ * eLpNorm g q μ

pp: case inr.inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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✝ : ∞.HolderTriple q r
hpqr : 1 / r = 1 / ∞ + 1 / q
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f ∞ μ * eLpNorm g q μ

pp: case inr.inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g q μ

Tactic:
·

Goal state after:
case inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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✝ : ENNReal.HolderTriple 0 q r
hpqr : 1 / r = 1 / 0 + 1 / q
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f 0 μ * eLpNorm g q μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inl
ι : Type u
s : Finset ι
w f : ι → ℝ≥0
hp : 1 ≤ 1
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - 1⁻¹) * (∑ i ∈ s, w i * f i ^ 1) ^ 1⁻¹

pp: case inr
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
·

Goal state after:
case inl
ι : Type u
s : Finset ι
w f : ι → ℝ≥0
hp : 1 ≤ 1
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - 1⁻¹) * (∑ i ∈ s, w i * f i ^ 1) ^ 1⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case inr.inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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✝ : ∞.HolderTriple q r
hpqr : 1 / r = 1 / ∞ + 1 / q
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f ∞ μ * eLpNorm g q μ

pp: case inr.inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g q μ

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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✝ : ∞.HolderTriple q r
hpqr : 1 / r = 1 / ∞ + 1 / q
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f ∞ μ * eLpNorm g q μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.calc_1
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ ∑ i ∈ s, w i * f i = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i)

pp: case inr.calc_2
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) * (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) =
    (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
·

Goal state after:
case inr.calc_1
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ ∑ i ∈ s, w i * f i = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.calc_2
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) * (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) =
    (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
·

Goal state after:
case inr.calc_2
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) * (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) =
    (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case inr.inr.inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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✝ : p.HolderTriple 0 r
hpqr : 1 / r = 1 / p + 1 / 0
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g 0 μ

pp: case inr.inr.inr.inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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✝ : p.HolderTriple ∞ r
hpqr : 1 / r = 1 / p + 1 / ∞
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g ∞ μ

pp: case inr.inr.inr.inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g q μ

Tactic:
·

Goal state after:
case inr.inr.inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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✝ : p.HolderTriple 0 r
hpqr : 1 / r = 1 / p + 1 / 0
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g 0 μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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✝ : p.HolderTriple ∞ r
hpqr : 1 / r = 1 / p + 1 / ∞
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g ∞ μ

pp: case inr.inr.inr.inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g q μ

Tactic:
·

Goal state after:
case inr.inr.inr.inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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✝ : p.HolderTriple ∞ r
hpqr : 1 / r = 1 / p + 1 / ∞
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g ∞ μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_1
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ (∑ i ∈ s, f i ^ p) ^ (r / p) ≤ (∑' (i : ι), f i ^ p) ^ (r / p)

pp: case refine_2
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ (∑ i ∈ s, g i ^ q) ^ (r / q) ≤ (∑' (i : ι), g i ^ q) ^ (r / q)

Tactic:
·

Goal state after:
case refine_1
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ (∑ i ∈ s, f i ^ p) ^ (r / p) ≤ (∑' (i : ι), f i ^ p) ^ (r / p)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_2
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ (∑ i ∈ s, g i ^ q) ^ (r / q) ≤ (∑' (i : ι), g i ^ q) ^ (r / q)

Tactic:
·

Goal state after:
case refine_2
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ (∑ i ∈ s, g i ^ q) ^ (r / q) ≤ (∑' (i : ι), g i ^ q) ^ (r / q)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_1
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ q) (B ^ q)
H₁ : Summable fun i ↦ f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ ∑' (i : ι), f i * g i ≤ A * B

pp: case refine_2
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ q) (B ^ q)
H₁ : Summable fun i ↦ f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ HasSum (fun i ↦ f i * g i) (∑' (i : ι), f i * g i)

Tactic:
·

Goal state after:
case refine_1
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ q) (B ^ q)
H₁ : Summable fun i ↦ f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ ∑' (i : ι), f i * g i ≤ A * B
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_2
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ q) (B ^ q)
H₁ : Summable fun i ↦ f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ HasSum (fun i ↦ f i * g i) (∑' (i : ι), f i * g i)

Tactic:
·

Goal state after:
case refine_2
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ q) (B ^ q)
H₁ : Summable fun i ↦ f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ HasSum (fun i ↦ f i * g i) (∑' (i : ι), f i * g i)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 = p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

pp: case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

Tactic:
·

Goal state after:
case inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 = p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case left
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ (fun g ↦ ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1}

pp: case right
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ upperBounds ((fun g ↦ ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1})

Tactic:
·

Goal state after:
case left
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ (fun g ↦ ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1}
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case h.inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p = 0
⊢ (fun i ↦ f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g ↦ ∑ i ∈ s, f i * g i) fun i ↦ f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

pp: case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
⊢ (fun i ↦ f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g ↦ ∑ i ∈ s, f i * g i) fun i ↦ f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Tactic:
·

Goal state after:
case h.inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p = 0
⊢ (fun i ↦ f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g ↦ ∑ i ∈ s, f i * g i) fun i ↦ f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
⊢ (fun i ↦ f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g ↦ ∑ i ∈ s, f i * g i) fun i ↦ f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Tactic:
·

Goal state after:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
⊢ (fun i ↦ f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g ↦ ∑ i ∈ s, f i * g i) fun i ↦ f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case right
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ upperBounds ((fun g ↦ ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1})

Tactic:
·

Goal state after:
case right
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ upperBounds ((fun g ↦ ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1})
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
hp : 1 ≤ 1
⊢ (∑ i ∈ s, (f i + g i) ^ 1) ^ (1 / 1) ≤ (∑ i ∈ s, f i ^ 1) ^ (1 / 1) + (∑ i ∈ s, g i ^ 1) ^ (1 / 1)

pp: case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
·

Goal state after:
case inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
hp : 1 ≤ 1
⊢ (∑ i ∈ s, (f i + g i) ^ 1) ^ (1 / 1) ≤ (∑ i ∈ s, f i ^ 1) ^ (1 / 1) + (∑ i ∈ s, g i ^ 1) ^ (1 / 1)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

pp: case inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ = ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

pp: case inr.inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ = ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)