mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
⊢ ⇑(f.pow n) = ⇑f ^ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
⊢ (PowerSeries.coeff 0) (qExpansion h f) = valueAtInfty f

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
⊢ ⟨n • k, GradedMonoid.GMonoid.gnpow n f⟩ = ⟨↑n * k, f.pow n⟩

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
⊢ (DirectSum.of (ModularForm Γ) k) f ^ n = (DirectSum.of (ModularForm Γ) (↑n * k)) (f.pow n)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
⊢ ∀ i ∈ s, MDiff ⇑(F i).toSlashInvariantForm

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
⊢ ?m.56 ∈ ball 0 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
⊢ HasSum (fun m ↦ (PowerSeries.coeff m) (qExpansion h f) • q ^ m) (cuspFunction h f q)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
γ : GL (Fin 2) ℝ
hγ : γ • OnePoint.infty = c✝
⊢ IsBoundedAtImInfty ((SlashInvariantForm.prod m hm fun i ↦ { toFun := ⇑(F i), slash_action_eq' := ⋯ }).toFun ∣[m] γ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: ι : Type
s : Finset ι
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
F : ι → ModularForm Γ k
⊢ ↑s.card * k = ∑ i ∈ s, k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
τ : ℍ
⊢ HasSum (fun m ↦ (PowerSeries.coeff m) (qExpansion h f) • 𝕢 h ↑τ ^ m) (f τ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |↑(Matrix.GeneralLinearGroup.det g)|
hD : ↑D ≠ 0
j : ℂ := denom g ↑τ
⊢ ↑D ^ (k - 2 + k) * (starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) *
      (↑τ.im ^ k * ↑(Complex.normSq j) ^ (-k)) =
    ↑D ^ (k - 2) * ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * (↑D * ↑τ.im / ↑(Complex.normSq j)) ^ k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
m : ℕ
⊢ (qExpansionFormalMultilinearSeries h f).coeff m = (PowerSeries.coeff m) (qExpansion h ⇑f)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
m : ℕ
⊢ ‖qExpansionFormalMultilinearSeries h f m‖ = ‖(PowerSeries.coeff m) (qExpansion h ⇑f)‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ IsBoundedAtImInfty ((SlashInvariantForm.translate f g).toFun ∣[k] γ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |↑(Matrix.GeneralLinearGroup.det g)|
hD : ↑D ≠ 0
j : ℂ := denom g ↑τ
⊢ ↑D ^ (k - 2) * ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * (↑D * ↑τ.im / ↑(Complex.normSq j)) ^ k) =
    ↑D ^ (k - 2) * ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * ↑(g • τ).im ^ k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |↑(Matrix.GeneralLinearGroup.det g)|
hD : ↑D ≠ 0
j : ℂ := denom g ↑τ
⊢ ↑D ^ (k - 2) * ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * ↑(g • τ).im ^ k) =
    ↑D ^ (k - 2) * (σ g) (petersson k f f' (g • τ))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
r : NNReal
hr : ↑r < 1
⊢ ‖↑↑r‖ < 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
⊢ 1 ≤ (qExpansionFormalMultilinearSeries h f).radius

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ IsZeroAtImInfty ((ModularForm.translate f g).toFun ∣[k] γ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
⊢ petersson k (f ∣[k] g) (f' ∣[k] g) τ =
    ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 2) * (σ g) (petersson k f f' (g • τ))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ?m.1
F : Sort ?u.11
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : Γ.IsArithmetic
⊢ IsCusp ∞ Γ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
h1 : 0 < (Periodic.invQParam h q).im
τ : ℍ := { coe := Periodic.invQParam h q, coe_im_pos := h1 }
h2 : Periodic.cuspFunction h (f ∘ ↑ofComplex) q = (f ∘ ↑ofComplex) (Periodic.invQParam h q)
⊢ cuspFunction h f q = f τ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
g : SL(2, ℤ)
τ : ℍ
⊢ petersson k (f ∣[k] g) (f' ∣[k] g) τ = petersson k f f' (g • τ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
τ : ℍ
⊢ petersson k f' f τ = (starRingEnd ℂ) (petersson k f f' τ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
τ : ℍ
⊢ ‖petersson k f' f τ‖ = ‖petersson k f f' τ‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ Tendsto (fun g ↦ (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
⊢ HasSum (fun m ↦ c m • q ^ m) (cuspFunction h f q)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
h : Int.cast ∘ p = 0
⊢ p = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
⊢ ↑(p 0) * ↑z + ↑(p 1) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ toGL ((map (Int.castRingHom ℝ)) g) • ∞ = (mapGL ℝ) g • ∞

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ IsBoundedAtImInfty (⇑f ∣[k] g)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
r : NNReal
hr : ↑r < 1
hr' : ↑r ≠ 0
this : FiniteDimensional ℝ ℂ := Module.Basis.finiteDimensional_of_finite basisOneI
⊢ ‖↑↑r‖ < 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
⊢ ‖petersson k (⇑f) (⇑f') (g • τ)‖ = ‖petersson k (⇑f) (⇑f') τ‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
⊢ petersson k (⇑f) (⇑f') (g • τ) = petersson k (⇑f) (⇑f') τ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hp : IsCoprime (↑g 1 0) (↑g 1 1)
nonZ1 : ↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2 ≠ 0
this : Int.cast ∘ ↑g 1 ≠ 0
nonZ2 : ↑(↑g 1 0) * ↑z + ↑(↑g 1 1) ≠ 0
⊢ ↑z * ↑(↑g 1 0) + ↑(↑g 1 1) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : CuspFormClass F Γ k
⊢ toGL ((map (Int.castRingHom ℝ)) g) • ∞ = (mapGL ℝ) g • ∞

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : CuspFormClass F Γ k
⊢ IsZeroAtImInfty (⇑f ∣[k] g)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
τ : ℍ
⊢ τ.im ^ t ≠ 0

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
⊢ ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
⊢ ∃ E_1, ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E_1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
⊢ ↑(g • z) =
    ↑((lcRow0 p) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) +
      (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : Tendsto (fun g ↦ (↑g • z).re) cofinite (cocompact ℝ)
⊢ Tendsto (fun g ↦ |(↑g • z).re|) cofinite atTop

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
⊢ HasFPowerSeriesOnBall (update (cuspFunction h f) 0 (c 0)) (FormalMultilinearSeries.ofScalars ℂ c) 0 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
⊢ f = fun τ ↦ update (cuspFunction h f) 0 (c 0) (𝕢 h ↑τ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
⊢ ∃ a > 0, petersson k ⇑f ⇑f' =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
hfeq : f = fun τ ↦ update (cuspFunction h f) 0 (c 0) (𝕢 h ↑τ)
⊢ Tendsto f atImInfty (𝓝 (c 0))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
⊢ IsBoundedAtImInfty f

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
f' : F'
h_bd : IsZeroAtImInfty ⇑f'
⊢ ∃ a > 0, petersson k ⇑f ⇑f' =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ Tendsto (fun g ↦ |(↑g • z).re|) cofinite atTop

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℍ → E
hf : ∃ c > 0, f =O[atImInfty] fun τ ↦ Real.exp (-c * τ.im)
⊢ IsZeroAtImInfty f

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℍ → E
hf : ∃ c > 0, f =O[atImInfty] fun τ ↦ Real.exp (-c * τ.im)
⊢ IsZeroAtImInfty f

Tactic:
by
  obtain ⟨a, ha, ha'⟩ := hf
  refine ha'.trans_tendsto <| (Real.tendsto_exp_atBot.comp ?_).comp tendsto_comap
  exact tendsto_id.const_mul_atTop_of_neg (neg_lt_zero.mpr ha)

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

Goal state before:
pp: E✝ : Type u_1
inst✝ : SeminormedAddCommGroup E✝
f : ℍ → E✝
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : y ≤ τ.im
⊢ 0 ≤ τ.im ^ t

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
H1 : HasFPowerSeriesOnBall (update (cuspFunction h f) 0 (c 0)) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
L1 : ContinuousAt (update (cuspFunction h f) 0 (c 0)) 0
L2 : ContinuousAt (cuspFunction h f) 0
⊢ update (cuspFunction h f) 0 (c 0) =ᶠ[𝓝[≠] 0] cuspFunction h f

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
τ : ℍ
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
hdenom : ‖denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1
⊢ ‖f τ‖ ≤ ‖f (γ • τ)‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this✝ : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = ↑UpperHalfPlane.I ^ k * c
h2I2 : c = ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^ k * c
this : 2 ^ k = 1 ↔ k = 0
⊢ k = 0 ∨ c = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
H1 : HasFPowerSeriesOnBall (update (cuspFunction h f) 0 (c 0)) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
⊢ c 0 = cuspFunction h f 0

Tactic:
by

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

Goal state before:
pp: E✝ : Type u_1
inst✝ : SeminormedAddCommGroup E✝
f : ℍ → E✝
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : τ.im ≤ y
⊢ 0 < τ.im ^ t

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = ↑UpperHalfPlane.I ^ k * c
h2I2 : c = ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^ k * c
⊢ 2 ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
⊢ HasFPowerSeriesOnBall (cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
⊢ k = 0 ∨ c = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
⊢ (Matrix.SpecialLinearGroup.mapGL ℝ).range =
    Subgroup.closure
      {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
        Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
h𝒮ℒ :
  (Matrix.SpecialLinearGroup.mapGL ℝ).range =
    Subgroup.closure
      {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
        Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}
g : GL (Fin 2) ℝ
hg :
  g ∈
    {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
      Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}
⊢ f ∣[k] g = f

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
⊢ ∀ (γ : SL(2, ℤ)), f ∣[k] γ = f

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: ⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
hq : 0 ∈ Metric.ball 0 1
⊢ ‖0‖ ≤ rexp (-π)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
g : { g // ↑g 1 = cd }
hg : ∀ (a : { g // ↑g 1 = cd }), |(↑g • z).re| ≤ |(↑a • z).re|
g1 : SL(2, ℤ)
hg1 : ↑↑g 1 = ↑g1 1
⊢ g1 ∈ (fun g ↦ ↑g 1) ⁻¹' {cd}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ∃ g, ↑g 1 = cd ∧ ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
ξ : ℍ
hξ : 1 / 2 ≤ ξ.im
hξ₂ : ‖f { coe := invQParam 1 q, coe_im_pos := ⋯ }‖ ≤ ‖f ξ‖
⊢ ‖UpperHalfPlane.cuspFunction 1 (⇑f) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) (𝕢 1 ↑ξ)‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
⊢ ↑(T ^ n • z) = ↑z + ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
⊢ (T ^ n • z).re = z.re + ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
⊢ (T ^ n • z).im = z.im

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
⊢ Set.EqOn (UpperHalfPlane.cuspFunction 1 ⇑f) (Function.const ℂ (UpperHalfPlane.cuspFunction 1 (⇑f) 0))
    (Metric.ball 0 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
⊢ (T • z).re = z.re + 1

Tactic:
by

Goal state after: