ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>min (f x) (f y) < f (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>hz : z ∈ openSegment 𝕜 x y<GOAL>f z < max (f x) (f y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>hz : z ∈ openSegment 𝕜 x y<GOAL>min (f x) (f y) < f z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>hfy : f y ≤ f (a • x + b • y)<GOAL>f (a • x + b • y) ≤ f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>hfy : f (a • x + b • y) ≤ f y<GOAL>f x ≤ f (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : E<VAR>a b : 𝕜<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hfx : f x ≤ f (a • x + b • y)<GOAL>f (a • x + b • y) ≤ f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>x y : E<VAR>a b : 𝕜<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hfx : f (a • x + b • y) ≤ f x<GOAL>f y ≤ f (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hz : z ∈ openSegment 𝕜 x y<VAR>hyz : f y ≤ f z<GOAL>f z ≤ f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hz : z ∈ openSegment 𝕜 x y<VAR>hyz : f z ≤ f y<GOAL>f x ≤ f z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hz : z ∈ openSegment 𝕜 x y<VAR>hxz : f x ≤ f z<GOAL>f z ≤ f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hz : z ∈ openSegment 𝕜 x y<VAR>hxz : f z ≤ f x<GOAL>f y ≤ f z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hfy : f y < f (a • x + b • y)<GOAL>f (a • x + b • y) < f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hfy : f (a • x + b • y) < f y<GOAL>f x < f (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : E<VAR>a b : 𝕜<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hfx : f x < f (a • x + b • y)<GOAL>f (a • x + b • y) < f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>x y : E<VAR>a b : 𝕜<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hfx : f (a • x + b • y) < f x<GOAL>f y < f (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hz : z ∈ openSegment 𝕜 x y<VAR>hyz : f y < f z<GOAL>f z < f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hz : z ∈ openSegment 𝕜 x y<VAR>hyz : f z < f y<GOAL>f x < f z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hz : z ∈ openSegment 𝕜 x y<VAR>hxz : f x < f z<GOAL>f z < f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hz : z ∈ openSegment 𝕜 x y<VAR>hxz : f z < f x<GOAL>f y < f z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommGroup β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>ConvexOn 𝕜 s (-f) ↔ ConcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommGroup β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>ConcaveOn 𝕜 s (-f) ↔ ConvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommGroup β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>StrictConvexOn 𝕜 s (-f) ↔ StrictConcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommGroup β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>StrictConcaveOn 𝕜 s (-f) ↔ StrictConvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommGroup β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<GOAL>ConvexOn 𝕜 s (f - g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommGroup β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<GOAL>ConcaveOn 𝕜 s (f - g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommGroup β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hg : StrictConcaveOn 𝕜 s g<GOAL>StrictConvexOn 𝕜 s (f - g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommGroup β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>hg : StrictConvexOn 𝕜 s g<GOAL>StrictConcaveOn 𝕜 s (f - g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommGroup β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : StrictConcaveOn 𝕜 s g<GOAL>StrictConvexOn 𝕜 s (f - g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommGroup β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : StrictConvexOn 𝕜 s g<GOAL>StrictConcaveOn 𝕜 s (f - g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommGroup β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<GOAL>StrictConvexOn 𝕜 s (f - g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommGroup β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<GOAL>StrictConcaveOn 𝕜 s (f - g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCancelCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>c : E<GOAL>StrictConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCancelCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>c : E<GOAL>StrictConcaveOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCancelCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>c : E<GOAL>StrictConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCancelCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>c : E<GOAL>StrictConcaveOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedCommSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>c : 𝕜<VAR>hc : 0 ≤ c<VAR>hf : ConvexOn 𝕜 s f<GOAL>ConvexOn 𝕜 s fun x => c • f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedCommSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>c : 𝕜<VAR>hc : 0 ≤ c<VAR>hf : ConcaveOn 𝕜 s f<GOAL>ConcaveOn 𝕜 s fun x => c • f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>SMul 𝕜 β<VAR>f : F → β<VAR>g : E →ᵃ[𝕜] F<VAR>s : Set F<VAR>hf : ConvexOn 𝕜 s f<GOAL>ConvexOn 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>SMul 𝕜 β<VAR>f : F → β<VAR>g : E →ᵃ[𝕜] F<VAR>s : Set F<VAR>hf : ConcaveOn 𝕜 s f<GOAL>ConcaveOn 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>ConvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>ConcaveOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • f x + (b / (a + b)) • f y ≤ f ((a / (a + b)) • x + (b / (a + b)) • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>StrictConvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>StrictConcaveOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • f x + (b / (a + b)) • f y < f ((a / (a + b)) • x + (b / (a + b)) • y)
<VAR>𝕜 : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommMonoid α<VAR>SMul 𝕜 α<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConcaveOn 𝕜 Set.univ ⇑f<GOAL>StrictConvexOn 𝕜 Set.univ ⇑f.symm
<VAR>𝕜 : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommMonoid α<VAR>SMul 𝕜 α<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConcaveOn 𝕜 Set.univ ⇑f<GOAL>ConvexOn 𝕜 Set.univ ⇑f.symm
<VAR>𝕜 : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommMonoid α<VAR>SMul 𝕜 α<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConvexOn 𝕜 Set.univ ⇑f<GOAL>StrictConcaveOn 𝕜 Set.univ ⇑f.symm
<VAR>𝕜 : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommMonoid α<VAR>SMul 𝕜 α<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConvexOn 𝕜 Set.univ ⇑f<GOAL>ConcaveOn 𝕜 Set.univ ⇑f.symm
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>OrderedAddCommMonoid β<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : E → β<VAR>s : Set E<VAR>x y : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hfx : IsMinOn f s x<VAR>hfy : IsMinOn f s y<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>OrderedAddCommMonoid β<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : E → β<VAR>s : Set E<VAR>x y : E<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>hfx : IsMaxOn f s x<VAR>hfy : IsMaxOn f s y<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>LinearOrderedCancelAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>x y z : 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → β<VAR>hf : ConvexOn 𝕜 s f<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y ≤ z<VAR>h : f x ≤ f y<GOAL>f y ≤ f z
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>LinearOrderedCancelAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>x y z : 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → β<VAR>hf : ConvexOn 𝕜 s f<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x ≤ y<VAR>hyz : y < z<VAR>h : f z ≤ f y<GOAL>f y ≤ f x
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>LinearOrderedCancelAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>x y z : 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y ≤ z<VAR>h : f y ≤ f x<GOAL>f z ≤ f y
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>LinearOrderedCancelAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>x y z : 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x ≤ y<VAR>hyz : y < z<VAR>h : f y ≤ f z<GOAL>f x ≤ f y
<GOAL>⇑Real.Angle.coeHom = Real.Angle.coe
<VAR>p : Real.Angle → Prop<VAR>θ : Real.Angle<VAR>h : ∀ (x : ℝ), p ↑x<GOAL>p θ
<VAR>x y : ℝ<GOAL>↑(x + y) = ↑x + ↑y
<VAR>x : ℝ<GOAL>↑(-x) = -↑x
<VAR>x y : ℝ<GOAL>↑(x - y) = ↑x - ↑y
<VAR>n : ℕ<VAR>x : ℝ<GOAL>↑(n • x) = n • ↑x
<VAR>z : ℤ<VAR>x : ℝ<GOAL>↑(z • x) = z • ↑x
<VAR>θ : Real.Angle<GOAL>θ - ↑π = θ + ↑π
<VAR>ψ θ : Real.Angle<VAR>z : ℤ<VAR>hz : z ≠ 0<GOAL>z • ψ = z • θ ↔ ∃ k, ψ = θ + ↑k • ↑(2 * π / ↑z)
<VAR>ψ θ : Real.Angle<VAR>n : ℕ<VAR>hz : n ≠ 0<GOAL>n • ψ = n • θ ↔ ∃ k, ψ = θ + ↑k • ↑(2 * π / ↑n)
<VAR>ψ θ : Real.Angle<GOAL>2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
<VAR>θ : Real.Angle<GOAL>2 • θ = 0 ↔ θ = 0 ∨ θ = ↑π
<VAR>θ : Real.Angle<GOAL>2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π
<VAR>θ : Real.Angle<GOAL>θ = -θ ↔ θ = 0 ∨ θ = ↑π
<VAR>θ : Real.Angle<GOAL>θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ ↑π
<VAR>θ : Real.Angle<GOAL>-θ = θ ↔ θ = 0 ∨ θ = ↑π
<VAR>θ : Real.Angle<GOAL>-θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ ↑π
<VAR>θ : Real.Angle<GOAL>2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
<VAR>θ ψ : ℝ<GOAL>Real.cos θ = Real.cos ψ ↔ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
<VAR>θ ψ : ℝ<GOAL>Real.sin θ = Real.sin ψ ↔ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
<VAR>θ ψ : ℝ<VAR>Hcos : Real.cos θ = Real.cos ψ<VAR>Hsin : Real.sin θ = Real.sin ψ<GOAL>↑θ = ↑ψ
<VAR>x : ℝ<GOAL>(↑x).sin = Real.sin x
<VAR>x : ℝ<GOAL>(↑x).cos = Real.cos x
<VAR>θ : Real.Angle<VAR>ψ : ℝ<GOAL>θ.cos = Real.cos ψ ↔ θ = ↑ψ ∨ θ = -↑ψ
<VAR>θ ψ : Real.Angle<GOAL>θ.cos = ψ.cos ↔ θ = ψ ∨ θ = -ψ
<VAR>θ : Real.Angle<VAR>ψ : ℝ<GOAL>θ.sin = Real.sin ψ ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑π
<VAR>θ ψ : Real.Angle<GOAL>θ.sin = ψ.sin ↔ θ = ψ ∨ θ + ψ = ↑π
<VAR>θ : Real.Angle<GOAL>θ.sin = 0 ↔ θ = 0 ∨ θ = ↑π
<VAR>θ : Real.Angle<GOAL>θ.sin ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π
<VAR>θ : Real.Angle<GOAL>(-θ).sin = -θ.sin
<GOAL>Function.Antiperiodic Real.Angle.sin ↑π
<VAR>θ : Real.Angle<GOAL>(θ + ↑π).sin = -θ.sin
<VAR>θ : Real.Angle<GOAL>(θ - ↑π).sin = -θ.sin
<VAR>θ : Real.Angle<GOAL>(-θ).cos = θ.cos
<GOAL>Function.Antiperiodic Real.Angle.cos ↑π
<VAR>θ : Real.Angle<GOAL>(θ + ↑π).cos = -θ.cos
<VAR>θ : Real.Angle<GOAL>(θ - ↑π).cos = -θ.cos
<VAR>θ : Real.Angle<GOAL>θ.cos = 0 ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
<VAR>θ₁ θ₂ : Real.Angle<GOAL>(θ₁ + θ₂).sin = θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin
<VAR>θ₁ θ₂ : Real.Angle<GOAL>(θ₁ + θ₂).cos = θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin
<VAR>θ : Real.Angle<GOAL>θ.cos ^ 2 + θ.sin ^ 2 = 1
<VAR>θ : Real.Angle<GOAL>(θ + ↑(π / 2)).sin = θ.cos
<VAR>θ : Real.Angle<GOAL>(θ - ↑(π / 2)).sin = -θ.cos
<VAR>θ : Real.Angle<GOAL>(↑(π / 2) - θ).sin = θ.cos
<VAR>θ : Real.Angle<GOAL>(θ + ↑(π / 2)).cos = -θ.sin
<VAR>θ : Real.Angle<GOAL>(θ - ↑(π / 2)).cos = θ.sin
<VAR>θ : Real.Angle<GOAL>(↑(π / 2) - θ).cos = θ.sin
<VAR>θ ψ : Real.Angle<VAR>h : 2 • θ = 2 • ψ<GOAL>|θ.sin| = |ψ.sin|
<VAR>θ ψ : Real.Angle<VAR>h : 2 • θ = 2 • ψ<GOAL>|θ.cos| = |ψ.cos|
<VAR>θ ψ : ℝ<GOAL>↑(toIcoMod Real.two_pi_pos ψ θ) = ↑θ
<VAR>θ ψ : ℝ<GOAL>↑(toIocMod Real.two_pi_pos ψ θ) = ↑θ
<VAR>θ : ℝ<GOAL>(↑θ).toReal = toIocMod Real.two_pi_pos (-π) θ
<VAR>θ ψ : Real.Angle<GOAL>θ.toReal = ψ.toReal ↔ θ = ψ
<VAR>θ : Real.Angle<GOAL>↑θ.toReal = θ
<VAR>θ : Real.Angle<GOAL>-π < θ.toReal
<VAR>θ : Real.Angle<GOAL>θ.toReal ≤ π
<VAR>θ : Real.Angle<GOAL>|θ.toReal| ≤ π
<VAR>θ : Real.Angle<GOAL>θ.toReal ∈ Set.Ioc (-π) π
<VAR>θ : Real.Angle<GOAL>toIocMod Real.two_pi_pos (-π) θ.toReal = θ.toReal
<VAR>θ : Real.Angle<GOAL>θ.toReal = 0 ↔ θ = 0
<VAR>θ : Real.Angle<GOAL>θ.toReal = π ↔ θ = ↑π
<VAR>θ : Real.Angle<GOAL>θ.toReal = π / 2 ↔ θ = ↑(π / 2)
<VAR>θ : Real.Angle<GOAL>θ.toReal = -π / 2 ↔ θ = ↑(-π / 2)
<VAR>θ : ℝ<GOAL>|(↑θ).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ π
<VAR>θ : Real.Angle<GOAL>|θ.toReal| = π / 2 ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>θ : Real.Angle<GOAL>(n • θ).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)
<VAR>θ : Real.Angle<GOAL>(2 • θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
<VAR>θ : Real.Angle<GOAL>(2 • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
<VAR>θ : Real.Angle<GOAL>(2 • θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
<VAR>θ : Real.Angle<GOAL>Real.sin θ.toReal = θ.sin
<VAR>θ : Real.Angle<GOAL>Real.cos θ.toReal = θ.cos
<VAR>θ : Real.Angle<GOAL>0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2
<VAR>θ : Real.Angle<GOAL>0 < θ.cos ↔ |θ.toReal| < π / 2
<VAR>θ : Real.Angle<GOAL>θ.cos < 0 ↔ π / 2 < |θ.toReal|
<VAR>θ ψ : Real.Angle<VAR>h : 2 • θ + 2 • ψ = ↑π<GOAL>|θ.cos| = |ψ.sin|
<VAR>θ : Real.Angle<GOAL>θ.tan = θ.sin / θ.cos
<VAR>θ : Real.Angle<GOAL>(θ + ↑π).tan = θ.tan
<VAR>θ : Real.Angle<GOAL>(θ - ↑π).tan = θ.tan
<VAR>θ : Real.Angle<GOAL>Real.tan θ.toReal = θ.tan
<VAR>θ ψ : Real.Angle<VAR>h : 2 • θ = 2 • ψ<GOAL>θ.tan = ψ.tan
<VAR>θ ψ : Real.Angle<VAR>h : 2 • θ + 2 • ψ = ↑π<GOAL>ψ.tan = θ.tan⁻¹
<VAR>θ : Real.Angle<GOAL>(-θ).sign = -θ.sign
<GOAL>Function.Antiperiodic Real.Angle.sign ↑π
<VAR>θ : Real.Angle<GOAL>(θ + ↑π).sign = -θ.sign
<VAR>θ : Real.Angle<GOAL>(↑π + θ).sign = -θ.sign
<VAR>θ : Real.Angle<GOAL>(θ - ↑π).sign = -θ.sign
<VAR>θ : Real.Angle<GOAL>(↑π - θ).sign = θ.sign
<VAR>θ : Real.Angle<GOAL>θ.sign = 0 ↔ θ = 0 ∨ θ = ↑π
<VAR>θ : Real.Angle<GOAL>θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π
<VAR>θ : Real.Angle<GOAL>θ.toReal < 0 ↔ θ.sign = -1
<VAR>θ : Real.Angle<GOAL>0 ≤ θ.toReal ↔ 0 ≤ θ.sign
<VAR>θ : Real.Angle<VAR>h : θ ≠ ↑π<GOAL>SignType.sign θ.toReal = θ.sign
<VAR>θ : Real.Angle<VAR>h : 0 ≤ θ.sign<GOAL>↑|θ.toReal| = θ
<VAR>θ : Real.Angle<VAR>h : θ.sign ≤ 0<GOAL>-↑|θ.toReal| = θ
<VAR>θ ψ : Real.Angle<GOAL>θ = ψ ↔ θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal|
<VAR>θ ψ : Real.Angle<VAR>h : θ.sign = ψ.sign<GOAL>θ = ψ ↔ |θ.toReal| = |ψ.toReal|
<VAR>θ : Real.Angle<GOAL>(2 • θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2
<VAR>θ : Real.Angle<VAR>h0 : θ ≠ 0<VAR>hpi : θ ≠ ↑π<GOAL>ContinuousAt Real.Angle.sign θ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → Real.Angle<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π<GOAL>ContinuousOn (Real.Angle.sign ∘ f) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → Real.Angle<VAR>s : Set α<VAR>x y : α<VAR>hc : IsConnected s<VAR>hf : ContinuousOn f s<VAR>hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>(f y).sign = (f x).sign
<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>expNegInvGlue x = 0
<VAR>x : ℝ<GOAL>expNegInvGlue x = 0 ↔ x ≤ 0
<VAR>p : ℝ[X]<GOAL>Filter.Tendsto (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (𝓝 0) (𝓝 0)
<VAR>p : ℝ[X]<VAR>x : ℝ<GOAL>HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (Polynomial.eval x⁻¹ (Polynomial.X ^ 2 * (p - Polynomial.derivative p)) * expNegInvGlue x) x
<VAR>p : ℝ[X]<GOAL>Differentiable ℝ fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
<VAR>p : ℝ[X]<GOAL>Continuous fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
<VAR>x : ℝ<GOAL>0 < expNegInvGlue x + expNegInvGlue (1 - x)
<VAR>x : ℝ<VAR>h : 1 ≤ x<GOAL>x.smoothTransition = 1
<VAR>x : ℝ<VAR>h : x ≤ 0<GOAL>x.smoothTransition = 0
<VAR>x : ℝ<GOAL>(↑(Set.projIcc 0 1 ⋯ x)).smoothTransition = x.smoothTransition
<VAR>x : ℝ<GOAL>x.smoothTransition ≤ 1
<VAR>x : ℝ<GOAL>0 ≤ x.smoothTransition
<VAR>x : ℝ<VAR>h : x < 1<GOAL>x.smoothTransition < 1
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>0 < x.smoothTransition
<VAR>n : ℕ∞<GOAL>ContDiff ℝ n Real.smoothTransition
<VAR>x : ℝ<VAR>n : ℕ∞<GOAL>ContDiffAt ℝ n Real.smoothTransition x
<VAR>x : ℝ<GOAL>ContinuousAt Real.smoothTransition x
<VAR>x : ℝ<GOAL>rexp (Real.arsinh x) = x + √(1 + x ^ 2)
<VAR>x : ℝ<GOAL>Real.arsinh (-x) = -Real.arsinh x
<VAR>x : ℝ<GOAL>Real.sinh (Real.arsinh x) = x
<VAR>x : ℝ<GOAL>Real.cosh (Real.arsinh x) = √(1 + x ^ 2)
<VAR>x : ℝ<GOAL>Real.arsinh (Real.sinh x) = x
<VAR>x : ℝ<GOAL>Real.sinhEquiv.symm x = Real.arsinh x
<VAR>x : ℝ<GOAL>Real.sinhEquiv x = Real.sinh x
<GOAL>⇑(RelIso.symm Real.sinhOrderIso) = Real.arsinh
<GOAL>⇑Real.sinhHomeomorph.symm = Real.arsinh