ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>a b c : ℝ<VAR>hne : a ≠ b<VAR>hc : c ∈ [[a, b]]<VAR>h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x<VAR>h_infty : Filter.Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) Filter.atTop<VAR>hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g<GOAL>¬IntervalIntegrable g MeasureTheory.volume a b
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>a b c : ℝ<VAR>h_deriv : ∀ᶠ (x : ℝ) in 𝓝[≠] c, DifferentiableAt ℝ f x<VAR>h_infty : Filter.Tendsto (fun x => ‖f x‖) (𝓝[≠] c) Filter.atTop<VAR>hg : deriv f =O[𝓝[≠] c] g<VAR>hne : a ≠ b<VAR>hc : c ∈ [[a, b]]<GOAL>¬IntervalIntegrable g MeasureTheory.volume a b
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>f : ℝ → F<VAR>a b c : ℝ<VAR>hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] c] f<VAR>hne : a ≠ b<VAR>hc : c ∈ [[a, b]]<GOAL>¬IntervalIntegrable f MeasureTheory.volume a b
<VAR>a b c : ℝ<GOAL>IntervalIntegrable (fun x => (x - c)⁻¹) MeasureTheory.volume a b ↔ a = b ∨ c ∉ [[a, b]]
<VAR>a b : ℝ<GOAL>IntervalIntegrable (fun x => x⁻¹) MeasureTheory.volume a b ↔ a = b ∨ 0 ∉ [[a, b]]
<VAR>a : ℝ<GOAL>¬MeasureTheory.IntegrableOn (fun x => x⁻¹) (Set.Ici a) MeasureTheory.volume
<VAR>a : ℝ<GOAL>¬MeasureTheory.IntegrableOn (fun x => x⁻¹) (Set.Ioi a) MeasureTheory.volume
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<GOAL>ConcaveOn 𝕜 s (⇑OrderDual.toDual ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<GOAL>ConvexOn 𝕜 s (⇑OrderDual.toDual ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConvexOn 𝕜 s f<GOAL>StrictConcaveOn 𝕜 s (⇑OrderDual.toDual ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<GOAL>StrictConvexOn 𝕜 s (⇑OrderDual.toDual ∘ f)
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 β<VAR>s : Set β<VAR>hs : Convex 𝕜 s<GOAL>ConvexOn 𝕜 s id
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 β<VAR>s : Set β<VAR>hs : Convex 𝕜 s<GOAL>ConcaveOn 𝕜 s id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>hfg : Set.EqOn f g s<GOAL>ConvexOn 𝕜 s g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>hfg : Set.EqOn f g s<GOAL>ConcaveOn 𝕜 s g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hfg : Set.EqOn f g s<GOAL>StrictConvexOn 𝕜 s g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>hfg : Set.EqOn f g s<GOAL>StrictConcaveOn 𝕜 s g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Set E<VAR>hf : ConvexOn 𝕜 t f<VAR>hst : s ⊆ t<VAR>hs : Convex 𝕜 s<GOAL>ConvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Set E<VAR>hf : ConcaveOn 𝕜 t f<VAR>hst : s ⊆ t<VAR>hs : Convex 𝕜 s<GOAL>ConcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Set E<VAR>hf : StrictConvexOn 𝕜 t f<VAR>hst : s ⊆ t<VAR>hs : Convex 𝕜 s<GOAL>StrictConvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Set E<VAR>hf : StrictConcaveOn 𝕜 t f<VAR>hst : s ⊆ t<VAR>hs : Convex 𝕜 s<GOAL>StrictConcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_4<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 α<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>g : β → α<VAR>hg : ConvexOn 𝕜 (f '' s) g<VAR>hf : ConvexOn 𝕜 s f<VAR>hg' : MonotoneOn g (f '' s)<GOAL>ConvexOn 𝕜 s (g ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_4<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 α<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>g : β → α<VAR>hg : ConcaveOn 𝕜 (f '' s) g<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg' : MonotoneOn g (f '' s)<GOAL>ConcaveOn 𝕜 s (g ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_4<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 α<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>g : β → α<VAR>hg : ConvexOn 𝕜 (f '' s) g<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg' : AntitoneOn g (f '' s)<GOAL>ConvexOn 𝕜 s (g ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_4<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 α<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>g : β → α<VAR>hg : ConcaveOn 𝕜 (f '' s) g<VAR>hf : ConvexOn 𝕜 s f<VAR>hg' : AntitoneOn g (f '' s)<GOAL>ConcaveOn 𝕜 s (g ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_4<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 α<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>g : β → α<VAR>hg : StrictConvexOn 𝕜 (f '' s) g<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hg' : StrictMonoOn g (f '' s)<VAR>hf' : Set.InjOn f s<GOAL>StrictConvexOn 𝕜 s (g ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_4<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 α<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>g : β → α<VAR>hg : StrictConcaveOn 𝕜 (f '' s) g<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>hg' : StrictMonoOn g (f '' s)<VAR>hf' : Set.InjOn f s<GOAL>StrictConcaveOn 𝕜 s (g ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_4<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 α<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>g : β → α<VAR>hg : StrictConvexOn 𝕜 (f '' s) g<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>hg' : StrictAntiOn g (f '' s)<VAR>hf' : Set.InjOn f s<GOAL>StrictConvexOn 𝕜 s (g ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_4<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>SMul 𝕜 α<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>g : β → α<VAR>hg : StrictConcaveOn 𝕜 (f '' s) g<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hg' : StrictAntiOn g (f '' s)<VAR>hf' : Set.InjOn f s<GOAL>StrictConcaveOn 𝕜 s (g ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>DistribMulAction 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 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>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>DistribMulAction 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 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>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>c : β<VAR>hs : Convex 𝕜 s<GOAL>ConvexOn 𝕜 s fun x => c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>c : β<VAR>hs : Convex 𝕜 s<GOAL>ConcaveOn 𝕜 s fun x => c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>b : β<GOAL>ConvexOn 𝕜 s (f + fun x => b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>b : β<GOAL>ConcaveOn 𝕜 s (f + fun x => b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>h : Convex 𝕜 {p | p.1 ∈ s ∧ f p.1 ≤ p.2}<GOAL>ConvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>h : Convex 𝕜 {p | p.1 ∈ s ∧ p.2 ≤ f p.1}<GOAL>ConcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ f x ≤ r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ r ≤ f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<GOAL>Convex 𝕜 {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<GOAL>Convex 𝕜 {p | p.1 ∈ s ∧ p.2 ≤ f p.1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>ConvexOn 𝕜 s f ↔ Convex 𝕜 {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>ConcaveOn 𝕜 s f ↔ Convex 𝕜 {p | p.1 ∈ s ∧ p.2 ≤ f p.1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>c : E<GOAL>ConvexOn 𝕜 ((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>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>c : E<GOAL>ConcaveOn 𝕜 ((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>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>c : E<GOAL>ConvexOn 𝕜 ((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>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>c : E<GOAL>ConcaveOn 𝕜 ((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>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<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 → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<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 → a + b = 1 → a • f x + b • 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>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>ConvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>ConcaveOn 𝕜 s f ↔ Convex 𝕜 s ∧ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • 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>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>f : E →ₗ[𝕜] β<VAR>s : Set E<VAR>hs : Convex 𝕜 s<GOAL>ConvexOn 𝕜 s ⇑f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>f : E →ₗ[𝕜] β<VAR>s : Set E<VAR>hs : Convex 𝕜 s<GOAL>ConcaveOn 𝕜 s ⇑f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConvexOn 𝕜 s f<GOAL>ConvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<GOAL>ConcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ f x < r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ r < f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>LinearOrder E<VAR>s : Set E<VAR>f : E → β<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y<GOAL>ConvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>LinearOrder E<VAR>s : Set E<VAR>f : E → β<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)<GOAL>ConcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>LinearOrder E<VAR>s : Set E<VAR>f : E → β<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y<GOAL>StrictConvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>LinearOrder E<VAR>s : Set E<VAR>f : E → β<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)<GOAL>StrictConcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>SMul 𝕜 β<VAR>f : F → β<VAR>s : Set F<VAR>hf : ConvexOn 𝕜 s f<VAR>g : E →ₗ[𝕜] 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>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>SMul 𝕜 β<VAR>f : F → β<VAR>s : Set F<VAR>hf : ConcaveOn 𝕜 s f<VAR>g : E →ₗ[𝕜] F<GOAL>ConcaveOn 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>DistribMulAction 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 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>OrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>DistribMulAction 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : StrictConvexOn 𝕜 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>OrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>DistribMulAction 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hg : StrictConvexOn 𝕜 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>OrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>DistribMulAction 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 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>OrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>DistribMulAction 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : StrictConcaveOn 𝕜 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>OrderedCancelAddCommMonoid β<VAR>SMul 𝕜 E<VAR>DistribMulAction 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>hg : StrictConcaveOn 𝕜 s g<GOAL>StrictConcaveOn 𝕜 s (f + g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>γ : Type u_7<VAR>f : E → γ<VAR>OrderedCancelAddCommMonoid γ<VAR>Module 𝕜 γ<VAR>hf : StrictConvexOn 𝕜 s f<VAR>b : γ<GOAL>StrictConvexOn 𝕜 s (f + fun x => b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>γ : Type u_7<VAR>f : E → γ<VAR>OrderedCancelAddCommMonoid γ<VAR>Module 𝕜 γ<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>b : γ<GOAL>StrictConcaveOn 𝕜 s (f + fun x => b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ f x < r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ r < f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>p q : E × β<VAR>hp : p.1 ∈ s ∧ f p.1 < p.2<VAR>hq : q.1 ∈ s ∧ f q.1 ≤ q.2<GOAL>openSegment 𝕜 p q ⊆ {p | p.1 ∈ s ∧ f p.1 < p.2}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>p q : E × β<VAR>hp : p.1 ∈ s ∧ p.2 < f p.1<VAR>hq : q.1 ∈ s ∧ q.2 ≤ f q.1<GOAL>openSegment 𝕜 p q ⊆ {p | p.1 ∈ s ∧ p.2 < f p.1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<GOAL>Convex 𝕜 {p | p.1 ∈ s ∧ f p.1 < p.2}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<GOAL>Convex 𝕜 {p | p.1 ∈ s ∧ p.2 < f p.1}
<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 g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 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>LinearOrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 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>LinearOrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hg : StrictConvexOn 𝕜 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>LinearOrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>hg : StrictConcaveOn 𝕜 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>LinearOrderedAddCommMonoid β<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<GOAL>f (a • x + b • y) ≤ 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 : 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<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 : ConvexOn 𝕜 s f<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hz : z ∈ [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 : ConcaveOn 𝕜 s f<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hz : z ∈ [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>LinearOrderedAddCommMonoid β<VAR>SMul 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConvexOn 𝕜 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>f (a • x + b • y) < max (f x) (f y)