mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞
hp' : 0 < p.toReal
this : 0 < 1 / p.toReal
⊢ eLpNorm f p μ < ∞

Tactic:
simpa using

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞
hp' : 0 < p.toReal
this : 0 < 1 / p.toReal
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: case inr
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
hc : c ≠ 0
⊢ eLpNorm' f q μ ≤ eLpNorm' (c • f) q μ / ‖c‖ₑ

Tactic:
simpa using

Goal state after:
case inr
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
hc : c ≠ 0
⊢ eLpNorm' f q μ ≤ ‖c‖ₑ⁻¹ * eLpNorm' (c • f) q μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: case inr
α : Type u_1
F : Type u_2
m : MeasurableSpace α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
⊢ eLpNorm f p μ ≤ eLpNorm (c • f) p μ / ‖c‖ₑ

Tactic:
simpa using

Goal state after:
case inr
α : Type u_1
F : Type u_2
m : MeasurableSpace α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
⊢ eLpNorm f p μ ≤ ‖c‖ₑ⁻¹ * eLpNorm (c • f) p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: α : Type u_1
F : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : α → F
⊢ eLpNorm (n • f) p μ = ↑n * eLpNorm f p μ

Tactic:
simpa using

Goal state after:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : α → F
⊢ eLpNorm (n • f) p μ = ↑n * eLpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg.inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
hμ_ne_top : μ Set.univ ≠ ∞
⊢ ‖c‖ₑ < ∞ ∧ μ Set.univ ^ (1 / p.toReal) < ∞ ∨ ‖c‖ₑ = 0 ∨ μ Set.univ ^ (1 / p.toReal) = 0 ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞

Tactic:
simpa using

Goal state after:
case neg.inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
hμ_ne_top : μ Set.univ ≠ ∞
⊢ μ Set.univ ^ p.toReal⁻¹ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
hp' : p = ∞
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
hp' : p = ∞
⊢ eLpNormEssSup f μ ≤ c * eLpNormEssSup g μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
hp' : ¬p = ∞
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
hp' : ¬p = ∞
⊢ eLpNorm' f p.toReal μ ≤ c * eLpNorm' g p.toReal μ
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α : Type u
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (Measure.pi fun x ↦ μ) (μ.prod μ)

Tactic:
simpa using

Goal state after:
α : Type u
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (Measure.pi fun x ↦ μ) (μ.prod μ)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ

Tactic:
simpa using

Goal state after:
α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
R : Type u_5
inst✝² : NormedAddCommGroup R
inst✝¹ : StarAddMonoid R
inst✝ : NormedStarGroup R
p : ℝ≥0∞
f : α → R
hf : MemLp f p μ
⊢ eLpNorm (star f) p μ < ∞

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
R : Type u_5
inst✝² : NormedAddCommGroup R
inst✝¹ : StarAddMonoid R
inst✝ : NormedStarGroup R
p : ℝ≥0∞
f : α → R
hf : MemLp f p μ
⊢ eLpNorm f p μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ

Tactic:
simpa using

Goal state after:
α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
⊢ 1 / p + 1 / q = 1 / r

Tactic:
simpa using

Goal state after:
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
⊢ p⁻¹ + q⁻¹ = r⁻¹
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hr : r ≠ 0
⊢ r⁻¹ < ∞

Tactic:
simpa using

Goal state after:
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hr : r ≠ 0
⊢ 0 < r
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
⊢ eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹

Tactic:
simpa using

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
⊢ eLpNorm f p μ ≤ ↑C * μ Set.univ ^ p.toReal⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
x✝ : α
hx : ‖f x✝‖₊ ≤ C
⊢ ‖f x✝‖ₑ ≤ ↑C

Tactic:
simpa using

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
x✝ : α
hx : ‖f x✝‖₊ ≤ C
⊢ ‖f x✝‖₊ ≤ C
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
⊢ 1 + p * s < rexp (log (1 + s) * p)

Tactic:
← exp_log hs2

Goal state after:
case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
⊢ rexp (log (1 + p * s)) < rexp (log (1 + s) * p)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
⊢ rexp (log (1 + s) * p) < 1 + p * s

Tactic:
← exp_log hs2

Goal state after:
case inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
⊢ rexp (log (1 + s) * p) < rexp (log (1 + p * s))
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ ¬p.toReal ≤ 0

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ 0 < p.toReal
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg.e_a
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
this : ¬p.toReal ≤ 0
⊢ (Function.support fun x ↦ ‖f x‖ₑ ^ p.toReal) ⊆ s

Tactic:
simpa using

Goal state after:
case neg.e_a
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
this : ¬p.toReal ≤ 0
⊢ ∀ (x : α), ¬f x = 0 → x ∈ s
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ
h : p.HolderTriple q r
⊢ 1 / p + 1 / q = 1 / r

Tactic:
simpa using

Goal state after:
p q r : ℝ
h : p.HolderTriple q r
⊢ p⁻¹ + q⁻¹ = r⁻¹
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ
h : p.HolderTriple q r
⊢ r < p

