ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<GOAL>(convexHull 𝕜) {x} = {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<GOAL>(convexHull 𝕜) 0 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x y : E<GOAL>(convexHull 𝕜) {x, y} = segment 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t : Set E<GOAL>(convexHull 𝕜) ((convexHull 𝕜) s ∪ t) = (convexHull 𝕜) (s ∪ t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t : Set E<GOAL>(convexHull 𝕜) (s ∪ (convexHull 𝕜) t) = (convexHull 𝕜) (s ∪ t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<GOAL>Convex 𝕜 (s \ {x}) ↔ x ∉ (convexHull 𝕜) (s \ {x})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>f : E → F<VAR>hf : IsLinearMap 𝕜 f<VAR>s : Set E<GOAL>f '' (convexHull 𝕜) s = (convexHull 𝕜) (f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>f : E →ₗ[𝕜] F<VAR>s : Set E<GOAL>⇑f '' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedCommSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>a : 𝕜<VAR>s : Set E<GOAL>(convexHull 𝕜) (a • s) = a • (convexHull 𝕜) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>f : E →ᵃ[𝕜] F<VAR>s : Set E<GOAL>⇑f '' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>(convexHull 𝕜) s ⊆ ↑(affineSpan 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>affineSpan 𝕜 ((convexHull 𝕜) s) = affineSpan 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>(convexHull 𝕜) (-s) = -(convexHull 𝕜) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<GOAL>(convexHull 𝕜) (x +ᵥ s) = x +ᵥ (convexHull 𝕜) s
<VAR>A : Type u_1<VAR>NonUnitalNormedRing A<VAR>CompleteSpace A<VAR>PartialOrder A<VAR>StarRing A<VAR>StarOrderedRing A<VAR>CstarRing A<VAR>NormedSpace ℂ A<VAR>StarModule ℂ A<VAR>SMulCommClass ℂ A A<VAR>IsScalarTower ℂ A A<VAR>a b : A<VAR>ha : IsSelfAdjoint a := by cfc_tac<VAR>hb : IsSelfAdjoint b := by cfc_tac<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>A : Type u_1<VAR>NonUnitalNormedRing A<VAR>CompleteSpace A<VAR>PartialOrder A<VAR>StarRing A<VAR>StarOrderedRing A<VAR>CstarRing A<VAR>NormedSpace ℂ A<VAR>StarModule ℂ A<VAR>SMulCommClass ℂ A A<VAR>IsScalarTower ℂ A A<VAR>a : A<GOAL>0 ≤ ↑a ↔ 0 ≤ a
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>a : A<VAR>ha : IsSelfAdjoint a := by cfc_tac<GOAL>a ≤ (algebraMap ℝ A) ‖a‖
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>a : A<VAR>ha : IsSelfAdjoint a := by cfc_tac<GOAL>-(algebraMap ℝ A) ‖a‖ ≤ a
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>a : A<GOAL>a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>a : A<GOAL>star a * a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>(spectralRadius ℝ a).toReal = ‖a‖
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>Nontrivial A<VAR>a : A<VAR>ha : IsSelfAdjoint a := by cfc_tac<GOAL>‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Nontrivial A<VAR>a : A<VAR>ha : 0 ≤ a := by cfc_tac<GOAL>‖a‖₊ ∈ spectrum ℝ≥0 a
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Nontrivial A<VAR>a : A<VAR>ha : 0 ≤ a := by cfc_tac<GOAL>‖a‖ ∈ spectrum ℝ a
<VAR>A : Type u_1<VAR>NonUnitalNormedRing A<VAR>CompleteSpace A<VAR>PartialOrder A<VAR>StarRing A<VAR>StarOrderedRing A<VAR>CstarRing A<VAR>NormedSpace ℂ A<VAR>StarModule ℂ A<VAR>SMulCommClass ℂ A A<VAR>IsScalarTower ℂ A A<VAR>a b : A<VAR>ha : 0 ≤ a := by cfc_tac<VAR>hab : a ≤ b<GOAL>‖a‖ ≤ ‖b‖
<VAR>A : Type u_1<VAR>NonUnitalNormedRing A<VAR>CompleteSpace A<VAR>PartialOrder A<VAR>StarRing A<VAR>StarOrderedRing A<VAR>CstarRing A<VAR>NormedSpace ℂ A<VAR>StarModule ℂ A<VAR>SMulCommClass ℂ A A<VAR>IsScalarTower ℂ A A<VAR>a b : A<VAR>hb : IsSelfAdjoint b := by cfc_tac<GOAL>star a * b * a ≤ ‖b‖ • (star a * a)
<VAR>A : Type u_1<VAR>NonUnitalNormedRing A<VAR>CompleteSpace A<VAR>PartialOrder A<VAR>StarRing A<VAR>StarOrderedRing A<VAR>CstarRing A<VAR>NormedSpace ℂ A<VAR>StarModule ℂ A<VAR>SMulCommClass ℂ A A<VAR>IsScalarTower ℂ A A<VAR>a b : A<VAR>hb : IsSelfAdjoint b := by cfc_tac<GOAL>a * b * star a ≤ ‖b‖ • (a * star a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Subsingleton ι<VAR>p : ι → E<GOAL>ConvexIndependent 𝕜 p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<GOAL>Function.Injective p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>ι' : Type u_4<VAR>f : ι' ↪ ι<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<GOAL>ConvexIndependent 𝕜 (p ∘ ⇑f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<VAR>s : Set ι<GOAL>ConvexIndependent 𝕜 fun i => p ↑i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<GOAL>ConvexIndependent 𝕜 Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>hc : ConvexIndependent 𝕜 Subtype.val<VAR>hs : s ⊆ t<GOAL>ConvexIndependent 𝕜 Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → E<VAR>hi : Function.Injective p<GOAL>ConvexIndependent 𝕜 Subtype.val ↔ ConvexIndependent 𝕜 p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<VAR>s : Set ι<VAR>i : ι<GOAL>p i ∈ (convexHull 𝕜) (p '' s) ↔ i ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → E<GOAL>ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>ConvexIndependent 𝕜 Subtype.val ↔ ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>ConvexIndependent 𝕜 Subtype.val ↔ ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → E<GOAL>ConvexIndependent 𝕜 p ↔ ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(Finset.image p s) → x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<GOAL>ConvexIndependent 𝕜 Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>NormedStarGroup E<VAR>NormedSpace 𝕜 E<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>RegularNormedAlgebra 𝕜 E<VAR>a : E<GOAL>‖(ContinuousLinearMap.mul 𝕜 E).flip a‖ = ‖a‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>NormedStarGroup E<VAR>NormedSpace 𝕜 E<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>RegularNormedAlgebra 𝕜 E<VAR>a : E<GOAL>‖(ContinuousLinearMap.mul 𝕜 E).flip a‖₊ = ‖a‖₊
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>NormedStarGroup E<VAR>NormedSpace 𝕜 E<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>RegularNormedAlgebra 𝕜 E<GOAL>Isometry ⇑(ContinuousLinearMap.mul 𝕜 E).flip
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>DenselyNormedField 𝕜<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>NormedSpace 𝕜 E<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>StarRing 𝕜<VAR>StarModule 𝕜 E<VAR>x : Unitization 𝕜 E<GOAL>‖((Unitization.splitMul 𝕜 E) x).2‖ ^ 2 ≤ ‖((Unitization.splitMul 𝕜 E) (x⋆ * x)).2‖
<VAR>A : Type u_1<VAR>NormedCommRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>I : Ideal A<VAR>I.IsMaximal<VAR>a : A<VAR>ha : a ∈ I<GOAL>I.toCharacterSpace a = 0
<VAR>A : Type u_1<VAR>NormedCommRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>a : A<VAR>ha : ¬IsUnit a<GOAL>∃ f, f a = 0
<VAR>A : Type u_1<VAR>NormedCommRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>a : A<VAR>z : ℂ<GOAL>z ∈ spectrum ℂ a ↔ ∃ f, f a = z
<VAR>A : Type u_1<VAR>NormedCommRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>a : A<GOAL>spectrum ℂ ((WeakDual.gelfandTransform ℂ A) a) = spectrum ℂ a
<VAR>A : Type u_1<VAR>NormedCommRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>a : A<GOAL>(WeakDual.gelfandTransform ℂ A) (star a) = star ((WeakDual.gelfandTransform ℂ A) a)
<VAR>A : Type u_1<VAR>NormedCommRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<GOAL>Isometry ⇑(WeakDual.gelfandTransform ℂ A)
<VAR>A : Type u_1<VAR>NormedCommRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<GOAL>Function.Bijective ⇑(WeakDual.gelfandTransform ℂ A)
<VAR>A : Type u_1<VAR>NormedCommRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<GOAL>∀ (a : C(↑(WeakDual.characterSpace ℂ A), ℂ)), (gelfandStarTransform A).symm a = (↑(RingEquiv.ofBijective { toAlgHom := WeakDual.gelfandTransform ℂ A, map_star' := ⋯ } ⋯)).symm a
<VAR>A : Type u_1<VAR>NormedCommRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>a : A<VAR>φ : ↑(WeakDual.characterSpace ℂ A)<GOAL>((gelfandStarTransform A) a) φ = φ a
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>𝕜 : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>StarRing A<VAR>NormedRing B<VAR>NormedAlgebra 𝕜 B<VAR>CompleteSpace B<VAR>StarRing B<VAR>ψ : A →⋆ₐ[𝕜] B<VAR>φ : ↑(WeakDual.characterSpace 𝕜 B)<GOAL>(WeakDual.CharacterSpace.compContinuousMap ψ) φ = WeakDual.CharacterSpace.equivAlgHom.symm ((WeakDual.CharacterSpace.equivAlgHom φ).comp ψ.toAlgHom)
<VAR>A : Type u_1<VAR>𝕜 : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>StarRing A<GOAL>WeakDual.CharacterSpace.compContinuousMap (StarAlgHom.id 𝕜 A) = ContinuousMap.id ↑(WeakDual.characterSpace 𝕜 A)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>𝕜 : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>StarRing A<VAR>NormedRing B<VAR>NormedAlgebra 𝕜 B<VAR>CompleteSpace B<VAR>StarRing B<VAR>NormedRing C<VAR>NormedAlgebra 𝕜 C<VAR>CompleteSpace C<VAR>StarRing C<VAR>ψ₂ : B →⋆ₐ[𝕜] C<VAR>ψ₁ : A →⋆ₐ[𝕜] B<GOAL>WeakDual.CharacterSpace.compContinuousMap (ψ₂.comp ψ₁) = (WeakDual.CharacterSpace.compContinuousMap ψ₁).comp (WeakDual.CharacterSpace.compContinuousMap ψ₂)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NormedCommRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>NormedCommRing B<VAR>NormedAlgebra ℂ B<VAR>CompleteSpace B<VAR>StarRing B<VAR>CstarRing B<VAR>StarModule ℂ B<VAR>φ : A →⋆ₐ[ℂ] B<GOAL>(↑(gelfandStarTransform B)).comp φ = (ContinuousMap.compStarAlgHom' ℂ ℂ (WeakDual.CharacterSpace.compContinuousMap φ)).comp ↑(gelfandStarTransform A)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>TopologicalSpace Y<VAR>CompactSpace Y<VAR>T2Space Y<VAR>f : C(X, Y)<GOAL>(WeakDual.CharacterSpace.homeoEval Y 𝕜).toContinuousMap.comp f = (WeakDual.CharacterSpace.compContinuousMap (ContinuousMap.compStarAlgHom' 𝕜 𝕜 f)).comp (WeakDual.CharacterSpace.homeoEval X 𝕜).toContinuousMap
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<GOAL>StrictConcaveOn NNReal Set.univ fun x => x ^ p
<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp₁ : p ≤ 1<GOAL>ConcaveOn NNReal Set.univ fun x => x ^ p
<GOAL>StrictConcaveOn NNReal Set.univ ⇑NNReal.sqrt
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<GOAL>StrictConcaveOn ℝ (Set.Ici 0) fun x => x ^ p
<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp₁ : p ≤ 1<GOAL>ConcaveOn ℝ (Set.Ici 0) fun x => x ^ p
<GOAL>StrictConcaveOn ℝ (Set.Ici 0) fun x => √x
<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>StrictConvexOn ℝ (Set.Ici 0) fun x => x ^ n
<VAR>n : ℕ<VAR>hn : Even n<VAR>h : n ≠ 0<GOAL>StrictConvexOn ℝ Set.univ fun x => x ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedCommRing β<VAR>f : α → β<VAR>DecidablePred fun x => f x ≤ 0<VAR>s : Finset α<VAR>h0 : Even (Finset.filter (fun x => f x ≤ 0) s).card<GOAL>0 ≤ ∏ x ∈ s, f x
<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : Even n<GOAL>0 ≤ ∏ k ∈ Finset.range n, (m - ↑k)
<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : Even n<VAR>hm : m ∉ Set.Ico 0 ↑n<GOAL>0 < ∏ k ∈ Finset.range n, (m - ↑k)
<VAR>m : ℤ<VAR>hm₀ : m ≠ 0<VAR>hm₁ : m ≠ 1<GOAL>StrictConvexOn ℝ (Set.Ioi 0) fun x => x ^ m
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>HasDerivAt (fun x => √x * Real.log x) ((2 + Real.log x) / (2 * √x)) x
<VAR>x : ℝ<GOAL>deriv (fun x => √x * Real.log x) x = (2 + Real.log x) / (2 * √x)
<GOAL>(deriv fun x => √x * Real.log x) = fun x => (2 + Real.log x) / (2 * √x)
<VAR>x : ℝ<GOAL>deriv^[2] (fun x => √x * Real.log x) x = -Real.log x / (4 * √x ^ 3)
<GOAL>StrictConcaveOn ℝ (Set.Ioi 1) fun x => √x * Real.log x
<GOAL>StrictConcaveOn ℝ (Set.Icc 0 π) Real.sin
<GOAL>StrictConcaveOn ℝ (Set.Icc (-(π / 2)) (π / 2)) Real.cos
<VAR>ι : Type u<VAR>E : Type v<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>l : BoxIntegral.IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : BoxIntegral.Box ι<VAR>y : E<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>BoxIntegral.HasIntegral I l (s.indicator fun x => y) μ.toBoxAdditive.toSMul ((μ (s ∩ ↑I)).toReal • y)
<VAR>ι : Type u<VAR>E : Type v<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>hf : f =ᵐ[μ.restrict ↑I] 0<VAR>hl : l.bRiemann = false<GOAL>BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul 0
<VAR>ι : Type u<VAR>E : Type v<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>y : E<VAR>f g : (ι → ℝ) → E<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>hf : BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul y<VAR>hfg : f =ᵐ[μ.restrict ↑I] g<VAR>hl : l.bRiemann = false<GOAL>BoxIntegral.HasIntegral I l g μ.toBoxAdditive.toSMul y
<VAR>ι : Type u<VAR>E : Type v<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : MeasureTheory.SimpleFunc (ι → ℝ) E<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>I : BoxIntegral.Box ι<VAR>l : BoxIntegral.IntegrationParams<VAR>hl : l.bRiemann = false<GOAL>BoxIntegral.HasIntegral I l (↑f) μ.toBoxAdditive.toSMul (MeasureTheory.SimpleFunc.integral (μ.restrict ↑I) f)
<VAR>ι : Type u<VAR>E : Type v<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : MeasureTheory.SimpleFunc (ι → ℝ) E<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>I : BoxIntegral.Box ι<VAR>l : BoxIntegral.IntegrationParams<VAR>hl : l.bRiemann = false<GOAL>BoxIntegral.integral I l (↑f) μ.toBoxAdditive.toSMul = MeasureTheory.SimpleFunc.integral (μ.restrict ↑I) f
<VAR>ι : Type u<VAR>E : Type v<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>I : BoxIntegral.Box ι<VAR>hf : MeasureTheory.IntegrableOn f (↑I) μ<VAR>l : BoxIntegral.IntegrationParams<VAR>hl : l.bRiemann = false<GOAL>BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>I : BoxIntegral.Box ι<VAR>hc : ContinuousOn f (BoxIntegral.Box.Icc I)<VAR>l : BoxIntegral.IntegrationParams<GOAL>BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>I : BoxIntegral.Box ι<VAR>hb : ∃ C, ∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ C<VAR>hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x<VAR>l : BoxIntegral.IntegrationParams<GOAL>BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
<GOAL>StrictConcaveOn ℝ (Set.Ioi 0) Real.log
<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>StrictConvexOn ℝ (Set.Ici 0) fun x => x ^ p
<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>ConvexOn ℝ (Set.Ici 0) fun x => x ^ p
<GOAL>StrictConcaveOn ℝ (Set.Iio 0) Real.log
<VAR>t : ℝ<VAR>ht : |t| ≤ 1<VAR>x : ℝ<GOAL>rexp (t * x) ≤ Real.cosh x + t * Real.sinh x
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<GOAL>AmpleSet Set.univ
<VAR>F : Type u_1<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<GOAL>AmpleSet ∅
<VAR>F : Type u_1<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<VAR>s t : Set F<VAR>hs : AmpleSet s<VAR>ht : AmpleSet t<GOAL>AmpleSet (s ∪ t)
<VAR>F : Type u_1<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>s : Set E<VAR>h : AmpleSet s<VAR>L : E ≃ᵃL[ℝ] F<GOAL>AmpleSet (⇑L '' s)
<VAR>F : Type u_1<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>s : Set E<VAR>L : E ≃ᵃL[ℝ] F<GOAL>AmpleSet (⇑L '' s) ↔ AmpleSet s
<VAR>F : Type u_1<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>s : Set F<VAR>h : AmpleSet s<VAR>L : E ≃ᵃL[ℝ] F<GOAL>AmpleSet (⇑L ⁻¹' s)
<VAR>F : Type u_1<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>s : Set F<VAR>L : E ≃ᵃL[ℝ] F<GOAL>AmpleSet (⇑L ⁻¹' s) ↔ AmpleSet s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>s : Set E<VAR>h : AmpleSet s<VAR>y : E<GOAL>AmpleSet (y +ᵥ s)
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>s : Set E<VAR>y : E<GOAL>AmpleSet (y +ᵥ s) ↔ AmpleSet s
<VAR>F : Type u_1<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul ℝ F<VAR>E : Submodule ℝ F<VAR>hcodim : 1 < Module.rank ℝ (F ⧸ E)<GOAL>AmpleSet (↑E)ᶜ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>self : UniformConvexSpace E<VAR>ε : ℝ<GOAL>0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>UniformConvexSpace E<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>UniformConvexSpace E<VAR>ε : ℝ<VAR>NormedSpace ℝ E<VAR>hε : 0 < ε<GOAL>∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>UniformConvexSpace E<VAR>ε : ℝ<VAR>NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>r : ℝ<GOAL>∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
<VAR>𝕜 : Type u_1<VAR>NNNorm 𝕜<VAR>E : Type u_2<VAR>SMul 𝕜 E<VAR>s t : Set E<VAR>h : s ⊆ t<VAR>x : E<GOAL>egauge 𝕜 t x ≤ egauge 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>NNNorm 𝕜<VAR>E : Type u_2<VAR>SMul 𝕜 E<VAR>x : E<GOAL>egauge 𝕜 ∅ x = ⊤
<VAR>𝕜 : Type u_1<VAR>NNNorm 𝕜<VAR>E : Type u_2<VAR>SMul 𝕜 E<VAR>c : 𝕜<VAR>s : Set E<VAR>x : E<VAR>h : x ∈ c • s<GOAL>egauge 𝕜 s x ≤ ↑‖c‖₊
<VAR>𝕜 : Type u_1<VAR>NNNorm 𝕜<VAR>E : Type u_2<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>r : ℝ≥0∞<GOAL>r ≤ egauge 𝕜 s x ↔ ∀ (c : 𝕜), x ∈ c • s → r ≤ ↑‖c‖₊
<VAR>𝕜 : Type u_1<VAR>NNNorm 𝕜<VAR>E : Type u_2<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>x : E<GOAL>egauge 𝕜 s x = ⊤ ↔ ∀ (c : 𝕜), x ∉ c • s
<VAR>𝕜 : Type u_1<VAR>NNNorm 𝕜<VAR>E : Type u_2<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>r : ℝ≥0∞<GOAL>egauge 𝕜 s x < r ↔ ∃ c, x ∈ c • s ∧ ↑‖c‖₊ < r
<VAR>𝕜 : Type u_1<VAR>NNNorm 𝕜<VAR>Nonempty 𝕜<VAR>E : Type u_2<VAR>Zero E<VAR>SMulZeroClass 𝕜 E<VAR>x : E<GOAL>egauge 𝕜 0 x = ⊤ ↔ x ≠ 0
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>c : 𝕜<VAR>s : Set E<VAR>x : E<VAR>h : c • x ∈ s<VAR>hc : c ≠ 0<GOAL>egauge 𝕜 s x ≤ ↑‖c‖₊⁻¹
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>c : 𝕜<VAR>s : Set E<VAR>x : E<VAR>h : c • x ∈ s<GOAL>egauge 𝕜 s x ≤ (↑‖c‖₊)⁻¹
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hs : Balanced 𝕜 s<VAR>hx : egauge 𝕜 s x < 1<GOAL>x ∈ s
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : s.Nonempty<GOAL>egauge 𝕜 s 0 = 0
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<GOAL>egauge 𝕜 0 0 = 0
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>h : x ∈ s<GOAL>egauge 𝕜 s x ≤ 1
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>c : 𝕜<VAR>s : Set E<VAR>x : E<GOAL>egauge 𝕜 s x / ↑‖c‖₊ ≤ egauge 𝕜 (c • s) x
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>s : Set E<VAR>x : E<GOAL>egauge 𝕜 (c • s) x = egauge 𝕜 s x / ↑‖c‖₊
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>c : 𝕜<VAR>s : Set E<VAR>x : E<GOAL>↑‖c‖₊ * egauge 𝕜 s x ≤ egauge 𝕜 s (c • x)
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>c : 𝕜<VAR>s : Set E<VAR>h : c = 0 → s.Nonempty<VAR>x : E<GOAL>egauge 𝕜 s (c • x) = ↑‖c‖₊ * egauge 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>NormedField 𝕜<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ≥0<VAR>x : E<GOAL>↑‖x‖₊ / ↑r ≤ egauge 𝕜 (Metric.closedBall 0 ↑r) x
<VAR>𝕜 : Type u_1<VAR>NormedField 𝕜<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>↑‖x‖₊ ≤ egauge 𝕜 (Metric.closedBall 0 1) x
<VAR>𝕜 : Type u_1<VAR>NormedField 𝕜<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ≥0<VAR>x : E<GOAL>↑‖x‖₊ / ↑r ≤ egauge 𝕜 (Metric.ball 0 ↑r) x