mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0∞
hp : 1 < p.toNNReal
⊢ p.toNNReal.HolderConjugate q.toNNReal ↔ p.HolderConjugate q

Tactic:
by

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

Goal state before:
pp: p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ AddLECancellable p⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
⊢ 0 < z - x

Tactic:
by

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

Goal state before:
pp: p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ p⁻¹ ≤ 1⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ε : Type u_8
inst✝ : ENorm ε
f : α → ε
μ ν : Measure α
⊢ eLpNorm f 1 (μ + ν) = eLpNorm f 1 μ + eLpNorm f 1 ν

Tactic:
by

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

Goal state before:
pp: p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
μ ν : Measure α
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ eLpNorm f p (μ + ν)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
μ ν : Measure α
p : ℝ≥0∞
⊢ eLpNorm f p ν ≤ eLpNorm f p (μ + ν)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f z - f x) / (z - x) < (f z - f y) / (z - y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
h : MemLp f p μ
⊢ eLpNorm (fun x ↦ ‖f x‖ₑ) p μ < ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
h : MemLp f p μ
x : α
⊢ ‖‖f x‖‖ ≤ ‖f x‖

Tactic:
by

Goal state after:
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
⊢ 0 < y - x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
h : MemLp (fun x ↦ ‖f x‖ₑ) p μ
⊢ eLpNorm f p μ < ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h : MemLp (fun x ↦ ‖f x‖) p μ
⊢ eLpNorm f p μ < ∞

Tactic:
rw [← eLpNorm_norm]

Goal state after:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h : MemLp (fun x ↦ ‖f x‖) p μ
⊢ eLpNorm (fun x ↦ ‖f x‖) p μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h : MemLp (fun x ↦ ‖f x‖) p μ
⊢ eLpNorm f p μ < ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
hq0_lt : 0 < q
hf_zero : f =ᵐ[μ] 0
⊢ eLpNorm' f q μ = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
hq0_ne : q ≠ 0
hμ : μ ≠ 0
f : α → ε
hf_zero : f =ᵐ[μ] 0
⊢ eLpNorm' f q μ = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
hf : f =ᵐ[μ] 0
⊢ eLpNorm f p μ = 0

Tactic:
by

Goal state after:
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
⊢ 0 < z - y

Tactic:
by

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

Goal state before:
pp: p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ (p - 1 + 1) / (p - 1) = (1⁻¹ - p⁻¹)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
p : ℝ
hp : 0 < p
hf : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖0 x‖ₑ

Tactic:
by

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

Goal state before:
pp: p : ℝ≥0∞
hp : 1 ≤ p
⊢ p.HolderConjugate p.conjExponent

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
p : ℝ
hp : 0 < p
hf : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0
⊢ eLpNorm' f p μ = 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
h : eLpNormEssSup f μ < ∞
⊢ ∀ᶠ (x : ℝ≥0) in map (fun x ↦ ‖f x‖₊) (ae μ), (fun x1 x2 ↦ x1 ≤ x2) x (eLpNormEssSup f μ).toNNReal

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p q : ℝ≥0∞
hp : 1 ≤ p
⊢ q = 1 + (p - 1)⁻¹ → p.HolderConjugate q

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : 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
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

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

Tactic:
by

Goal state after:
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
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
⊢ eLpNorm f p μ < ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
inst✝ : IsEmpty α
f : α → ε
p : ℝ≥0∞
⊢ eLpNorm f p μ = 0

Tactic:
by

Goal state after:
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 : 𝕜
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
⊢ ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : α → ε
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : eLpNorm' f q μ = 0
⊢ f =ᵐ[μ] 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : α → ε
⊢ eLpNormEssSup f μ = 0 ↔ f =ᵐ[μ] 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
⊢ StrictConvexOn ℝ (Ici 0) fun x ↦ x ^ p

Tactic:
by

Goal state after:
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 ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
⊢ eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ ConvexOn ℝ univ fun x ↦ b ^ x

Tactic:
by

Goal state after:
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 : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
⊢ StrictMonoOn f (s ∩ Set.Ici y)

Tactic:
by

Goal state after:
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
⊢ -y ∈ ⇑(-AffineMap.id 𝕜 𝕜) ⁻¹' s

Tactic:
by

Goal state after:
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
⊢ (f ∘ ⇑(-AffineMap.id 𝕜 𝕜)) (-y) < (f ∘ ⇑(-AffineMap.id 𝕜 𝕜)) (-x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < -x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
⊢ 0 < -y

Tactic:
by

Goal state after:
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))
x✝¹ : 𝕜
x✝ : x✝¹ ∈ s ∩ Set.Iic x
⊢ -id x✝¹ ∈ ⇑(-AffineMap.id 𝕜 𝕜) ⁻¹' s ∩ Set.Ici (-x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
⊢ -x ≠ -y

Tactic:
by

Goal state after:
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
⊢ StrictAntiOn f (s ∩ Set.Iic x)

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : 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 μ
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a • log x + b • log y = a • log (-x) + b • log (-y)

Tactic:
by

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

Goal state before:
pp: α : 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 μ
⊢ MemLp g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ log (a • -x + b • -y) = log (-(a • x + b • y))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_8
mβ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] E
hf : MeasurePreserving f μ ν
⊢ eLpNorm (↑(g.compMeasurePreserving f hf)) p μ = eLpNorm (↑g) p ν

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ log (-(a • x + b • y)) = log (a • x + b • y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔ Monovary (fun i ↦ f ↑i) fun i ↦ g ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn f g s ↔ Antivary (fun i ↦ f ↑i) fun i ↦ g ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: ⊢ StrictConcaveOn ℝ (Iio 0) log

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ rexp (t * x) = rexp ((1 + t) / 2 * x + (1 - t) / 2 * -x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ 0 ≤ (1 + t) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ 0 ≤ (1 - t) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ (1 + t) / 2 + (1 - t) / 2 = 1

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ MemLp g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ (1 + t) / 2 * rexp x + (1 - t) / 2 * rexp (-x) = cosh x + t * sinh x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: t : ℝ
ht : |t| ≤ 1
x : ℝ
⊢ rexp (t * x) ≤ cosh x + t * sinh x

Tactic:
by

Goal state after:
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
hp0 : ¬p.toReal = 0
h : p = 0
⊢ False

Tactic:
by

Goal state after:
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
hp0 : ¬p.toReal = 0
hp : p ≠ 0
h : p = ∞
⊢ False

Tactic:
by

Goal state after:
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
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
⊢ ↑R ^ p.toReal < ∞

Tactic:
by

Goal state after:
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

Goal state after:
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∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ∞
x : α
hx : liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞
hppos : 0 < p.toReal
⊢ liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop = liminf (fun n ↦ ‖f n x‖ₑ) atTop ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

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

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

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

Tactic:
by

Goal state after: