ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<GOAL>AnalyticAt 𝕜 f x → DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : AnalyticAt 𝕜 f x<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>x : E<VAR>h : HasFPowerSeriesAt f p x<GOAL>fderiv 𝕜 f x = (continuousMultilinearCurryFin1 𝕜 E F) (p 1)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>CompleteSpace F<VAR>h : HasFPowerSeriesOnBall f p x r<GOAL>DifferentiableOn 𝕜 f (EMetric.ball x r)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>h : AnalyticOn 𝕜 f s<GOAL>DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>CompleteSpace F<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>hy : ↑‖y‖₊ < r<GOAL>HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (x + y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>CompleteSpace F<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>hy : ↑‖y‖₊ < r<GOAL>fderiv 𝕜 f (x + y) = (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>CompleteSpace F<VAR>h : HasFPowerSeriesOnBall f p x r<GOAL>HasFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x r
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>CompleteSpace F<VAR>h : AnalyticOn 𝕜 f s<GOAL>AnalyticOn 𝕜 (fderiv 𝕜 f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>CompleteSpace F<VAR>h : AnalyticOn 𝕜 f s<VAR>n : ℕ<GOAL>AnalyticOn 𝕜 (iteratedFDeriv 𝕜 n f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>CompleteSpace F<VAR>h : AnalyticOn 𝕜 f s<VAR>n : ℕ∞<GOAL>ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>CompleteSpace F<VAR>h : AnalyticAt 𝕜 f x<VAR>n : ℕ∞<GOAL>ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>h : HasFPowerSeriesAt f p x<GOAL>HasStrictDerivAt f ((p 1) fun x => 1) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>h : HasFPowerSeriesAt f p x<GOAL>HasDerivAt f ((p 1) fun x => 1) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>h : HasFPowerSeriesAt f p x<GOAL>deriv f x = (p 1) fun x => 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>CompleteSpace F<VAR>h : AnalyticOn 𝕜 f s<GOAL>AnalyticOn 𝕜 (deriv f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>CompleteSpace F<VAR>h : AnalyticOn 𝕜 f s<VAR>n : ℕ<GOAL>AnalyticOn 𝕜 (deriv^[n] f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>f : E → F<VAR>x : E<VAR>h : HasFiniteFPowerSeriesOnBall f p x n r<GOAL>DifferentiableOn 𝕜 f (EMetric.ball x r)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>f : E → F<VAR>x : E<VAR>h : HasFiniteFPowerSeriesOnBall f p x n r<VAR>y : E<VAR>hy : ↑‖y‖₊ < r<GOAL>HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (x + y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>f : E → F<VAR>x : E<VAR>h : HasFiniteFPowerSeriesOnBall f p x n r<VAR>y : E<VAR>hy : ↑‖y‖₊ < r<GOAL>fderiv 𝕜 f (x + y) = (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>f : E → F<VAR>x : E<VAR>h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r<GOAL>HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x n r
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>f : E → F<VAR>x : E<VAR>h : HasFiniteFPowerSeriesOnBall f p x n r<GOAL>HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x (n - 1) r
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>h : CPolynomialOn 𝕜 f s<GOAL>CPolynomialOn 𝕜 (fderiv 𝕜 f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>h : CPolynomialOn 𝕜 f s<VAR>n : ℕ<GOAL>CPolynomialOn 𝕜 (iteratedFDeriv 𝕜 n f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>h : CPolynomialOn 𝕜 f s<VAR>n : ℕ∞<GOAL>ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : CPolynomialAt 𝕜 f x<VAR>n : ℕ∞<GOAL>ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>h : CPolynomialOn 𝕜 f s<GOAL>CPolynomialOn 𝕜 (deriv f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>h : CPolynomialOn 𝕜 f s<VAR>n : ℕ<GOAL>CPolynomialOn 𝕜 (deriv^[n] f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<GOAL>HasFiniteFPowerSeriesOnBall (⇑f) f.toFormalMultilinearSeries 0 (Fintype.card ι + 1) ⊤
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>k l : ℕ<VAR>h : k + l ≠ Fintype.card ι<GOAL>f.toFormalMultilinearSeries.changeOriginSeries k l = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : (i : ι) → E i<VAR>DecidableEq ι<GOAL>(continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F) (f.toFormalMultilinearSeries.changeOrigin x 1) = f.linearDeriv x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : (i : ι) → E i<VAR>DecidableEq ι<GOAL>HasFDerivAt (⇑f) (f.linearDeriv x) x
<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>n : ℕ<VAR>e : Fin (n + 1) ↪ ι<VAR>k : ι<VAR>h'k : k ∈ Set.range ⇑((Equiv.embeddingFinSucc n ι) e).fst<VAR>hk : k ∈ Set.range ⇑e<GOAL>(((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨k, h'k⟩).succ = e.toEquivRange.symm ⟨k, hk⟩
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<GOAL>HasFTaylorSeriesUpTo ⊤ ⇑f fun v n => f.iteratedFDeriv n v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ<GOAL>iteratedFDeriv 𝕜 n ⇑f = f.iteratedFDeriv n
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ<VAR>x : (i : ι) → E i<GOAL>‖iteratedFDeriv 𝕜 n (⇑f) x‖ ≤ ↑((Fintype.card ι).descFactorial n) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : (i : ι) → E i<GOAL>CPolynomialAt 𝕜 (⇑f) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<GOAL>CPolynomialOn 𝕜 ⇑f ⊤
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<GOAL>ContDiffAt 𝕜 n (⇑f) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>x : E<GOAL>((p.derivSeries n) fun x_1 => x) x = (n + 1) • (p (n + 1)) fun x_1 => x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>h : HasFPowerSeriesOnBall f p x r<GOAL>iteratedFDeriv 𝕜 0 f x = p 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>r : ℝ≥0∞<VAR>y : E<VAR>n : ℕ<VAR>F : Type (max u v)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<GOAL>HasFPowerSeriesOnBall f p x r → (n.factorial • (p n) fun x => y) = (iteratedFDeriv 𝕜 n f x) fun x => y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>CompleteSpace F<VAR>n : ℕ<GOAL>(n.factorial • (p n) fun x => y) = (iteratedFDeriv 𝕜 n f x) fun x => y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>CompleteSpace F<VAR>CharZero 𝕜<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 r<GOAL>HasSum (fun n => (↑n.factorial)⁻¹ • (iteratedFDeriv 𝕜 n f x) fun x => y) (f (x + y))
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>x : E<VAR>hf' : UniformCauchySeqOnFilter f' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : Cauchy (Filter.map (fun n => f n x) l)<GOAL>UniformCauchySeqOnFilter f l (𝓝 x)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>x : E<VAR>r : ℝ<VAR>hf' : UniformCauchySeqOn f' l (Metric.ball x r)<VAR>hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y<VAR>hfg : Cauchy (Filter.map (fun n => f n x) l)<GOAL>UniformCauchySeqOn f l (Metric.ball x r)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x ∈ s<VAR>hfg : Cauchy (Filter.map (fun n => f n x₀) l)<GOAL>Cauchy (Filter.map (fun n => f n x) l)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Filter.Tendsto (fun n => f n y) l (𝓝 (g y))<GOAL>TendstoUniformlyOnFilter (fun n y => (↑‖y - x‖)⁻¹ • (f n y - f n x)) (fun y => (↑‖y - x‖)⁻¹ • (g y - g x)) l (𝓝 x)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Filter.Tendsto (fun n => f n y) l (𝓝 (g y))<GOAL>HasFDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>l.NeBot<VAR>s : Set E<VAR>hs : IsOpen s<VAR>hf' : TendstoLocallyUniformlyOn f' g' l s<VAR>hf : ∀ (n : ι), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x<VAR>hfg : ∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hx : x ∈ s<GOAL>HasFDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>l.NeBot<VAR>s : Set E<VAR>hs : IsOpen s<VAR>hf' : TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s<VAR>hf : ∀ (n : ι), DifferentiableOn 𝕜 (f n) s<VAR>hfg : ∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hx : x ∈ s<GOAL>HasFDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>l.NeBot<VAR>s : Set E<VAR>hs : IsOpen s<VAR>hf' : TendstoUniformlyOn f' g' l s<VAR>hf : ∀ (n : ι), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x<VAR>hfg : ∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>x : E<GOAL>x ∈ s → HasFDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>l.NeBot<VAR>hf' : TendstoUniformly f' g' l<VAR>hf : ∀ (n : ι) (x : E), HasFDerivAt (f n) (f' n x) x<VAR>hfg : ∀ (x : E), Filter.Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>x : E<GOAL>HasFDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f' : ι → 𝕜 → G<VAR>l' : Filter 𝕜<VAR>hf' : UniformCauchySeqOnFilter f' l l'<GOAL>UniformCauchySeqOnFilter (fun n z => ContinuousLinearMap.smulRight 1 (f' n z)) l l'
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f f' : ι → 𝕜 → G<VAR>x : 𝕜<VAR>hf' : UniformCauchySeqOnFilter f' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : Cauchy (Filter.map (fun n => f n x) l)<GOAL>UniformCauchySeqOnFilter f l (𝓝 x)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f f' : ι → 𝕜 → G<VAR>x : 𝕜<VAR>r : ℝ<VAR>hf' : UniformCauchySeqOn f' l (Metric.ball x r)<VAR>hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasDerivAt (f n) (f' n y) y<VAR>hfg : Cauchy (Filter.map (fun n => f n x) l)<GOAL>UniformCauchySeqOn f l (Metric.ball x r)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Filter.Tendsto (fun n => f n y) l (𝓝 (g y))<GOAL>HasDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l.NeBot<VAR>s : Set 𝕜<VAR>hs : IsOpen s<VAR>hf' : TendstoLocallyUniformlyOn f' g' l s<VAR>hf : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x<VAR>hfg : ∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hx : x ∈ s<GOAL>HasDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g g' : 𝕜 → G<VAR>x : 𝕜<VAR>l.NeBot<VAR>s : Set 𝕜<VAR>hs : IsOpen s<VAR>hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s<VAR>hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s<VAR>hfg : ∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hx : x ∈ s<GOAL>HasDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>l.NeBot<VAR>s : Set 𝕜<VAR>hs : IsOpen s<VAR>hf' : TendstoUniformlyOn f' g' l s<VAR>hf : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x<VAR>hfg : ∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>x : 𝕜<GOAL>x ∈ s → HasDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>l.NeBot<VAR>hf' : TendstoUniformly f' g' l<VAR>hf : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x<VAR>hfg : ∀ (x : 𝕜), Filter.Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>x : 𝕜<GOAL>HasDerivAt g (g' x) x
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>X : Condensed A<GOAL>CategoryTheory.regularTopology.EqualizerCondition X.val
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Profinite) A<GOAL>CategoryTheory.regularTopology.EqualizerCondition X.val
<VAR>e : ℂ → ℂ<VAR>z : ℝ<VAR>n : ℕ∞<VAR>h : ContDiffAt ℂ n e ↑z<GOAL>ContDiffAt ℝ n (fun x => (e ↑x).re) z
<VAR>e : ℂ → ℂ<VAR>n : ℕ∞<VAR>h : ContDiff ℂ n e<GOAL>ContDiff ℝ n fun x => (e ↑x).re
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>x : ℂ<VAR>f' : E<VAR>h : HasStrictDerivAt f f' x<GOAL>HasStrictFDerivAt f (Complex.reCLM.smulRight f' + Complex.I • Complex.imCLM.smulRight f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>x : ℂ<VAR>f' : E<VAR>h : HasDerivAt f f' x<GOAL>HasFDerivAt f (Complex.reCLM.smulRight f' + Complex.I • Complex.imCLM.smulRight f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>x : ℂ<VAR>f' : E<VAR>h : HasDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt f (Complex.reCLM.smulRight f' + Complex.I • Complex.imCLM.smulRight f') s x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>h : HasStrictDerivAt f f' x<GOAL>HasStrictFDerivAt f (f' • 1) x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>h : HasDerivAt f f' x<GOAL>HasFDerivAt f (f' • 1) x
<VAR>f : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' x : ℂ<VAR>h : HasDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt f (f' • 1) s x
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>hf : HasDerivAt e e' ↑z<GOAL>HasDerivAt (fun y => e ↑y) e' z
<VAR>z : ℝ<VAR>f : ℝ → ℝ<VAR>u : ℝ<VAR>hf : HasDerivAt f u z<GOAL>HasDerivAt (fun y => ↑(f y)) (↑u) z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>z : ℂ<VAR>f : ℂ → E<VAR>h : DifferentiableAt ℂ f z<VAR>hf' : deriv f z ≠ 0<GOAL>ConformalAt f z
<VAR>f : ℂ → ℂ<VAR>z : ℂ<GOAL>ConformalAt f z ↔ (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0