ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>c : F<GOAL>deriv (fun x => c) x = 0
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>c : F<GOAL>(deriv fun x => c) = fun x => 0
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>c : F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => c) s x = 0
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>hL : L ≤ 𝓝 x<VAR>h : HasDerivAtFilter f f' x L<GOAL>Filter.Tendsto f L (𝓝 (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>s : Set 𝕜<VAR>h : HasDerivWithinAt f f' s x<GOAL>ContinuousWithinAt f s 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<GOAL>ContinuousAt f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set 𝕜<VAR>f f' : 𝕜 → F<VAR>hderiv : ∀ x ∈ s, HasDerivAt f (f' x) x<GOAL>ContinuousOn f s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x₀ : 𝕜<VAR>hf : HasDerivAt f f' x₀<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : 𝕜) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>‖f'‖ ≤ C
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x₀ : 𝕜<VAR>hf : HasDerivAt f f' x₀<VAR>s : Set 𝕜<VAR>hs : s ∈ 𝓝 x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzOnWith C f s<GOAL>‖f'‖ ≤ ↑C
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x₀ : 𝕜<VAR>hf : HasDerivAt f f' x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzWith C f<GOAL>‖f'‖ ≤ ↑C
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x₀ : 𝕜<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : 𝕜) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>‖deriv f x₀‖ ≤ C
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x₀ : 𝕜<VAR>s : Set 𝕜<VAR>hs : s ∈ 𝓝 x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzOnWith C f s<GOAL>‖deriv f x₀‖ ≤ ↑C
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x₀ : 𝕜<VAR>C : ℝ≥0<VAR>hlip : LipschitzWith C f<GOAL>‖deriv f x₀‖ ≤ ↑C
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : 𝕜 → F<VAR>f' g' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>hf : HasDerivAtFilter f f' x L<VAR>hg : HasDerivAtFilter g g' x L<GOAL>HasDerivAtFilter (fun y => f y + g y) (f' + g') x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : 𝕜 → F<VAR>f' g' : F<VAR>x : 𝕜<VAR>hf : HasStrictDerivAt f f' x<VAR>hg : HasStrictDerivAt g g' x<GOAL>HasStrictDerivAt (fun y => f y + g y) (f' + g') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : 𝕜 → F<VAR>f' g' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hf : HasDerivWithinAt f f' s x<VAR>hg : HasDerivWithinAt g g' s x<GOAL>HasDerivWithinAt (fun y => f y + g y) (f' + g') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : 𝕜 → F<VAR>f' g' : F<VAR>x : 𝕜<VAR>hf : HasDerivAt f f' x<VAR>hg : HasDerivAt g g' x<GOAL>HasDerivAt (fun x => f x + g x) (f' + g') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>hg : DifferentiableWithinAt 𝕜 g s x<GOAL>derivWithin (fun y => f y + g y) s x = derivWithin f s x + derivWithin g s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : 𝕜 → F<VAR>x : 𝕜<VAR>hf : DifferentiableAt 𝕜 f x<VAR>hg : DifferentiableAt 𝕜 g x<GOAL>deriv (fun y => f y + g y) x = deriv f x + deriv g 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>c : F<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun y => f y + c) 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>L : Filter 𝕜<VAR>hf : HasDerivAtFilter f f' x L<VAR>c : F<GOAL>HasDerivAtFilter (fun y => f y + c) f' x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hf : HasDerivWithinAt f f' s x<VAR>c : F<GOAL>HasDerivWithinAt (fun y => f y + c) f' s 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>hf : HasDerivAt f f' x<VAR>c : F<GOAL>HasDerivAt (fun x => f x + c) f' x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : F<GOAL>derivWithin (fun y => f y + c) s x = derivWithin f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>c : F<GOAL>deriv (fun y => f y + c) x = deriv f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>c : F<GOAL>(deriv fun y => f y + c) = deriv f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>c : F<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun y => c + f y) 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>L : Filter 𝕜<VAR>c : F<VAR>hf : HasDerivAtFilter f f' x L<GOAL>HasDerivAtFilter (fun y => c + f y) f' x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>c : F<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun y => c + f y) f' s 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>c : F<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => c + f x) f' x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : F<GOAL>derivWithin (fun y => c + f y) s x = derivWithin f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>c : F<GOAL>deriv (fun y => c + f y) x = deriv f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>c : F<GOAL>(deriv fun y => c + f y) = deriv f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>ι : Type u_1<VAR>u : Finset ι<VAR>A : ι → 𝕜 → F<VAR>A' : ι → F<VAR>h : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) x L<GOAL>HasDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>ι : Type u_1<VAR>u : Finset ι<VAR>A : ι → 𝕜 → F<VAR>A' : ι → F<VAR>h : ∀ i ∈ u, HasStrictDerivAt (A i) (A' i) x<GOAL>HasStrictDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>ι : Type u_1<VAR>u : Finset ι<VAR>A : ι → 𝕜 → F<VAR>A' : ι → F<VAR>h : ∀ i ∈ u, HasDerivWithinAt (A i) (A' i) s x<GOAL>HasDerivWithinAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>ι : Type u_1<VAR>u : Finset ι<VAR>A : ι → 𝕜 → F<VAR>A' : ι → F<VAR>h : ∀ i ∈ u, HasDerivAt (A i) (A' i) x<GOAL>HasDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>ι : Type u_1<VAR>u : Finset ι<VAR>A : ι → 𝕜 → F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x<GOAL>derivWithin (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, derivWithin (A i) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>ι : Type u_1<VAR>u : Finset ι<VAR>A : ι → 𝕜 → F<VAR>h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x<GOAL>deriv (fun y => ∑ i ∈ u, A i y) x = ∑ i ∈ u, deriv (A i) 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>L : Filter 𝕜<VAR>h : HasDerivAtFilter f f' x L<GOAL>HasDerivAtFilter (fun x => -f x) (-f') x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => -f x) (-f') s 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<GOAL>HasDerivAt (fun x => -f x) (-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 : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => -f x) (-f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun y => -f y) s x = -derivWithin f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<GOAL>deriv (fun y => -f y) x = -deriv f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<GOAL>(deriv fun y => -f y) = fun x => -deriv f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>L : Filter 𝕜<GOAL>HasDerivAtFilter Neg.neg (-1) x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>HasDerivWithinAt Neg.neg (-1) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>HasDerivAt Neg.neg (-1) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>HasDerivAt (fun x => -x) (-1) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>HasStrictDerivAt Neg.neg (-1) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>deriv Neg.neg x = -1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<GOAL>deriv Neg.neg = fun x => -1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>deriv (fun x => -x) x = -1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin Neg.neg s x = -1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<GOAL>Differentiable 𝕜 Neg.neg
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>s : Set 𝕜<GOAL>DifferentiableOn 𝕜 Neg.neg s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>a : 𝕜<GOAL>DifferentiableAt 𝕜 f (-a) ↔ DifferentiableAt 𝕜 (fun x => f (-x)) a
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : 𝕜 → F<VAR>f' g' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>hf : HasDerivAtFilter f f' x L<VAR>hg : HasDerivAtFilter g g' x L<GOAL>HasDerivAtFilter (fun x => f x - g x) (f' - g') x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : 𝕜 → F<VAR>f' g' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hf : HasDerivWithinAt f f' s x<VAR>hg : HasDerivWithinAt g g' s x<GOAL>HasDerivWithinAt (fun x => f x - g x) (f' - g') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : 𝕜 → F<VAR>f' g' : F<VAR>x : 𝕜<VAR>hf : HasDerivAt f f' x<VAR>hg : HasDerivAt g g' x<GOAL>HasDerivAt (fun x => f x - g x) (f' - g') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : 𝕜 → F<VAR>f' g' : F<VAR>x : 𝕜<VAR>hf : HasStrictDerivAt f f' x<VAR>hg : HasStrictDerivAt g g' x<GOAL>HasStrictDerivAt (fun x => f x - g x) (f' - g') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>hg : DifferentiableWithinAt 𝕜 g s x<GOAL>derivWithin (fun y => f y - g y) s x = derivWithin f s x - derivWithin g s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : 𝕜 → F<VAR>x : 𝕜<VAR>hf : DifferentiableAt 𝕜 f x<VAR>hg : DifferentiableAt 𝕜 g x<GOAL>deriv (fun y => f y - g y) x = deriv f x - deriv g 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>L : Filter 𝕜<VAR>hf : HasDerivAtFilter f f' x L<VAR>c : F<GOAL>HasDerivAtFilter (fun x => f x - c) f' x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hf : HasDerivWithinAt f f' s x<VAR>c : F<GOAL>HasDerivWithinAt (fun x => f x - c) f' s 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>hf : HasDerivAt f f' x<VAR>c : F<GOAL>HasDerivAt (fun x => f x - c) f' x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : F<GOAL>derivWithin (fun y => f y - c) s x = derivWithin f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>c : F<GOAL>deriv (fun y => f y - c) x = deriv 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>L : Filter 𝕜<VAR>c : F<VAR>hf : HasDerivAtFilter f f' x L<GOAL>HasDerivAtFilter (fun x => c - f x) (-f') x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>c : F<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => c - f x) (-f') s 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>c : F<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => c - f x) (-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>c : F<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => c - f x) (-f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : F<GOAL>derivWithin (fun y => c - f y) s x = -derivWithin f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>c : F<GOAL>deriv (fun y => c - f y) x = -deriv f x
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>NormedAddCommGroup E'<VAR>g : G → E'<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ E'<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>HasContDiffBump G<VAR>CompleteSpace E'<VAR>φ : ContDiffBump 0<VAR>x₀ : G<VAR>hg : ∀ x ∈ Metric.ball x₀ φ.rOut, g x = g x₀<GOAL>(↑φ ⋆[ContinuousLinearMap.lsmul ℝ ℝ, μ] g) x₀ = MeasureTheory.integral μ ↑φ • g x₀
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>NormedAddCommGroup E'<VAR>g : G → E'<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ E'<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>HasContDiffBump G<VAR>CompleteSpace E'<VAR>φ : ContDiffBump 0<VAR>BorelSpace G<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<VAR>FiniteDimensional ℝ G<VAR>x₀ : G<VAR>hg : ∀ x ∈ Metric.ball x₀ φ.rOut, g x = g x₀<GOAL>(φ.normed μ ⋆[ContinuousLinearMap.lsmul ℝ ℝ, μ] g) x₀ = g x₀
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>NormedAddCommGroup E'<VAR>g : G → E'<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ E'<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>HasContDiffBump G<VAR>CompleteSpace E'<VAR>φ : ContDiffBump 0<VAR>BorelSpace G<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<VAR>FiniteDimensional ℝ G<VAR>μ.IsAddLeftInvariant<VAR>x₀ : G<VAR>ε : ℝ<VAR>hmg : MeasureTheory.AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ Metric.ball x₀ φ.rOut, dist (g x) (g x₀) ≤ ε<GOAL>dist ((φ.normed μ ⋆[ContinuousLinearMap.lsmul ℝ ℝ, μ] g) x₀) (g x₀) ≤ ε
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>NormedAddCommGroup E'<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ E'<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>HasContDiffBump G<VAR>CompleteSpace E'<VAR>BorelSpace G<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<VAR>FiniteDimensional ℝ G<VAR>μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>g : ι → G → E'<VAR>k : ι → G<VAR>x₀ : G<VAR>z₀ : E'<VAR>l : Filter ι<VAR>hφ : Filter.Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>hig : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (g i) μ<VAR>hcg : Filter.Tendsto (Function.uncurry g) (l ×ˢ 𝓝 x₀) (𝓝 z₀)<VAR>hk : Filter.Tendsto k l (𝓝 x₀)<GOAL>Filter.Tendsto (fun i => ((φ i).normed μ ⋆[ContinuousLinearMap.lsmul ℝ ℝ, μ] g i) (k i)) l (𝓝 z₀)
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>NormedAddCommGroup E'<VAR>g : G → E'<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ E'<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>HasContDiffBump G<VAR>CompleteSpace E'<VAR>BorelSpace G<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<VAR>FiniteDimensional ℝ G<VAR>μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>l : Filter ι<VAR>hφ : Filter.Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>hg : Continuous g<VAR>x₀ : G<GOAL>Filter.Tendsto (fun i => ((φ i).normed μ ⋆[ContinuousLinearMap.lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>NormedAddCommGroup E'<VAR>g : G → E'<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ E'<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>HasContDiffBump G<VAR>CompleteSpace E'<VAR>BorelSpace G<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<VAR>FiniteDimensional ℝ G<VAR>μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>l : Filter ι<VAR>K : ℝ<VAR>hφ : Filter.Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn<VAR>hg : MeasureTheory.LocallyIntegrable g μ<GOAL>∀ᵐ (x₀ : G) ∂μ, Filter.Tendsto (fun i => ((φ i).normed μ ⋆[ContinuousLinearMap.lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>b : AffineBasis ι 𝕜 E<VAR>i : ι<GOAL>ContDiff 𝕜 ⊤ ⇑(b.coord i)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>NormedAddCommGroup W<VAR>NormedSpace 𝕜 W<VAR>n : ℕ∞<VAR>f : V →ᴬ[𝕜] W<GOAL>ContDiff 𝕜 n ⇑f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : QuadraticMap 𝕜 E F<VAR>a b : E<GOAL>HasLineDerivAt 𝕜 (⇑f) (QuadraticMap.polar (⇑f) a b) a b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : QuadraticMap 𝕜 E F<VAR>a b : E<GOAL>LineDifferentiableAt 𝕜 (⇑f) a b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : QuadraticMap 𝕜 E F<GOAL>lineDeriv 𝕜 ⇑f = QuadraticMap.polar ⇑f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>x : E<GOAL>f.normed μ x = ↑f x / ∫ (x : E), ↑f x ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>x : E<GOAL>0 ≤ f.normed μ x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>n : ℕ∞<GOAL>ContDiff ℝ n (f.normed μ)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<GOAL>Continuous (f.normed μ)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>x : E<GOAL>f.normed μ (c - x) = f.normed μ (c + x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>f : ContDiffBump 0<VAR>x : E<GOAL>f.normed μ (-x) = f.normed μ x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>MeasureTheory.Integrable (↑f) μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>MeasureTheory.Integrable (f.normed μ) μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<GOAL>0 < ∫ (x : E), ↑f x ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<GOAL>∫ (x : E), f.normed μ x ∂μ = 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<GOAL>Function.support (f.normed μ) = Metric.ball c f.rOut
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<GOAL>tsupport (f.normed μ) = Metric.closedBall c f.rOut