ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ᶠ (x : ℝ) in Filter.atTop, HasDerivAt f (f' x) x<VAR>hgg' : ∀ᶠ (x : ℝ) in Filter.atTop, HasDerivAt g (g' x) x<VAR>hg' : ∀ᶠ (x : ℝ) in Filter.atTop, g' x ≠ 0<VAR>hftop : Filter.Tendsto f Filter.atTop (𝓝 0)<VAR>hgtop : Filter.Tendsto g Filter.atTop (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => f' x / g' x) Filter.atTop l<GOAL>Filter.Tendsto (fun x => f x / g x) Filter.atTop l
<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ᶠ (x : ℝ) in Filter.atBot, HasDerivAt f (f' x) x<VAR>hgg' : ∀ᶠ (x : ℝ) in Filter.atBot, HasDerivAt g (g' x) x<VAR>hg' : ∀ᶠ (x : ℝ) in Filter.atBot, g' x ≠ 0<VAR>hfbot : Filter.Tendsto f Filter.atBot (𝓝 0)<VAR>hgbot : Filter.Tendsto g Filter.atBot (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => f' x / g' x) Filter.atBot l<GOAL>Filter.Tendsto (fun x => f x / g x) Filter.atBot l
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>f g : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in 𝓝[>] a, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, deriv g x ≠ 0<VAR>hfa : Filter.Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Filter.Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>f g : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0<VAR>hfa : Filter.Tendsto f (𝓝[<] a) (𝓝 0)<VAR>hga : Filter.Tendsto g (𝓝[<] a) (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] a) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[<] a) l
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>f g : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in 𝓝[≠] a, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, deriv g x ≠ 0<VAR>hfa : Filter.Tendsto f (𝓝[≠] a) (𝓝 0)<VAR>hga : Filter.Tendsto g (𝓝[≠] a) (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) (𝓝[≠] a) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[≠] a) l
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>f g : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0<VAR>hfa : Filter.Tendsto f (𝓝 a) (𝓝 0)<VAR>hga : Filter.Tendsto g (𝓝 a) (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) (𝓝 a) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[≠] a) l
<VAR>l : Filter ℝ<VAR>f g : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in Filter.atTop, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in Filter.atTop, deriv g x ≠ 0<VAR>hftop : Filter.Tendsto f Filter.atTop (𝓝 0)<VAR>hgtop : Filter.Tendsto g Filter.atTop (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) Filter.atTop l<GOAL>Filter.Tendsto (fun x => f x / g x) Filter.atTop l
<VAR>l : Filter ℝ<VAR>f g : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in Filter.atBot, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in Filter.atBot, deriv g x ≠ 0<VAR>hfbot : Filter.Tendsto f Filter.atBot (𝓝 0)<VAR>hgbot : Filter.Tendsto g Filter.atBot (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) Filter.atBot l<GOAL>Filter.Tendsto (fun x => f x / g x) Filter.atBot l
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>x : E<VAR>hs : s ∈ 𝓝 x<GOAL>∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ Set.range f ⊆ Set.Icc 0 1 ∧ f x = 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>∃ f, Function.support f = s ∧ ContDiff ℝ ⊤ f ∧ Set.range f ⊆ Set.Icc 0 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<GOAL>∃ u, ContDiff ℝ ⊤ u ∧ (∀ (x : E), u x ∈ Set.Icc 0 1) ∧ Function.support u = Metric.ball 0 1 ∧ ∀ (x : E), u (-x) = u x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<GOAL>ContDiff ℝ ⊤ ExistsContDiffBumpBase.u
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<GOAL>Continuous ExistsContDiffBumpBase.u
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<GOAL>Function.support ExistsContDiffBumpBase.u = Metric.ball 0 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<GOAL>HasCompactSupport ExistsContDiffBumpBase.u
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<GOAL>0 ≤ ExistsContDiffBumpBase.u x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<GOAL>ExistsContDiffBumpBase.u x ≤ 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<GOAL>ExistsContDiffBumpBase.u (-x) = ExistsContDiffBumpBase.u x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<GOAL>0 < ∫ (x : E), ExistsContDiffBumpBase.u x ∂MeasureTheory.Measure.addHaar
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<GOAL>ExistsContDiffBumpBase.w D = fun x => ((∫ (x : E), ExistsContDiffBumpBase.u x ∂MeasureTheory.Measure.addHaar) * |D| ^ FiniteDimensional.finrank ℝ E)⁻¹ • ExistsContDiffBumpBase.u (D⁻¹ • x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<VAR>x : E<GOAL>0 ≤ ExistsContDiffBumpBase.w D x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<VAR>x y : E<GOAL>0 ≤ ExistsContDiffBumpBase.w D y * ExistsContDiffBumpBase.φ (x - y)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<VAR>Dpos : 0 < D<GOAL>∫ (x : E), ExistsContDiffBumpBase.w D x ∂MeasureTheory.Measure.addHaar = 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<VAR>Dpos : 0 < D<GOAL>Function.support (ExistsContDiffBumpBase.w D) = Metric.ball 0 D
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<VAR>Dpos : 0 < D<GOAL>HasCompactSupport (ExistsContDiffBumpBase.w D)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<VAR>x : E<GOAL>ExistsContDiffBumpBase.y D (-x) = ExistsContDiffBumpBase.y D x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>hx : x ∈ Metric.closedBall 0 (1 - D)<GOAL>ExistsContDiffBumpBase.y D x = 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>hx : x ∉ Metric.ball 0 (1 + D)<GOAL>ExistsContDiffBumpBase.y D x = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<VAR>x : E<GOAL>0 ≤ ExistsContDiffBumpBase.y D x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<GOAL>ExistsContDiffBumpBase.y D x ≤ 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>D_lt_one : D < 1<VAR>hx : x ∈ Metric.ball 0 (1 + D)<GOAL>0 < ExistsContDiffBumpBase.y D x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<GOAL>ContDiffOn ℝ ⊤ (Function.uncurry ExistsContDiffBumpBase.y) (Set.Ioo 0 1 ×ˢ Set.univ)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>D : ℝ<VAR>Dpos : 0 < D<VAR>D_lt_one : D < 1<GOAL>Function.support (ExistsContDiffBumpBase.y D) = Metric.ball 0 (1 + D)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>hf : ContDiffOn 𝕜 (↑n) f s<VAR>hg : ContDiffOn 𝕜 (↑n) g s<GOAL>iteratedDerivWithin n (f + g) s x = iteratedDerivWithin n f s x + iteratedDerivWithin n g s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>s : Set 𝕜<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>hfg : Set.EqOn f g s<GOAL>Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f : 𝕜 → F<VAR>hn : 0 < n<VAR>c : F<GOAL>iteratedDerivWithin n (fun z => c + f z) s x = iteratedDerivWithin n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f : 𝕜 → F<VAR>hn : 0 < n<VAR>c : F<GOAL>iteratedDerivWithin n (fun z => c - f z) s x = iteratedDerivWithin n (fun z => -f z) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f : 𝕜 → F<VAR>c : R<VAR>hf : ContDiffOn 𝕜 (↑n) f s<GOAL>iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>c : 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ContDiffOn 𝕜 (↑n) f s<GOAL>iteratedDerivWithin n (fun z => c * f z) s x = c * iteratedDerivWithin n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f : 𝕜 → F<GOAL>iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f : 𝕜 → F<GOAL>iteratedDerivWithin n (fun z => -f z) s x = -iteratedDerivWithin n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>hf : ContDiffOn 𝕜 (↑n) f s<VAR>hg : ContDiffOn 𝕜 (↑n) g s<GOAL>iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>h : ContDiff 𝕜 (↑n) f<VAR>c : 𝕜<GOAL>(iteratedDeriv n fun x => f (c * x)) = fun x => c ^ n • iteratedDeriv n f (c * x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ<VAR>f : 𝕜 → 𝕜<VAR>h : ContDiff 𝕜 (↑n) f<VAR>c : 𝕜<GOAL>(iteratedDeriv n fun x => f (c * x)) = fun x => c ^ n * iteratedDeriv n f (c * x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>a : 𝕜<GOAL>iteratedDeriv n (fun x => -f x) a = -iteratedDeriv n f a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>a : 𝕜<GOAL>iteratedDeriv n (fun x => f (-x)) a = (-1) ^ n • iteratedDeriv n f (-a)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<GOAL>logDeriv f x = deriv f x / f x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>h : ¬DifferentiableAt 𝕜 f x<GOAL>logDeriv f x = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>logDeriv id x = 1 / x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>logDeriv (fun x => x) x = 1 / x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>a : 𝕜'<GOAL>(logDeriv fun x => a) = 0
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>f g : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hf : f x ≠ 0<VAR>hg : g x ≠ 0<VAR>hdf : DifferentiableAt 𝕜 f x<VAR>hdg : DifferentiableAt 𝕜 g x<GOAL>logDeriv (fun z => f z * g z) x = logDeriv f x + logDeriv g x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>a : 𝕜'<VAR>ha : a ≠ 0<GOAL>logDeriv (fun z => f z * a) x = logDeriv f x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>a : 𝕜'<VAR>ha : a ≠ 0<GOAL>logDeriv (fun z => a * f z) x = logDeriv f x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hf : ∀ i ∈ s, f i x ≠ 0<VAR>hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x<GOAL>logDeriv (fun x => ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hdf : DifferentiableAt 𝕜 f x<VAR>n : ℤ<GOAL>logDeriv (fun x => f x ^ n) x = ↑n * logDeriv f x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hdf : DifferentiableAt 𝕜 f x<VAR>n : ℕ<GOAL>logDeriv (fun x => f x ^ n) x = ↑n * logDeriv f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>n : ℤ<GOAL>logDeriv (fun x => x ^ n) x = ↑n / x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>n : ℕ<GOAL>logDeriv (fun x => x ^ n) x = ↑n / x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>logDeriv (fun x => x⁻¹) x = -1 / x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜' → 𝕜'<VAR>g : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hf : DifferentiableAt 𝕜' f (g x)<VAR>hg : DifferentiableAt 𝕜 g x<GOAL>logDeriv (f ∘ g) x = logDeriv f (g x) * deriv g x
<VAR>X : Type u_1<VAR>MetricSpace X<VAR>CompleteSpace X<VAR>x : X<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ϕ : X → ℝ<VAR>cont : Continuous ϕ<VAR>nonneg : ∀ (y : X), 0 ≤ ϕ y<GOAL>∃ ε' > 0, ∃ x', ε' ≤ ε ∧ d x' x ≤ 2 * ε ∧ ε * ϕ x ≤ ε' * ϕ x' ∧ ∀ (y : X), d x' y ≤ ε' → ϕ y ≤ 2 * ϕ 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₁ : E → F<VAR>f₁' : E →L[𝕜] F<VAR>x : E<VAR>f₂ : E → G<VAR>f₂' : E →L[𝕜] G<VAR>hf₁ : HasStrictFDerivAt f₁ f₁' x<VAR>hf₂ : HasStrictFDerivAt f₂ f₂' x<GOAL>HasStrictFDerivAt (fun x => (f₁ x, f₂ x)) (f₁'.prod 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₁ : E → F<VAR>f₁' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<VAR>f₂ : E → G<VAR>f₂' : E →L[𝕜] G<VAR>hf₁ : HasFDerivAtFilter f₁ f₁' x L<VAR>hf₂ : HasFDerivAtFilter f₂ f₂' x L<GOAL>HasFDerivAtFilter (fun x => (f₁ x, f₂ x)) (f₁'.prod f₂') x L
<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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₁ : E → F<VAR>f₁' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>f₂ : E → G<VAR>f₂' : E →L[𝕜] G<VAR>hf₁ : HasFDerivWithinAt f₁ f₁' s x<VAR>hf₂ : HasFDerivWithinAt f₂ f₂' s x<GOAL>HasFDerivWithinAt (fun x => (f₁ x, f₂ x)) (f₁'.prod f₂') s 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₁ : E → F<VAR>f₁' : E →L[𝕜] F<VAR>x : E<VAR>f₂ : E → G<VAR>f₂' : E →L[𝕜] G<VAR>hf₁ : HasFDerivAt f₁ f₁' x<VAR>hf₂ : HasFDerivAt f₂ f₂' x<GOAL>HasFDerivAt (fun x => (f₁ x, f₂ x)) (f₁'.prod 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>e₀ : E<VAR>f₀ : F<GOAL>HasFDerivAt (fun e => (e, f₀)) (ContinuousLinearMap.inl 𝕜 E F) e₀
<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>e₀ : E<VAR>f₀ : F<GOAL>HasFDerivAt (fun f => (e₀, f)) (ContinuousLinearMap.inr 𝕜 E F) 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₁ : E → F<VAR>x : E<VAR>s : Set E<VAR>f₂ : E → G<VAR>hf₁ : DifferentiableWithinAt 𝕜 f₁ s x<VAR>hf₂ : DifferentiableWithinAt 𝕜 f₂ s x<GOAL>DifferentiableWithinAt 𝕜 (fun x => (f₁ x, f₂ x)) s 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₁ : E → F<VAR>x : E<VAR>f₂ : E → G<VAR>hf₁ : DifferentiableAt 𝕜 f₁ x<VAR>hf₂ : DifferentiableAt 𝕜 f₂ x<GOAL>DifferentiableAt 𝕜 (fun x => (f₁ x, f₂ x)) 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₁ : E → F<VAR>s : Set E<VAR>f₂ : E → G<VAR>hf₁ : DifferentiableOn 𝕜 f₁ s<VAR>hf₂ : DifferentiableOn 𝕜 f₂ s<GOAL>DifferentiableOn 𝕜 (fun x => (f₁ x, f₂ x)) 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₁ : E → F<VAR>f₂ : E → G<VAR>hf₁ : Differentiable 𝕜 f₁<VAR>hf₂ : Differentiable 𝕜 f₂<GOAL>Differentiable 𝕜 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₁ : E → F<VAR>x : E<VAR>f₂ : E → G<VAR>hf₁ : DifferentiableAt 𝕜 f₁ x<VAR>hf₂ : DifferentiableAt 𝕜 f₂ x<GOAL>fderiv 𝕜 (fun x => (f₁ x, f₂ x)) x = (fderiv 𝕜 f₁ x).prod (fderiv 𝕜 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₁ : E → F<VAR>x : E<VAR>s : Set E<VAR>f₂ : E → G<VAR>hf₁ : DifferentiableWithinAt 𝕜 f₁ s x<VAR>hf₂ : DifferentiableWithinAt 𝕜 f₂ s x<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun x => (f₁ x, f₂ x)) s x = (fderivWithin 𝕜 f₁ s x).prod (fderivWithin 𝕜 f₂ s 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>p : E × F<GOAL>HasStrictFDerivAt Prod.fst (ContinuousLinearMap.fst 𝕜 E F) p
<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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>f₂ : E → F × G<VAR>f₂' : E →L[𝕜] F × G<VAR>h : HasStrictFDerivAt f₂ f₂' x<GOAL>HasStrictFDerivAt (fun x => (f₂ x).1) ((ContinuousLinearMap.fst 𝕜 F G).comp 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>p : E × F<VAR>L : Filter (E × F)<GOAL>HasFDerivAtFilter Prod.fst (ContinuousLinearMap.fst 𝕜 E F) p L
<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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>L : Filter E<VAR>f₂ : E → F × G<VAR>f₂' : E →L[𝕜] F × G<VAR>h : HasFDerivAtFilter f₂ f₂' x L<GOAL>HasFDerivAtFilter (fun x => (f₂ x).1) ((ContinuousLinearMap.fst 𝕜 F G).comp f₂') x L
<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>p : E × F<GOAL>HasFDerivAt Prod.fst (ContinuousLinearMap.fst 𝕜 E F) p
<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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>f₂ : E → F × G<VAR>f₂' : E →L[𝕜] F × G<VAR>h : HasFDerivAt f₂ f₂' x<GOAL>HasFDerivAt (fun x => (f₂ x).1) ((ContinuousLinearMap.fst 𝕜 F G).comp 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>p : E × F<VAR>s : Set (E × F)<GOAL>HasFDerivWithinAt Prod.fst (ContinuousLinearMap.fst 𝕜 E F) s p
<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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>s : Set E<VAR>f₂ : E → F × G<VAR>f₂' : E →L[𝕜] F × G<VAR>h : HasFDerivWithinAt f₂ f₂' s x<GOAL>HasFDerivWithinAt (fun x => (f₂ x).1) ((ContinuousLinearMap.fst 𝕜 F G).comp f₂') s 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>p : E × F<GOAL>DifferentiableAt 𝕜 Prod.fst p
<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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>f₂ : E → F × G<VAR>h : DifferentiableAt 𝕜 f₂ x<GOAL>DifferentiableAt 𝕜 (fun x => (f₂ x).1) 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<GOAL>Differentiable 𝕜 Prod.fst
<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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₂ : E → F × G<VAR>h : Differentiable 𝕜 f₂<GOAL>Differentiable 𝕜 fun x => (f₂ x).1
<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>p : E × F<VAR>s : Set (E × F)<GOAL>DifferentiableWithinAt 𝕜 Prod.fst s p
<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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>s : Set E<VAR>f₂ : E → F × G<VAR>h : DifferentiableWithinAt 𝕜 f₂ s x<GOAL>DifferentiableWithinAt 𝕜 (fun x => (f₂ x).1) s 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>s : Set (E × F)<GOAL>DifferentiableOn 𝕜 Prod.fst s