ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>Fintype ι<VAR>v : Basis ι 𝕜 E<VAR>u : E →L[𝕜] F<VAR>M : ℝ≥0<VAR>hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M<GOAL>‖u‖₊ ≤ Fintype.card ι • ‖↑v.equivFunL‖₊ * M
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>Fintype ι<VAR>v : Basis ι 𝕜 E<VAR>u : E →L[𝕜] F<VAR>M : ℝ<VAR>hM : 0 ≤ M<VAR>hu : ∀ (i : ι), ‖u (v i)‖ ≤ M<GOAL>‖u‖ ≤ Fintype.card ι • ‖↑v.equivFunL‖ * M
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>Finite ι<VAR>v : Basis ι 𝕜 E<GOAL>∃ C > 0, ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>Finite ι<VAR>v : Basis ι 𝕜 E<GOAL>∃ C > 0, ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ (i : ι), ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>P : Type u_1<VAR>MetricSpace P<VAR>NormedAddTorsor E P<VAR>s : AffineSubspace 𝕜 P<VAR>FiniteDimensional 𝕜 ↥s.direction<GOAL>IsClosed ↑s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>s : Finset E<GOAL>∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>h : ¬FiniteDimensional 𝕜 E<GOAL>∃ f, (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>h : ¬FiniteDimensional 𝕜 E<GOAL>∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>r : ℝ<VAR>rpos : 0 < r<VAR>h : IsCompact (Metric.closedBall 0 r)<GOAL>FiniteDimensional 𝕜 E
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>r : ℝ<VAR>rpos : 0 < r<VAR>c : E<VAR>h : IsCompact (Metric.closedBall c r)<GOAL>FiniteDimensional 𝕜 E
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>LocallyCompactSpace E<GOAL>FiniteDimensional 𝕜 E
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Zero X<VAR>T1Space X<VAR>f : E → X<VAR>hf : HasCompactSupport f<VAR>h'f : Continuous f<GOAL>f = 0 ∨ FiniteDimensional 𝕜 E
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>One X<VAR>T1Space X<VAR>f : E → X<VAR>hf : HasCompactMulSupport f<VAR>h'f : Continuous f<GOAL>f = 1 ∨ FiniteDimensional 𝕜 E
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>LocallyCompactSpace E<GOAL>ProperSpace E
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>Nontrivial E<VAR>LocallyCompactSpace E<GOAL>ProperSpace 𝕜
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>FiniteDimensional 𝕜 E<VAR>f : X → E →L[𝕜] F<VAR>s : Set X<GOAL>ContinuousOn f s ↔ ∀ (y : E), ContinuousOn (fun x => (f x) y) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>FiniteDimensional 𝕜 E<VAR>f : X → E →L[𝕜] F<GOAL>Continuous f ↔ ∀ (y : E), Continuous fun x => (f x) y
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>LocallyCompactSpace 𝕜<VAR>FiniteDimensional 𝕜 E<GOAL>ProperSpace E
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>s : Set E<VAR>hx : x ∈ s<VAR>hs : s ≠ Set.univ<GOAL>∃ y ∈ frontier s, Metric.infDist x sᶜ = dist x y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Nontrivial E<VAR>x : E<VAR>K : Set E<VAR>hK : IsCompact K<VAR>hx : x ∈ K<GOAL>∃ y ∈ frontier K, Metric.infDist x Kᶜ = dist x y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>f : α → E<GOAL>(Summable fun x => ‖f x‖) ↔ Summable f
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>f : ι → E<VAR>g : ι → F<VAR>hg : Summable g<VAR>h : f =O[Filter.cofinite] g<GOAL>Summable f
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>f : E → F<VAR>hf : f =O[𝓝 0] id<VAR>g : ι → E<VAR>hg : Summable g<GOAL>Summable (f ∘ g)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>f : ℕ → E<VAR>g : ℕ → F<VAR>hg : Summable g<VAR>h : f =O[Filter.atTop] g<GOAL>Summable f
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>f g : ι → E<VAR>hg : Summable g<VAR>h : f ~[Filter.cofinite] g<GOAL>Summable f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>f g : ℕ → E<VAR>hg : Summable g<VAR>h : f ~[Filter.atTop] g<GOAL>Summable f
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>f g : ι → E<VAR>h : f ~[Filter.cofinite] g<GOAL>Summable f ↔ Summable g
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>f g : ℕ → E<VAR>h : f ~[Filter.atTop] g<GOAL>Summable f ↔ Summable g
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : ∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x<VAR>m : ℝ<VAR>hma : f' a < m<VAR>hmb : m < f' b<GOAL>m ∈ f' '' Set.Ioo a b
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : ∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x<VAR>m : ℝ<VAR>hma : m < f' a<VAR>hmb : f' b < m<GOAL>m ∈ f' '' Set.Ioo a b
<VAR>f f' : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : s.OrdConnected<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<GOAL>(f' '' s).OrdConnected
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : s.OrdConnected<VAR>hf : DifferentiableOn ℝ f s<GOAL>(derivWithin f s '' s).OrdConnected
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : s.OrdConnected<VAR>hf : ∀ x ∈ s, DifferentiableAt ℝ f x<GOAL>(deriv f '' s).OrdConnected
<VAR>f f' : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : Convex ℝ s<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<GOAL>Convex ℝ (f' '' s)
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : Convex ℝ s<VAR>hf : DifferentiableOn ℝ f s<GOAL>Convex ℝ (derivWithin f s '' s)
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : Convex ℝ s<VAR>hf : ∀ x ∈ s, DifferentiableAt ℝ f x<GOAL>Convex ℝ (deriv f '' s)
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : ∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x<VAR>m : ℝ<VAR>hma : f' a ≤ m<VAR>hmb : m ≤ f' b<GOAL>m ∈ f' '' Set.Icc a b
<VAR>f f' : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : Convex ℝ s<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>m : ℝ<VAR>hf' : ∀ x ∈ s, f' x ≠ m<GOAL>(∀ x ∈ s, f' x < m) ∨ ∀ x ∈ s, m < f' x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<GOAL>Function.support (deriv f) ⊆ tsupport f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>hf : HasCompactSupport f<GOAL>HasCompactSupport (deriv f)
<VAR>a : Quaternion ℝ<GOAL>⟪a, a⟫_ℝ = Quaternion.normSq a
<VAR>a b : Quaternion ℝ<GOAL>⟪a, b⟫_ℝ = (a * star b).re
<VAR>a : Quaternion ℝ<GOAL>Quaternion.normSq a = ‖a‖ * ‖a‖
<VAR>a : ℝ<GOAL>‖↑a‖₊ = ‖a‖₊
<VAR>a : Quaternion ℝ<GOAL>‖star a‖ = ‖a‖
<VAR>a : Quaternion ℝ<GOAL>‖star a‖₊ = ‖a‖₊
<VAR>z : ℂ<GOAL>(↑z).re = z.re
<VAR>z : ℂ<GOAL>(↑z).imI = z.im
<VAR>z : ℂ<GOAL>(↑z).imJ = 0
<VAR>z : ℂ<GOAL>(↑z).imK = 0
<VAR>z w : ℂ<GOAL>↑(z + w) = ↑z + ↑w
<VAR>z w : ℂ<GOAL>↑(z * w) = ↑z * ↑w
<VAR>r : ℝ<VAR>z : ℂ<GOAL>r • ↑z = ↑r * ↑z
<VAR>r : ℝ<GOAL>↑↑r = ↑r
<GOAL>⇑Quaternion.ofComplex = Quaternion.coeComplex
<VAR>x : Quaternion ℝ<GOAL>‖(WithLp.equiv 2 (Fin 4 → ℝ)).symm ((Quaternion.equivTuple ℝ) x)‖ = ‖x‖
<VAR>a : Quaternion ℝ<GOAL>Quaternion.linearIsometryEquivTuple a = (WithLp.equiv 2 (Fin 4 → ℝ)).symm ![a.re, a.imI, a.imJ, a.imK]
<VAR>a : EuclideanSpace ℝ (Fin 4)<GOAL>Quaternion.linearIsometryEquivTuple.symm a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>r : ℝ<GOAL>HasSum (fun a => ↑(f a)) ↑r ↔ HasSum f r
<VAR>α : Type u_1<VAR>f : α → ℝ<GOAL>∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>f : 𝕜 → 𝕜<VAR>f' x : 𝕜<VAR>hf : HasStrictDerivAt f f' x<VAR>hf' : f' ≠ 0<GOAL>HasStrictFDerivAt f (↑((ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 f' hf'))) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>f : 𝕜 → 𝕜<VAR>f' x : 𝕜<VAR>hf : HasDerivAt f f' x<VAR>hf' : f' ≠ 0<GOAL>HasFDerivAt f (↑((ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 f' hf'))) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>f g : 𝕜 → 𝕜<VAR>f' a : 𝕜<VAR>hg : ContinuousAt g a<VAR>hf : HasStrictDerivAt f f' (g a)<VAR>hf' : f' ≠ 0<VAR>hfg : ∀ᶠ (y : 𝕜) in 𝓝 a, f (g y) = y<GOAL>HasStrictDerivAt g f'⁻¹ a
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>f : PartialHomeomorph 𝕜 𝕜<VAR>a f' : 𝕜<VAR>ha : a ∈ f.target<VAR>hf' : f' ≠ 0<VAR>htff' : HasStrictDerivAt (↑f) f' (↑f.symm a)<GOAL>HasStrictDerivAt (↑f.symm) f'⁻¹ a
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>f g : 𝕜 → 𝕜<VAR>f' a : 𝕜<VAR>hg : ContinuousAt g a<VAR>hf : HasDerivAt f f' (g a)<VAR>hf' : f' ≠ 0<VAR>hfg : ∀ᶠ (y : 𝕜) in 𝓝 a, f (g y) = y<GOAL>HasDerivAt g f'⁻¹ a
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>f : PartialHomeomorph 𝕜 𝕜<VAR>a f' : 𝕜<VAR>ha : a ∈ f.target<VAR>hf' : f' ≠ 0<VAR>htff' : HasDerivAt (↑f) f' (↑f.symm a)<GOAL>HasDerivAt (↑f.symm) f'⁻¹ a
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>h : HasDerivAt f f' x<VAR>hf' : f' ≠ 0<GOAL>∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>h : HasDerivAt f f' x<VAR>hf' : f' ≠ 0<GOAL>Filter.Tendsto f (𝓝[≠] x) (𝓝[≠] f x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>f g : 𝕜 → 𝕜<VAR>a : 𝕜<VAR>s t : Set 𝕜<VAR>ha : a ∈ s<VAR>hsu : UniqueDiffWithinAt 𝕜 s a<VAR>hf : HasDerivWithinAt f 0 t (g a)<VAR>hst : Set.MapsTo g s t<VAR>hfg : f ∘ g =ᶠ[𝓝[s] a] id<GOAL>¬DifferentiableWithinAt 𝕜 g s a
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>f g : 𝕜 → 𝕜<VAR>a : 𝕜<VAR>hf : HasDerivAt f 0 (g a)<VAR>hfg : f ∘ g =ᶠ[𝓝 a] id<GOAL>¬DifferentiableAt 𝕜 g a
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<VAR>E' : Type u_2<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕂 F'<VAR>s : Set E'<VAR>f : E' → F'<VAR>x : E'<VAR>p : E' → FormalMultilinearSeries 𝕂 E' F'<VAR>hf : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hs : s ∈ 𝓝 x<GOAL>HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕂 E' F') (p x 1)) x
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<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>x : E'<VAR>hf : ContDiffAt 𝕂 n f x<VAR>hf' : HasFDerivAt f f' x<VAR>hn : 1 ≤ n<GOAL>HasStrictFDerivAt f f' x
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕂 F'<VAR>f : 𝕂 → F'<VAR>f' : F'<VAR>x : 𝕂<VAR>hf : ContDiffAt 𝕂 n f x<VAR>hf' : HasDerivAt f f' x<VAR>hn : 1 ≤ n<GOAL>HasStrictDerivAt f f' x
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<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>x : E'<VAR>hf : ContDiffAt 𝕂 n f x<VAR>hn : 1 ≤ n<GOAL>HasStrictFDerivAt f (fderiv 𝕂 f x) x
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕂 F'<VAR>f : 𝕂 → F'<VAR>x : 𝕂<VAR>hf : ContDiffAt 𝕂 n f x<VAR>hn : 1 ≤ n<GOAL>HasStrictDerivAt f (deriv f x) x
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<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>x : E'<VAR>hf : ContDiff 𝕂 n f<VAR>hn : 1 ≤ n<GOAL>HasStrictFDerivAt f (fderiv 𝕂 f x) x
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕂 F'<VAR>f : 𝕂 → F'<VAR>x : 𝕂<VAR>hf : ContDiff 𝕂 n f<VAR>hn : 1 ≤ n<GOAL>HasStrictDerivAt f (deriv f x) x
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>s : Set E<VAR>x : E<VAR>hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)<VAR>hs : Convex ℝ s<VAR>K : ℝ≥0<VAR>hK : ‖p x 1‖₊ < K<GOAL>∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>s : Set E<VAR>x : E<VAR>hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)<VAR>hs : Convex ℝ s<GOAL>∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : ContDiffWithinAt ℝ 1 f s x<VAR>hs : Convex ℝ s<GOAL>∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<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>x : E'<VAR>hf : ContDiffAt 𝕂 1 f x<VAR>K : ℝ≥0<VAR>hK : ‖fderiv 𝕂 f x‖₊ < K<GOAL>∃ t ∈ 𝓝 x, LipschitzOnWith K f t
<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<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>x : E'<VAR>hf : ContDiffAt 𝕂 1 f x<GOAL>∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<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>hf : ContDiff 𝕂 1 f<GOAL>LocallyLipschitz f
<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<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>n : ℕ∞<VAR>hf : HasCompactSupport f<VAR>h'f : ContDiff 𝕂 n f<VAR>hn : 1 ≤ n<GOAL>∃ C, LipschitzWith C f
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_ne_zero : f ≠ 0<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<GOAL>f 1 ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>x : R<VAR>hx : IsUnit x<VAR>hfx : f x ≠ 0<VAR>n : ℕ<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<GOAL>f (x ^ n) ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<VAR>hx : f x = 0<VAR>y : R<GOAL>f (x * y) = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>f_zero : f 0 = 0<GOAL>seminormFromBounded' f 0 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<GOAL>0 ≤ c * f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<GOAL>BddAbove (Set.range fun y => f (x * y) / f y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<GOAL>seminormFromBounded' f x ≤ c * f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<GOAL>f x ≤ f 1 * seminormFromBounded' f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<GOAL>0 ≤ seminormFromBounded' f
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<GOAL>seminormFromBounded' f x = 0 ↔ f x = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>f_neg : ∀ (x : R), f (-x) = f x<VAR>x : R<GOAL>seminormFromBounded' f (-x) = seminormFromBounded' f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x y : R<GOAL>seminormFromBounded' f (x * y) ≤ seminormFromBounded' f x * seminormFromBounded' f y
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_ne_zero : f ≠ 0<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<GOAL>seminormFromBounded' f 1 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<GOAL>seminormFromBounded' f 1 ≤ 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>f_add : ∀ (a b : R), f (a + b) ≤ f a + f b<VAR>x y : R<GOAL>seminormFromBounded' f (x + y) ≤ seminormFromBounded' f x + seminormFromBounded' f y
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>hna : IsNonarchimedean f<GOAL>IsNonarchimedean (seminormFromBounded' f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<GOAL>seminormFromBounded' f x = f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>f_nonneg : 0 ≤ f<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) ≤ f x * f y<VAR>h_one : f 1 ≤ 1<GOAL>seminormFromBounded' f x = f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_ne_zero : f ≠ 0<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<GOAL>seminormFromBounded' f ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<GOAL>seminormFromBounded' f ⁻¹' {0} = f ⁻¹' {0}
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_zero : f 0 = 0<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>f_add : ∀ (a b : R), f (a + b) ≤ f a + f b<VAR>f_neg : ∀ (x : R), f (-x) = f x<GOAL>(∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0) ↔ f ⁻¹' {0} = {0}
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<VAR>y : R<GOAL>seminormFromBounded' f (x * y) = seminormFromBounded' f x * seminormFromBounded' f y
<VAR>x : ℝ<GOAL>x ∈ Set.univ → HasDerivWithinAt (rexp ∘ Neg.neg) (-rexp (-x)) Set.univ x
<GOAL>rexp ∘ Neg.neg '' Set.univ = Set.Ioi 0
<GOAL>Set.InjOn (rexp ∘ Neg.neg) Set.univ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>x : ℝ<VAR>s : ℂ<VAR>f : E<GOAL>rexp (-x) • cexp (-↑x) ^ (s - 1) • f = cexp (-s * ↑x) • f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<GOAL>mellin f s = 𝓕 (fun u => rexp (-s.re * u) • f (rexp (-u))) (s.im / (2 * π))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>σ : ℝ<VAR>f : ℂ → E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>mellinInv σ f x = ↑x ^ (-↑σ) • 𝓕⁻ (fun y => f (↑σ + 2 * ↑π * ↑y * Complex.I)) (-Real.log x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>σ : ℝ<VAR>f : ℝ → E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hf : MellinConvergent f ↑σ<VAR>hFf : Complex.VerticalIntegrable (mellin f) σ MeasureTheory.volume<VAR>hfx : ContinuousAt f x<GOAL>mellinInv σ (mellin f) x = f x
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>h : HasConstantSpeedOnWith f s l<GOAL>LocallyBoundedVariationOn f s
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>hs : s.Subsingleton<VAR>l : ℝ≥0<GOAL>HasConstantSpeedOnWith f s l
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<GOAL>HasConstantSpeedOnWith f s l ↔ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Set.Icc x y) = ENNReal.ofReal (↑l * (y - x))
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<GOAL>HasConstantSpeedOnWith f s l ↔ LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>t : Set ℝ<VAR>hfs : HasConstantSpeedOnWith f s l<VAR>hft : HasConstantSpeedOnWith f t l<VAR>x : ℝ<VAR>hs : IsGreatest s x<VAR>ht : IsLeast t x<GOAL>HasConstantSpeedOnWith f (s ∪ t) l
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>l : ℝ≥0<VAR>x y z : ℝ<VAR>hfs : HasConstantSpeedOnWith f (Set.Icc x y) l<VAR>hft : HasConstantSpeedOnWith f (Set.Icc y z) l<GOAL>HasConstantSpeedOnWith f (Set.Icc x z) l
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<GOAL>HasConstantSpeedOnWith f s 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l l' : ℝ≥0<VAR>hl' : l' ≠ 0<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ s<VAR>hfφ : HasConstantSpeedOnWith (f ∘ φ) s l<VAR>hf : HasConstantSpeedOnWith f (φ '' s) l'<VAR>x : ℝ<VAR>xs : x ∈ s<GOAL>Set.EqOn φ (fun y => ↑l / ↑l' * (y - x) + φ x) s
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s t : Set ℝ<VAR>x : ℝ<VAR>hfs : HasUnitSpeedOn f s<VAR>hft : HasUnitSpeedOn f t<VAR>hs : IsGreatest s x<VAR>ht : IsLeast t x<GOAL>HasUnitSpeedOn f (s ∪ t)
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>x y z : ℝ<VAR>hfs : HasUnitSpeedOn f (Set.Icc x y)<VAR>hft : HasUnitSpeedOn f (Set.Icc y z)<GOAL>HasUnitSpeedOn f (Set.Icc x z)
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ s<VAR>hfφ : HasUnitSpeedOn (f ∘ φ) s<VAR>hf : HasUnitSpeedOn f (φ '' s)<VAR>x : ℝ<VAR>xs : x ∈ s<GOAL>Set.EqOn φ (fun y => y - x + φ x) s
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s t : ℝ<VAR>hs : 0 ≤ s<VAR>ht : 0 ≤ t<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ (Set.Icc 0 s)<VAR>φst : φ '' Set.Icc 0 s = Set.Icc 0 t<VAR>hfφ : HasUnitSpeedOn (f ∘ φ) (Set.Icc 0 s)<VAR>hf : HasUnitSpeedOn f (Set.Icc 0 t)<GOAL>Set.EqOn φ id (Set.Icc 0 s)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<VAR>b : α<VAR>bs : b ∈ s<GOAL>edist (naturalParameterization f s a (variationOnFromTo f s a b)) (f b) = 0