Tactic:
simpa using

Goal state after:
p q r : ℝ
h : p.HolderTriple q r
⊢ r < p
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ
h : p.HolderConjugate q
⊢ p⁻¹ - 1 = -q⁻¹

Tactic:
simpa using

Goal state after:
p q : ℝ
h : p.HolderConjugate q
⊢ p⁻¹ - 1 = -q⁻¹
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ
h : p.HolderConjugate q
⊢ p * q = p + q

Tactic:
simpa using

Goal state after:
p q : ℝ
h : p.HolderConjugate q
⊢ p * q = p + q
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a⁻¹⁻¹ + b⁻¹⁻¹ = 1⁻¹

Tactic:
simpa using

Goal state after:
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a + b = 1
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (1 / a).HolderConjugate (1 / b)

Tactic:
simpa using

Goal state after:
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a⁻¹.HolderConjugate b⁻¹
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: ⊢ 2⁻¹ + 2⁻¹ = 1⁻¹

Tactic:
simpa using

Goal state after:
⊢ 2⁻¹ + 2⁻¹ = 1
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0
h : p.HolderConjugate q
⊢ p * q = p + q

Tactic:
simpa using

Goal state after:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ p * q = p + q
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a⁻¹⁻¹ + b⁻¹⁻¹ = 1⁻¹

Tactic:
simpa using

Goal state after:
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a + b = 1
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: a : ℝ≥0
ha₀ : 0 < a
ha₁ : a < 1
⊢ a⁻¹⁻¹ + (1 - a)⁻¹⁻¹ = 1

Tactic:
simpa using

Goal state after:
a : ℝ≥0
ha₀ : 0 < a
ha₁ : a < 1
⊢ a + (1 - a) = 1
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (1 / a).HolderConjugate (1 / b)

Tactic:
simpa using

Goal state after:
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a⁻¹.HolderConjugate b⁻¹
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ
h : p.HolderConjugate q
⊢ p.toNNReal.HolderConjugate q.toNNReal

Tactic:
simpa using

Goal state after:
p q : ℝ
h : p.HolderConjugate q
⊢ p.toNNReal.HolderConjugate q.toNNReal
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ
h : p.HolderTriple q r
⊢ (ENNReal.ofReal p).HolderTriple (ENNReal.ofReal q) (ENNReal.ofReal r)

Tactic:
simpa using

