ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<GOAL>IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s)) MeasureTheory.volume 0 X
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>Y : ℝ<VAR>hY : 0 ≤ Y<GOAL>IntervalIntegrable (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) MeasureTheory.volume 0 Y
<VAR>s : ℂ<VAR>n : ℕ<VAR>h1 : -s.re < ↑n<GOAL>Complex.GammaAux n s = Complex.GammaAux n (s + 1) / s
<VAR>s : ℂ<VAR>n : ℕ<VAR>h1 : -s.re < ↑n<GOAL>Complex.GammaAux n s = Complex.GammaAux (n + 1) s
<VAR>s : ℂ<GOAL>Complex.Gamma s = Complex.GammaAux ⌊1 - s.re⌋₊ s
<VAR>s : ℂ<VAR>n : ℕ<VAR>h1 : -s.re < ↑n<GOAL>Complex.Gamma s = Complex.GammaAux n s
<VAR>s : ℂ<VAR>h2 : s ≠ 0<GOAL>Complex.Gamma (s + 1) = s * Complex.Gamma s
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>Complex.Gamma s = s.GammaIntegral
<VAR>n : ℕ<GOAL>Complex.Gamma (↑n + 1) = ↑n !
<VAR>n : ℕ<VAR>(n + 1).AtLeastTwo<GOAL>Complex.Gamma (OfNat.ofNat (n + 1)) = ↑n !
<VAR>n : ℕ<GOAL>Complex.Gamma (-↑n) = 0
<VAR>s : ℂ<GOAL>Complex.Gamma ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Complex.Gamma s)
<VAR>a : ℂ<VAR>r : ℝ<VAR>ha : 0 < a.re<VAR>hr : 0 < r<GOAL>∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (a - 1) * Complex.exp (-(↑r * ↑t)) = (1 / ↑r) ^ a * Complex.Gamma a
<GOAL>Complex.GammaIntegral = mellin fun x => ↑(rexp (-x))
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>HasDerivAt Complex.GammaIntegral (∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(rexp (-t)))) s
<VAR>s : ℂ<VAR>n : ℕ<VAR>h1 : 1 - s.re < ↑n<VAR>h2 : ∀ (m : ℕ), s ≠ -↑m<GOAL>DifferentiableAt ℂ (Complex.GammaAux n) s
<VAR>s : ℂ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<GOAL>DifferentiableAt ℂ Complex.Gamma s
<GOAL>Filter.Tendsto (fun z => z * Complex.Gamma z) (𝓝[≠] 0) (𝓝 1)
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>Real.Gamma s = ∫ (x : ℝ) in Set.Ioi 0, rexp (-x) * x ^ (s - 1)
<VAR>s : ℝ<VAR>hs : s ≠ 0<GOAL>Real.Gamma (s + 1) = s * Real.Gamma s
<VAR>s : ℝ<GOAL>Complex.Gamma ↑s = ↑(Real.Gamma s)
<VAR>n : ℕ<GOAL>Real.Gamma (↑n + 1) = ↑n !
<VAR>n : ℕ<VAR>(n + 1).AtLeastTwo<GOAL>Real.Gamma (OfNat.ofNat (n + 1)) = ↑n !
<VAR>n : ℕ<GOAL>Real.Gamma (-↑n) = 0
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>0 < Real.Gamma s
<VAR>s : ℝ<VAR>hs : 0 ≤ s<GOAL>0 ≤ Real.Gamma s
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<GOAL>∫ (t : ℝ) in Set.Ioi 0, t ^ (a - 1) * rexp (-(r * t)) = (1 / r) ^ a * Real.Gamma a
<VAR>s : ℝ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<GOAL>Real.Gamma s ≠ 0
<VAR>s : ℝ<GOAL>Real.Gamma s = 0 ↔ ∃ m, s = -↑m
<VAR>s : ℝ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<GOAL>DifferentiableAt ℝ Real.Gamma s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>NormedField R<VAR>SeminormedAddCommGroup M<VAR>NormedSpace R M<GOAL>IsConformalMap (ContinuousLinearMap.id R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>NormedField R<VAR>SeminormedAddCommGroup M<VAR>SeminormedAddCommGroup N<VAR>NormedSpace R M<VAR>NormedSpace R N<VAR>f : M →L[R] N<VAR>hf : IsConformalMap f<VAR>c : R<VAR>hc : c ≠ 0<GOAL>IsConformalMap (c • f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>NormedField R<VAR>SeminormedAddCommGroup M<VAR>NormedSpace R M<VAR>c : R<VAR>hc : c ≠ 0<GOAL>IsConformalMap (c • ContinuousLinearMap.id R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>NormedField R<VAR>SeminormedAddCommGroup M<VAR>SeminormedAddCommGroup N<VAR>NormedSpace R M<VAR>NormedSpace R N<VAR>f' : M →ₗᵢ[R] N<GOAL>IsConformalMap f'.toContinuousLinearMap
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>NormedField R<VAR>SeminormedAddCommGroup M<VAR>SeminormedAddCommGroup N<VAR>NormedSpace R M<VAR>NormedSpace R N<VAR>Subsingleton M<VAR>f' : M →L[R] N<GOAL>IsConformalMap f'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>G : Type u_4<VAR>NormedField R<VAR>SeminormedAddCommGroup M<VAR>SeminormedAddCommGroup N<VAR>SeminormedAddCommGroup G<VAR>NormedSpace R M<VAR>NormedSpace R N<VAR>NormedSpace R G<VAR>f : M →L[R] N<VAR>g : N →L[R] G<VAR>hg : IsConformalMap g<VAR>hf : IsConformalMap f<GOAL>IsConformalMap (g.comp f)
<VAR>R : Type u_1<VAR>N : Type u_3<VAR>M' : Type u_5<VAR>NormedField R<VAR>SeminormedAddCommGroup N<VAR>NormedSpace R N<VAR>NormedAddCommGroup M'<VAR>NormedSpace R M'<VAR>f : M' →L[R] N<VAR>h : IsConformalMap f<GOAL>Function.Injective ⇑f
<VAR>R : Type u_1<VAR>N : Type u_3<VAR>M' : Type u_5<VAR>NormedField R<VAR>SeminormedAddCommGroup N<VAR>NormedSpace R N<VAR>NormedAddCommGroup M'<VAR>NormedSpace R M'<VAR>Nontrivial M'<VAR>f' : M' →L[R] N<VAR>hf' : IsConformalMap f'<GOAL>f' ≠ 0
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>w : ι → R<VAR>z : ι → E<GOAL>∅.centerMass w z = 0
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>i j : ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hne : i ≠ j<GOAL>{i, j}.centerMass w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>i : ι<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>ha : i ∉ t<VAR>hw : ∑ j ∈ t, w j ≠ 0<GOAL>(insert i t).centerMass w z = (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>i : ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hw : w i ≠ 0<GOAL>{i}.centerMass w z = z i
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<GOAL>t.centerMass (-w) z = t.centerMass w z
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>LinearOrderedField R'<VAR>AddCommGroup E<VAR>Module R E<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>c : R'<VAR>Module R' R<VAR>Module R' E<VAR>SMulCommClass R' R R<VAR>IsScalarTower R' R R<VAR>SMulCommClass R R' E<VAR>IsScalarTower R' R E<VAR>hc : c ≠ 0<GOAL>t.centerMass (c • w) z = t.centerMass w z
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hw : ∑ i ∈ t, w i = 1<GOAL>t.centerMass w z = ∑ i ∈ t, w i • z i
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<GOAL>(t.centerMass w fun i => c • z i) = c • t.centerMass w z
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>ws : ι → R<VAR>zs : ι → E<VAR>wt : ι' → R<VAR>zt : ι' → E<VAR>hws : ∑ i ∈ s, ws i = 1<VAR>hwt : ∑ i ∈ t, wt i = 1<VAR>a b : R<VAR>hab : a + b = 1<GOAL>a • s.centerMass ws zs + b • t.centerMass wt zt = (s.disjSum t).centerMass (Sum.elim (fun i => a * ws i) fun j => b * wt j) (Sum.elim zs zt)
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Finset ι<VAR>w₁ w₂ : ι → R<VAR>z : ι → E<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>a b : R<VAR>hab : a + b = 1<GOAL>a • s.centerMass w₁ z + b • s.centerMass w₂ z = s.centerMass (fun i => a * w₁ i + b * w₂ i) z
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>i : ι<VAR>t : Finset ι<VAR>z : ι → E<VAR>hi : i ∈ t<GOAL>t.centerMass (fun j => if i = j then 1 else 0) z = z i
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>t' : Finset ι<VAR>ht : t ⊆ t'<VAR>h : ∀ i ∈ t', i ∉ t → w i = 0<GOAL>t.centerMass w z = t'.centerMass w z
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<GOAL>(Finset.filter (fun i => w i ≠ 0) t).centerMass w z = t.centerMass w z
<VAR>R : Type u_1<VAR>ι : Type u_5<VAR>α : Type u_7<VAR>LinearOrderedField R<VAR>LinearOrderedAddCommGroup α<VAR>Module R α<VAR>OrderedSMul R α<VAR>s : Finset ι<VAR>f : ι → α<VAR>w : ι → R<VAR>hw₀ : ∀ i ∈ s, 0 ≤ w i<VAR>hw₁ : 0 < ∑ i ∈ s, w i<GOAL>s.centerMass w f ≤ s.sup' ⋯ f
<VAR>R : Type u_1<VAR>ι : Type u_5<VAR>α : Type u_7<VAR>LinearOrderedField R<VAR>LinearOrderedAddCommGroup α<VAR>Module R α<VAR>OrderedSMul R α<VAR>s : Finset ι<VAR>f : ι → α<VAR>w : ι → R<VAR>hw₀ : ∀ i ∈ s, 0 ≤ w i<VAR>hw₁ : 0 < ∑ i ∈ s, w i<GOAL>s.inf' ⋯ f ≤ s.centerMass w f
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>w : ι → R<VAR>z : ι → E<VAR>s t : Finset ι<VAR>hw : ∑ i ∈ s, w i + ∑ i ∈ t, w i = 0<VAR>hz : ∑ i ∈ s, w i • z i + ∑ i ∈ t, w i • z i = 0<GOAL>s.centerMass w z = t.centerMass w z
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Set E<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hs : Convex R s<GOAL>(∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Set E<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hs : Convex R s<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hz : ∀ i ∈ t, z i ∈ s<GOAL>∑ i ∈ t, w i • z i ∈ s
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>ι : Sort u_8<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Set E<VAR>hs : Convex R s<VAR>h₀ : ∀ (i : ι), 0 ≤ w i<VAR>h₁ : ∑ᶠ (i : ι), w i = 1<VAR>hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s<GOAL>∑ᶠ (i : ι), w i • z i ∈ s
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Set E<GOAL>Convex R s ↔ ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Set E<VAR>t : Finset ι<VAR>w : ι → R<VAR>hw₀ : ∀ i ∈ t, 0 ≤ w i<VAR>hws : 0 < ∑ i ∈ t, w i<VAR>z : ι → E<VAR>hz : ∀ i ∈ t, z i ∈ s<GOAL>t.centerMass w z ∈ (convexHull R) s
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Set E<VAR>w : ι → R<VAR>z : ι → E<VAR>t : Finset ι<VAR>hw₀ : ∀ i ∈ t, w i ≤ 0<VAR>hws : ∑ i ∈ t, w i < 0<VAR>hz : ∀ i ∈ t, z i ∈ s<GOAL>t.centerMass w z ∈ (convexHull R) s
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>t : Finset E<VAR>w : E → R<VAR>hw₀ : ∀ i ∈ t, 0 ≤ w i<VAR>hws : 0 < ∑ i ∈ t, w i<GOAL>t.centerMass w id ∈ (convexHull R) ↑t
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>t : Finset E<VAR>w : E → R<VAR>hw₀ : ∀ i ∈ t, w i ≤ 0<VAR>hws : ∑ i ∈ t, w i < 0<GOAL>t.centerMass w id ∈ (convexHull R) ↑t
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>ι : Type u_8<VAR>t : Finset ι<VAR>p : ι → E<VAR>w : ι → R<VAR>hw₂ : ∑ i ∈ t, w i = 1<GOAL>(Finset.affineCombination R t p) w = t.centerMass w p
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Finset ι<VAR>v : ι → E<VAR>w : ι → R<VAR>hw₀ : ∀ i ∈ s, 0 ≤ w i<VAR>hw₁ : s.sum w = 1<GOAL>(Finset.affineCombination R s v) w ∈ (convexHull R) (Set.range v)
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>p : ι → E<GOAL>Finset.centroid R s p = s.centerMass (Finset.centroidWeights R s) p
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Finset E<VAR>hs : s.Nonempty<GOAL>Finset.centroid R s id ∈ (convexHull R) ↑s
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>v : ι → E<GOAL>(convexHull R) (Set.range v) = {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (Finset.affineCombination R s v) w = x}
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Set E<GOAL>(convexHull R) s = {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Set E<VAR>x : E<VAR>Fintype ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hw₀ : ∀ (i : ι), 0 ≤ w i<VAR>hw₁ : ∑ i : ι, w i = 1<VAR>hz : ∀ (i : ι), z i ∈ s<VAR>hx : ∑ i : ι, w i • z i = x<GOAL>x ∈ (convexHull R) s
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Set E<VAR>x : E<GOAL>x ∈ (convexHull R) s ↔ ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Finset E<GOAL>(convexHull R) ↑s = {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Finset E<VAR>x : E<GOAL>x ∈ (convexHull R) ↑s ↔ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Finset E<VAR>x : E<GOAL>x ∈ (convexHull R) ↑s ↔ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Set E<VAR>hs : s.Finite<GOAL>(convexHull R) s = {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ hs.toFinset, w y = 1 ∧ hs.toFinset.centerMass w id = x}
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Set E<GOAL>(convexHull R) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>y : F<VAR>hx : x ∈ (convexHull R) s<VAR>hy : y ∈ (convexHull R) t<GOAL>(x, y) ∈ (convexHull R) (s ×ˢ t)
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>s : Set E<VAR>t : Set F<GOAL>(convexHull R) (s ×ˢ t) = (convexHull R) s ×ˢ (convexHull R) t
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s t : Set E<GOAL>(convexHull R) (s + t) = (convexHull R) s + (convexHull R) t
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>a : Set E<GOAL>(convexHullAddMonoidHom R E) a = (convexHull R) a
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s t : Set E<GOAL>(convexHull R) (s - t) = (convexHull R) s - (convexHull R) t
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>l : List (Set E)<GOAL>(convexHull R) l.sum = (List.map (⇑(convexHull R)) l).sum
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Multiset (Set E)<GOAL>(convexHull R) s.sum = (Multiset.map (⇑(convexHull R)) s).sum
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>ι : Type u_8<VAR>s : Finset ι<VAR>t : ι → Set E<GOAL>(convexHull R) (∑ i ∈ s, t i) = ∑ i ∈ s, (convexHull R) (t i)
<VAR>R : Type u_1<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>Fintype ι<GOAL>(convexHull R) (Set.range fun i j => if i = j then 1 else 0) = stdSimplex R ι
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s : Set E<VAR>hs : s.Finite<GOAL>(convexHull R) s = ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) '' stdSimplex R ↑s
<VAR>R : Type u_1<VAR>ι : Type u_5<VAR>LinearOrderedField R<VAR>Fintype ι<VAR>f : ι → R<VAR>hf : f ∈ stdSimplex R ι<VAR>x : ι<GOAL>f x ∈ Set.Icc 0 1
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>ι : Type u_8<VAR>b : AffineBasis ι R E<GOAL>(convexHull R) (Set.range ⇑b) = {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>s t₁ t₂ : Finset E<VAR>hs : AffineIndependent R Subtype.val<VAR>ht₁ : t₁ ⊆ s<VAR>ht₂ : t₂ ⊆ s<GOAL>(convexHull R) (↑t₁ ∩ ↑t₂) = (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂
<VAR>R : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField R<VAR>AddCommGroup E<VAR>Module R E<VAR>t₁ t₂ : Finset E<VAR>hs : AffineIndependent R Subtype.val<GOAL>(convexHull R) (↑t₁ ∩ ↑t₂) = (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>Finite ι<VAR>LinearOrderedField 𝕜<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>s : Set ι<VAR>t : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>h : ∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)<GOAL>x ∈ (convexHull 𝕜) (s.pi t)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>Finite ι<VAR>LinearOrderedField 𝕜<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>s : Set ι<VAR>t : (i : ι) → Set (E i)<GOAL>(convexHull 𝕜) (s.pi t) = s.pi fun i => (convexHull 𝕜) (t i)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>‖f‖₊ = sInf {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊}
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>M : ℝ≥0<VAR>hM : ∀ (x : E), ‖f x‖₊ ≤ M * ‖x‖₊<GOAL>‖f‖₊ ≤ M
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>M : ℝ≥0<VAR>hM : ∀ (x : E), ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊<GOAL>‖f‖₊ ≤ M
<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ F<VAR>f : E →L[ℝ] F<VAR>C : ℝ≥0<VAR>hf : ∀ (x : E), ‖x‖₊ = 1 → ‖f x‖₊ ≤ C<GOAL>‖f‖₊ ≤ C
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>K : ℝ≥0<VAR>hf : LipschitzWith K ⇑f<GOAL>‖f‖₊ ≤ K
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>φ : E →SL[σ₁₂] F<VAR>M : ℝ≥0<VAR>h_above : ∀ (x : E), ‖φ x‖₊ ≤ M * ‖x‖₊<VAR>h_below : ∀ (N : ℝ≥0), (∀ (x : E), ‖φ x‖₊ ≤ N * ‖x‖₊) → M ≤ N<GOAL>‖φ‖₊ = M
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>C : ℝ≥0<GOAL>‖f‖₊ ≤ C ↔ ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>IsLeast {C | ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊} ‖f‖₊
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>F : Type u_6<VAR>G : Type u_8<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>SeminormedAddCommGroup G<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomIsometric σ₁₂<VAR>RingHomIsometric σ₂₃<VAR>h : F →SL[σ₂₃] G<VAR>RingHomIsometric σ₁₃<VAR>f : E →SL[σ₁₂] F<GOAL>‖h.comp f‖₊ ≤ ‖h‖₊ * ‖f‖₊
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>x : E<GOAL>‖f x‖₊ ≤ ‖f‖₊ * ‖x‖₊
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>x y : E<GOAL>nndist (f x) (f y) ≤ ‖f‖₊ * nndist x y
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>LipschitzWith ‖f‖₊ ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>x : E<GOAL>LipschitzWith ‖x‖₊ fun f => f x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ≥0<VAR>hr : r < ‖f‖₊<GOAL>∃ x, r * ‖x‖₊ < ‖f x‖₊
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ<VAR>hr₀ : 0 ≤ r<VAR>hr : r < ‖f‖<GOAL>∃ x, r * ‖x‖ < ‖f x‖
<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>NormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>DenselyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ≥0<VAR>hr : r < ‖f‖₊<GOAL>∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>NormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>DenselyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ<VAR>hr : r < ‖f‖<GOAL>∃ x, ‖x‖ < 1 ∧ r < ‖f x‖
<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>NormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>DenselyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>sSup ((fun x => ‖f x‖₊) '' Metric.ball 0 1) = ‖f‖₊
<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>NormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>DenselyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>sSup ((fun x => ‖f x‖) '' Metric.ball 0 1) = ‖f‖
<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>NormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>DenselyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>sSup ((fun x => ‖f x‖₊) '' Metric.closedBall 0 1) = ‖f‖₊