mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r : ℝ
⊢ (fun x ↦ P.f_modif x - 0) =O[atTop] fun x ↦ x ^ r

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ
this✝ : Summable fun x ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 2⁻¹ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha : 0 ≤ 0
⊢ (fun t ↦
      rexp (-π * (0 ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + 0 * rexp (-π * 0 ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
    fun t ↦ rexp (-π * t)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 0 < 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ) ↔ 0 < τ.im

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ EqOn (fun x ↦ P.f_modif x - P.f x + P.f₀)
    (((Ioo 0 1).indicator fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) + {1}.indicator fun x ↦ P.f₀ - P.f 1) (Ioi 0)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
⊢ -1 < (s - 1).re

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s) (mellin F s)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
⊢ ∃ p, 0 < p ∧ F_nat 1 a =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
⊢ -1 < (s - ↑P.k - 1).re

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
⊢ 0 ≤ ↑n + a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑x ^ (s - 1) • (fun x ↦ P.f_modif x - P.f x + P.f₀) x =
    ↑x ^ (s - 1) •
      ((Ioo 0 1).indicator (fun t ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
⊢ f_int k a t (Int.ofNat n) = f_nat k a t n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ ↑(Int.negSucc n) + a = -(↑n + (1 - a))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 0 ≤ 2 * π * ↑|n|

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ ∫ (x : ℝ) in Ioi 0,
      ↑x ^ (s - 1) •
        ((Ioo 0 1).indicator (fun t ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x) =
    ∫ (x : ℝ) in Ioi 0, ↑x ^ (s - 1) • (Ioo 0 1).indicator (fun t ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : ↑(Int.negSucc n) + a = -(↑n + (1 - a))
⊢ 0 ≤ ↑n + (1 - a)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂'_term x z τ) ↔ 0 < τ.im

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
i : ι
⊢ a' i = 0 ∨ 0 < p i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂ z τ = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂_fderiv z τ = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
i : ι
t : ℝ
⊢ (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' z τ = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ -↑(m + 1) + a = -(↑m + (1 - a))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ ∫ (x : ℝ) in Ioi 0, ↑x ^ (s - 1) • (Ioo 0 1).indicator (fun t ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x =
    ∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1) • (P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable (f_int k a t)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
⊢ IsOpen V

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
⊢ IsPreconnected V

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
⊢ F_int k (↑a) t = F_nat k a t + F_nat k (1 - a) t

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t ↦ F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t ↦ F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-q * t)
⊢ 1 - a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
n : ℤ
p : ℂ × ℂ
hp : p ∈ V
⊢ 0 ≤ 3 * π * ↑|n| ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ ∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1) • (P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) =
    ∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
⊢ Summable fun i ↦ ‖a' i‖ / p i ^ s.re

Tactic:
refine h_sum.of_norm_bounded (fun i ↦ ?_)

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
⊢ ‖‖a' i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
⊢ ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t ↦ F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t ↦ F_nat 0 (1 - a) t) =O[atTop] fun t ↦ rexp (-q * t)
⊢ (fun t ↦ F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t ↦
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
h✝ : p i = 0
⊢ ‖‖0‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re

Tactic:
simp only [norm_zero, zero_div]

Goal state after:
case pos
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
h✝ : p i = 0
⊢ 0 ≤ ‖a i‖ / p i ^ s.re
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_int 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this✝ : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
h✝ : ¬p i = 0
this : 0 ≤ p i
⊢ 0 ≤ ‖a i‖ / p i ^ s.re

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
⊢ Summable u

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t ↦ rexp (-q * t)
⊢ F_int 1 ↑a =ᶠ[atTop] fun t ↦ F_nat 1 a t + F_nat 1 (1 - a) t

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
⊢ Summable fun n ↦ f n (z, τ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ ∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀ =
    (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1)) • P.f₀ - P.ε • (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - ↑P.k - 1)) • P.g₀

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (x y : ℂ × ℂ →L[ℂ] ℂ), (x + y) (1, 0) = x (1, 0) + y (1, 0)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
⊢ 0 < (s / 2).re

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (m : ℂ) (x : ℂ × ℂ →L[ℂ] ℂ), (m • x) (1, 0) = (RingHom.id ℂ) m • x (1, 0)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ F_int 1 a =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f ↦ f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasSum (fun n ↦ (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f ↦ f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 : HasSum (fun n ↦ (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0))
n : ℤ
⊢ (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x ξ : ℝ
⊢ cexp (-↑π * I * (I * ↑x + 2 * (↑ξ * I * ↑x))) = ↑(rexp (π * (x + 2 * ξ * x)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a x : ℝ
⊢ ↑(evenKernel (↑a) x) = cexp (-↑π * ↑a ^ 2 * ↑x) * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ (I * ↑x).im ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ evenKernel a x = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a x : ℝ
⊢ ↑(cosKernel (↑a) x) = jacobiTheta₂ (↑a) (I * ↑x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: x : ℝ
hx : x ≤ 0
z✝ : ℝ
⊢ (I * ↑x).im ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1)) • P.f₀ - P.ε • (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - ↑P.k - 1)) • P.g₀ =
    (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ HasDerivAt (fun x ↦ jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ cosKernel a x = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: ⊢ evenKernel 0 = cosKernel 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ evenKernel (-a) x = evenKernel a x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
⊢ mellin (fun x ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ cosKernel (-a) x = cosKernel a x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a' x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x ↦ cexp (-↑π * ↑a' ^ 2 * ↑x)) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ P.Λ₀ s = P.Λ s + (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a' x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < (I * ↑x).im

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ P.symm.Λ₀ s = P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / (↑P.k - s)) • P.f₀

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a' x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun u ↦ (↑a' * I * ↑u, I * ↑u)) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
⊢ ContinuousOn (evenKernel a) (Ioi 0)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a' x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun u ↦ (↑a', I * ↑u)) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
⊢ ContinuousOn (cosKernel a) (Ioi 0)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n ↦ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
⊢ Summable u

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ P.Λ s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
⊢ I * ↑(1 / x) = -1 / (I * ↑x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
⊢ ↑a * I * ↑x / (I * ↑x) = ↑a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
⊢ HasMellin (fun x ↦ P.f x - P.f₀) s (P.Λ s)

Tactic:
by

Goal state after: