ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>_i : Fact (1 ≤ p)<VAR>F : ℕ → ↥(lp E p)<VAR>hF : CauchySeq F<VAR>f : ↥(lp E p)<VAR>hf : Filter.Tendsto (id fun i => ↑(F i)) Filter.atTop (nhds ↑f)<GOAL>Filter.Tendsto F Filter.atTop (nhds f)
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>PseudoMetricSpace α<VAR>g : α → ι → ℝ<VAR>K : ℝ≥0<VAR>hg : ∀ (i : ι), LipschitzWith K fun x => g x i<VAR>a₀ : α<VAR>hga₀b : Memℓp (g a₀) ⊤<VAR>a : α<GOAL>Memℓp (g a) ⊤
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>PseudoMetricSpace α<VAR>f : α → ↥(lp (fun i => ℝ) ⊤)<VAR>s : Set α<VAR>K : ℝ≥0<GOAL>LipschitzOnWith K f s ↔ ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>PseudoMetricSpace α<VAR>f : α → ↥(lp (fun i => ℝ) ⊤)<VAR>K : ℝ≥0<GOAL>LipschitzWith K f ↔ ∀ (i : ι), LipschitzWith K fun a => ↑(f a) i
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>n : ℕ<VAR>s : Set ℝ<VAR>x₀ : ℝ<GOAL>taylorWithin f (n + 1) s x₀ = taylorWithin f n s x₀ + (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀)) ((PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀))
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>n : ℕ<VAR>s : Set ℝ<VAR>x₀ x : ℝ<GOAL>taylorWithinEval f (n + 1) s x₀ x = taylorWithinEval f n s x₀ x + (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>x₀ x : ℝ<GOAL>taylorWithinEval f 0 s x₀ x = f x₀
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>n : ℕ<VAR>s : Set ℝ<VAR>x₀ : ℝ<GOAL>taylorWithinEval f n s x₀ x₀ = f x₀
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>n : ℕ<VAR>s : Set ℝ<VAR>x₀ x : ℝ<GOAL>taylorWithinEval f n s x₀ x = ∑ k ∈ Finset.range (n + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x : ℝ<VAR>n : ℕ<VAR>s : Set ℝ<VAR>hs : UniqueDiffOn ℝ s<VAR>hf : ContDiffOn ℝ (↑n) f s<GOAL>ContinuousOn (fun t => taylorWithinEval f n s t x) s
<VAR>t x : ℝ<VAR>n : ℕ<GOAL>HasDerivAt (fun y => (x - y) ^ (n + 1)) (-(↑n + 1) * (x - t) ^ n) t
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>k : ℕ<VAR>s t : Set ℝ<VAR>ht : UniqueDiffWithinAt ℝ t y<VAR>hs : s ∈ 𝓝[t] y<VAR>hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y<GOAL>HasDerivWithinAt (fun z => (((↑k + 1) * ↑k !)⁻¹ * (x - z) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s z) ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y - ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) t y
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>n : ℕ<VAR>s s' : Set ℝ<VAR>hs'_unique : UniqueDiffWithinAt ℝ s' y<VAR>hs_unique : UniqueDiffOn ℝ s<VAR>hs' : s' ∈ 𝓝[s] y<VAR>hy : y ∈ s'<VAR>h : s' ⊆ s<VAR>hf : ContDiffOn ℝ (↑n) f s<VAR>hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin n f s) s y<GOAL>HasDerivWithinAt (fun t => taylorWithinEval f n s t x) (((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f s y) s' y
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b t : ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hx : a < b<VAR>ht : t ∈ Set.Ioo a b<VAR>hf : ContDiffOn ℝ (↑n) f (Set.Icc a b)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc a b)) (Set.Ioo a b)<GOAL>HasDerivAt (fun y => taylorWithinEval f n (Set.Icc a b) y x) (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Set.Icc a b) t) t
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b t : ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hx : a < b<VAR>ht : t ∈ Set.Icc a b<VAR>hf : ContDiffOn ℝ (↑n) f (Set.Icc a b)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc a b)) (Set.Icc a b)<GOAL>HasDerivWithinAt (fun y => taylorWithinEval f n (Set.Icc a b) y x) (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Set.Icc a b) t) (Set.Icc a b) t
<VAR>f g g' : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Set.Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)<VAR>gcont : ContinuousOn g (Set.Icc x₀ x)<VAR>gdiff : ∀ x_1 ∈ Set.Ioo x₀ x, HasDerivAt g (g' x_1) x_1<VAR>g'_ne : ∀ x_1 ∈ Set.Ioo x₀ x, g' x_1 ≠ 0<GOAL>∃ x' ∈ Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x'
<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Set.Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)<GOAL>∃ x' ∈ Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Set.Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)<GOAL>∃ x' ∈ Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x') ^ n / ↑n ! * (x - x₀)
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b C x : ℝ<VAR>n : ℕ<VAR>hab : a ≤ b<VAR>hf : ContDiffOn ℝ (↑n + 1) f (Set.Icc a b)<VAR>hx : x ∈ Set.Icc a b<VAR>hC : ∀ y ∈ Set.Icc a b, ‖iteratedDerivWithin (n + 1) f (Set.Icc a b) y‖ ≤ C<GOAL>‖f x - taylorWithinEval f n (Set.Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>n : ℕ<VAR>hab : a ≤ b<VAR>hf : ContDiffOn ℝ (↑n + 1) f (Set.Icc a b)<GOAL>∃ C, ∀ x ∈ Set.Icc a b, ‖f x - taylorWithinEval f n (Set.Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>MeasureTheory.SigmaFinite μ<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : MeasureTheory.Integrable (fun x => (B (f' x)) (g x)) (μ.prod MeasureTheory.volume)<VAR>hfg' : MeasureTheory.Integrable (fun x => (B (f x)) (g' x)) (μ.prod MeasureTheory.volume)<VAR>hfg : MeasureTheory.Integrable (fun x => (B (f x)) (g x)) (μ.prod MeasureTheory.volume)<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<GOAL>∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ.prod MeasureTheory.volume = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ.prod MeasureTheory.volume
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure (E × ℝ)<VAR>μ.IsAddHaarMeasure<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : MeasureTheory.Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : MeasureTheory.Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : MeasureTheory.Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<GOAL>∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>FiniteDimensional ℝ E<VAR>μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : MeasureTheory.Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : MeasureTheory.Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : MeasureTheory.Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v<GOAL>∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>FiniteDimensional ℝ E<VAR>μ.IsAddHaarMeasure<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>g : E → G<VAR>g' : E → E →L[ℝ] G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : MeasureTheory.Integrable (fun x => (B ((f' x) v)) (g x)) μ<VAR>hfg' : MeasureTheory.Integrable (fun x => (B (f x)) ((g' x) v)) μ<VAR>hfg : MeasureTheory.Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasFDerivAt f (f' x) x<VAR>hg : ∀ (x : E), HasFDerivAt g (g' x) x<GOAL>∫ (x : E), (B (f x)) ((g' x) v) ∂μ = -∫ (x : E), (B ((f' x) v)) (g x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>FiniteDimensional ℝ E<VAR>μ.IsAddHaarMeasure<VAR>f : E → F<VAR>g : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : MeasureTheory.Integrable (fun x => (B ((fderiv ℝ f x) v)) (g x)) μ<VAR>hfg' : MeasureTheory.Integrable (fun x => (B (f x)) ((fderiv ℝ g x) v)) μ<VAR>hfg : MeasureTheory.Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : Differentiable ℝ f<VAR>hg : Differentiable ℝ g<GOAL>∫ (x : E), (B (f x)) ((fderiv ℝ g x) v) ∂μ = -∫ (x : E), (B ((fderiv ℝ f x) v)) (g x) ∂μ
<VAR>E : Type u_1<VAR>G : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>FiniteDimensional ℝ E<VAR>μ.IsAddHaarMeasure<VAR>𝕜 : Type u_5<VAR>NormedField 𝕜<VAR>NormedAlgebra ℝ 𝕜<VAR>NormedSpace 𝕜 G<VAR>IsScalarTower ℝ 𝕜 G<VAR>f : E → 𝕜<VAR>g : E → G<VAR>v : E<VAR>hf'g : MeasureTheory.Integrable (fun x => (fderiv ℝ f x) v • g x) μ<VAR>hfg' : MeasureTheory.Integrable (fun x => f x • (fderiv ℝ g x) v) μ<VAR>hfg : MeasureTheory.Integrable (fun x => f x • g x) μ<VAR>hf : Differentiable ℝ f<VAR>hg : Differentiable ℝ g<GOAL>∫ (x : E), f x • (fderiv ℝ g x) v ∂μ = -∫ (x : E), (fderiv ℝ f x) v • g x ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>FiniteDimensional ℝ E<VAR>μ.IsAddHaarMeasure<VAR>𝕜 : Type u_5<VAR>NormedField 𝕜<VAR>NormedAlgebra ℝ 𝕜<VAR>f g : E → 𝕜<VAR>v : E<VAR>hf'g : MeasureTheory.Integrable (fun x => (fderiv ℝ f x) v * g x) μ<VAR>hfg' : MeasureTheory.Integrable (fun x => f x * (fderiv ℝ g x) v) μ<VAR>hfg : MeasureTheory.Integrable (fun x => f x * g x) μ<VAR>hf : Differentiable ℝ f<VAR>hg : Differentiable ℝ g<GOAL>∫ (x : E), f x * (fderiv ℝ g x) v ∂μ = -∫ (x : E), (fderiv ℝ f x) v * g x ∂μ
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕂] F<VAR>a : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕂 n f a<VAR>hf' : HasFDerivAt f (↑f') a<VAR>hn : 1 ≤ n<GOAL>↑(ContDiffAt.toPartialHomeomorph f hf hf' hn) = 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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕂] F<VAR>a : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕂 n f a<VAR>hf' : HasFDerivAt f (↑f') a<VAR>hn : 1 ≤ n<GOAL>a ∈ (ContDiffAt.toPartialHomeomorph f hf hf' hn).source
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕂] F<VAR>a : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕂 n f a<VAR>hf' : HasFDerivAt f (↑f') a<VAR>hn : 1 ≤ n<GOAL>f a ∈ (ContDiffAt.toPartialHomeomorph f hf hf' hn).target
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕂] F<VAR>a : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕂 n f a<VAR>hf' : HasFDerivAt f (↑f') a<VAR>hn : 1 ≤ n<GOAL>hf.localInverse hf' hn (f a) = a
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕂] F<VAR>a : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕂 n f a<VAR>hf' : HasFDerivAt f (↑f') a<VAR>hn : 1 ≤ n<GOAL>ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)
<VAR>f : ℝ → ℝ<VAR>x a c d : ℝ<VAR>l : Filter ℝ<VAR>hl : l ≤ 𝓝[≠] x<VAR>hf : Filter.Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)<VAR>h' : Filter.Tendsto (fun y => y + c * (y - x) ^ 2) l l<GOAL>Filter.Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
<VAR>f : StieltjesFunction<GOAL>∀ᵐ (x : ℝ), HasDerivAt (↑f) (f.measure.rnDeriv MeasureTheory.volume x).toReal x
<VAR>f : ℝ → ℝ<VAR>hf : Monotone f<GOAL>∀ᵐ (x : ℝ), HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv MeasureTheory.volume x).toReal x
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hf : MonotoneOn f s<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt ℝ f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>u : 𝕜 → E<VAR>v : 𝕜 → F<VAR>u' : E<VAR>v' : F<VAR>hu : HasDerivWithinAt u u' s x<VAR>hv : HasDerivWithinAt v v' s x<GOAL>HasDerivWithinAt (fun x => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : 𝕜<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>u : 𝕜 → E<VAR>v : 𝕜 → F<VAR>u' : E<VAR>v' : F<VAR>hu : HasDerivAt u u' x<VAR>hv : HasDerivAt v v' x<GOAL>HasDerivAt (fun x => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : 𝕜<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>u : 𝕜 → E<VAR>v : 𝕜 → F<VAR>u' : E<VAR>v' : F<VAR>hu : HasStrictDerivAt u u' x<VAR>hv : HasStrictDerivAt v v' x<GOAL>HasStrictDerivAt (fun x => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>u : 𝕜 → E<VAR>v : 𝕜 → F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hu : DifferentiableWithinAt 𝕜 u s x<VAR>hv : DifferentiableWithinAt 𝕜 v s x<GOAL>derivWithin (fun y => (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : 𝕜<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>u : 𝕜 → E<VAR>v : 𝕜 → F<VAR>hu : DifferentiableAt 𝕜 u x<VAR>hv : DifferentiableAt 𝕜 v x<GOAL>deriv (fun y => (B (u y)) (v y)) x = (B (u x)) (deriv v x) + (B (deriv u x)) (v 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>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun y => c y • f y) (c x • f' + c' • f x) 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>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivAt c c' x<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun y => c y • f y) (c x • f' + c' • f x) 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>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun y => c y • f y) (c x • f' + c' • f x) 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>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hf : DifferentiableWithinAt 𝕜 f s x<GOAL>derivWithin (fun y => c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hf : DifferentiableAt 𝕜 f x<GOAL>deriv (fun y => c y • f y) x = c x • deriv f x + deriv c x • f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>f : F<GOAL>HasStrictDerivAt (fun y => c y • f) (c' • f) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>f : F<GOAL>HasDerivWithinAt (fun y => c y • f) (c' • f) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivAt c c' x<VAR>f : F<GOAL>HasDerivAt (fun y => c y • f) (c' • f) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>f : F<GOAL>derivWithin (fun y => c y • f) s x = derivWithin c s x • f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>hc : DifferentiableAt 𝕜 c x<VAR>f : F<GOAL>deriv (fun y => c y • f) x = deriv c x • 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>R : Type u_2<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>c : R<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun y => c • 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>R : Type u_2<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>c : R<VAR>hf : HasDerivAtFilter f f' x L<GOAL>HasDerivAtFilter (fun y => c • 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>R : Type u_2<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>c : R<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun y => c • 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>R : Type u_2<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>c : R<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun y => c • f y) (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>R : Type u_2<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : R<VAR>hf : DifferentiableWithinAt 𝕜 f s x<GOAL>derivWithin (fun y => c • f y) s x = c • 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>R : Type u_2<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>c : R<VAR>hf : DifferentiableAt 𝕜 f x<GOAL>deriv (fun y => c • f y) x = c • deriv f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>R : Type u_3<VAR>Field R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>c : R<GOAL>deriv (fun y => c • f y) x = c • deriv f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>c d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>hc : HasDerivWithinAt c c' s x<VAR>hd : HasDerivWithinAt d d' s x<GOAL>HasDerivWithinAt (fun y => c y * d y) (c' * d x + c x * d') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>c d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>hc : HasDerivAt c c' x<VAR>hd : HasDerivAt d d' x<GOAL>HasDerivAt (fun y => c y * d y) (c' * d x + c x * d') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>c d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>hc : HasStrictDerivAt c c' x<VAR>hd : HasStrictDerivAt d d' x<GOAL>HasStrictDerivAt (fun y => c y * d y) (c' * d x + c x * d') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>c d : 𝕜 → 𝔸<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hd : DifferentiableWithinAt 𝕜 d s x<GOAL>derivWithin (fun y => c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>c d : 𝕜 → 𝔸<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hd : DifferentiableAt 𝕜 d x<GOAL>deriv (fun y => c y * d y) x = deriv c x * d x + c x * deriv d x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>c : 𝕜 → 𝔸<VAR>c' : 𝔸<VAR>hc : HasDerivWithinAt c c' s x<VAR>d : 𝔸<GOAL>HasDerivWithinAt (fun y => c y * d) (c' * d) s x