mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.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
hs' : 0 < s
⊢ 1 + p * s < 1 + s

Tactic:
· gcongr
      exact mul_lt_of_lt_one_left hs' hp2

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

Goal state before:
pp: case refine_2
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
⊢ (↑p).HolderTriple ↑q ↑r

Tactic:
·

Goal state after:
case refine_2
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
⊢ (↑p).HolderTriple ↑q ↑r
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inl
s : ℝ
hs : -1 ≤ s
hp1 : 0 ≤ 0
hp2 : 0 ≤ 1
⊢ (1 + s) ^ 0 ≤ 1 + 0 * s

pp: case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2 : p ≤ 1
hp1 : 0 < p
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
·

Goal state after:
case inl
s : ℝ
hs : -1 ≤ s
hp1 : 0 ≤ 0
hp2 : 0 ≤ 1
⊢ (1 + s) ^ 0 ≤ 1 + 0 * s
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inl
s : ℝ
hs : -1 ≤ s
hp1✝ : 0 ≤ 1
hp2 : 1 ≤ 1
hp1 : 0 < 1
⊢ (1 + s) ^ 1 ≤ 1 + 1 * s

pp: case inr.inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
·

Goal state after:
case inr.inl
s : ℝ
hs : -1 ≤ s
hp1✝ : 0 ≤ 1
hp2 : 1 ≤ 1
hp1 : 0 < 1
⊢ (1 + s) ^ 1 ≤ 1 + 1 * s
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case pos
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
hs' : s = 0
⊢ (1 + s) ^ p ≤ 1 + p * s

pp: case neg
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
hs' : ¬s = 0
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
·

Goal state after:
case pos
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
hs' : s = 0
⊢ (1 + s) ^ p ≤ 1 + p * s
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case inl
hp : 1 ≤ 1
this : 1 ≠ 0
⊢ 1 + (1 - 1)⁻¹ = (1⁻¹ - 1⁻¹)⁻¹

pp: case inr
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹

Tactic:
·

Goal state after:
case inl
hp : 1 ≤ 1
this : 1 ≠ 0
⊢ 1 + (1 - 1)⁻¹ = (1⁻¹ - 1⁻¹)⁻¹
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case inr.inl
hp : 1 ≤ ∞
this : ∞ ≠ 0
hp₁ : 1 < ∞
⊢ 1 + (∞ - 1)⁻¹ = (1⁻¹ - ∞⁻¹)⁻¹

pp: case inr.inr
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹

Tactic:
·

Goal state after:
case inr.inl
hp : 1 ≤ ∞
this : ∞ ≠ 0
hp₁ : 1 < ∞
⊢ 1 + (∞ - 1)⁻¹ = (1⁻¹ - ∞⁻¹)⁻¹
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)

pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)

Tactic:
·

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya : y ≠ a
hxy : x < y
hxa : x < a
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya : y ≠ a
hxy : x < y
hxa : a < x
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya : y ≠ a
hxy : x < y
hxa : x < a
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inl.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

pp: case inl.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : a < y
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

Tactic:
·

Goal state after:
case inl.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ -1 ≤ x / y - 1

pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ x / y - 1 ≠ 0

Tactic:
·

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ -1 ≤ x / y - 1
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ x / y - 1 ≠ 0

Tactic:
·

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ x / y - 1 ≠ 0
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)

Tactic:
·

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : a < y
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

Tactic:
·

Goal state after:
case inl.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : a < y
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
Module: Mathlib.Data.Real.ConjExponents

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

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

Tactic:
·

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

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

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

Tactic:
·

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

Goal state before:
pp: case inl
p : ℝ≥0∞
h : p.HolderConjugate ∞
⊢ p / ∞ = p - 1

pp: case inr
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
⊢ p / q = p - 1

Tactic:
·

Goal state after:
case inl
p : ℝ≥0∞
h : p.HolderConjugate ∞
⊢ p / ∞ = p - 1
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya : y ≠ a
hxy : x < y
hxa : a < x
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya : y ≠ a
hxy : x < y
hxa : a < x
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
⊢ (IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) fun x ↦ ‖f x‖₊) → eLpNormEssSup f μ < ∞

Tactic:
rintro ⟨C, hC⟩; exact eLpNormEssSup_lt_top_of_ae_nnnorm_bound (C := C) hC

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case inl
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
⊢ eLpNorm f 0 μ < ∞

pp: case inr
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
⊢ eLpNorm f p μ < ∞

Tactic:
·

Goal state after:
case inl
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
⊢ eLpNorm f 0 μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : ∞ ≠ 0
⊢ eLpNorm f ∞ μ < ∞

pp: case inr.inr
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
⊢ eLpNorm f p μ < ∞

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : ∞ ≠ 0
⊢ eLpNorm f ∞ μ < ∞
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ -1 ≤ z / y - 1

pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ z / y - 1 ≠ 0

Tactic:
·

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ -1 ≤ z / y - 1
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ z / y - 1 ≠ 0

Tactic:
·

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ z / y - 1 ≠ 0
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu : y ∈ s ∩ Set.Ici y
huv : y < v
⊢ f y < f v

pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ f u < f v

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu : y ∈ s ∩ Set.Ici y
huv : y < v
⊢ f y < f v
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 = ∞
⊢ eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0

pp: case neg
α : 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 = ∞
⊢ eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0

Tactic:
·

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 = ∞
⊢ eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ f u < f v

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ f u < f v
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inr.refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ s

pp: case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ u ∈ openSegment 𝕜 y v

Tactic:
·

Goal state after:
case inr.refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ s
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inl
hp : 1 ≤ 1
⊢ ConvexOn ℝ (Ici 0) fun x ↦ x ^ 1

pp: case inr
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ ConvexOn ℝ (Ici 0) fun x ↦ x ^ p

Tactic:
·

Goal state after:
case inl
hp : 1 ≤ 1
⊢ ConvexOn ℝ (Ici 0) fun x ↦ x ^ 1
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✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
·

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ u ∈ openSegment 𝕜 y v

Tactic:
·

Goal state after:
case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ u ∈ openSegment 𝕜 y v
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✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : p = ∞
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
·

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : p = ∞
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
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✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
·

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
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✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : p = ∞
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : ¬p = ∞
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
·

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : p = ∞
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : ¬p = ∞
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
·

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : ¬p = ∞
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞

Tactic:
by_cases hp0 : p.toReal = 0

Goal state after:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞

case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞

pp: case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞

Tactic:
·

Goal state after:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : p = ∞
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ) atTop < ∞

pp: case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ∞
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ) atTop < ∞

Tactic:
·

Goal state after:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : p = ∞
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ) atTop < ∞