awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst_2 : ModularFormClass F Γ (↑k : ℤ)
hC :
  HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    C * (HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖)
hC' : 0 ≤ C
h_1 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
t : NNReal
h : τ.im = (↑t : ℝ)
ht : 0 < t
rw :
  max (t ^ k / ‖(↑(t ^ k) : ℝ)‖₊) ((1 / t) ^ k / ‖(↑(t ^ k) : ℝ)‖₊) =
    max (HPow.hPow (α := NNReal) (β := ℕ) 1 2) (HPow.hPow (β := ℕ) (1 / t ^ k) 2)
⊢ max t (1 / t) ^ k / ‖(↑(t ^ k) : ℝ)‖₊ = HPow.hPow (β := ℕ) (max 1 (1 / t ^ k)) 2

Tactic:
rw [(pow_left_mono k).map_max, (pow_left_mono 2).map_max, ← max_div_div_right (by positivity)]

Premises used: max_div_div_right, pow_left_mono, Monotone.map_max, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst_2 : ModularFormClass F Γ (↑k : ℤ)
hC :
  HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    C * (HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖)
hC' : 0 ≤ C
h_1 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
t : NNReal
h : τ.im = (↑t : ℝ)
ht : 0 < t
e_a : t ^ k / ‖(↑(t ^ k) : ℝ)‖₊ = HPow.hPow (α := NNReal) (β := ℕ) 1 2
e_a₁ : (1 / t) ^ k / ‖(↑(t ^ k) : ℝ)‖₊ = HPow.hPow (β := ℕ) (1 / t ^ k) 2
⊢ max (t ^ k / ‖(↑(t ^ k) : ℝ)‖₊) ((1 / t) ^ k / ‖(↑(t ^ k) : ℝ)‖₊) =
    max (HPow.hPow (α := NNReal) (β := ℕ) 1 2) (HPow.hPow (β := ℕ) (1 / t ^ k) 2)

Tactic:
congr
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst_2 : ModularFormClass F Γ (↑k : ℤ)
hC :
  HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    C * (HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖)
hC' : 0 ≤ C
h_1 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
t : NNReal
h : τ.im = (↑t : ℝ)
ht : 0 < t
⊢ t ^ k / ‖(↑(t ^ k) : ℝ)‖₊ = HPow.hPow (α := NNReal) (β := ℕ) 1 2

Tactic:
simp [field, ht.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst_2 : ModularFormClass F Γ (↑k : ℤ)
hC :
  HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    C * (HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖)
hC' : 0 ≤ C
h_1 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
t : NNReal
h : τ.im = (↑t : ℝ)
ht : 0 < t
⊢ (1 / t) ^ k / ‖(↑(t ^ k) : ℝ)‖₊ = HPow.hPow (β := ℕ) (1 / t ^ k) 2

Tactic:
simp [field, ht.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
⊢ 0 < h

Tactic:
have hh : 0 < h := Γ.strictWidthInfty_pos_iff.mpr Fact.out
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
⊢ NeZero h

Tactic:
have : NeZero h := ⟨hh.ne'⟩
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
e : ℝ
hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
⊢ h ∈ Γ.strictPeriods

Tactic:
have hΓ : h ∈ Γ.strictPeriods := Γ.strictWidthInfty_mem_strictPeriods
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
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
obtain :
  ∀ (C : ℝ) (Cpos : C > 0)
    (hC : IsBigOWith (E := ℂ) (F := ℝ) C (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)),
    IsBigO (E := ℂ) (F := ℝ) atTop
      (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
      fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) e
⊢ IsBigO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) e

Tactic:
obtain ⟨C, Cpos, hC⟩ := hF.exists_pos

Premises used: Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
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 : IsBigOWith (E := ℂ) (F := ℝ) C (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
rw :
  ∃ (c : ℝ),
    ∀ᶠ (x : ℕ) in atTop,
      norm (E := ℂ)
          ((PowerSeries.coeff x : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) : ℂ) ≤
        c * ‖HPow.hPow (α := ℝ) (↑x : ℝ) e‖
⊢ IsBigO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) e

Tactic:
rw [isBigO_iff]

Premises used: Asymptotics.isBigO_iff
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
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 : IsBigOWith (E := ℂ) (F := ℝ) C (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ τ.im ^ (-e)
⊢ ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖

Tactic:
rw [IsBigOWith, eventually_comap] at hC

Premises used: Asymptotics.IsBigOWith, Filter.eventually_comap
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
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)‖
h₁ :
  ∀ᶠ (x : ℕ) in atTop,
    norm (E := ℂ)
        ((PowerSeries.coeff x : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) : ℂ) ≤
      1 / Real.exp (-2 * Real.pi / h) * C * ‖HPow.hPow (α := ℝ) (↑x : ℝ) e‖
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : ℕ) in atTop,
      norm (E := ℂ)
          ((PowerSeries.coeff x : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) : ℂ) ≤
        c * ‖HPow.hPow (α := ℝ) (↑x : ℝ) e‖

