ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>0 < 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 r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r'_pos : 0 < r'<VAR>hr : r' ≤ r<GOAL>HasFPowerSeriesOnBall f 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 g : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hf : HasFPowerSeriesAt f p x<VAR>hg : f =ᶠ[𝓝 x] g<GOAL>HasFPowerSeriesAt g 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>∀ᶠ (r : ℝ≥0∞) in 𝓝[>] 0, HasFPowerSeriesOnBall f 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<GOAL>∀ᶠ (y : E) in 𝓝 0, 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>x : E<VAR>hf : HasFPowerSeriesAt f p x<GOAL>∀ᶠ (y : E) in 𝓝 0, 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>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<GOAL>∀ᶠ (y : E) in 𝓝 x, 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>hf : HasFPowerSeriesAt f p x<GOAL>∀ᶠ (y : E) in 𝓝 x, 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>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f 0 x r<GOAL>∀ᶠ (z : E) in 𝓝 x, f z = 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>x : E<VAR>hf : HasFPowerSeriesAt f 0 x<GOAL>∀ᶠ (z : E) in 𝓝 x, f z = 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>c : F<VAR>e : E<GOAL>HasFPowerSeriesOnBall (fun x => c) (constFormalMultilinearSeries 𝕜 E c) e ⊤
<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>HasFPowerSeriesAt (fun x => c) (constFormalMultilinearSeries 𝕜 E c) e
<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>AnalyticAt 𝕜 (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>AnalyticOn 𝕜 (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>hf : HasFPowerSeriesOnBall f pf x r<VAR>hg : HasFPowerSeriesOnBall g pg x r<GOAL>HasFPowerSeriesOnBall (f + g) (pf + pg) 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 g : E → F<VAR>pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hf : HasFPowerSeriesAt f pf x<VAR>hg : HasFPowerSeriesAt g pg x<GOAL>HasFPowerSeriesAt (f + g) (pf + pg) 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 : AnalyticAt 𝕜 f x<VAR>hg : f =ᶠ[𝓝 x] g<GOAL>AnalyticAt 𝕜 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>AnalyticAt 𝕜 f x ↔ AnalyticAt 𝕜 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 : AnalyticAt 𝕜 f x<VAR>hg : AnalyticAt 𝕜 g x<GOAL>AnalyticAt 𝕜 (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>hf : HasFPowerSeriesOnBall f pf x r<GOAL>HasFPowerSeriesOnBall (-f) (-pf) 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>pf : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hf : HasFPowerSeriesAt f pf x<GOAL>HasFPowerSeriesAt (-f) (-pf) 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 : AnalyticAt 𝕜 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 g : E → F<VAR>pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f pf x r<VAR>hg : HasFPowerSeriesOnBall g pg x r<GOAL>HasFPowerSeriesOnBall (f - g) (pf - pg) 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 g : E → F<VAR>pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hf : HasFPowerSeriesAt f pf x<VAR>hg : HasFPowerSeriesAt g pg x<GOAL>HasFPowerSeriesAt (f - g) (pf - pg) 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 : AnalyticAt 𝕜 f x<VAR>hg : AnalyticAt 𝕜 g x<GOAL>AnalyticAt 𝕜 (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 : AnalyticOn 𝕜 f t<VAR>hst : s ⊆ t<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>s : Set E<VAR>hf : AnalyticOn 𝕜 f s<VAR>hg : f =ᶠ[𝓝ˢ s] g<GOAL>AnalyticOn 𝕜 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>AnalyticOn 𝕜 f s ↔ AnalyticOn 𝕜 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 : AnalyticOn 𝕜 f s<VAR>hg : Set.EqOn f g s<GOAL>AnalyticOn 𝕜 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>AnalyticOn 𝕜 f s ↔ AnalyticOn 𝕜 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 : AnalyticOn 𝕜 f s<VAR>hg : AnalyticOn 𝕜 g s<GOAL>AnalyticOn 𝕜 (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 : E → F<VAR>s : Set E<VAR>hf : AnalyticOn 𝕜 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>s : Set E<VAR>hf : AnalyticOn 𝕜 f s<VAR>hg : AnalyticOn 𝕜 g s<GOAL>AnalyticOn 𝕜 (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 : E → F<VAR>pf : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f pf x r<VAR>v : Fin 0 → E<GOAL>(pf 0) v = 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 : HasFPowerSeriesAt f pf x<VAR>v : Fin 0 → E<GOAL>(pf 0) v = f 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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>g : F →L[𝕜] G<VAR>h : HasFPowerSeriesOnBall f p x r<GOAL>HasFPowerSeriesOnBall (⇑g ∘ f) (g.compFormalMultilinearSeries p) x 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 : AnalyticOn 𝕜 f s<GOAL>AnalyticOn 𝕜 (⇑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>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<GOAL>∃ a ∈ Set.Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<GOAL>∃ a ∈ Set.Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ 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>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hf : HasFPowerSeriesAt f p x<VAR>n : ℕ<GOAL>(fun y => f (x + y) - p.partialSum n y) =O[𝓝 0] fun y => ‖y‖ ^ 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 r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>hr : r' < r<GOAL>(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<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>hf : HasFPowerSeriesOnBall f p x r<VAR>hr : r' < r<GOAL>∃ C, ∀ y ∈ EMetric.ball x r', ∀ z ∈ EMetric.ball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
<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>(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓝 (x, x)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<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>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<GOAL>TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) Filter.atTop (Metric.ball 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>TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) Filter.atTop (EMetric.ball 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>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<GOAL>TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f Filter.atTop (Metric.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>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<GOAL>TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f Filter.atTop (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>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x 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>hf : HasFPowerSeriesAt f p 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>x : E<VAR>hf : AnalyticAt 𝕜 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 : AnalyticOn 𝕜 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 : AnalyticOn 𝕜 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>CompleteSpace F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : 0 < p.radius<GOAL>HasFPowerSeriesOnBall p.sum p 0 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>h : HasFPowerSeriesOnBall f p x 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>CompleteSpace F<GOAL>ContinuousOn p.sum (EMetric.ball 0 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>n : ℕ<VAR>p : ContinuousMultilinearMap 𝕜 (fun i => E) F<VAR>h : (fun y => p fun x => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)<VAR>y : E<GOAL>(p fun x => 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>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>h : HasFPowerSeriesAt 0 p x<VAR>n : ℕ<VAR>y : E<GOAL>((p n) fun x => y) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>x : 𝕜<VAR>h : HasFPowerSeriesAt 0 p x<GOAL>p = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>h₁ : HasFPowerSeriesAt f p₁ x<VAR>h₂ : HasFPowerSeriesAt f p₂ x<GOAL>p₁ = p₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hp : HasFPowerSeriesAt f p x<VAR>hq : HasFPowerSeriesAt g q x<VAR>heq : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = g z<GOAL>p = q
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hp : HasFPowerSeriesAt f p x<VAR>hf : f =ᶠ[𝓝 x] 0<GOAL>p = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>r₁ r₂ : ℝ≥0∞<VAR>x : 𝕜<VAR>h₁ : HasFPowerSeriesOnBall f p₁ x r₁<VAR>h₂ : HasFPowerSeriesOnBall f p₂ x r₂<GOAL>HasFPowerSeriesOnBall f p₁ x r₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>r : ℝ≥0∞<VAR>x : 𝕜<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>h' : ∀ (r' : ℝ≥0), 0 < r' → ∃ p', HasFPowerSeriesOnBall f p' x ↑r'<GOAL>HasFPowerSeriesOnBall 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>p : FormalMultilinearSeries 𝕜 E F<VAR>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<VAR>x y : E<GOAL>(((p.changeOriginSeriesTerm k l s hs) fun x_1 => x) fun x => y) = (p (k + l)) (s.piecewise (fun x_1 => x) fun 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>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<GOAL>‖p.changeOriginSeriesTerm k l s hs‖ = ‖p (k + l)‖
<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>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<GOAL>‖p.changeOriginSeriesTerm k l s hs‖₊ = ‖p (k + l)‖₊
<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>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<VAR>x y : E<GOAL>‖((p.changeOriginSeriesTerm k l s hs) fun x_1 => x) fun x => y‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ 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>p : FormalMultilinearSeries 𝕜 E F<VAR>k l : ℕ<GOAL>‖p.changeOriginSeries k l‖₊ ≤ ∑' (x : { s // s.card = l }), ‖p (k + l)‖₊
<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>k l : ℕ<VAR>x : E<GOAL>‖(p.changeOriginSeries k l) fun x_1 => x‖₊ ≤ ∑' (x_1 : { s // s.card = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l
<VAR>s : (n : ℕ) × Finset (Fin n)<GOAL>(FormalMultilinearSeries.changeOriginIndexEquiv.symm s).fst = s.fst - s.snd.card
<VAR>s : (n : ℕ) × Finset (Fin n)<GOAL>↑(FormalMultilinearSeries.changeOriginIndexEquiv.symm s).snd.snd = Finset.map (finCongr ⋯).toEmbedding s.snd
<VAR>s : (n : ℕ) × Finset (Fin n)<GOAL>(FormalMultilinearSeries.changeOriginIndexEquiv.symm s).snd.fst = s.snd.card
<VAR>s : (k : ℕ) × (l : ℕ) × { s // s.card = l }<GOAL>(FormalMultilinearSeries.changeOriginIndexEquiv s).snd = ↑s.snd.snd
<VAR>s : (k : ℕ) × (l : ℕ) × { s // s.card = l }<GOAL>(FormalMultilinearSeries.changeOriginIndexEquiv s).fst = s.fst + s.snd.fst
<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 y : E<VAR>n : ℕ<VAR>t : Finset (Fin n)<GOAL>let s := FormalMultilinearSeries.changeOriginIndexEquiv.symm ⟨n, t⟩;
(((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y) = (p n) (t.piecewise (fun x_1 => x) fun 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>r r' : ℝ≥0<VAR>hr : ↑r + ↑r' < p.radius<GOAL>Summable fun s => ‖p (s.fst + s.snd.fst)‖₊ * r ^ s.snd.fst * r' ^ s.fst
<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>hr : ↑r < p.radius<VAR>k : ℕ<GOAL>Summable fun s => ‖p (k + s.fst)‖₊ * r ^ s.fst
<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>hr : ↑r < p.radius<VAR>k : ℕ<GOAL>Summable fun l => ‖p.changeOriginSeries k l‖₊ * r ^ l
<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>k : ℕ<GOAL>p.radius ≤ (p.changeOriginSeries k).radius