ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Zero X<VAR>A : Type u_2<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module ℝ A<VAR>TopologicalRing A<VAR>φ : ContinuousMapZero X NNReal →⋆ₙₐ[NNReal] A<VAR>hφ : Continuous ⇑φ<GOAL>Continuous ⇑φ.realContinuousMapZeroOfNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Zero X<VAR>A : Type u_2<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module ℝ A<VAR>φ : ContinuousMapZero X NNReal →⋆ₙₐ[NNReal] A<VAR>f : ContinuousMapZero X NNReal<GOAL>φ.realContinuousMapZeroOfNNReal ({ toFun := NNReal.toReal, continuous_toFun := NNReal.continuous_coe, map_zero' := ⋯ }.comp f) = φ f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Zero X<VAR>A : Type u_2<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module ℝ A<GOAL>Function.Injective NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>hf : ConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : 0 < ∑ i ∈ t, w i<VAR>hmem : ∀ i ∈ t, p i ∈ s<GOAL>f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>hf : ConcaveOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : 0 < ∑ i ∈ t, w i<VAR>hmem : ∀ i ∈ t, p i ∈ s<GOAL>t.centerMass w (f ∘ p) ≤ f (t.centerMass w p)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>hf : ConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<GOAL>f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>hf : ConcaveOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<GOAL>∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : ConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : v + ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hv : 0 ≤ v<VAR>hq : q ∈ s<GOAL>f (v • q + ∑ i ∈ t, w i • p i) ≤ v • f q + ∑ i ∈ t, w i • f (p i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : ConcaveOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : v + ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hv : 0 ≤ v<VAR>hq : q ∈ s<GOAL>v • f q + ∑ i ∈ t, w i • f (p i) ≤ f (v • q + ∑ i ∈ t, w i • p i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 < w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hp : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k<GOAL>f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 < w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hp : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k<GOAL>∑ i ∈ t, w i • f (p i) < f (∑ i ∈ t, w i • p i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 < w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)<VAR>j : ι<GOAL>j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 < w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>h_eq : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)<VAR>j : ι<GOAL>j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 < w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<GOAL>f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 < w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<GOAL>f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<GOAL>f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, w i • p i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>OrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<GOAL>f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, w i • p i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>LinearOrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : E → β<VAR>x : E<VAR>s : Finset E<VAR>hf : ConvexOn 𝕜 ((convexHull 𝕜) ↑s) f<VAR>hx : x ∈ (convexHull 𝕜) ↑s<GOAL>f x ≤ s.sup' ⋯ f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>LinearOrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : E → β<VAR>x : E<VAR>s : Finset E<VAR>hf : ConcaveOn 𝕜 ((convexHull 𝕜) ↑s) f<VAR>hx : x ∈ (convexHull 𝕜) ↑s<GOAL>s.inf' ⋯ f ≤ f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>LinearOrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>h : ConvexOn 𝕜 s f<VAR>hw₀ : ∀ i ∈ t, 0 ≤ w i<VAR>hw₁ : 0 < ∑ i ∈ t, w i<VAR>hp : ∀ i ∈ t, p i ∈ s<GOAL>∃ i ∈ t, f (t.centerMass w p) ≤ f (p i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>LinearOrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>h : ConcaveOn 𝕜 s f<VAR>hw₀ : ∀ i ∈ t, 0 ≤ w i<VAR>hw₁ : 0 < ∑ i ∈ t, w i<VAR>hp : ∀ i ∈ t, p i ∈ s<GOAL>∃ i ∈ t, f (p i) ≤ f (t.centerMass w p)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>LinearOrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 ((convexHull 𝕜) s) f<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<GOAL>∃ y ∈ s, f x ≤ f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>LinearOrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 ((convexHull 𝕜) s) f<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<GOAL>∃ y ∈ s, f y ≤ f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>LinearOrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : E → β<VAR>x y z : E<VAR>hf : ConvexOn 𝕜 [x-[𝕜]y] f<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_4<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>LinearOrderedAddCommGroup β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : E → β<VAR>x y z : E<VAR>hf : ConcaveOn 𝕜 [x-[𝕜]y] f<VAR>hz : z ∈ [x-[𝕜]y]<GOAL>min (f x) (f y) ≤ f z
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>LinearOrderedField 𝕜<VAR>LinearOrderedAddCommGroup β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : 𝕜 → β<VAR>x y z : 𝕜<VAR>hf : ConvexOn 𝕜 (Set.Icc x y) f<VAR>hz : z ∈ Set.Icc x y<GOAL>f z ≤ max (f x) (f y)
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>LinearOrderedField 𝕜<VAR>LinearOrderedAddCommGroup β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : 𝕜 → β<VAR>x y z : 𝕜<VAR>hf : ConcaveOn 𝕜 (Set.Icc x y) f<VAR>hz : z ∈ Set.Icc x y<GOAL>min (f x) (f y) ≤ f z
<VAR>V : Type u_2<VAR>TopologicalSpace V<VAR>AddCommMonoid V<VAR>SMul ℝ V<VAR>self : ConvexBody V<GOAL>IsCompact self.carrier
<VAR>V : Type u_2<VAR>TopologicalSpace V<VAR>AddCommMonoid V<VAR>SMul ℝ V<VAR>self : ConvexBody V<GOAL>Convex ℝ self.carrier
<VAR>V : Type u_2<VAR>TopologicalSpace V<VAR>AddCommMonoid V<VAR>SMul ℝ V<VAR>self : ConvexBody V<GOAL>self.carrier.Nonempty
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>K : ConvexBody V<GOAL>Convex ℝ ↑K
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>K : ConvexBody V<GOAL>IsCompact ↑K
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>T2Space V<VAR>K : ConvexBody V<GOAL>IsClosed ↑K
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>K : ConvexBody V<GOAL>(↑K).Nonempty
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>K L : ConvexBody V<VAR>h : ↑K = ↑L<GOAL>K = L
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>s : Set V<VAR>h₁ : Convex ℝ s<VAR>h₂ : IsCompact s<VAR>h₃ : s.Nonempty<GOAL>↑{ carrier := s, convex' := h₁, isCompact' := h₂, nonempty' := h₃ } = s
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>K : ConvexBody V<VAR>h_symm : ∀ x ∈ K, -x ∈ K<GOAL>0 ∈ K
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>ContinuousAdd V<VAR>n : ℕ<VAR>K : ConvexBody V<GOAL>↑(n • K) = n • ↑K
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>ContinuousAdd V<VAR>K L : ConvexBody V<GOAL>↑(K + L) = ↑K + ↑L
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<GOAL>↑0 = 0
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>ContinuousSMul ℝ V<VAR>c : ℝ<VAR>K : ConvexBody V<GOAL>↑(c • K) = c • ↑K
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>ContinuousSMul ℝ V<VAR>ContinuousAdd V<VAR>c : ℝ≥0<VAR>K : ConvexBody V<GOAL>↑(c • K) = c • ↑K
<VAR>V : Type u_1<VAR>TopologicalSpace V<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>ContinuousSMul ℝ V<VAR>ContinuousAdd V<VAR>K : ConvexBody V<VAR>h_zero : 0 ∈ K<VAR>a b : ℝ≥0<VAR>h : a ≤ b<GOAL>a • K ≤ b • K
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>K : ConvexBody V<GOAL>Bornology.IsBounded ↑K
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>K L : ConvexBody V<GOAL>EMetric.hausdorffEdist ↑K ↑L ≠ ⊤
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>K L : ConvexBody V<GOAL>Metric.hausdorffDist ↑K ↑L = dist K L
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>K L : ConvexBody V<GOAL>EMetric.hausdorffEdist ↑K ↑L = edist K L
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>T2Space V<VAR>u : ℕ → ℝ≥0<VAR>K : ConvexBody V<VAR>h_zero : 0 ∈ K<VAR>hu : Filter.Tendsto u Filter.atTop (𝓝 0)<GOAL>⋂ n, (1 + ↑(u n)) • ↑K = ↑K
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>f : α → E<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>∫ (x : α), f x ∂μ ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>f : α → E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NeZero μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>⨍ (x : α), f x ∂μ ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>h0 : μ t ≠ 0<VAR>ht : μ t ≠ ⊤<VAR>hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s<VAR>hfi : MeasureTheory.IntegrableOn f t μ<GOAL>⨍ (x : α) in t, f x ∂μ ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>hs : Convex ℝ s<VAR>h0 : μ t ≠ 0<VAR>ht : μ t ≠ ⊤<VAR>hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s<VAR>hfi : MeasureTheory.IntegrableOn f t μ<GOAL>⨍ (x : α) in t, f x ∂μ ∈ closure s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>f : α → E<VAR>g : E → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NeZero μ<VAR>hg : ConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hgi : MeasureTheory.Integrable (g ∘ f) μ<GOAL>(⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>f : α → E<VAR>g : E → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NeZero μ<VAR>hg : ConcaveOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hgi : MeasureTheory.Integrable (g ∘ f) μ<GOAL>(⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ p.2 ≤ g p.1}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>f : α → E<VAR>g : E → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NeZero μ<VAR>hg : ConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hgi : MeasureTheory.Integrable (g ∘ f) μ<GOAL>g (⨍ (x : α), f x ∂μ) ≤ ⨍ (x : α), g (f x) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>f : α → E<VAR>g : E → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NeZero μ<VAR>hg : ConcaveOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hgi : MeasureTheory.Integrable (g ∘ f) μ<GOAL>⨍ (x : α), g (f x) ∂μ ≤ g (⨍ (x : α), f x ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>hg : ConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>h0 : μ t ≠ 0<VAR>ht : μ t ≠ ⊤<VAR>hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s<VAR>hfi : MeasureTheory.IntegrableOn f t μ<VAR>hgi : MeasureTheory.IntegrableOn (g ∘ f) t μ<GOAL>(⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>hg : ConcaveOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>h0 : μ t ≠ 0<VAR>ht : μ t ≠ ⊤<VAR>hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s<VAR>hfi : MeasureTheory.IntegrableOn f t μ<VAR>hgi : MeasureTheory.IntegrableOn (g ∘ f) t μ<GOAL>(⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ p.2 ≤ g p.1}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>hg : ConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>h0 : μ t ≠ 0<VAR>ht : μ t ≠ ⊤<VAR>hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s<VAR>hfi : MeasureTheory.IntegrableOn f t μ<VAR>hgi : MeasureTheory.IntegrableOn (g ∘ f) t μ<GOAL>g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>hg : ConcaveOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>h0 : μ t ≠ 0<VAR>ht : μ t ≠ ⊤<VAR>hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s<VAR>hfi : MeasureTheory.IntegrableOn f t μ<VAR>hgi : MeasureTheory.IntegrableOn (g ∘ f) t μ<GOAL>⨍ (x : α) in t, g (f x) ∂μ ≤ g (⨍ (x : α) in t, f x ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>f : α → E<VAR>g : E → ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hg : ConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hgi : MeasureTheory.Integrable (g ∘ f) μ<GOAL>g (∫ (x : α), f x ∂μ) ≤ ∫ (x : α), g (f x) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>f : α → E<VAR>g : E → ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hg : ConcaveOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hgi : MeasureTheory.Integrable (g ∘ f) μ<GOAL>∫ (x : α), g (f x) ∂μ ≤ g (∫ (x : α), f x ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ ∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hs : Convex ℝ s<VAR>h0 : μ t ≠ 0<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : MeasureTheory.Integrable f μ<VAR>ht : ⨍ (x : α) in t, f x ∂μ ∈ interior s<GOAL>⨍ (x : α), f x ∂μ ∈ interior s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>f : α → E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hs : StrictConvex ℝ s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), f x ∂μ ∈ interior s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>f : α → E<VAR>g : E → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hg : StrictConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hgi : MeasureTheory.Integrable (g ∘ f) μ<GOAL>f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set E<VAR>f : α → E<VAR>g : E → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hg : StrictConcaveOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hgi : MeasureTheory.Integrable (g ∘ f) μ<GOAL>f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), g (f x) ∂μ < g (⨍ (x : α), f x ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>C : ℝ<VAR>StrictConvexSpace ℝ E<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>C : ℝ<VAR>StrictConvexSpace ℝ E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < (μ Set.univ).toReal * C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>f : α → E<VAR>C : ℝ<VAR>StrictConvexSpace ℝ E<VAR>ht : μ t ≠ ⊤<VAR>h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C<GOAL>f =ᵐ[μ.restrict t] Function.const α (⨍ (x : α) in t, f x ∂μ) ∨ ‖∫ (x : α) in t, f x ∂μ‖ < (μ t).toReal * C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : Set E<VAR>hs : Convex ℝ s<GOAL>μ (frontier s) = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : Set E<VAR>hs : Convex ℝ s<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>LinearOrderedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module E F<VAR>IsScalarTower 𝕜 E F<VAR>SMulCommClass 𝕜 E F<VAR>OrderedSMul 𝕜 F<VAR>OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (f • g)