Tactic:
use (1 / Real.exp (-2 * Real.pi / ↑h)) * C

Premises used: Real.pi, HMul.hMul, HDiv.hDiv, Real.exp, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
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)‖
h₁ :
  ∀ (n : ℕ) (hn : 0 < n)
    (hn' :
      ∀ (a : ℍ),
        a.im = ((fun (r : ℝ) ↦ r⁻¹) ∘ Nat.cast) n → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖),
    norm (E := ℂ)
        ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) : ℂ) ≤
      1 / Real.exp (-2 * Real.pi / h) * C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖
⊢ ∀ᶠ (x : ℕ) in atTop,
    norm (E := ℂ)
        ((PowerSeries.coeff x : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) : ℂ) ≤
      1 / Real.exp (-2 * Real.pi / h) * C * ‖HPow.hPow (α := ℝ) (↑x : ℝ) e‖

Tactic:
filter_upwards [eventually_gt_atTop 0,
    (tendsto_inv_atTop_zero.comp tendsto_natCast_atTop_atTop).eventually hC] with n hn hn'

Premises used: tendsto_inv_atTop_zero, tendsto_natCast_atTop_atTop, Filter.Tendsto.eventually, Filter.Tendsto.comp, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
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)‖
⊢ 0 < HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
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)‖
h₁ :
  norm (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‖
⊢ norm (E := ℂ)
      ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) : ℂ) ≤
    1 / Real.exp (-2 * Real.pi / h) * C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖

Tactic:
rw [ModularFormClass.qExpansion_coeff_eq_intervalIntegral (t := 1 / n) f hh hΓ _ (by positivity),
    ← intervalIntegral.integral_const_mul]

Premises used: ModularFormClass.qExpansion_coeff_eq_intervalIntegral, intervalIntegral.integral_const_mul
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
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)‖
h₁ :
  norm (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‖
⊢ norm (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:
simp only [ofReal_div, ofReal_one, ofReal_natCast]

Premises used: Complex.ofReal_one, Complex.ofReal_natCast, Complex.ofReal_div
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
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)‖
⊢ 0 ≤ h

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
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)‖
h₁ :
  ∫ (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‖
⊢ norm (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.norm_integral_le_integral_norm (by positivity) |>.trans ?_

Premises used: intervalIntegral.norm_integral_le_integral_norm, LE.le.trans
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : ModularFormClass F Γ k
f : F
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)‖
x : ℝ
⊢ 0 < ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I).im

Tactic:
simp [hn]
-- 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 := ⋯ : ℍ } : ℂ)‖
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑n : ℝ) e

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 : 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 := ⋯ : ℍ } : ℂ)‖
⊢ ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e

Tactic:
have hne : ‖(n : ℝ) ^ e‖ = n ^ e := Real.norm_of_nonneg (by 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 : 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 : ℝ
simp :
  1 / ‖h‖ *
      (1 / ‖𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I)‖ ^ n *
        norm (E := ℂ)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)) ≤
    1 / h * (1 / Real.exp (-2 * Real.pi / h) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e))
⊢ F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)

Tactic:
simp only [F, norm_mul, norm_div, norm_real, norm_one, norm_pow, mul_assoc]

Premises used: norm_pow, mul_assoc, NormOneClass.norm_one, norm_mul, Complex.norm_real, norm_div
-- 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 : ℝ
rw :
  1 / h *
      (1 / Real.exp ((↑n : ℝ) * (-2 * Real.pi * ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I).im / h)) *
        norm (E := ℂ)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)) ≤
    1 / h * (1 / Real.exp (-2 * Real.pi / h) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e))
⊢ 1 / ‖h‖ *
      (1 / ‖𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I)‖ ^ n *
        norm (E := ℂ)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)) ≤
    1 / h * (1 / Real.exp (-2 * Real.pi / h) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e))

Tactic:
rw [Real.norm_of_nonneg hh.le, Function.Periodic.norm_qParam, ← Real.exp_nat_mul]

Premises used: LT.lt.le, Function.Periodic.norm_qParam, Real.exp_nat_mul, Real.norm_of_nonneg
-- 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 : -2 * Real.pi / h ≤ (↑n : ℝ) * (-2 * Real.pi * ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I).im / h)
hbc₁ :
  norm (E := ℂ) ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ) ≤
    C * HPow.hPow (α := ℝ) (↑n : ℝ) e
⊢ 1 / h *
      (1 / Real.exp ((↑n : ℝ) * (-2 * Real.pi * ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I).im / h)) *
        norm (E := ℂ)
          ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)) ≤
    1 / h * (1 / Real.exp (-2 * Real.pi / h) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e))

Tactic:
gcongr
-- 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 : ℝ
⊢ -2 * Real.pi / h ≤ (↑n : ℝ) * (-2 * Real.pi * ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I).im / h)

Tactic:
simp [field]