Theorems · Theorem · number theory

EisensteinSeries.summand_bound_of_mem_verticalStrip

∀ {z : UpperHalfPlane} {k : ℝ},
  0 ≤ k →
    ∀ (x : Fin 2 → ℤ) {A B : ℝ} (hB : 0 < B),
      z ∈ UpperHalfPlane.verticalStrip A B →
        ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤
          EisensteinSeries.r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-k) * ‖x‖ ^ (-k)

Defined in

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Cited by

2 results in Mathlib

Foundations

Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound