ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>self : 𝓜(𝕜, A)<GOAL>DoubleCentralizer.toProdHom self = self.toProd
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<GOAL>∀ (a : 𝓜(𝕜, A)), DoubleCentralizer.toProdMulOppositeHom a = a.toProdMulOpposite
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>k : 𝕜<GOAL>((algebraMap 𝕜 𝓜(𝕜, A)) k).toProd = (algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A))) k
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>k : 𝕜<GOAL>((algebraMap 𝕜 𝓜(𝕜, A)) k).toProd.1 = (algebraMap 𝕜 (A →L[𝕜] A)) k
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>k : 𝕜<GOAL>((algebraMap 𝕜 𝓜(𝕜, A)) k).toProd.2 = (algebraMap 𝕜 (A →L[𝕜] A)) k
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>StarRing 𝕜<VAR>StarRing A<VAR>StarModule 𝕜 A<VAR>NormedStarGroup A<VAR>a : 𝓜(𝕜, A)<VAR>b : A<GOAL>(star a).toProd.1 b = star (a.toProd.2 (star b))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>StarRing 𝕜<VAR>StarRing A<VAR>StarModule 𝕜 A<VAR>NormedStarGroup A<VAR>a : 𝓜(𝕜, A)<VAR>b : A<GOAL>(star a).toProd.2 b = star (a.toProd.1 (star b))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a : A<GOAL>(↑𝕜 a).toProd.1 = (ContinuousLinearMap.mul 𝕜 A) a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a : A<GOAL>(↑𝕜 a).toProd.2 = (ContinuousLinearMap.mul 𝕜 A).flip a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<GOAL>↑𝕜 = ⇑(algebraMap 𝕜 𝓜(𝕜, 𝕜))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>StarRing 𝕜<VAR>StarRing A<VAR>StarModule 𝕜 A<VAR>NormedStarGroup A<VAR>a : A<GOAL>DoubleCentralizer.coeHom a = ↑𝕜 a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a : 𝓜(𝕜, A)<GOAL>‖a‖ = ‖DoubleCentralizer.toProdHom a‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a : 𝓜(𝕜, A)<GOAL>‖a‖₊ = ‖DoubleCentralizer.toProdHom a‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a : 𝓜(𝕜, A)<GOAL>‖a‖ = ‖DoubleCentralizer.toProdMulOppositeHom a‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a : 𝓜(𝕜, A)<GOAL>‖a‖₊ = ‖DoubleCentralizer.toProdMulOppositeHom a‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<GOAL>UniformEmbedding DoubleCentralizer.toProdMulOpposite
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>StarRing A<VAR>CstarRing A<VAR>a : 𝓜(𝕜, A)<GOAL>‖a.toProd.1‖ = ‖a.toProd.2‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>StarRing A<VAR>CstarRing A<VAR>a : 𝓜(𝕜, A)<GOAL>‖a.toProd.1‖₊ = ‖a.toProd.2‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>StarRing A<VAR>CstarRing A<VAR>a : 𝓜(𝕜, A)<GOAL>‖a.toProd.1‖ = ‖a‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>StarRing A<VAR>CstarRing A<VAR>a : 𝓜(𝕜, A)<GOAL>‖a.toProd.2‖ = ‖a‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>StarRing A<VAR>CstarRing A<VAR>a : 𝓜(𝕜, A)<GOAL>‖a.toProd.1‖₊ = ‖a‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>StarRing A<VAR>CstarRing A<VAR>a : 𝓜(𝕜, A)<GOAL>‖a.toProd.2‖₊ = ‖a‖₊
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConcaveOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(f y - f x) / (y - x) < (f z - f y) / (z - y)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(f z - f y) / (z - y) < (f y - f x) / (y - x)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)<GOAL>ConvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)<GOAL>ConcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)<GOAL>StrictConvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)<GOAL>StrictConcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<GOAL>ConvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<GOAL>ConcaveOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<GOAL>StrictConvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<GOAL>StrictConcaveOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(z - x) * f y ≤ (z - y) * f x + (y - x) * f z
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(f y - f x) / (y - x) ≤ (f z - f x) / (z - x)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(f z - f x) / (z - x) ≤ (f z - f y) / (z - y)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>a x y : 𝕜<VAR>ha : a ∈ s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxa : x ≠ a<VAR>hya : y ≠ a<VAR>hxy : x ≤ y<GOAL>(f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(z - x) * f y < (z - y) * f x + (y - x) * f z
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(f y - f x) / (y - x) < (f z - f x) / (z - x)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(f z - f x) / (z - x) < (f z - f y) / (z - y)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>a x y : 𝕜<VAR>ha : a ∈ s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxa : x ≠ a<VAR>hya : y ≠ a<VAR>hxy : x < y<GOAL>(f x - f a) / (x - a) < (f y - f a) / (y - a)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>a x y : 𝕜<VAR>ha : a ∈ s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxa : x ≠ a<VAR>hya : y ≠ a<VAR>hxy : x < y<GOAL>(f y - f a) / (y - a) < (f x - f a) / (x - a)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : 𝕜<VAR>hx : x ∈ s<VAR>hxy : x < y<VAR>hxy' : f x < f y<GOAL>StrictMonoOn f (s ∩ Set.Ici y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalAddGroup E<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 E<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>Continuous (p.partialSum n)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>C : ℝ<VAR>r : ℝ≥0<VAR>h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C<GOAL>↑r ≤ p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>C : ℝ≥0<VAR>r : ℝ≥0<VAR>h : ∀ (n : ℕ), ‖p n‖₊ * r ^ n ≤ C<GOAL>↑r ≤ p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : (fun n => ‖p n‖ * ↑r ^ n) =O[Filter.atTop] fun x => 1<GOAL>↑r ≤ p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>C : ℝ<VAR>h : ∀ᶠ (n : ℕ) in Filter.atTop, ‖p n‖ * ↑r ^ n ≤ C<GOAL>↑r ≤ p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : Summable fun n => ‖p n‖₊ * r ^ n<GOAL>↑r ≤ p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : Summable fun n => ‖p n‖ * ↑r ^ n<GOAL>↑r ≤ p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : ∀ (r : ℝ≥0), (fun n => ‖p n‖ * ↑r ^ n) =O[Filter.atTop] fun x => 1<GOAL>p.radius = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : ∀ᶠ (n : ℕ) in Filter.atTop, p n = 0<GOAL>p.radius = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), p (m + n) = 0<GOAL>p.radius = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>v : F<GOAL>(constFormalMultilinearSeries 𝕜 E v).radius = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<GOAL>FormalMultilinearSeries.radius 0 = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<GOAL>∃ a ∈ Set.Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[Filter.atTop] fun x => a ^ x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<GOAL>(fun n => ‖p n‖ * ↑r ^ n) =o[Filter.atTop] fun x => 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<GOAL>∃ a ∈ Set.Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h₀ : r ≠ 0<VAR>a : ℝ<VAR>ha : a ∈ Set.Ioo (-1) 1<VAR>hp : (fun n => ‖p n‖ * ↑r ^ n) =O[Filter.atTop] fun x => a ^ x<GOAL>↑r < p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<GOAL>∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h0 : 0 < r<VAR>h : ↑r < p.radius<GOAL>∃ C > 0, ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<GOAL>∃ C > 0, ∀ (n : ℕ), ‖p n‖₊ * r ^ n ≤ C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>r : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>l : ℝ<VAR>h : Filter.Tendsto (fun n => ‖p n‖ * ↑r ^ n) Filter.atTop (𝓝 l)<GOAL>↑r ≤ p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>r : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hs : Summable fun n => ‖p n‖ * ↑r ^ n<GOAL>↑r ≤ p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>h : p.radius < ↑‖x‖₊<GOAL>¬Summable fun n => ‖p n‖ * ‖x‖ ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<GOAL>Summable fun n => ‖p n‖ * ↑r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hx : x ∈ EMetric.ball 0 p.radius<GOAL>Summable fun n => ‖(p n) fun x_1 => x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<GOAL>Summable fun n => ‖p n‖₊ * r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hx : x ∈ EMetric.ball 0 p.radius<GOAL>Summable fun n => (p n) fun x_1 => x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hs : ∀ (r : ℝ≥0), Summable fun n => ‖p n‖ * ↑r ^ n<GOAL>p.radius = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<GOAL>p.radius = ⊤ ↔ ∀ (r : ℝ≥0), Summable fun n => ‖p n‖ * ↑r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : 0 < p.radius<GOAL>∃ C r, ∃ (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p q : FormalMultilinearSeries 𝕜 E F<GOAL>min p.radius q.radius ≤ (p + q).radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<GOAL>(-p).radius = p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hx : x ∈ EMetric.ball 0 p.radius<GOAL>HasSum (fun n => (p n) fun x_1 => x) (p.sum x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : F →L[𝕜] G<GOAL>p.radius ≤ (f.compFormalMultilinearSeries p).radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>self : HasFPowerSeriesOnBall f p x r<GOAL>r ≤ p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>self : HasFPowerSeriesOnBall f p x r<GOAL>0 < r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>self : HasFPowerSeriesOnBall f p x r<VAR>y : E<GOAL>y ∈ EMetric.ball 0 r → HasSum (fun n => (p n) fun x => y) (f (x + y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>x : E<VAR>r : ℝ≥0∞<VAR>self : HasFPowerSeriesWithinOnBall f p s x r<GOAL>ContinuousWithinAt f s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>x : E<VAR>r : ℝ≥0∞<VAR>self : HasFPowerSeriesWithinOnBall f p s x r<GOAL>r ≤ p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>x : E<VAR>r : ℝ≥0∞<VAR>self : HasFPowerSeriesWithinOnBall f p s x r<VAR>y : E<GOAL>x + y ∈ s → y ∈ EMetric.ball 0 r → HasSum (fun n => (p n) fun x => y) (f (x + y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>x : E<VAR>r : ℝ≥0∞<VAR>self : HasFPowerSeriesWithinOnBall f p s x r<GOAL>0 < r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<GOAL>HasFPowerSeriesAt f p x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hf : HasFPowerSeriesAt f p x<GOAL>AnalyticAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<GOAL>AnalyticAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>hg : Set.EqOn f g (EMetric.ball x r)<GOAL>HasFPowerSeriesOnBall g p x r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>y : E<GOAL>HasFPowerSeriesOnBall (fun z => f (z - y)) p (x + y) r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>hy : y ∈ EMetric.ball x r<GOAL>HasSum (fun n => (p n) fun x_1 => y - x) (f y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<GOAL>0 < p.radius