awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F_1 : Type u_2
inst_1 : FunLike F_1 ℍ ℂ
inst_2 : ModularFormClass F_1 Γ k
f : F_1
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    ‖1 / (↑h : ℂ) *
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
x : ℝ
⊢ { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ }.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n

Tactic:
simp [← UpperHalfPlane.coe_im]

Premises used: UpperHalfPlane.coe_im
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F_1 : Type u_2
inst_1 : FunLike F_1 ℍ ℂ
inst_2 : ModularFormClass F_1 Γ k
f : F_1
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    ‖1 / (↑h : ℂ) *
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
x : ℝ
hbc :
  C * ‖{ coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ }.im ^ (-e)‖ ≤
    C * HPow.hPow (α := ℝ) (↑n : ℝ) e
⊢ norm (E := ℂ) ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ) ≤
    C * HPow.hPow (α := ℝ) (↑n : ℝ) e

Tactic:
grw [hn' _ (by simp [← UpperHalfPlane.coe_im])]
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F_1 : Type u_2
inst_1 : FunLike F_1 ℍ ℂ
inst_2 : ModularFormClass F_1 Γ k
f : F_1
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    ‖1 / (↑h : ℂ) *
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
x : ℝ
⊢ C * ‖{ coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ }.im ^ (-e)‖ ≤
    C * HPow.hPow (α := ℝ) (↑n : ℝ) e

Tactic:
simp [← UpperHalfPlane.coe_im, Real.rpow_neg_eq_inv_rpow, hne]

Premises used: Real.rpow_neg_eq_inv_rpow, UpperHalfPlane.coe_im
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F_1 : Type u_2
inst_1 : FunLike F_1 ℍ ℂ
inst_2 : ModularFormClass F_1 Γ k
f : F_1
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    ‖1 / (↑h : ℂ) *
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
⊢ ∀ (x : ℝ), F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)

Tactic:
have (x : ℝ) : F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / ↑h)) * (C * n ^ e) := by
    simp only [F, norm_mul, norm_div, norm_real, norm_one, norm_pow, mul_assoc]
    rw [Real.norm_of_nonneg hh.le, Function.Periodic.norm_qParam, ← Real.exp_nat_mul]
    gcongr
    · simp [field]
    · grw [hn' _ (by simp [← UpperHalfPlane.coe_im])]
      simp [← UpperHalfPlane.coe_im, Real.rpow_neg_eq_inv_rpow, hne]
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F_1 : Type u_2
inst_1 : FunLike F_1 ℍ ℂ
inst_2 : ModularFormClass F_1 Γ k
f : F_1
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this_1 : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    ‖1 / (↑h : ℂ) *
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
this : ∀ (x : ℝ), F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)
⊢ 0 ≤ h

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F_1 : Type u_2
inst_1 : FunLike F_1 ℍ ℂ
inst_2 : ModularFormClass F_1 Γ k
f : F_1
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this_1 : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    ‖1 / (↑h : ℂ) *
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
this : ∀ (x : ℝ), F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)
h₁ : IntervalIntegrable F MeasureTheory.volume 0 h
h₂ :
  IntervalIntegrable (ε := ℝ)
    (fun (i : ℝ) ↦ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)) MeasureTheory.volume
    0 h
h₃ :
  ∫ (u : ℝ) in 0..h, 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e) =
    1 / Real.exp (-2 * Real.pi / h) * C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖
⊢ ∫ (x : ℝ) in 0..h,
      ‖1 / (↑h : ℂ) *
          HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
            ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖ ≤
    1 / Real.exp (-2 * Real.pi / h) * C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖

Tactic:
refine (intervalIntegral.integral_mono (by positivity) ?_ ?_ this).trans (le_of_eq ?_)

Premises used: intervalIntegral.integral_mono, LE.le.trans, le_of_eq
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F_1 : Type u_2
inst_1 : FunLike F_1 ℍ ℂ
inst_2 : ModularFormClass F_1 Γ k
f : F_1
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this_1 : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    ‖1 / (↑h : ℂ) *
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
this : ∀ (x : ℝ), F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)
h₁ : Continuous F
⊢ IntervalIntegrable F MeasureTheory.volume 0 h

Tactic:
apply Continuous.intervalIntegrable

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F_1 : Type u_2
inst_1 : FunLike F_1 ℍ ℂ
inst_2 : ModularFormClass F_1 Γ k
f : F_1
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this_1 : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    ‖1 / (↑h : ℂ) *
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
this : ∀ (x : ℝ), F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)
⊢ ∀ (x : ℝ), 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n ≠ 0

Tactic:
simp [Function.Periodic.qParam_ne_zero]

Premises used: Function.Periodic.qParam_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F_1 : Type u_2
inst_1 : FunLike F_1 ℍ ℂ
inst_2 : ModularFormClass F_1 Γ k
f : F_1
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this_1 : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    ‖1 / (↑h : ℂ) *
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
this : ∀ (x : ℝ), F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)
funProp : ∀ (x : ℝ), 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n ≠ 0
⊢ Continuous F

Tactic:
fun_prop (disch := simp [Function.Periodic.qParam_ne_zero])

