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

Goal state before:
pp: case e'_1
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x))

pp: case e'_2
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
⊢ (∀ j ∈ s, z j = ∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x

Tactic:
·

Goal state after:
case e'_1
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x))
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case inl
a b : ℝ≥0
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0

pp: case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
·

Goal state after:
case inl
a b : ℝ≥0
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_2
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
⊢ (∀ j ∈ s, z j = ∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x

Tactic:
·

Goal state after:
case e'_2
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
⊢ (∀ j ∈ s, z j = ∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

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

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

Tactic:
·

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

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

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

Tactic:
·

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

Goal state before:
pp: case refine_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
⊢ (∑ i ∈ s, w i * z i) ^ p = ∞ → ∑ i ∈ s, w i * z i ^ p = ∞

pp: case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
⊢ (∑ i ∈ s, w i * z i) ^ p ≠ ∞ →
    ∑ i ∈ s, w i * z i ^ p ≠ ∞ → ((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ (∑ i ∈ s, w i * z i ^ p).toNNReal

Tactic:
·

Goal state after:
case refine_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
⊢ (∑ i ∈ s, w i * z i) ^ p = ∞ → ∑ i ∈ s, w i * z i ^ p = ∞
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

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

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
·

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

Goal state before:
pp: case e'_2.mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
⊢ log (z j) = ∑ x ∈ s, log (z x) * w x

pp: case e'_2.mpr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
⊢ z j = ∑ i ∈ s, w i * z i

Tactic:
·

Goal state after:
case e'_2.mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
⊢ log (z j) = ∑ x ∈ s, log (z x) * w x
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
⊢ (∑ i ∈ s, w i * z i) ^ p ≠ ∞ →
    ∑ i ∈ s, w i * z i ^ p ≠ ∞ → ((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ (∑ i ∈ s, w i * z i ^ p).toNNReal

Tactic:
·

Goal state after:
case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
⊢ (∑ i ∈ s, w i * z i) ^ p ≠ ∞ →
    ∑ i ∈ s, w i * z i ^ p ≠ ∞ → ((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ (∑ i ∈ s, w i * z i ^ p).toNNReal
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
hg_top : ∫⁻ (a : α), g a ^ q ∂μ = ∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
hg_top : ¬∫⁻ (a : α), g a ^ q ∂μ = ∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
·

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
q : ℝ
hq : 0 ≤ q
hp : 0 ≤ 0
hpq : 0 + q = 1
⊢ ∫⁻ (a : α), f a ^ 0 * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ 0 * (∫⁻ (a : α), g a ∂μ) ^ q

pp: case inr
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
q : ℝ
hq : 0 ≤ q
hp : 0 ≤ 0
hpq : 0 + q = 1
⊢ ∫⁻ (a : α), f a ^ 0 * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ 0 * (∫⁻ (a : α), g a ∂μ) ^ q
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p : ℝ
hp✝ : 0 ≤ p
hp : 0 < p
hq : 0 ≤ 0
hpq : p + 0 = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ 0 ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ 0

pp: case inr.inr
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
·

Goal state after:
case inr.inl
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p : ℝ
hp✝ : 0 ≤ p
hp : 0 < p
hq : 0 ≤ 0
hpq : p + 0 = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ 0 ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ 0
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_2.mpr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
⊢ z j = ∑ i ∈ s, w i * z i

Tactic:
·

Goal state after:
case e'_2.mpr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
⊢ z j = ∑ i ∈ s, w i * z i
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case insert.inl
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

pp: case insert.inr
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
·

Goal state after:
case insert.inl
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case refine_2
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
h : (∑ i, ![w₁, w₂] i * ![z₁, z₂] i) ^ p ≤ ∑ i, ![w₁, w₂] i * ![z₁, z₂] i ^ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p

pp: case refine_1
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i, ![w₁, w₂] i = 1

Tactic:
·

Goal state after:
case refine_2
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
h : (∑ i, ![w₁, w₂] i * ![z₁, z₂] i) ^ p ≤ ∑ i, ![w₁, w₂] i * ![z₁, z₂] i ^ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case refine_1
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i, ![w₁, w₂] i = 1

Tactic:
·

Goal state after:
case refine_1
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i, ![w₁, w₂] i = 1
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case e'_3
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p

pp: case e'_4
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p

Tactic:
·

Goal state after:
case e'_3
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case e'_4
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p

Tactic:
·

Goal state after:
case e'_4
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case pos
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : a + b = ∞
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

pp: case neg
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ∞
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
·

Goal state after:
case pos
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : a + b = ∞
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case insert.inr
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
·

Goal state after:
case insert.inr
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case inl
a b : ℝ≥0∞
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0

pp: case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
·

Goal state after:
case inl
a b : ℝ≥0∞
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case pos
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 2 ^ (1 / p.toReal - 1) < ∞

pp: case neg
p : ℝ≥0∞
h : p ∉ Set.Ioo 0 1
⊢ 1 < ∞

Tactic:
·

Goal state after:
case pos
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 2 ^ (1 / p.toReal - 1) < ∞
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case neg
p : ℝ≥0∞
h : p ∉ Set.Ioo 0 1
⊢ 1 < ∞

Tactic:
·

Goal state after:
case neg
p : ℝ≥0∞
h : p ∉ Set.Ioo 0 1
⊢ 1 < ∞
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case pos
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)

pp: case neg
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)

Tactic:
·

Goal state after:
case pos
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case left
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ 0 < (ENNReal.ofReal p)⁻¹

pp: case right
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ (ENNReal.ofReal p)⁻¹ < 1

Tactic:
·

Goal state after:
case left
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ 0 < (ENNReal.ofReal p)⁻¹
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case right
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ (ENNReal.ofReal p)⁻¹ < 1

Tactic:
·

Goal state after:
case right
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ (ENNReal.ofReal p)⁻¹ < 1
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i → ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k

pp: case mpr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ (∃ j ∈ s, ∃ k ∈ s, z j ≠ z k) → ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i

Tactic:
·

Goal state after:
case mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i → ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case neg
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)

Tactic:
·

Goal state after:
case neg
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case pos
z₁ z₂ p : ℝ≥0∞
p_zero : p = 0
⊢ (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)

pp: case neg
z₁ z₂ p : ℝ≥0∞
p_zero : ¬p = 0
⊢ (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)

Tactic:
·

Goal state after:
case pos
z₁ z₂ p : ℝ≥0∞
p_zero : p = 0
⊢ (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : p = q
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)

pp: case neg
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)

Tactic:
·

Goal state after:
case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : p = q
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∑ i ∈ s, w i * z i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ False

pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
·

Goal state after:
case mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∑ i ∈ s, w i * z i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ False
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
·

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i