Goal state after:
p q r : ℝ
h : p.HolderTriple q r
⊢ (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = (ENNReal.ofReal r)⁻¹
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ
h : p.HolderConjugate q
⊢ (ENNReal.ofReal p).HolderConjugate (ENNReal.ofReal q)

Tactic:
simpa using

Goal state after:
p q : ℝ
h : p.HolderConjugate q
⊢ (ENNReal.ofReal p).HolderConjugate (ENNReal.ofReal q)
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p ∧ p < ∞
hq : 0 < q ∧ q < ∞
hr : 0 < r ∧ r < ∞
⊢ p.HolderTriple q r

Tactic:
simpa using

Goal state after:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p ∧ p < ∞
hq : 0 < q ∧ q < ∞
hr : 0 < r ∧ r < ∞
⊢ p.HolderTriple q r
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ≥0∞
hp : 0 < p ∧ p < ∞
hq : 0 < q ∧ q < ∞
h : p.HolderTriple q r
⊢ p.toReal⁻¹ + q.toReal⁻¹ = r.toReal⁻¹

Tactic:
simpa using

Goal state after:
p q r : ℝ≥0∞
hp : 0 < p ∧ p < ∞
hq : 0 < q ∧ q < ∞
h : p.HolderTriple q r
⊢ p.toReal⁻¹ + q.toReal⁻¹ = r.toReal⁻¹
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ≥0∞
h : p.toNNReal.HolderTriple q.toNNReal r.toNNReal
⊢ p.toReal.HolderTriple q.toReal r.toReal

Tactic:
simpa using

Goal state after:
p q r : ℝ≥0∞
h : p.toNNReal.HolderTriple q.toNNReal r.toNNReal
⊢ p.toReal.HolderTriple q.toReal r.toReal
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
hq : 0 < q.toReal
⊢ p.toReal.HolderConjugate q.toReal

Tactic:
simpa using

Goal state after:
p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
hq : 0 < q.toReal
⊢ p.toReal.HolderConjugate q.toReal
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0∞
h : p.toNNReal.HolderConjugate q.toNNReal
⊢ p.toReal.HolderConjugate q.toReal

Tactic:
simpa using

Goal state after:
p q : ℝ≥0∞
h : p.toNNReal.HolderConjugate q.toNNReal
⊢ p.toReal.HolderConjugate q.toReal
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case inr.inr
p q : ℝ≥0∞
h : p.HolderConjugate q
hp : p ≠ ∞
hq : q ≠ ∞
⊢ p * q = p + q

Tactic:
simpa using

Goal state after:
case inr.inr
p q : ℝ≥0∞
h : p.HolderConjugate q
hp : p ≠ ∞
hq : q ≠ ∞
⊢ p * q = q + p
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: a b : ℝ≥0∞
hab : a + b = 1
⊢ a⁻¹⁻¹ + b⁻¹⁻¹ = 1⁻¹

Tactic:
simpa using

Goal state after:
a b : ℝ≥0∞
hab : a + b = 1
⊢ a + b = 1
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: a b : ℝ≥0∞
hab : a + b = 1
⊢ a⁻¹⁻¹ + b⁻¹⁻¹ = 1⁻¹

Tactic:
by simpa [inv_inv] using hab

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: a : ℝ≥0∞
ha : 1 ≤ a
⊢ a.HolderConjugate (1 - a⁻¹)⁻¹

Tactic:
simpa using

Goal state after:
a : ℝ≥0∞
ha : 1 ≤ a
⊢ a.HolderConjugate (1 - a⁻¹)⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : p = ∞
⊢ eLpNormEssSup f μ = 0 ↔ f =ᵐ[μ] 0

Tactic:
eLpNormEssSup_eq_zero_iff

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : p = ∞
⊢ f =ᵐ[μ] 0 ↔ f =ᵐ[μ] 0
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hy : y ∈ s
hxy : x < y
hxy' : f y < f x
this : StrictMonoOn (f ∘ ⇑(-AffineMap.id 𝕜 𝕜)) (⇑(-AffineMap.id 𝕜 𝕜) ⁻¹' s ∩ Set.Ici (-x))
⊢ StrictAntiOn f (s ∩ Set.Iic x)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hy : y ∈ s
hxy : x < y
hxy' : f y < f x
this : StrictMonoOn (f ∘ ⇑(-AffineMap.id 𝕜 𝕜)) (⇑(-AffineMap.id 𝕜 𝕜) ⁻¹' s ∩ Set.Ici (-x))
⊢ StrictAntiOn f (s ∩ Set.Iic x)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y : 𝕜
hy : y ∈ s
hxy : x < y
hxy' : f x < f y
⊢ StrictMonoOn f (s ∩ Set.Iic x)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y : 𝕜
hy : y ∈ s
hxy : x < y
hxy' : f x < f y
⊢ StrictMonoOn f (s ∩ Set.Iic x)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f y < f x
⊢ StrictAntiOn f (s ∩ Set.Ici y)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f y < f x
⊢ StrictAntiOn f (s ∩ Set.Ici y)
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : CommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedMonoid β
s : Set ι
f : ι → α
g : ι → β
⊢ MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : CommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedMonoid β
s : Set ι
f : ι → α
g : ι → β
⊢ (∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → g j < g i → f i ≤ f j) ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → g i < g j → f j ≤ f i
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : CommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedMonoid β
s : Set ι
f : ι → α
g : ι → β
⊢ AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : CommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedMonoid β
s : Set ι
f : ι → α
g : ι → β
⊢ (∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → g j < g i → f j ≤ f i) ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → g i < g j → f i ≤ f j
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : CommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedMonoid β
f : ι → α
g : ι → β
⊢ Monovary f g⁻¹ ↔ Antivary f g

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : CommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedMonoid β
f : ι → α
g : ι → β
⊢ (∀ ⦃i j : ι⦄, g j < g i → f i ≤ f j) ↔ ∀ ⦃i j : ι⦄, g i < g j → f j ≤ f i
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : CommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedMonoid β
f : ι → α
g : ι → β
⊢ Antivary f g⁻¹ ↔ Monovary f g

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : CommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedMonoid β
f : ι → α
g : ι → β
⊢ (∀ ⦃i j : ι⦄, g j < g i → f j ≤ f i) ↔ ∀ ⦃i j : ι⦄, g i < g j → f i ≤ f j
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

Tactic:
simpa using

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_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:
· simpa [Fin.sum_univ_succ] using h

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.MeasureTheory.Integral.MeanInequalities

Goal state before:
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
h2p : 1 < 1 / p
h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1
this :
  ∫⁻ (a : α), ((fun x ↦ f x ^ p) * fun x ↦ g x ^ q) a ∂μ ≤
    (∫⁻ (a : α), (f a ^ p) ^ (1 / p) ∂μ) ^ (1 / (1 / p)) * (∫⁻ (a : α), (g a ^ q) ^ (1 / q) ∂μ) ^ (1 / (1 / q))
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
simpa using

Goal state after:
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
h2p : 1 < 1 / p
h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1
this :
  ∫⁻ (a : α), ((fun x ↦ f x ^ p) * fun x ↦ g x ^ q) a ∂μ ≤
    (∫⁻ (a : α), (f a ^ p) ^ (1 / p) ∂μ) ^ (1 / (1 / p)) * (∫⁻ (a : α), (g a ^ q) ^ (1 / q) ∂μ) ^ (1 / (1 / q))
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q