ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>SecondCountableTopology V<VAR>μ : MeasureTheory.Measure V<VAR>hf : MeasureTheory.Integrable f μ<VAR>hf' : MeasureTheory.Integrable (fun v => ‖v‖ * ‖f v‖) μ<GOAL>fderiv ℝ (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f) = VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ (VectorFourier.fourierSMulRight L f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>SecondCountableTopology V<VAR>μ : MeasureTheory.Measure V<VAR>hf : MeasureTheory.Integrable f μ<VAR>hf' : MeasureTheory.Integrable (fun v => ‖v‖ * ‖f v‖) μ<GOAL>Differentiable ℝ (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>FiniteDimensional ℝ V<VAR>μ : MeasureTheory.Measure V<VAR>μ.IsAddHaarMeasure<VAR>hf : MeasureTheory.Integrable f μ<VAR>h'f : Differentiable ℝ f<VAR>hf' : MeasureTheory.Integrable (fderiv ℝ f) μ<GOAL>VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ (fderiv ℝ f) = VectorFourier.fourierSMulRight (-L.flip) (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<VAR>n : ℕ<VAR>m : Fin n → W<GOAL>(VectorFourier.fourierPowSMulRight L f v n) m = (-(2 * ↑π * Complex.I)) ^ n • (∏ i : Fin n, (L v) (m i)) • f v
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<VAR>n : ℕ<GOAL>VectorFourier.fourierPowSMulRight L f v n = (-(2 * ↑π * Complex.I)) ^ n • ((ContinuousMultilinearMap.smulRightL ℝ (fun x => W) E) ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v)) (f v)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>hf : Continuous f<VAR>n : ℕ<GOAL>Continuous fun v => VectorFourier.fourierPowSMulRight L f v n
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>k : ℕ∞<VAR>hf : ContDiff ℝ k f<VAR>n : ℕ<GOAL>ContDiff ℝ k fun v => VectorFourier.fourierPowSMulRight L f v n
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<VAR>n : ℕ<GOAL>‖VectorFourier.fourierPowSMulRight L f v n‖ ≤ (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>K : ℕ∞<VAR>C : ℝ<VAR>hf : ContDiff ℝ K f<VAR>n k : ℕ<VAR>hk : ↑k ≤ K<VAR>v : V<VAR>hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C<GOAL>‖iteratedFDeriv ℝ k (fun v => VectorFourier.fourierPowSMulRight L f v n) v‖ ≤ (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>SecondCountableTopology V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>μ : MeasureTheory.Measure V<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>n : ℕ<GOAL>MeasureTheory.AEStronglyMeasurable (fun v => VectorFourier.fourierPowSMulRight L f v n) μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>SecondCountableTopology V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>μ : MeasureTheory.Measure V<VAR>n : ℕ<VAR>hf : MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ<VAR>h'f : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.Integrable (fun v => VectorFourier.fourierPowSMulRight L f v n) μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>SecondCountableTopology V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>μ : MeasureTheory.Measure V<VAR>N : ℕ∞<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ<VAR>h'f : MeasureTheory.AEStronglyMeasurable f μ<GOAL>HasFTaylorSeriesUpTo N (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f) fun w n => VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => VectorFourier.fourierPowSMulRight L f v n) w
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>SecondCountableTopology V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>μ : MeasureTheory.Measure V<VAR>N : ℕ∞<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ<GOAL>ContDiff ℝ N (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>SecondCountableTopology V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>μ : MeasureTheory.Measure V<VAR>N : ℕ∞<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ<VAR>h'f : MeasureTheory.AEStronglyMeasurable f μ<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>iteratedFDeriv ℝ n (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f) = VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ fun v => VectorFourier.fourierPowSMulRight L f v n
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>FiniteDimensional ℝ V<VAR>μ : MeasureTheory.Measure V<VAR>μ.IsAddHaarMeasure<VAR>N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (iteratedFDeriv ℝ n f) μ<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ (iteratedFDeriv ℝ n f) = fun w => VectorFourier.fourierPowSMulRight (-L.flip) (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f) w n
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>SecondCountableTopology V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>FiniteDimensional ℝ V<VAR>μ : MeasureTheory.Measure V<VAR>μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : W<GOAL>VectorFourier.fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f)) w n = VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ (iteratedFDeriv ℝ n fun v => VectorFourier.fourierPowSMulRight L f v k) w
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>SecondCountableTopology V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>FiniteDimensional ℝ V<VAR>μ : MeasureTheory.Measure V<VAR>μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : W<GOAL>‖VectorFourier.fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f)) w n‖ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>SecondCountableTopology V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>FiniteDimensional ℝ V<VAR>μ : MeasureTheory.Measure V<VAR>μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>v : V<VAR>w : W<GOAL>|(L v) w| ^ n * ‖iteratedFDeriv ℝ k (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f) w‖ ≤ ‖v‖ ^ n * (2 * π * ‖L‖) ^ k * (2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>f : V → E<VAR>hf_int : MeasureTheory.Integrable f MeasureTheory.volume<VAR>hvf_int : MeasureTheory.Integrable (fun v => ‖v‖ * ‖f v‖) MeasureTheory.volume<VAR>x : V<GOAL>HasFDerivAt (𝓕 f) (𝓕 (VectorFourier.fourierSMulRight (innerSL ℝ) f) x) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>f : V → E<VAR>hf_int : MeasureTheory.Integrable f MeasureTheory.volume<VAR>hvf_int : MeasureTheory.Integrable (fun v => ‖v‖ * ‖f v‖) MeasureTheory.volume<GOAL>fderiv ℝ (𝓕 f) = 𝓕 (VectorFourier.fourierSMulRight (innerSL ℝ) f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>f : V → E<VAR>hf_int : MeasureTheory.Integrable f MeasureTheory.volume<VAR>hvf_int : MeasureTheory.Integrable (fun v => ‖v‖ * ‖f v‖) MeasureTheory.volume<GOAL>Differentiable ℝ (𝓕 f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>f : V → E<VAR>hf : MeasureTheory.Integrable f MeasureTheory.volume<VAR>h'f : Differentiable ℝ f<VAR>hf' : MeasureTheory.Integrable (fderiv ℝ f) MeasureTheory.volume<GOAL>𝓕 (fderiv ℝ f) = VectorFourier.fourierSMulRight (-innerSL ℝ) (𝓕 f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>f : V → E<VAR>N : ℕ∞<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) MeasureTheory.volume<GOAL>ContDiff ℝ N (𝓕 f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>f : V → E<VAR>N : ℕ∞<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) MeasureTheory.volume<VAR>h'f : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>iteratedFDeriv ℝ n (𝓕 f) = 𝓕 fun v => VectorFourier.fourierPowSMulRight (innerSL ℝ) f v n
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>f : V → E<VAR>N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (iteratedFDeriv ℝ n f) MeasureTheory.volume<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>𝓕 (iteratedFDeriv ℝ n f) = fun w => VectorFourier.fourierPowSMulRight (-innerSL ℝ) (𝓕 f) w n
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>f : V → E<VAR>FiniteDimensional ℝ V<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) MeasureTheory.volume<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : V<GOAL>‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>hf : MeasureTheory.Integrable f MeasureTheory.volume<VAR>hf' : MeasureTheory.Integrable (fun x => x • f x) MeasureTheory.volume<VAR>w : ℝ<GOAL>HasDerivAt (𝓕 f) (𝓕 (fun x => (-2 * ↑π * Complex.I * ↑x) • f x) w) w
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>hf : MeasureTheory.Integrable f MeasureTheory.volume<VAR>hf' : MeasureTheory.Integrable (fun x => x • f x) MeasureTheory.volume<GOAL>deriv (𝓕 f) = 𝓕 fun x => (-2 * ↑π * Complex.I * ↑x) • f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>hf : MeasureTheory.Integrable f MeasureTheory.volume<VAR>h'f : Differentiable ℝ f<VAR>hf' : MeasureTheory.Integrable (deriv f) MeasureTheory.volume<GOAL>𝓕 (deriv f) = fun x => (2 * ↑π * Complex.I * ↑x) • 𝓕 f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun x => x ^ n • f x) MeasureTheory.volume<VAR>hn : ↑n ≤ N<GOAL>iteratedDeriv n (𝓕 f) = 𝓕 fun x => (-2 * ↑π * Complex.I * ↑x) ^ n • f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (iteratedDeriv n f) MeasureTheory.volume<VAR>hn : ↑n ≤ N<GOAL>𝓕 (iteratedDeriv n f) = fun x => (2 * ↑π * Complex.I * ↑x) ^ n • 𝓕 f x
<VAR>z : ℂ<GOAL>z ∈ circle ↔ Complex.abs z = 1
<VAR>z : ↥circle<GOAL>Complex.abs ↑z = 1
<VAR>z : ℂ<GOAL>z ∈ circle ↔ Complex.normSq z = 1
<VAR>z : ↥circle<GOAL>Complex.normSq ↑z = 1
<VAR>z : ↥circle<GOAL>↑z ≠ 0
<VAR>z : ↥circle<GOAL>↑z⁻¹ = (↑z)⁻¹
<VAR>z w : ↥circle<GOAL>↑(z / w) = ↑z / ↑w
<VAR>z : ↥circle<GOAL>circle.toUnits z = Units.mk0 ↑z ⋯
<VAR>z : ℂ<VAR>hz : z ≠ 0<GOAL>↑(circle.ofConjDivSelf z hz) = (starRingEnd ℂ) z / z
<VAR>t : ℝ<GOAL>↑(expMapCircle t) = cexp (↑t * Complex.I)
<VAR>x y : ℝ<GOAL>expMapCircle (x + y) = expMapCircle x * expMapCircle y
<GOAL>∀ (a : ℝ), expMapCircleHom a = (⇑Additive.ofMul ∘ ⇑expMapCircle) a
<VAR>x y : ℝ<GOAL>expMapCircle (x - y) = expMapCircle x / expMapCircle y
<VAR>x : ℝ<GOAL>expMapCircle (-x) = (expMapCircle x)⁻¹
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>u : ↥circle<VAR>v : E<GOAL>‖u • v‖ = ‖v‖
<VAR>x y : ℂ<GOAL>Complex.abs (x + y) = Complex.abs x + Complex.abs y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
<VAR>x y : ℂ<GOAL>Complex.abs (x - y) = |Complex.abs x - Complex.abs y| ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
<VAR>x y : ℂ<VAR>h : x.arg = y.arg<GOAL>SameRay ℝ x y
<VAR>x y : ℂ<VAR>h : x.arg = y.arg<GOAL>Complex.abs (x + y) = Complex.abs x + Complex.abs y
<VAR>x y : ℂ<VAR>h : x.arg = y.arg<GOAL>Complex.abs (x - y) = ‖Complex.abs x - Complex.abs y‖
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z<VAR>hc : ContinuousAt f c<GOAL>AnalyticAt ℂ f c
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hs : s ∈ 𝓝 c<GOAL>DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c ↔ DifferentiableOn ℂ f s
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hc : s ∈ 𝓝 c<GOAL>DifferentiableOn ℂ (dslope f c) s ↔ DifferentiableOn ℂ f s
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hc : s ∈ 𝓝 c<VAR>hd : DifferentiableOn ℂ f (s \ {c})<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<GOAL>DifferentiableOn ℂ (Function.update f c (limUnder (𝓝[≠] c) f)) s
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hc : s ∈ 𝓝[≠] c<VAR>hd : DifferentiableOn ℂ f s<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<GOAL>DifferentiableOn ℂ (Function.update f c (limUnder (𝓝[≠] c) f)) (insert c s)
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hc : s ∈ 𝓝 c<VAR>hd : DifferentiableOn ℂ f (s \ {c})<VAR>hb : BddAbove (norm ∘ f '' (s \ {c}))<GOAL>DifferentiableOn ℂ (Function.update f c (limUnder (𝓝[≠] c) f)) s
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<GOAL>Filter.Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z<VAR>hb : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[≠] c) fun z => ‖f z - f c‖<GOAL>Filter.Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>U : Set ℂ<VAR>hU : IsOpen U<VAR>c w₀ : ℂ<VAR>R : ℝ<VAR>f : ℂ → E<VAR>hc : Metric.closedBall c R ⊆ U<VAR>hf : DifferentiableOn ℂ f U<VAR>hw₀ : w₀ ∈ Metric.ball c R<GOAL>((2 * ↑π * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = deriv f w₀
<VAR>f : ℂ → ℂ<VAR>z₀ : ℂ<VAR>ε r : ℝ<VAR>h : DiffContOnCl ℂ f (Metric.ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ Metric.sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<GOAL>Metric.ball (f z₀) (ε / 2) ⊆ f '' Metric.closedBall z₀ r
<VAR>f : ℂ → ℂ<VAR>z₀ : ℂ<VAR>hf : AnalyticAt ℂ f z₀<GOAL>(∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀) ∨ 𝓝 (f z₀) ≤ Filter.map f (𝓝 z₀)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>g : E → ℂ<VAR>z₀ : E<VAR>hg : AnalyticAt ℂ g z₀<GOAL>(∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ Filter.map g (𝓝 z₀)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>U : Set E<VAR>g : E → ℂ<VAR>hg : AnalyticOn ℂ g U<VAR>hU : IsPreconnected U<GOAL>(∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<GOAL>(fun h => f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w - (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0] fun h => h ^ 2
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w : E<VAR>h4v : x + 4 • v ∈ interior s<VAR>h4w : x + 4 • w ∈ interior s<GOAL>(fun h => f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) - h ^ 2 • (f'' v) w) =o[𝓝[>] 0] fun h => h ^ 2
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w : E<VAR>h4v : x + 4 • v ∈ interior s<VAR>h4w : x + 4 • w ∈ interior s<GOAL>(f'' w) v = (f'' v) w
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>hne : (interior s).Nonempty<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w : E<GOAL>(f'' v) w = (f'' w) v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>x : E<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hx : HasFDerivAt f' f'' x<VAR>v w : E<GOAL>(f'' v) w = (f'' w) v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>x : E<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ (y : E), HasFDerivAt f (f' y) y<VAR>hx : HasFDerivAt f' f'' x<VAR>v w : E<GOAL>(f'' v) w = (f'' w) v
<VAR>C : Type w<VAR>CategoryTheory.Category.{v, w} C<VAR>X : Condensed C<GOAL>(𝟙 X).val = 𝟙 X.val
<VAR>C : Type w<VAR>CategoryTheory.Category.{v, w} C<VAR>X Y Z : Condensed C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).val = f.val ≫ g.val
<VAR>C : Type w<VAR>CategoryTheory.Category.{v, w} C<VAR>X Y : Condensed C<VAR>f g : X ⟶ Y<VAR>h : ∀ (S : CompHausᵒᵖ), f.val.app S = g.val.app S<GOAL>f = g
<VAR>X Y : CondensedSet<VAR>f : X ⟶ Y<VAR>S T : CompHausᵒᵖ<VAR>g : S ⟶ T<VAR>x : X.val.obj S<GOAL>f.val.app T (X.val.map g x) = Y.val.map g (f.val.app S x)
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>X : Condensed A<VAR>∀ (Y : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow Y profiniteToCompHaus.op) A<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology Profinite) (profiniteToCompHaus.op ⋙ X.val)
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>X : Condensed A<VAR>∀ (Y : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow Y Stonean.toCompHaus.op) A<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology Stonean) (Stonean.toCompHaus.op ⋙ X.val)
<VAR>C : Type w<VAR>CategoryTheory.Category.{v, w} C<VAR>X : LightCondensed C<GOAL>(𝟙 X).val = 𝟙 X.val
<VAR>C : Type w<VAR>CategoryTheory.Category.{v, w} C<VAR>X Y Z : LightCondensed C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).val = f.val ≫ g.val
<VAR>C : Type w<VAR>CategoryTheory.Category.{v, w} C<VAR>X Y : LightCondensed C<VAR>f g : X ⟶ Y<VAR>h : ∀ (S : LightProfiniteᵒᵖ), f.val.app S = g.val.app S<GOAL>f = g
<VAR>X Y : LightCondSet<VAR>f : X ⟶ Y<VAR>S T : LightProfiniteᵒᵖ<VAR>g : S ⟶ T<VAR>x : X.val.obj S<GOAL>f.val.app T (X.val.map g x) = Y.val.map g (f.val.app S x)
<VAR>R₁ R₂ : ℝ<VAR>c z : ℂ<VAR>f : ℂ → ℂ<VAR>hd : DifferentiableOn ℂ f (Metric.ball c R₁)<VAR>h_maps : Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂)<VAR>hz : z ∈ Metric.ball c R₁<GOAL>‖dslope f c z‖ ≤ R₂ / R₁