Premises used: Function.Periodic.qParam_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F_1 : Type u_2
inst_1 : FunLike F_1 ℍ ℂ
inst_2 : ModularFormClass F_1 Γ k
f : F_1
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this_1 : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    ‖1 / (↑h : ℂ) *
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
this : ∀ (x : ℝ), F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)
⊢ IntervalIntegrable (ε := ℝ)
    (fun (i : ℝ) ↦ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)) MeasureTheory.volume
    0 h

Tactic:
continuous_const.intervalIntegrable ..

Premises used: continuous_const, Continuous.intervalIntegrable
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F_1 : Type u_2
inst_1 : FunLike F_1 ℍ ℂ
inst_2 : ModularFormClass F_1 Γ k
f : F_1
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this_1 : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    ‖1 / (↑h : ℂ) *
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
this : ∀ (x : ℝ), F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)
⊢ IntervalIntegrable (ε := ℝ)
    (fun (i : ℝ) ↦ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)) MeasureTheory.volume
    0 h

Tactic:
exact continuous_const.intervalIntegrable ..

Premises used: continuous_const, Continuous.intervalIntegrable
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F_1 : Type u_2
inst_1 : FunLike F_1 ℍ ℂ
inst_2 : ModularFormClass F_1 Γ k
f : F_1
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this_1 : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    ‖1 / (↑h : ℂ) *
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
this : ∀ (x : ℝ), F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)
⊢ ∫ (u : ℝ) in 0..h, 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e) =
    1 / Real.exp (-2 * Real.pi / h) * C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖

Tactic:
simp [field, intervalIntegral.integral_const, hne]

Premises used: intervalIntegral.integral_const
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
simp :
  IsBigO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (↑k : ℝ)
⊢ IsBigO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
simp only [← Real.rpow_intCast]

Premises used: Real.rpow_intCast
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
hF :
  IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦
    HPow.hPow (β := ℝ) τ.im (-(↑k : ℝ))
⊢ IsBigO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (↑k : ℝ)

Tactic:
apply qExpansion_coeff_isBigO_of_norm_isBigO

Premises used: qExpansion_coeff_isBigO_of_norm_isBigO
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
hF :
  ∀ (C : ℝ) (hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)),
    IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦
      HPow.hPow (β := ℝ) τ.im (-(↑k : ℝ))
⊢ IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦
    HPow.hPow (β := ℝ) τ.im (-(↑k : ℝ))

Tactic:
obtain ⟨C, hC⟩ := exists_bound hk f

Premises used: ModularFormClass.exists_bound
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)
hF : ∃ (c : ℝ), ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ c * ‖a.im ^ (-k)‖
⊢ IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦
    HPow.hPow (β := ℝ) τ.im (-(↑k : ℝ))

Tactic:
simp_rw [IsBigO, ← Int.cast_neg, Real.rpow_intCast, IsBigOWith, eventually_comap]

Premises used: Int.cast_neg, Asymptotics.IsBigOWith, Asymptotics.IsBigO, Filter.eventually_comap, Real.rpow_intCast
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)
h : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-k)‖
⊢ ∃ (c : ℝ), ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ c * ‖a.im ^ (-k)‖

Tactic:
use C
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)
h : ∀ (τ : ℍ) (hτ : τ.im ≤ 1), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * ‖τ.im ^ (-k)‖
⊢ ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-k)‖

Tactic:
filter_upwards [eventually_le_nhds zero_lt_one] with _ hτ τ rfl

Premises used: zero_lt_one, eventually_le_nhds, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * ‖τ.im ^ (-k)‖

Tactic:
(hC τ).trans (le_of_eq ?_)

Premises used: LE.le.trans, le_of_eq
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
h : C * max 1 (1 / τ.im ^ k) = C * ‖τ.im ^ (-k)‖
⊢ norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * ‖τ.im ^ (-k)‖

Tactic:
refine (hC τ).trans (le_of_eq ?_)

Premises used: LE.le.trans, le_of_eq
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ 0 ≤ (τ.im ^ k)⁻¹

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
h : 1 ≤ 1 / τ.im ^ k
⊢ C * max 1 (1 / τ.im ^ k) = C * ‖τ.im ^ (-k)‖

Tactic:
rw [max_eq_right, zpow_neg, Real.norm_of_nonneg (by positivity), one_div]

Premises used: max_eq_right, zpow_neg, one_div, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ 0 < τ.im ^ k

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ 1 ≤ 1 / τ.im ^ k

Tactic:
exact one_le_one_div (by positivity) (zpow_le_one₀ τ.im_pos hτ hk)

Premises used: UpperHalfPlane.im_pos, zpow_le_one₀, one_le_one_div
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : CuspFormClass F Γ k
f : F
hF :
  ∀ (C : ℝ) (hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2),
    IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦
      τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
⊢ IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦
    τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)

Tactic:
obtain ⟨C, hC⟩ := exists_bound f

Premises used: CuspFormClass.exists_bound
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
⊢ IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦
    τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)

Tactic:
isBigO_of_le' (c := C) _ fun τ ↦ (hC τ).trans (of_eq ?_)

Premises used: Asymptotics.isBigO_of_le', of_eq, LE.le.trans