ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>z : ℂ<VAR>hz : Complex.abs (-z) < 1<GOAL>Complex.UnitDisc.mk (-z) hz = -Complex.UnitDisc.mk z ⋯
<VAR>z : Complex.UnitDisc<GOAL>↑z = 0 ↔ z = 0
<VAR>z : ↥circle<VAR>w : Complex.UnitDisc<GOAL>↑(z • w) = ↑z * ↑w
<VAR>z : ↑(Metric.closedBall 0 1)<VAR>w : Complex.UnitDisc<GOAL>↑(z • w) = ↑z * ↑w
<VAR>z : Complex.UnitDisc<GOAL>(↑z).re = z.re
<VAR>z : Complex.UnitDisc<GOAL>(↑z).im = z.im
<VAR>z : Complex.UnitDisc<GOAL>(-z).re = -z.re
<VAR>z : Complex.UnitDisc<GOAL>(-z).im = -z.im
<VAR>z : Complex.UnitDisc<GOAL>↑z.conj = conj' ↑z
<VAR>z : Complex.UnitDisc<GOAL>z.conj.conj = z
<VAR>z : Complex.UnitDisc<GOAL>(-z).conj = -z.conj
<VAR>z : Complex.UnitDisc<GOAL>z.conj.re = z.re
<VAR>z : Complex.UnitDisc<GOAL>z.conj.im = -z.im
<VAR>z w : Complex.UnitDisc<GOAL>(z * w).conj = z.conj * w.conj
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>l : Filter α<GOAL>(fun x => ↑(f x)) =Θ[l] f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>Norm E<VAR>l : Filter α<VAR>f : α → ℝ<VAR>g : α → E<GOAL>(fun x => ↑(f x)) =o[l] g ↔ f =o[l] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>Norm E<VAR>l : Filter α<VAR>f : α → E<VAR>g : α → ℝ<GOAL>(f =o[l] fun x => ↑(g x)) ↔ f =o[l] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>Norm E<VAR>l : Filter α<VAR>f : α → ℝ<VAR>g : α → E<GOAL>(fun x => ↑(f x)) =O[l] g ↔ f =O[l] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>Norm E<VAR>l : Filter α<VAR>f : α → E<VAR>g : α → ℝ<GOAL>(f =O[l] fun x => ↑(g x)) ↔ f =O[l] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>Norm E<VAR>l : Filter α<VAR>f : α → ℝ<VAR>g : α → E<GOAL>(fun x => ↑(f x)) =Θ[l] g ↔ f =Θ[l] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>Norm E<VAR>l : Filter α<VAR>f : α → E<VAR>g : α → ℝ<GOAL>(f =Θ[l] fun x => ↑(g x)) ↔ f =Θ[l] g
<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>CompleteSpace F<VAR>R : ℝ<VAR>c : ℂ<VAR>f : ℂ → F<VAR>hR : 0 < R<VAR>hf : DiffContOnCl ℂ f (Metric.ball c R)<GOAL>deriv f c = (2 * ↑π * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c) ^ (-2) • f z
<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>CompleteSpace F<VAR>c : ℂ<VAR>R C : ℝ<VAR>f : ℂ → F<VAR>hR : 0 < R<VAR>hf : DiffContOnCl ℂ f (Metric.ball c R)<VAR>hC : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C<GOAL>‖deriv f c‖ ≤ C / R
<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>c : ℂ<VAR>R C : ℝ<VAR>f : ℂ → F<VAR>hR : 0 < R<VAR>hd : DiffContOnCl ℂ f (Metric.ball c R)<VAR>hC : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C<GOAL>‖deriv f c‖ ≤ C / R
<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>f : ℂ → F<VAR>hf : Differentiable ℂ f<VAR>hb : Bornology.IsBounded (Set.range f)<VAR>z w : ℂ<GOAL>f z = f w
<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>hf : Differentiable ℂ f<VAR>hb : Bornology.IsBounded (Set.range f)<VAR>z w : E<GOAL>f z = f w
<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>hf : Differentiable ℂ f<VAR>hb : Bornology.IsBounded (Set.range f)<GOAL>∃ c, ∀ (z : E), f z = c
<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>hf : Differentiable ℂ f<VAR>hb : Bornology.IsBounded (Set.range f)<GOAL>∃ c, f = Function.const E c
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>Nontrivial E<VAR>f : E → F<VAR>hf : Differentiable ℂ f<VAR>c : F<VAR>hb : Filter.Tendsto f (Filter.cocompact E) (𝓝 c)<GOAL>f = Function.const E c
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>Nontrivial E<VAR>f : E → F<VAR>hf : Differentiable ℂ f<VAR>c : F<VAR>x : E<VAR>hb : Filter.Tendsto f (Filter.cocompact E) (𝓝 c)<GOAL>f x = c
<GOAL>IsHomeomorphicTrivialFiberBundle ℝ Complex.re
<GOAL>IsHomeomorphicTrivialFiberBundle ℝ Complex.im
<VAR>s : Set ℝ<GOAL>interior (Complex.re ⁻¹' s) = Complex.re ⁻¹' interior s
<VAR>s : Set ℝ<GOAL>interior (Complex.im ⁻¹' s) = Complex.im ⁻¹' interior s
<VAR>s : Set ℝ<GOAL>closure (Complex.re ⁻¹' s) = Complex.re ⁻¹' closure s
<VAR>s : Set ℝ<GOAL>closure (Complex.im ⁻¹' s) = Complex.im ⁻¹' closure s
<VAR>s : Set ℝ<GOAL>frontier (Complex.re ⁻¹' s) = Complex.re ⁻¹' frontier s
<VAR>s : Set ℝ<GOAL>frontier (Complex.im ⁻¹' s) = Complex.im ⁻¹' frontier s
<VAR>a : ℝ<GOAL>frontier {z | z.re ≤ a} = {z | z.re = a}
<VAR>s t : Set ℝ<VAR>hs : IsOpen s<VAR>ht : IsOpen t<GOAL>IsOpen (s ×ℂ t)
<VAR>s t : Set ℝ<VAR>hs : IsClosed s<VAR>ht : IsClosed t<GOAL>IsClosed (s ×ℂ t)
<VAR>s t : Set ℝ<VAR>hs : Bornology.IsBounded s<VAR>ht : Bornology.IsBounded t<GOAL>Bornology.IsBounded (s ×ℂ t)
<VAR>x : EReal<GOAL>IsOpen {z | ↑z.re < x}
<VAR>x : EReal<GOAL>IsOpen {z | x < ↑z.re}
<VAR>x : EReal<GOAL>IsOpen {z | ↑z.im < x}
<VAR>x : EReal<GOAL>IsOpen {z | x < ↑z.im}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>c : ℝ≥0<GOAL>ApproximatesLinearOn f f' ∅ c
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>s : Set E<VAR>c c' : ℝ≥0<VAR>hc : c ≤ c'<VAR>hf : ApproximatesLinearOn f f' s c<GOAL>ApproximatesLinearOn f f' s c'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>s t : Set E<VAR>c : ℝ≥0<VAR>hst : s ⊆ t<VAR>hf : ApproximatesLinearOn f f' t c<GOAL>ApproximatesLinearOn f f' s c
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<GOAL>ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ⇑f') s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f f' s c<GOAL>LipschitzWith c fun x => f ↑x - f' ↑x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f f' s c<GOAL>LipschitzWith (‖f'‖₊ + c) (s.restrict f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f f' s c<GOAL>Continuous (s.restrict f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f f' s c<GOAL>ContinuousOn f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : Metric.closedBall b ε ⊆ s<GOAL>Set.SurjOn f (Metric.closedBall b ε) (Metric.closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>hs : IsOpen s<VAR>hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹<GOAL>IsOpen (f '' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹<GOAL>f '' s ∈ 𝓝 (f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹<GOAL>Filter.map f (𝓝 x) = 𝓝 (f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<GOAL>AntilipschitzWith (‖↑f'.symm‖₊⁻¹ - c)⁻¹ (s.restrict f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<GOAL>Function.Injective (s.restrict f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<GOAL>Set.InjOn f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>c : ℝ≥0<VAR>CompleteSpace E<VAR>hf : ApproximatesLinearOn f (↑f') Set.univ c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<GOAL>Function.Surjective f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<GOAL>ContinuousOn (↑(hf.toPartialEquiv hc).symm) (f '' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<GOAL>ApproximatesLinearOn (↑(hf.toPartialEquiv hc).symm) (↑f'.symm) (f '' s) (‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<VAR>hs : IsOpen s<GOAL>↑(ApproximatesLinearOn.toPartialHomeomorph f s hf hc hs) = f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<VAR>hs : IsOpen s<GOAL>(ApproximatesLinearOn.toPartialHomeomorph f s hf hc hs).source = s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<VAR>hs : IsOpen s<GOAL>(ApproximatesLinearOn.toPartialHomeomorph f s hf hc hs).target = f '' s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ε : ℝ<VAR>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<VAR>hs : IsOpen s<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : Metric.closedBall b ε ⊆ s<GOAL>Metric.closedBall (f b) ((↑‖↑f'.symm‖₊⁻¹ - ↑c) * ε) ⊆ (ApproximatesLinearOn.toPartialHomeomorph f s hf hc hs).target
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>x : ℝ<GOAL>0 ≤ Complex.HadamardThreeLines.sSupNormIm f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>x : ℝ<GOAL>0 < ε + Complex.HadamardThreeLines.sSupNormIm f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>Complex.abs (Complex.HadamardThreeLines.invInterpStrip f z ε) = (ε + Complex.HadamardThreeLines.sSupNormIm f 0) ^ (z.re - 1) * (ε + Complex.HadamardThreeLines.sSupNormIm f 1) ^ (-z.re)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>DiffContOnCl ℂ (fun z => Complex.HadamardThreeLines.invInterpStrip f z ε) (Complex.HadamardThreeLines.verticalStrip 0 1)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hD : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1<VAR>hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)<GOAL>‖f z‖ ≤ Complex.HadamardThreeLines.sSupNormIm f z.re
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>z : ℂ<VAR>hD : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1<VAR>hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)<GOAL>‖f z‖ < ε + Complex.HadamardThreeLines.sSupNormIm f z.re
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)<GOAL>BddAbove (norm ∘ Complex.HadamardThreeLines.F f ε '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>z : ℂ<VAR>hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)<VAR>hz : z ∈ Complex.re ⁻¹' {0, 1}<GOAL>‖Complex.HadamardThreeLines.F f ε z‖ ≤ 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)<VAR>hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1<GOAL>‖Complex.HadamardThreeLines.F f ε z‖ ≤ 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>h0 : 0 < Complex.HadamardThreeLines.sSupNormIm f 0<VAR>h1 : 0 < Complex.HadamardThreeLines.sSupNormIm f 1<GOAL>Complex.HadamardThreeLines.interpStrip f z = ↑(Complex.HadamardThreeLines.sSupNormIm f 0) ^ (1 - z) * ↑(Complex.HadamardThreeLines.sSupNormIm f 1) ^ z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>h : Complex.HadamardThreeLines.sSupNormIm f 0 = 0 ∨ Complex.HadamardThreeLines.sSupNormIm f 1 = 0<GOAL>Complex.HadamardThreeLines.interpStrip f z = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hz : z ∈ Complex.HadamardThreeLines.verticalStrip 0 1<GOAL>Complex.HadamardThreeLines.interpStrip f z = ↑(Complex.HadamardThreeLines.sSupNormIm f 0) ^ (1 - z) * ↑(Complex.HadamardThreeLines.sSupNormIm f 1) ^ z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<GOAL>DiffContOnCl ℂ (Complex.HadamardThreeLines.interpStrip f) (Complex.HadamardThreeLines.verticalStrip 0 1)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>z : ℂ<VAR>hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)<VAR>hd : DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1)<VAR>hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1<GOAL>‖f z‖ ≤ ‖(↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 1)) ^ z‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)<VAR>hd : DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1)<VAR>hz : z ∈ Complex.HadamardThreeLines.verticalStrip 0 1<GOAL>(fun x => ‖f z‖) ≤ᶠ[𝓝[>] 0] fun ε => ‖(↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 1)) ^ z‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)<VAR>hz : z ∈ Complex.HadamardThreeLines.verticalStrip 0 1<GOAL>‖f z‖ ≤ ‖Complex.HadamardThreeLines.interpStrip f z‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1<VAR>hd : DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)<GOAL>‖f z‖ ≤ ‖Complex.HadamardThreeLines.interpStrip f z‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>a b : ℝ<VAR>hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1<VAR>hd : DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)<VAR>ha : ∀ z ∈ Complex.re ⁻¹' {0}, ‖f z‖ ≤ a<VAR>hb : ∀ z ∈ Complex.re ⁻¹' {1}, ‖f z‖ ≤ b<GOAL>‖f z‖ ≤ a ^ (1 - z.re) * b ^ z.re
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>n : ℕ<GOAL>0 n = 0
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>f : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>(-f) n = -f n
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p q : FormalMultilinearSeries 𝕜 E F<VAR>h : ∀ (n : ℕ), p n = q n<GOAL>p = q
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p q : FormalMultilinearSeries 𝕜 E F<GOAL>p = q ↔ ∀ (n : ℕ), p n = q n
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p q : FormalMultilinearSeries 𝕜 E F<GOAL>p ≠ q ↔ ∃ n, p n ≠ q n
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<GOAL>p.removeZero 0 = 0
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>p.removeZero (n + 1) = p (n + 1)
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>h : 0 < n<GOAL>p.removeZero n = p n
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>m n : ℕ<VAR>v : Fin m → E<VAR>w : Fin n → E<VAR>h1 : m = n<VAR>h2 : ∀ (i : ℕ) (him : i < m) (hin : i < n), v ⟨i, him⟩ = w ⟨i, hin⟩<GOAL>(p m) v = (p n) w
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>AddCommGroup G<VAR>Module 𝕜 G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 F G<VAR>u : E →L[𝕜] F<VAR>n : ℕ<VAR>v : Fin n → E<GOAL>(p.compContinuousLinearMap u n) v = (p n) (⇑u ∘ v)
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>AddCommGroup G<VAR>Module 𝕜 G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>ContinuousConstSMul 𝕜 G<VAR>f : F →L[𝕜] G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>f.compFormalMultilinearSeries p n = f.compContinuousMultilinearMap (p n)
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>AddCommGroup G<VAR>Module 𝕜 G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>ContinuousConstSMul 𝕜 G<VAR>f : F →L[𝕜] G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>v : Fin n → E<GOAL>(f.compFormalMultilinearSeries p n) v = f ((p n) v)
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<GOAL>FormalMultilinearSeries.order 0 = 0
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hp : p.order ≠ 0<GOAL>p ≠ 0