ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>s : Set ι<GOAL>Submodule.span 𝕜 (gramSchmidtNormed 𝕜 f '' s) = Submodule.span 𝕜 (gramSchmidt 𝕜 f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<GOAL>Submodule.span 𝕜 (Set.range (gramSchmidtNormed 𝕜 f)) = Submodule.span 𝕜 (Set.range (gramSchmidt 𝕜 f))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>Fintype ι<VAR>FiniteDimensional 𝕜 E<VAR>h : FiniteDimensional.finrank 𝕜 E = Fintype.card ι<VAR>f : ι → E<VAR>i : ι<VAR>hi : gramSchmidtNormed 𝕜 f i ≠ 0<GOAL>(gramSchmidtOrthonormalBasis h f) i = gramSchmidtNormed 𝕜 f i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>Fintype ι<VAR>FiniteDimensional 𝕜 E<VAR>h : FiniteDimensional.finrank 𝕜 E = Fintype.card ι<VAR>f : ι → E<VAR>hf : Pairwise fun i j => ⟪f i, f j⟫_𝕜 = 0<VAR>i : ι<VAR>hi : f i ≠ 0<GOAL>(gramSchmidtOrthonormalBasis h f) i = (↑‖f i‖)⁻¹ • f i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>Fintype ι<VAR>FiniteDimensional 𝕜 E<VAR>h : FiniteDimensional.finrank 𝕜 E = Fintype.card ι<VAR>f : ι → E<VAR>i : ι<VAR>hi : gramSchmidtNormed 𝕜 f i = 0<VAR>j : ι<GOAL>⟪(gramSchmidtOrthonormalBasis h f) i, f j⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>Fintype ι<VAR>FiniteDimensional 𝕜 E<VAR>h : FiniteDimensional.finrank 𝕜 E = Fintype.card ι<VAR>f : ι → E<VAR>i j : ι<VAR>hij : i < j<GOAL>⟪(gramSchmidtOrthonormalBasis h f) j, f i⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>Fintype ι<VAR>FiniteDimensional 𝕜 E<VAR>h : FiniteDimensional.finrank 𝕜 E = Fintype.card ι<VAR>f : ι → E<VAR>i j : ι<VAR>hij : i < j<GOAL>(gramSchmidtOrthonormalBasis h f).repr (f i) j = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>Fintype ι<VAR>FiniteDimensional 𝕜 E<VAR>h : FiniteDimensional.finrank 𝕜 E = Fintype.card ι<VAR>f : ι → E<GOAL>((gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f).BlockTriangular id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>Fintype ι<VAR>FiniteDimensional 𝕜 E<VAR>h : FiniteDimensional.finrank 𝕜 E = Fintype.card ι<VAR>f : ι → E<VAR>DecidableEq ι<GOAL>(gramSchmidtOrthonormalBasis h f).toBasis.det f = ∏ i : ι, ⟪(gramSchmidtOrthonormalBasis h f) i, f i⟫_𝕜
<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>n : ℕ<VAR>r : ℝ≥0∞<VAR>self : HasFiniteFPowerSeriesOnBall f p x n r<VAR>m : ℕ<GOAL>n ≤ m → p m = 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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>n : ℕ<VAR>r : ℝ≥0∞<VAR>finite : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>pos : 0 < r<VAR>sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i ∈ Finset.range n, (p i) fun x => y) = f (x + y)<GOAL>HasFiniteFPowerSeriesOnBall f p x n 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>n : ℕ<VAR>hf : HasFiniteFPowerSeriesAt f p x n<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>n : ℕ<VAR>hf : HasFiniteFPowerSeriesAt f p x n<VAR>m : ℕ<GOAL>n ≤ m → p m = 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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<GOAL>HasFiniteFPowerSeriesAt f p 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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>n : ℕ<VAR>hf : HasFiniteFPowerSeriesAt f p x n<GOAL>CPolynomialAt 𝕜 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>n : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<GOAL>CPolynomialAt 𝕜 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>x : E<VAR>hf : CPolynomialAt 𝕜 f 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>s : Set E<VAR>hf : CPolynomialOn 𝕜 f s<GOAL>AnalyticOn 𝕜 f s
<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>n : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>hg : Set.EqOn f g (EMetric.ball x r)<GOAL>HasFiniteFPowerSeriesOnBall g p x n 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>n : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>y : E<GOAL>HasFiniteFPowerSeriesOnBall (fun z => f (z - y)) p (x + y) n 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 r' : ℝ≥0∞<VAR>n : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>r'_pos : 0 < r'<VAR>hr : r' ≤ r<GOAL>HasFiniteFPowerSeriesOnBall f p x n 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 g : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>n : ℕ<VAR>hf : HasFiniteFPowerSeriesAt f p x n<VAR>hg : f =ᶠ[𝓝 x] g<GOAL>HasFiniteFPowerSeriesAt g p 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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>n : ℕ<VAR>hf : HasFiniteFPowerSeriesAt f p x n<GOAL>∀ᶠ (r : ℝ≥0∞) in 𝓝[>] 0, HasFiniteFPowerSeriesOnBall f p x n 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>c : F<VAR>e : E<GOAL>HasFiniteFPowerSeriesOnBall (fun x => c) (constFormalMultilinearSeries 𝕜 E c) e 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>c : F<VAR>e : E<GOAL>HasFiniteFPowerSeriesAt (fun x => c) (constFormalMultilinearSeries 𝕜 E c) e 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>x : E<VAR>v : F<GOAL>CPolynomialAt 𝕜 (fun x => v) 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>v : F<VAR>s : Set E<GOAL>CPolynomialOn 𝕜 (fun x => v) s
<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>pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>n m : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f pf x n r<VAR>hg : HasFiniteFPowerSeriesOnBall g pg x m r<GOAL>HasFiniteFPowerSeriesOnBall (f + g) (pf + pg) x (max n m) 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 g : E → F<VAR>pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>n m : ℕ<VAR>hf : HasFiniteFPowerSeriesAt f pf x n<VAR>hg : HasFiniteFPowerSeriesAt g pg x m<GOAL>HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)
<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>x : E<VAR>hf : CPolynomialAt 𝕜 f x<VAR>hg : f =ᶠ[𝓝 x] g<GOAL>CPolynomialAt 𝕜 g 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>x : E<VAR>h : f =ᶠ[𝓝 x] g<GOAL>CPolynomialAt 𝕜 f x ↔ CPolynomialAt 𝕜 g 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>x : E<VAR>hf : CPolynomialAt 𝕜 f x<VAR>hg : CPolynomialAt 𝕜 g x<GOAL>CPolynomialAt 𝕜 (f + g) 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>pf : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f pf x n r<GOAL>HasFiniteFPowerSeriesOnBall (-f) (-pf) x n 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>pf : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>n : ℕ<VAR>hf : HasFiniteFPowerSeriesAt f pf x n<GOAL>HasFiniteFPowerSeriesAt (-f) (-pf) 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>f : E → F<VAR>x : E<VAR>hf : CPolynomialAt 𝕜 f x<GOAL>CPolynomialAt 𝕜 (-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>pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>n m : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f pf x n r<VAR>hg : HasFiniteFPowerSeriesOnBall g pg x m r<GOAL>HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (max n m) 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 g : E → F<VAR>pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>n m : ℕ<VAR>hf : HasFiniteFPowerSeriesAt f pf x n<VAR>hg : HasFiniteFPowerSeriesAt g pg x m<GOAL>HasFiniteFPowerSeriesAt (f - g) (pf - pg) x (max n m)
<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>x : E<VAR>hf : CPolynomialAt 𝕜 f x<VAR>hg : CPolynomialAt 𝕜 g x<GOAL>CPolynomialAt 𝕜 (f - g) 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>s t : Set E<VAR>hf : CPolynomialOn 𝕜 f t<VAR>hst : s ⊆ t<GOAL>CPolynomialOn 𝕜 f s
<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>s : Set E<VAR>hf : CPolynomialOn 𝕜 f s<VAR>hg : f =ᶠ[𝓝ˢ s] g<GOAL>CPolynomialOn 𝕜 g s
<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>s : Set E<VAR>h : f =ᶠ[𝓝ˢ s] g<GOAL>CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s
<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>s : Set E<VAR>hs : IsOpen s<VAR>hf : CPolynomialOn 𝕜 f s<VAR>hg : Set.EqOn f g s<GOAL>CPolynomialOn 𝕜 g s
<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>s : Set E<VAR>hs : IsOpen s<VAR>h : Set.EqOn f g s<GOAL>CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s
<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>s : Set E<VAR>hf : CPolynomialOn 𝕜 f s<VAR>hg : CPolynomialOn 𝕜 g s<GOAL>CPolynomialOn 𝕜 (f + g) s
<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>s : Set E<VAR>hf : CPolynomialOn 𝕜 f s<VAR>hg : CPolynomialOn 𝕜 g s<GOAL>CPolynomialOn 𝕜 (f - g) s
<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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>g : F →L[𝕜] G<VAR>h : HasFiniteFPowerSeriesOnBall f p x n r<GOAL>HasFiniteFPowerSeriesOnBall (⇑g ∘ f) (g.compFormalMultilinearSeries p) x n r
<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>f : E → F<VAR>s : Set E<VAR>g : F →L[𝕜] G<VAR>h : CPolynomialOn 𝕜 f s<GOAL>CPolynomialOn 𝕜 (⇑g ∘ f) s
<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>n : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>y : E<GOAL>y ∈ EMetric.ball 0 r → ∀ (m : ℕ), n ≤ m → f (x + y) = p.partialSum m 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>n : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>y : E<GOAL>y ∈ EMetric.ball x r → ∀ (m : ℕ), n ≤ m → f y = p.partialSum m (y - 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>pf : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFiniteFPowerSeriesOnBall f pf x 0 r<VAR>y : E<GOAL>y ∈ EMetric.ball x r → f y = 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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : ∀ y ∈ EMetric.ball x r, f y = 0<VAR>r_pos : 0 < r<VAR>hp : ∀ (n : ℕ), p n = 0<GOAL>HasFiniteFPowerSeriesOnBall f p x 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>pf : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hf : HasFiniteFPowerSeriesAt f pf x 0<GOAL>f =ᶠ[𝓝 x] 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>f : E → F<VAR>pf : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFiniteFPowerSeriesOnBall f pf x 1 r<VAR>y : E<GOAL>y ∈ EMetric.ball x r → f y = 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>pf : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hf : HasFiniteFPowerSeriesAt f pf x 1<GOAL>f =ᶠ[𝓝 x] fun x_1 => 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>n : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<GOAL>ContinuousOn f (EMetric.ball 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>n : ℕ<VAR>hf : HasFiniteFPowerSeriesAt f p x n<GOAL>ContinuousAt 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>x : E<VAR>hf : CPolynomialAt 𝕜 f x<GOAL>ContinuousAt 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>s : Set E<VAR>hf : CPolynomialOn 𝕜 f s<GOAL>ContinuousOn f s
<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>fa : CPolynomialOn 𝕜 f Set.univ<GOAL>Continuous f
<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 : ℕ), n ≤ m → p m = 0<VAR>x : E<GOAL>p.sum x = p.partialSum n 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>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>x : E<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>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<GOAL>HasFiniteFPowerSeriesOnBall p.sum p 0 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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>h : HasFiniteFPowerSeriesOnBall f p x n r<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 r<GOAL>f (x + y) = p.sum 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>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<GOAL>Continuous p.sum
<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 : ℕ), n ≤ m → p m = 0<VAR>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<VAR>hkl : n ≤ k + l<GOAL>p.changeOriginSeriesTerm k l s hs = 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>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<VAR>m : ℕ<GOAL>n ≤ k + m → p.changeOriginSeries k m = 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>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<GOAL>(p.changeOriginSeries k).sum = (p.changeOriginSeries k).partialSum (n - k)
<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>x : E<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<VAR>hk : n ≤ k<GOAL>p.changeOrigin x k = 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>n : ℕ<VAR>k : ℕ<VAR>hn : ∀ (m : ℕ), n + k ≤ m → p m = 0<GOAL>HasFiniteFPowerSeriesOnBall (fun x => p.changeOrigin x k) (p.changeOriginSeries k) 0 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>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>x y : E<GOAL>(p.changeOrigin x).sum y = p.sum (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>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<GOAL>CPolynomialAt 𝕜 (fun x => p.changeOrigin x k) 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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>x y : E<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>h : ↑‖y‖₊ < r<GOAL>HasFiniteFPowerSeriesOnBall f (p.changeOrigin y) (x + y) n (r - ↑‖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>r : ℝ≥0∞<VAR>n : ℕ<VAR>x y : E<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>h : y ∈ EMetric.ball x r<GOAL>CPolynomialAt 𝕜 f y