ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>x : ℤ_[p]<VAR>a b : ℤ<VAR>ha : x - ↑a ∈ Ideal.span {↑p ^ n}<VAR>hb : x - ↑b ∈ Ideal.span {↑p ^ n}<GOAL>↑a = ↑b
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>x : ℤ_[p]<VAR>a b : ℕ<VAR>ha : x - ↑a ∈ Ideal.span {↑p ^ n}<VAR>hb : x - ↑b ∈ Ideal.span {↑p ^ n}<GOAL>↑a = ↑b
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>m n : ℕ<VAR>hm : x - ↑m ∈ LocalRing.maximalIdeal ℤ_[p]<VAR>hn : x - ↑n ∈ LocalRing.maximalIdeal ℤ_[p]<GOAL>↑m = ↑n
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<GOAL>∃ n < p, x - ↑n ∈ LocalRing.maximalIdeal ℤ_[p]
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<GOAL>x.zmodRepr < p ∧ x - ↑x.zmodRepr ∈ LocalRing.maximalIdeal ℤ_[p]
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<GOAL>x.zmodRepr < p
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<GOAL>x - ↑x.zmodRepr ∈ LocalRing.maximalIdeal ℤ_[p]
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<GOAL>x - (PadicInt.toZMod x).cast ∈ LocalRing.maximalIdeal ℤ_[p]
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<GOAL>RingHom.ker PadicInt.toZMod = LocalRing.maximalIdeal ℤ_[p]
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>n : ℕ<GOAL>x.appr n < p ^ n
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<GOAL>Monotone x.appr
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>p ^ m ∣ x.appr n - x.appr m
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>x : ℤ_[p]<GOAL>x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>RingHom.ker (PadicInt.toZModPow n) = Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>(ZMod.castHom ⋯ (ZMod (p ^ m))).comp (PadicInt.toZModPow n) = PadicInt.toZModPow m
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>x : ℤ_[p]<GOAL>((PadicInt.toZModPow n) x).cast = (PadicInt.toZModPow m) x
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<GOAL>DenseRange Nat.cast
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<GOAL>DenseRange Int.cast
<VAR>p : ℕ<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<GOAL>PadicInt.nthHom f 0 = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>i j : ℕ<VAR>h : i ≤ j<GOAL>↑p ^ i ∣ PadicInt.nthHom f r j - PadicInt.nthHom f r i
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<GOAL>IsCauSeq (padicNorm p) fun n => ↑(PadicInt.nthHom f r n)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<GOAL>PadicInt.nthHomSeq f_compat 1 ≈ 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<GOAL>PadicInt.nthHomSeq f_compat (r + s) ≈ PadicInt.nthHomSeq f_compat r + PadicInt.nthHomSeq f_compat s
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<GOAL>PadicInt.nthHomSeq f_compat (r * s) ≈ PadicInt.nthHomSeq f_compat r * PadicInt.nthHomSeq f_compat s
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℝ<GOAL>0 < ε → ∃ N, ∀ n ≥ N, ‖PadicInt.limNthHom f_compat r - ↑(PadicInt.nthHom f r n)‖ < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<GOAL>PadicInt.limNthHom f_compat 0 = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<GOAL>PadicInt.limNthHom f_compat 1 = 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<GOAL>PadicInt.limNthHom f_compat (r + s) = PadicInt.limNthHom f_compat r + PadicInt.limNthHom f_compat s
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<GOAL>PadicInt.limNthHom f_compat (r * s) = PadicInt.limNthHom f_compat r * PadicInt.limNthHom f_compat s
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>n : ℕ<GOAL>(PadicInt.lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>n : ℕ<GOAL>(PadicInt.toZModPow n).comp (PadicInt.lift f_compat) = f n
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>g : R →+* ℤ_[p]<VAR>hg : ∀ (n : ℕ), (PadicInt.toZModPow n).comp g = f n<GOAL>PadicInt.lift f_compat = g
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<GOAL>(PadicInt.lift ⋯) z = z
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>x y : ℤ_[p]<GOAL>(∀ (n : ℕ), (PadicInt.toZModPow n) x = (PadicInt.toZModPow n) y) ↔ x = y
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>g g' : R →+* ℤ_[p]<GOAL>(∀ (n : ℕ), (PadicInt.toZModPow n).comp g = (PadicInt.toZModPow n).comp g') ↔ g = g'
<VAR>a x : ℝ<GOAL>↑(HurwitzZeta.evenKernel (↑a) x) = cexp (-↑π * ↑a ^ 2 * ↑x) * jacobiTheta₂ (↑a * Complex.I * ↑x) (Complex.I * ↑x)
<VAR>a : UnitAddCircle<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>HurwitzZeta.evenKernel a x = 0
<VAR>a x : ℝ<GOAL>↑(HurwitzZeta.cosKernel (↑a) x) = jacobiTheta₂ (↑a) (Complex.I * ↑x)
<VAR>a : UnitAddCircle<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>HurwitzZeta.cosKernel a x = 0
<GOAL>HurwitzZeta.evenKernel 0 = HurwitzZeta.cosKernel 0
<VAR>a : UnitAddCircle<VAR>x : ℝ<GOAL>HurwitzZeta.evenKernel (-a) x = HurwitzZeta.evenKernel a x
<VAR>a : UnitAddCircle<VAR>x : ℝ<GOAL>HurwitzZeta.cosKernel (-a) x = HurwitzZeta.cosKernel a x
<VAR>a : UnitAddCircle<GOAL>ContinuousOn (HurwitzZeta.evenKernel a) (Set.Ioi 0)
<VAR>a : UnitAddCircle<GOAL>ContinuousOn (HurwitzZeta.cosKernel a) (Set.Ioi 0)
<VAR>a : UnitAddCircle<VAR>x : ℝ<GOAL>HurwitzZeta.evenKernel a x = 1 / x ^ (1 / 2) * HurwitzZeta.cosKernel a (1 / x)
<VAR>a : ℝ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => rexp (-π * (↑n + a) ^ 2 * t)) (HurwitzZeta.evenKernel (↑a) t)
<VAR>a : ℝ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => cexp (2 * ↑π * Complex.I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) ↑(HurwitzZeta.cosKernel (↑a) t)
<VAR>a : ℝ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (HurwitzZeta.evenKernel (↑a) t - if ↑a = 0 then 1 else 0)
<VAR>a : ℝ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => if n = 0 then 0 else cexp (2 * ↑π * Complex.I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(HurwitzZeta.cosKernel (↑a) t) - 1)
<VAR>a : ℝ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => 2 * Real.cos (2 * π * a * (↑n + 1)) * rexp (-π * (↑n + 1) ^ 2 * t)) (HurwitzZeta.cosKernel (↑a) t - 1)
<VAR>a : UnitAddCircle<GOAL>∃ p, 0 < p ∧ (fun x => HurwitzZeta.evenKernel a x - if a = 0 then 1 else 0) =O[Filter.atTop] fun x => rexp (-p * x)
<VAR>a : UnitAddCircle<GOAL>∃ p, 0 < p ∧ (fun x => HurwitzZeta.cosKernel a x - 1) =O[Filter.atTop] fun x => rexp (-p * x)
<GOAL>(HurwitzZeta.hurwitzEvenFEPair 0).symm = HurwitzZeta.hurwitzEvenFEPair 0
<VAR>a : UnitAddCircle<GOAL>HurwitzZeta.hurwitzEvenFEPair (-a) = HurwitzZeta.hurwitzEvenFEPair a
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedHurwitzZetaEven a s = HurwitzZeta.completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedCosZeta a s = HurwitzZeta.completedCosZeta₀ a s - 1 / s - (if a = 0 then 1 else 0) / (1 - s)
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedHurwitzZetaEven (-a) s = HurwitzZeta.completedHurwitzZetaEven a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedHurwitzZetaEven₀ (-a) s = HurwitzZeta.completedHurwitzZetaEven₀ a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedCosZeta (-a) s = HurwitzZeta.completedCosZeta a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedCosZeta₀ (-a) s = HurwitzZeta.completedCosZeta₀ a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedHurwitzZetaEven a (1 - s) = HurwitzZeta.completedCosZeta a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedHurwitzZetaEven₀ a (1 - s) = HurwitzZeta.completedCosZeta₀ a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedCosZeta a (1 - s) = HurwitzZeta.completedHurwitzZetaEven a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedCosZeta₀ a (1 - s) = HurwitzZeta.completedHurwitzZetaEven₀ a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 0 ∨ a ≠ 0<VAR>hs' : s ≠ 1<GOAL>DifferentiableAt ℂ (HurwitzZeta.completedHurwitzZetaEven a) s
<VAR>a : UnitAddCircle<GOAL>Differentiable ℂ (HurwitzZeta.completedHurwitzZetaEven₀ a)
<VAR>a b : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => HurwitzZeta.completedHurwitzZetaEven a s - HurwitzZeta.completedHurwitzZetaEven b s) 1
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 0<VAR>hs' : s ≠ 1 ∨ a ≠ 0<GOAL>DifferentiableAt ℂ (HurwitzZeta.completedCosZeta a) s
<VAR>a : UnitAddCircle<GOAL>Differentiable ℂ (HurwitzZeta.completedCosZeta₀ a)
<VAR>a : ℂ<GOAL>Filter.Tendsto (fun s => s / 2) (𝓝[≠] a) (𝓝[≠] (a / 2))
<VAR>a : UnitAddCircle<GOAL>Filter.Tendsto (fun s => (s - 1) * HurwitzZeta.completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)
<VAR>a : UnitAddCircle<GOAL>Filter.Tendsto (fun s => s * HurwitzZeta.completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
<VAR>a : UnitAddCircle<GOAL>Filter.Tendsto (fun s => s * HurwitzZeta.completedCosZeta a s) (𝓝[≠] 0) (𝓝 (-1))
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => s.Gammaℝ * cexp (2 * ↑π * Complex.I * ↑a * ↑n) / ↑|n| ^ s / 2) (HurwitzZeta.completedCosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (HurwitzZeta.completedCosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => s.Gammaℝ / ↑|↑n + a| ^ s / 2) (HurwitzZeta.completedHurwitzZetaEven (↑a) s)
<VAR>Λ : ℂ → ℂ<VAR>hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s<VAR>L : ℂ<VAR>h_lim : Filter.Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)<VAR>s : ℂ<VAR>hs' : s ≠ 1<GOAL>DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>h : a ≠ 0 ∨ s ≠ 0<GOAL>HurwitzZeta.hurwitzZetaEven a s = HurwitzZeta.completedHurwitzZetaEven a s / s.Gammaℝ
<VAR>a : UnitAddCircle<GOAL>HurwitzZeta.hurwitzZetaEven a 0 = if a = 0 then -1 / 2 else 0
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.hurwitzZetaEven (-a) s = HurwitzZeta.hurwitzZetaEven a s
<VAR>a : UnitAddCircle<VAR>n : ℕ<GOAL>HurwitzZeta.hurwitzZetaEven a (-2 * (↑n + 1)) = 0
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs' : s ≠ 1<GOAL>DifferentiableAt ℂ (HurwitzZeta.hurwitzZetaEven a) s
<VAR>a : UnitAddCircle<GOAL>Filter.Tendsto (fun s => (s - 1) * HurwitzZeta.hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)
<VAR>a : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => HurwitzZeta.hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1
<VAR>a : UnitAddCircle<GOAL>Filter.Tendsto (fun s => HurwitzZeta.hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (HurwitzZeta.hurwitzZetaEven a 1))
<VAR>a b : UnitAddCircle<GOAL>Differentiable ℂ fun s => HurwitzZeta.hurwitzZetaEven a s - HurwitzZeta.hurwitzZetaEven b s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => 1 / ↑|↑n + a| ^ s / 2) (HurwitzZeta.hurwitzZetaEven (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => (1 / ↑|↑n + a| ^ s + 1 / ↑|↑n + 1 - a| ^ s) / 2) (HurwitzZeta.hurwitzZetaEven (↑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 + 1 / (↑n + 1 - ↑a) ^ s) / 2) (HurwitzZeta.hurwitzZetaEven (↑a) s)
<VAR>a : UnitAddCircle<GOAL>HurwitzZeta.cosZeta a 0 = -1 / 2
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.cosZeta (-a) s = HurwitzZeta.cosZeta a s
<VAR>a : UnitAddCircle<VAR>n : ℕ<GOAL>HurwitzZeta.cosZeta a (-2 * (↑n + 1)) = 0
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs' : s ≠ 1 ∨ a ≠ 0<GOAL>DifferentiableAt ℂ (HurwitzZeta.cosZeta a) s
<VAR>a : UnitAddCircle<VAR>ha : a ≠ 0<GOAL>Differentiable ℂ (HurwitzZeta.cosZeta a)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => cexp (2 * ↑π * Complex.I * ↑a * ↑n) / ↑|n| ^ s / 2) (HurwitzZeta.cosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (HurwitzZeta.cosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesHasSum (fun x => ↑(Real.cos (2 * π * a * ↑x))) s (HurwitzZeta.cosZeta (↑a) s)
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>hs' : a ≠ 0 ∨ s ≠ 1<GOAL>HurwitzZeta.hurwitzZetaEven a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.cos (↑π * s / 2) * HurwitzZeta.cosZeta a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ 1 - ↑n<GOAL>HurwitzZeta.cosZeta a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.cos (↑π * s / 2) * HurwitzZeta.hurwitzZetaEven a s
<VAR>Fq F : Type<VAR>Field Fq<VAR>Fintype Fq<VAR>Field F<VAR>Algebra (Polynomial Fq) F<VAR>Algebra (RatFunc Fq) F<VAR>IsScalarTower (Polynomial Fq) (RatFunc Fq) F<VAR>FunctionField Fq F<VAR>Algebra.IsSeparable (RatFunc Fq) F<GOAL>FunctionField.classNumber Fq F = 1 ↔ IsPrincipalIdealRing ↥(FunctionField.ringOfIntegers Fq F)
<VAR>R : Type u_1<VAR>EuclideanDomain R<VAR>abv : AbsoluteValue R ℤ<VAR>self : abv.IsAdmissible<VAR>n : ℕ<VAR>ε : ℝ<GOAL>0 < ε → ∀ {b : R}, b ≠ 0 → ∀ (A : Fin n → R), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε
<VAR>R : Type u_1<VAR>EuclideanDomain R<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_2<VAR>Finite ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : R<VAR>hb : b ≠ 0<VAR>A : ι → R<VAR>h : abv.IsAdmissible<GOAL>∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε
<VAR>R : Type u_1<VAR>EuclideanDomain R<VAR>abv : AbsoluteValue R ℤ<VAR>n : ℕ<VAR>h : abv.IsAdmissible<VAR>ε : ℝ<VAR>_hε : 0 < ε<VAR>b : R<VAR>_hb : b ≠ 0<VAR>A : Fin (h.card ε ^ n).succ → Fin n → R<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
<VAR>R : Type u_1<VAR>EuclideanDomain R<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_2<VAR>Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : R<VAR>hb : b ≠ 0<VAR>h : abv.IsAdmissible<VAR>A : Fin (h.card ε ^ Fintype.card ι).succ → ι → R<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>x y : ℤ_[p]<GOAL>‖Polynomial.eval x F - Polynomial.eval y F‖ ≤ ‖x - y‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>ncs : CauSeq ℤ_[p] norm<GOAL>Filter.Tendsto (fun i => Polynomial.eval (↑ncs i) F) Filter.atTop (𝓝 (Polynomial.eval ncs.lim F))
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>ncs : CauSeq ℤ_[p] norm<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>ncs_der_val : ∀ (n : ℕ), ‖Polynomial.eval (↑ncs n) (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖<GOAL>Filter.Tendsto (fun i => ‖Polynomial.eval (↑ncs i) (Polynomial.derivative F)‖) Filter.atTop (𝓝 ‖Polynomial.eval a (Polynomial.derivative F)‖)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>ncs : CauSeq ℤ_[p] norm<VAR>F : Polynomial ℤ_[p]<GOAL>Filter.Tendsto (fun i => ‖Polynomial.eval (↑ncs i) (Polynomial.derivative F)‖) Filter.atTop (𝓝 ‖Polynomial.eval ncs.lim (Polynomial.derivative F)‖)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>ncs : CauSeq ℤ_[p] norm<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>ncs_der_val : ∀ (n : ℕ), ‖Polynomial.eval (↑ncs n) (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖<GOAL>‖Polynomial.eval ncs.lim (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>ncs : CauSeq ℤ_[p] norm<VAR>F : Polynomial ℤ_[p]<VAR>hnorm : Filter.Tendsto (fun i => ‖Polynomial.eval (↑ncs i) F‖) Filter.atTop (𝓝 0)<GOAL>Filter.Tendsto (fun i => Polynomial.eval (↑ncs i) F) Filter.atTop (𝓝 0)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>ncs : CauSeq ℤ_[p] norm<VAR>F : Polynomial ℤ_[p]<VAR>hnorm : Filter.Tendsto (fun i => ‖Polynomial.eval (↑ncs i) F‖) Filter.atTop (𝓝 0)<GOAL>Polynomial.eval ncs.lim F = 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>0 < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 ≠ 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>‖Polynomial.eval a (Polynomial.derivative F)‖ ≠ 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>0 < ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>Polynomial.eval a (Polynomial.derivative F) ≠ 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<GOAL>T_gen p F a = ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>T_gen p F a < 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<GOAL>0 ≤ T_gen p F a
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>n : ℕ<GOAL>0 ≤ T_gen p F a ^ n
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>T_gen p F a ^ n < 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>n : ℕ<GOAL>T_gen p F a ^ 2 ^ n < 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>ih_gen 0 a
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>n : ℕ<VAR>z : ℤ_[p]<VAR>hz : ih_gen n z<GOAL>‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (Polynomial.derivative F))‖ ≤ 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>z z' z1 : ℤ_[p]<VAR>hz' : z' = z - z1<VAR>hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>n : ℕ<VAR>hz : ih_gen n z<GOAL>‖Polynomial.eval z' (Polynomial.derivative F) - Polynomial.eval z (Polynomial.derivative F)‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>n : ℕ<GOAL>‖Polynomial.eval (newton_seq_gen hnorm n) (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>n : ℕ<GOAL>‖Polynomial.eval (newton_seq_gen hnorm n) F‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>n : ℕ<GOAL>‖newton_seq_gen hnorm (n + 1) - newton_seq_gen hnorm n‖ = ‖Polynomial.eval (newton_seq_gen hnorm n) F‖ / ‖Polynomial.eval (newton_seq_gen hnorm n) (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>n : ℕ<GOAL>‖newton_seq_gen hnorm (n + 1) - newton_seq_gen hnorm n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>T_gen p F a > 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n : ℕ<GOAL>‖newton_seq_gen hnorm (n + 2) - newton_seq_gen hnorm (n + 1)‖ < ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>n k : ℕ<GOAL>‖newton_seq_gen hnorm (n + k) - newton_seq_gen hnorm n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>n k : ℕ<VAR>hnk : n ≤ k<GOAL>‖newton_seq_gen hnorm k - newton_seq_gen hnorm n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n : ℕ<GOAL>0 < n → ‖newton_seq_gen hnorm n - a‖ = ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>Filter.Tendsto (fun n => ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) Filter.atTop (𝓝 0)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>ε : ℝ<GOAL>ε > 0 → ∃ N, ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>Filter.Tendsto (fun n => ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) Filter.atTop (𝓝 0)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>IsCauSeq norm (newton_seq_gen hnorm)