ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>z : ℂ<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>HasSum (fun n => jacobiTheta₂'_term n z τ) (jacobiTheta₂' z τ)
<VAR>z : ℂ<VAR>τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>jacobiTheta₂ z τ = 0
<VAR>z : ℂ<VAR>τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>jacobiTheta₂_fderiv z τ = 0
<VAR>z : ℂ<VAR>τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>jacobiTheta₂' z τ = 0
<VAR>z : ℂ<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z : ℂ<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>ContinuousAt (fun p => jacobiTheta₂ p.1 p.2) (z, τ)
<VAR>z : ℂ<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>DifferentiableAt ℂ (fun x => jacobiTheta₂ x τ) z
<VAR>z : ℂ<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>DifferentiableAt ℂ (jacobiTheta₂ z) τ
<VAR>z : ℂ<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
<VAR>z : ℂ<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)
<VAR>z τ : ℂ<GOAL>jacobiTheta₂ (z + τ) τ = cexp (-↑π * Complex.I * (τ + 2 * z)) * jacobiTheta₂ z τ
<VAR>z τ : ℂ<GOAL>jacobiTheta₂' (z + 1) τ = jacobiTheta₂' z τ
<VAR>z τ : ℂ<GOAL>jacobiTheta₂' (z + τ) τ = cexp (-↑π * Complex.I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * Complex.I * jacobiTheta₂ z τ)
<VAR>z τ : ℂ<GOAL>jacobiTheta₂ z τ = 1 / (-Complex.I * τ) ^ (1 / 2) * cexp (-↑π * Complex.I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
<VAR>z τ : ℂ<GOAL>jacobiTheta₂' z τ = 1 / (-Complex.I * τ) ^ (1 / 2) * cexp (-↑π * Complex.I * z ^ 2 / τ) / τ * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * Complex.I * z * jacobiTheta₂ (z / τ) (-1 / τ))
<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>∫ (x : ℝ) in 0 ..1, bernoulliFun k x = 0
<VAR>k : ℕ<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>bernoulliFourierCoeff k n = 1 / (-2 * ↑π * Complex.I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * bernoulliFourierCoeff (k - 1) n)
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>n : ℤ<GOAL>bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * Complex.I * ↑n) ^ k
<VAR>k : ℕ<VAR>hk : k ≠ 1<GOAL>Continuous (periodizedBernoulli k)
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>n : ℤ<GOAL>fourierCoeff (Complex.ofReal' ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * Complex.I * ↑n) ^ k
<VAR>k : ℕ<VAR>hk : 2 ≤ k<GOAL>Summable fun n => -↑k ! / (2 * ↑π * Complex.I * ↑n) ^ k
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>x : ℝ<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HasSum (fun n => 1 / ↑n ^ k * (fourier n) ↑x) (-(2 * ↑π * Complex.I) ^ k / ↑k ! * ↑(bernoulliFun k x))
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>x : ℝ<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HasSum (fun n => 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x)) (-(2 * ↑π * Complex.I) ^ k / ↑k ! * ↑(bernoulliFun k x))
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>x : ℝ<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HasSum (fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x)) ((-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! * Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>x : ℝ<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x)) ((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! * Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
<GOAL>Polynomial.eval (1 / 4) (Polynomial.bernoulli 3) = 3 / 64
<VAR>s : ℂ<GOAL>HurwitzZeta.completedHurwitzZetaEven 0 s = completedRiemannZeta s
<VAR>s : ℂ<GOAL>HurwitzZeta.completedHurwitzZetaEven₀ 0 s = completedRiemannZeta₀ s
<VAR>s : ℂ<GOAL>HurwitzZeta.completedCosZeta 0 s = completedRiemannZeta s
<VAR>s : ℂ<GOAL>HurwitzZeta.completedCosZeta₀ 0 s = completedRiemannZeta₀ s
<GOAL>Differentiable ℂ completedRiemannZeta₀
<VAR>s : ℂ<VAR>hs : s ≠ 0<VAR>hs' : s ≠ 1<GOAL>DifferentiableAt ℂ completedRiemannZeta s
<GOAL>Filter.Tendsto (fun s => (s - 1) * completedRiemannZeta s) (𝓝[≠] 1) (𝓝 1)
<GOAL>HurwitzZeta.hurwitzZetaEven 0 = riemannZeta
<GOAL>HurwitzZeta.cosZeta 0 = riemannZeta
<GOAL>HurwitzZeta.hurwitzZeta 0 = riemannZeta
<GOAL>HurwitzZeta.expZeta 0 = riemannZeta
<VAR>s : ℂ<VAR>hs' : s ≠ 1<GOAL>DifferentiableAt ℂ riemannZeta s
<VAR>n : ℕ<GOAL>riemannZeta (-2 * (↑n + 1)) = 0
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>completedRiemannZeta s = ↑π ^ (-s / 2) * Complex.Gamma (s / 2) * ∑' (n : ℕ), 1 / ↑n ^ s
<GOAL>Filter.Tendsto (fun s => (s - 1) * riemannZeta s) (𝓝[≠] 1) (𝓝 1)
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<GOAL>LSeries.term (f + g) s = LSeries.term f s + LSeries.term g s
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<GOAL>LSeries.term (f + g) s n = LSeries.term f s n + LSeries.term g s n
<VAR>f : ℕ → ℂ<VAR>s : ℂ<GOAL>LSeries.term (-f) s = -LSeries.term f s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<GOAL>LSeries.term (-f) s n = -LSeries.term f s n
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>hf : LSeriesSummable f s<GOAL>LSeriesSummable (-f) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<GOAL>LSeriesSummable (-f) s ↔ LSeriesSummable f s
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<GOAL>LSeries.term (f - g) s = LSeries.term f s - LSeries.term g s
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<GOAL>LSeries.term (f - g) s n = LSeries.term f s n - LSeries.term g s n
<VAR>f : ℕ → ℂ<VAR>c s : ℂ<GOAL>LSeries.term (c • f) s = c • LSeries.term f s
<VAR>f : ℕ → ℂ<VAR>c s : ℂ<VAR>n : ℕ<GOAL>LSeries.term (c • f) s n = c * LSeries.term f s n
<VAR>f : ℕ → ℂ<VAR>c : ℂ<VAR>s a : ℂ<VAR>hf : LSeriesHasSum f s a<GOAL>LSeriesHasSum (c • f) s (c * a)
<VAR>f : ℕ → ℂ<VAR>c : ℂ<VAR>s : ℂ<VAR>hf : LSeriesSummable f s<GOAL>LSeriesSummable (c • f) s
<VAR>f : ℕ → ℂ<VAR>c s : ℂ<VAR>hc : c ≠ 0<GOAL>LSeriesSummable (c • f) s ↔ LSeriesSummable f s
<VAR>F : Type u_1<VAR>NormedField F<VAR>CompleteSpace F<VAR>f : ℕ →* F<VAR>hsum : Summable ⇑f<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>‖f p‖ < 1
<VAR>R : Type u_1<VAR>NormedCommRing R<GOAL>T0Space R
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖<VAR>s : Finset ℕ<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ Finset.filter Nat.Prime s, ∑' (n : ℕ), f (p ^ n))
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>s : Finset ℕ<GOAL>∏ p ∈ Finset.filter Nat.Prime s, ∑' (n : ℕ), f (p ^ n) = ∑' (m : ↑(Nat.factoredNumbers s)), f ↑m
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ℕ → R<VAR>hsum : Summable f<VAR>hf₀ : f 0 = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∃ N, ∀ (s : Finset ℕ), N.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(Nat.factoredNumbers s)), f ↑m‖ < ε
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖<VAR>N : ℕ<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n))
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>N : ℕ<GOAL>∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n) = ∑' (m : ↑N.smoothNumbers), f ↑m
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ℕ → R<VAR>hsum : Summable f<VAR>hf₀ : f 0 = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∃ N₀, ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑N.smoothNumbers), f ↑m‖ < ε
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<GOAL>HasProd (fun p => ∑' (e : ℕ), f (↑p ^ e)) (∑' (n : ℕ), f n)
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<GOAL>HasProd ({p | Nat.Prime p}.mulIndicator fun p => ∑' (e : ℕ), f (p ^ e)) (∑' (n : ℕ), f n)
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<GOAL>Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) Filter.atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<GOAL>∏' (p : Nat.Primes), ∑' (e : ℕ), f (↑p ^ e) = ∑' (n : ℕ), f n
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hsum : Summable fun x => ‖f x‖<GOAL>HasProd (fun p => ∑' (e : ℕ), f (↑p ^ e)) (∑' (n : ℕ), f n)
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hsum : Summable fun x => ‖f x‖<GOAL>Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) Filter.atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>R : Type u_1<VAR>NormedCommRing R<VAR>CompleteSpace R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hsum : Summable fun x => ‖f x‖<GOAL>∏' (p : Nat.Primes), ∑' (e : ℕ), f (↑p ^ e) = ∑' (n : ℕ), f n
<VAR>F : Type u_1<VAR>NormedField F<VAR>CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hsum : Summable fun x => ‖f x‖<GOAL>(1 - f p)⁻¹ = ∑' (e : ℕ), f (p ^ e)
<VAR>F : Type u_1<VAR>NormedField F<VAR>CompleteSpace F<VAR>f : ℕ →* F<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1<VAR>s : Finset ℕ<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ Finset.filter Nat.Prime s, (1 - f p)⁻¹)
<VAR>F : Type u_1<VAR>NormedField F<VAR>CompleteSpace F<VAR>f : ℕ →* F<VAR>hsum : Summable ⇑f<VAR>s : Finset ℕ<GOAL>∏ p ∈ Finset.filter Nat.Prime s, (1 - f p)⁻¹ = ∑' (m : ↑(Nat.factoredNumbers s)), f ↑m
<VAR>F : Type u_1<VAR>NormedField F<VAR>CompleteSpace F<VAR>f : ℕ →* F<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1<VAR>N : ℕ<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ N.primesBelow, (1 - f p)⁻¹)
<VAR>F : Type u_1<VAR>NormedField F<VAR>CompleteSpace F<VAR>f : ℕ →* F<VAR>hsum : Summable ⇑f<VAR>N : ℕ<GOAL>∏ p ∈ N.primesBelow, (1 - f p)⁻¹ = ∑' (m : ↑N.smoothNumbers), f ↑m
<VAR>F : Type u_1<VAR>NormedField F<VAR>CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>hsum : Summable fun x => ‖f x‖<GOAL>HasProd (fun p => (1 - f ↑p)⁻¹) (∑' (n : ℕ), f n)
<VAR>F : Type u_1<VAR>NormedField F<VAR>CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>hsum : Summable fun x => ‖f x‖<GOAL>∏' (p : Nat.Primes), (1 - f ↑p)⁻¹ = ∑' (n : ℕ), f n
<VAR>F : Type u_1<VAR>NormedField F<VAR>CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>hsum : Summable fun x => ‖f x‖<GOAL>Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) Filter.atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>n : ℕ<GOAL>Polynomial.bernoulli n = ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial i) (bernoulli (n - i) * ↑(n.choose i))
<VAR>n : ℕ<GOAL>Polynomial.eval 0 (Polynomial.bernoulli n) = bernoulli n
<VAR>n : ℕ<GOAL>Polynomial.eval 1 (Polynomial.bernoulli n) = bernoulli' n
<VAR>k : ℕ<GOAL>Polynomial.derivative (Polynomial.bernoulli (k + 1)) = (↑k + 1) * Polynomial.bernoulli k
<VAR>k : ℕ<GOAL>Polynomial.derivative (Polynomial.bernoulli k) = ↑k * Polynomial.bernoulli (k - 1)
<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range (n + 1), ↑((n + 1).choose k) • Polynomial.bernoulli k = (Polynomial.monomial n) (↑n + 1)
<VAR>n : ℕ<GOAL>↑n.succ • Polynomial.bernoulli n = (Polynomial.monomial n) ↑n.succ - ∑ k ∈ Finset.range n, ↑((n + 1).choose k) • Polynomial.bernoulli k
<VAR>n p : ℕ<GOAL>(↑p + 1) * ∑ k ∈ Finset.range n, ↑k ^ p = Polynomial.eval (↑n) (Polynomial.bernoulli p.succ) - bernoulli p.succ
<VAR>n p : ℕ<GOAL>Polynomial.eval (↑n) (Polynomial.bernoulli p.succ) = bernoulli p.succ + (↑p + 1) * ∑ k ∈ Finset.range n, ↑k ^ p
<VAR>n : ℕ<VAR>x : ℚ<GOAL>Polynomial.eval (1 + x) (Polynomial.bernoulli n) = Polynomial.eval x (Polynomial.bernoulli n) + ↑n * x ^ (n - 1)
<VAR>A : Type u_1<VAR>CommRing A<VAR>Algebra ℚ A<VAR>t : A<GOAL>(PowerSeries.mk fun n => (Polynomial.aeval t) ((1 / ↑n !) • Polynomial.bernoulli n)) * (PowerSeries.exp A - 1) = PowerSeries.X * (PowerSeries.rescale t) (PowerSeries.exp A)
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<GOAL>LSeries.term f s n = if n = 0 then 0 else f n / ↑n ^ s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<GOAL>LSeries.term f s 0 = 0
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>f : ℕ → ℂ<VAR>s : ℂ<GOAL>LSeries.term f s n = f n / ↑n ^ s
<VAR>f g : ℕ → ℂ<VAR>h : ∀ {n : ℕ}, n ≠ 0 → f n = g n<VAR>s : ℂ<VAR>n : ℕ<GOAL>LSeries.term f s n = LSeries.term g s n
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<GOAL>‖LSeries.term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<VAR>h : ‖f n‖ ≤ ‖g n‖<GOAL>‖LSeries.term f s n‖ ≤ ‖LSeries.term g s n‖
<VAR>f : ℕ → ℂ<VAR>s s' : ℂ<VAR>h : s.re ≤ s'.re<VAR>n : ℕ<GOAL>‖LSeries.term f s' n‖ ≤ ‖LSeries.term f s n‖
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>h : ∀ {n : ℕ}, n ≠ 0 → f n = g n<GOAL>LSeries f s = LSeries g s
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>h : ∀ {n : ℕ}, n ≠ 0 → f n = g n<GOAL>LSeriesSummable f s ↔ LSeriesSummable g s
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>h : f =ᶠ[Filter.atTop] g<VAR>hf : LSeriesSummable f s<GOAL>LSeriesSummable g s
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>h : f =ᶠ[Filter.atTop] g<GOAL>LSeriesSummable f s ↔ LSeriesSummable g s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<GOAL>¬LSeriesSummable f s → LSeries f s = 0
<VAR>f : ℕ → ℂ<VAR>s a : ℂ<VAR>h : LSeriesHasSum f s a<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>s a : ℂ<VAR>h : LSeriesHasSum f s a<GOAL>LSeries f s = a
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<GOAL>LSeriesHasSum f s (LSeries f s)
<VAR>f : ℕ → ℂ<VAR>s a : ℂ<GOAL>LSeriesHasSum f s a ↔ LSeriesSummable f s ∧ LSeries f s = a
<VAR>f : ℕ → ℂ<VAR>s s' : ℂ<VAR>h : s.re = s'.re<GOAL>LSeriesSummable f s ↔ LSeriesSummable f s'
<VAR>s : ℂ<VAR>n : ℕ<GOAL>LSeries.term LSeries.delta s n = if n = 1 then 1 else 0
<VAR>f : ℕ → ℂ<GOAL>f * LSeries.delta = f 1 • LSeries.delta
<VAR>f : ℕ → ℂ<VAR>h : f 1 = 1<GOAL>f * LSeries.delta = LSeries.delta
<VAR>f : ℕ → ℂ<GOAL>LSeries.delta * f = f 1 • LSeries.delta
<VAR>f : ℕ → ℂ<VAR>h : f 1 = 1<GOAL>LSeries.delta * f = LSeries.delta
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<GOAL>∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<GOAL>f =O[Filter.atTop] fun n => ↑n ^ s.re
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>h : f =O[Filter.atTop] fun n => ↑n ^ (x - 1)<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>m : ℝ<VAR>h : ∀ (n : ℕ), n ≠ 0 → Complex.abs (f n) ≤ m<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>LSeriesSummable f ↑s
<VAR>f g : ℕ → ℂ<VAR>h : ∀ {n : ℕ}, n ≠ 0 → f n = g n<GOAL>LSeries.abscissaOfAbsConv f = LSeries.abscissaOfAbsConv g
<VAR>f g : ℕ → ℂ<VAR>h : f =ᶠ[Filter.atTop] g<GOAL>LSeries.abscissaOfAbsConv f = LSeries.abscissaOfAbsConv g
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>hs : LSeries.abscissaOfAbsConv f < ↑s.re<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>hs : LSeries.abscissaOfAbsConv f < ↑s.re<GOAL>∃ x < s.re, LSeriesSummable f ↑x
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<GOAL>LSeries.abscissaOfAbsConv f ≤ ↑s.re
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y<GOAL>LSeries.abscissaOfAbsConv f ≤ ↑x
<VAR>f : ℕ → ℂ<VAR>x : EReal<VAR>h : ∀ (y : ℝ), x < ↑y → LSeriesSummable f ↑y<GOAL>LSeries.abscissaOfAbsConv f ≤ x
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ x<GOAL>LSeries.abscissaOfAbsConv f ≤ ↑x + 1
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : f =O[Filter.atTop] fun n => ↑n ^ x<GOAL>LSeries.abscissaOfAbsConv f ≤ ↑x + 1
<VAR>f : ℕ → ℂ<VAR>h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C<GOAL>LSeries.abscissaOfAbsConv f ≤ 1
<VAR>f : ℕ → ℂ<VAR>h : f =O[Filter.atTop] 1<GOAL>LSeries.abscissaOfAbsConv f ≤ 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x y : S<VAR>h : ↑(Algebra.adjoin R {x}) = ↑(Algebra.adjoin R {y})<GOAL>conductor R x = conductor R y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<GOAL>↑(conductor R x) ⊆ ↑(Algebra.adjoin R {x})
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x y : S<GOAL>y ∈ conductor R x ↔ ∀ (b : S), y * b ∈ Algebra.adjoin R {x}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>h : Algebra.adjoin R {x} = ⊤<GOAL>conductor R x = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>pb : PowerBasis R S<GOAL>conductor R pb.gen = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>L : Type u_3<VAR>CommRing L<VAR>Algebra S L<VAR>Algebra R L<VAR>IsScalarTower R S L<VAR>NoZeroSMulDivisors S L<VAR>x : S<VAR>y : L<GOAL>y ∈ IsLocalization.coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ Algebra.adjoin R {(algebraMap S L) x}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>p : R<VAR>z : S<VAR>hp : p ∈ Ideal.comap (algebraMap R S) (conductor R x)<VAR>hz' : z ∈ Ideal.map (algebraMap R S) I<GOAL>(algebraMap R S) p * z ∈ ⇑(algebraMap (↥(Algebra.adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>h_alg : Function.Injective ⇑(algebraMap (↥(Algebra.adjoin R {x})) S)<GOAL>Ideal.comap (algebraMap (↥(Algebra.adjoin R {x})) S) (Ideal.map (algebraMap R S) I) = Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>h_alg : Function.Injective ⇑(algebraMap (↥(Algebra.adjoin R {x})) S)<VAR>a : ↥(Algebra.adjoin R {x})<GOAL>(quotAdjoinEquivQuotMap hx h_alg) ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I)) a) = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ↑a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>IsDomain R<VAR>IsIntegrallyClosed R<VAR>IsDedekindDomain S<VAR>NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : IsIntegral R x<VAR>J : Ideal S<VAR>hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I)<GOAL>multiplicity J (Ideal.map (algebraMap R S) I) = multiplicity (↑((KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>IsDomain R<VAR>IsIntegrallyClosed R<VAR>IsDedekindDomain S<VAR>NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : IsIntegral R x<GOAL>UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I) = Multiset.map (fun f => ↑((KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f)) (UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>IsDomain R<VAR>IsIntegrallyClosed R<VAR>IsDedekindDomain S<VAR>NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : IsIntegral R x<VAR>hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>Irreducible (Ideal.map (algebraMap R S) I)
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.hurwitzZetaEven a s = (HurwitzZeta.hurwitzZeta a s + HurwitzZeta.hurwitzZeta (-a) s) / 2
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.hurwitzZetaOdd a s = (HurwitzZeta.hurwitzZeta a s - HurwitzZeta.hurwitzZeta (-a) s) / 2
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 1<GOAL>DifferentiableAt ℂ (HurwitzZeta.hurwitzZeta a) s
<VAR>a : ℝ<VAR>ha : a ∈ Set.Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => 1 / (↑n + ↑a) ^ s) (HurwitzZeta.hurwitzZeta (↑a) s)
<VAR>a : UnitAddCircle<GOAL>Filter.Tendsto (fun s => (s - 1) * HurwitzZeta.hurwitzZeta a s) (𝓝[≠] 1) (𝓝 1)
<VAR>a : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => HurwitzZeta.hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) 1
<VAR>a : UnitAddCircle<GOAL>Filter.Tendsto (fun s => HurwitzZeta.hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (HurwitzZeta.hurwitzZeta a 1))
<VAR>a b : UnitAddCircle<GOAL>Differentiable ℂ fun s => HurwitzZeta.hurwitzZeta a s - HurwitzZeta.hurwitzZeta b s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.cosZeta a s = (HurwitzZeta.expZeta a s + HurwitzZeta.expZeta (-a) s) / 2
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.sinZeta a s = (HurwitzZeta.expZeta a s - HurwitzZeta.expZeta (-a) s) / (2 * Complex.I)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => cexp (2 * ↑π * Complex.I * ↑a * ↑n) / ↑n ^ s) (HurwitzZeta.expZeta (↑a) s)
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 1 ∨ a ≠ 0<GOAL>DifferentiableAt ℂ (HurwitzZeta.expZeta a) s
<VAR>a : UnitAddCircle<VAR>ha : a ≠ 0<GOAL>Differentiable ℂ (HurwitzZeta.expZeta a)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesHasSum (fun x => cexp (2 * ↑π * Complex.I * ↑a * ↑x)) s (HurwitzZeta.expZeta (↑a) s)
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>hs' : a ≠ 0 ∨ s ≠ 1<GOAL>HurwitzZeta.hurwitzZeta a (1 - s) = (2 * ↑π) ^ (-s) * Complex.Gamma s * (cexp (-↑π * Complex.I * s / 2) * HurwitzZeta.expZeta a s + cexp (↑π * Complex.I * s / 2) * HurwitzZeta.expZeta (-a) s)
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ 1 - ↑n<GOAL>HurwitzZeta.expZeta a (1 - s) = (2 * ↑π) ^ (-s) * Complex.Gamma s * (cexp (↑π * Complex.I * s / 2) * HurwitzZeta.hurwitzZeta a s + cexp (-↑π * Complex.I * s / 2) * HurwitzZeta.hurwitzZeta (-a) s)
<VAR>R : Type u<VAR>CommRing R<VAR>Fintype R<VAR>R' : Type v<VAR>CommRing R'<VAR>χ : MulChar R R'<VAR>ψ : AddChar R R'<VAR>a : Rˣ<GOAL>χ ↑a * gaussSum χ (ψ.mulShift ↑a) = gaussSum χ ψ
<VAR>R : Type u<VAR>Field R<VAR>Fintype R<VAR>R' : Type v<VAR>CommRing R'<VAR>IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<VAR>ψ : AddChar R R'<VAR>b : R<GOAL>∑ a : R, χ (a * b⁻¹) * ψ (a - b) = ∑ c : R, χ c * ψ (b * (c - 1))
<VAR>R : Type u<VAR>Field R<VAR>Fintype R<VAR>R' : Type v<VAR>CommRing R'<VAR>IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<GOAL>gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card R)
<VAR>R : Type u<VAR>Field R<VAR>Fintype R<VAR>R' : Type v<VAR>CommRing R'<VAR>IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<GOAL>gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
<VAR>R : Type u<VAR>CommRing R<VAR>Fintype R<VAR>R' : Type v<VAR>CommRing R'<VAR>p : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>hch : CharP R' p<VAR>χ : MulChar R R'<VAR>ψ : AddChar R R'<GOAL>gaussSum χ ψ ^ p = gaussSum (χ ^ p) (ψ ^ p)
<VAR>R : Type u<VAR>CommRing R<VAR>Fintype R<VAR>R' : Type v<VAR>CommRing R'<VAR>p : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>hch : CharP R' p<VAR>hp : IsUnit ↑p<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>ψ : AddChar R R'<GOAL>gaussSum χ ψ ^ p = χ ↑p * gaussSum χ ψ
<VAR>R : Type u<VAR>CommRing R<VAR>Fintype R<VAR>R' : Type v<VAR>CommRing R'<VAR>p : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>hch : CharP R' p<VAR>n : ℕ<VAR>hp : IsUnit ↑p<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>ψ : AddChar R R'<GOAL>gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ
<VAR>R : Type u<VAR>CommRing R<VAR>Fintype R<VAR>R' : Type v<VAR>CommRing R'<VAR>IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>ψ : AddChar R R'<VAR>p n : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>hch : CharP R' p<VAR>hp : IsUnit ↑p<VAR>hp' : p ≠ 2<VAR>hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)<GOAL>(χ (-1) * ↑(Fintype.card R)) ^ (p ^ n / 2) = χ (↑p ^ n)
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>F' : Type u_2<VAR>Field F'<VAR>Fintype F'<VAR>χ : MulChar F F'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>hch₁ : ringChar F' ≠ ringChar F<VAR>hch₂ : ringChar F' ≠ 2<GOAL>(χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = χ ↑(Fintype.card F')