awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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 :
  ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)
⊢ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C * max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))
have hC' : 0 ≤ C
Tactic: have hC' : 0 ≤ C := le_trans (by positivity) <| (div_le_iff₀ (by positivity)).mpr hC
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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 :
  ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)
hC' : 0 ≤ C
⊢ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C * max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))
have h : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
Tactic: have h : 0 < ‖(τ.im : ℂ) ^ (k : ℤ)‖ := mod_cast norm_pos_iff.mpr (pow_ne_zero _ τ.im_ne_zero)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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 :
  ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)
hC' : 0 ≤ C
h : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
⊢ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C * max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))
have hC₁ : HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
  C * (HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖)
Tactic: rw [petersson, norm_mul, norm_mul, Complex.norm_conj, ← sq, ← le_div_iff₀ h, mul_div_assoc] at hC
Cleared hypotheses: hC, hC', h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
⊢ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C * max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))
have rw : HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
  C * HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))) 2
Tactic: rw [← sq_le_sq₀ (by positivity) (by positivity), mul_pow, sq_sqrt hC']
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
⊢ HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    C * HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))) 2
have refine : HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖ =
  HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))) 2
Tactic: refine hC.trans (congrArg (C * ·) ?_).le
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
⊢ HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖ =
    HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))) 2
have generalize : ∀ (t : ℝ) (h : τ.im = t),
  HPow.hPow (β := ℤ) (max t (1 / t)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑t : ℂ) (↑k : ℤ)‖ =
    HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) t (↑k : ℤ))) 2
Tactic: generalize h : τ.im = t
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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 : ℝ
h : τ.im = t
⊢ HPow.hPow (β := ℤ) (max t (1 / t)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑t : ℂ) (↑k : ℤ)‖ =
    HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) t (↑k : ℤ))) 2
have ht : 0 < t
Tactic: have ht : 0 < t := h ▸ τ.im_pos
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 : ℝ
h : τ.im = t
ht : 0 < t
⊢ HPow.hPow (β := ℤ) (max t (1 / t)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑t : ℂ) (↑k : ℤ)‖ =
    HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) t (↑k : ℤ))) 2
have lift : ∀ (t : NNReal) (h : τ.im = (↑t : ℝ)) (ht : 0 < (↑t : ℝ)),
  HPow.hPow (β := ℤ) (max (↑t : ℝ) (1 / (↑t : ℝ))) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑(↑t : ℝ) : ℂ) (↑k : ℤ)‖ =
    HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) (↑t : ℝ) (↑k : ℤ))) 2
Tactic: lift t to NNReal using ht.le
Cleared hypotheses: t, h, ht
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 : ℝ)
⊢ HPow.hPow (β := ℤ) (max (↑t : ℝ) (1 / (↑t : ℝ))) (↑k : ℤ) / (↑‖HPow.hPow (β := ℤ) (↑(↑t : ℝ) : ℂ) (↑k : ℤ)‖₊ : ℝ) =
    HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) (↑t : ℝ) (↑k : ℤ))) 2
have norm_cast : ∀ (ht : 0 < t), max t (1 / t) ^ k / ‖(↑(t ^ k) : ℝ)‖₊ = HPow.hPow (β := ℕ) (max 1 (1 / t ^ k)) 2
Tactic: norm_cast at ⊢ ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
⊢ max t (1 / t) ^ k / ‖(↑(t ^ k) : ℝ)‖₊ = HPow.hPow (β := ℕ) (max 1 (1 / t ^ k)) 2
have rw : max (t ^ k / ‖(↑(t ^ k) : ℝ)‖₊) ((1 / t) ^ k / ‖(↑(t ^ k) : ℝ)‖₊) =
  max (HPow.hPow (α := NNReal) (β := ℕ) 1 2) (HPow.hPow (β := ℕ) (1 / t ^ k) 2)
Tactic: rw [(pow_left_mono k).map_max, (pow_left_mono 2).map_max, ← max_div_div_right (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
⊢ max (t ^ k / ‖(↑(t ^ k) : ℝ)‖₊) ((1 / t) ^ k / ‖(↑(t ^ k) : ℝ)‖₊) =
    max (HPow.hPow (α := NNReal) (β := ℕ) 1 2) (HPow.hPow (β := ℕ) (1 / t ^ k) 2)
have e_a : t ^ k / ‖(↑(t ^ k) : ℝ)‖₊ = HPow.hPow (α := NNReal) (β := ℕ) 1 2
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
⊢ max (t ^ k / ‖(↑(t ^ k) : ℝ)‖₊) ((1 / t) ^ k / ‖(↑(t ^ k) : ℝ)‖₊) =
    max (HPow.hPow (α := NNReal) (β := ℕ) 1 2) (HPow.hPow (β := ℕ) (1 / t ^ k) 2)
have e_a₁ : (1 / t) ^ k / ‖(↑(t ^ k) : ℝ)‖₊ = HPow.hPow (β := ℕ) (1 / t ^ k) 2
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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
⊢ IsBigO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) e
have hh : 0 < h
Tactic: have hh : 0 < h := Γ.strictWidthInfty_pos_iff.mpr Fact.out
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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
⊢ IsBigO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) e
have this : NeZero h
Tactic: have : NeZero h := ⟨hh.ne'⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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
⊢ IsBigO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) e
have hΓ : h ∈ Γ.strictPeriods
Tactic: have hΓ : h ∈ Γ.strictPeriods := Γ.strictWidthInfty_mem_strictPeriods
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
⊢ IsBigO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) e
have 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
Tactic: obtain ⟨C, Cpos, hC⟩ := hF.exists_pos
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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)
⊢ IsBigO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) e
have rw : ∃ (c : ℝ),
  ∀ᶠ (x : ℕ) in atTop,
    norm (E := ℂ)
        ((PowerSeries.coeff x : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) : ℂ) ≤
      c * ‖HPow.hPow (α := ℝ) (↑x : ℝ) e‖
Tactic: rw [isBigO_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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)
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : ℕ) in atTop,
      norm (E := ℂ)
          ((PowerSeries.coeff x : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) : ℂ) ≤
        c * ‖HPow.hPow (α := ℝ) (↑x : ℝ) e‖
have hC₁ : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-e)‖
Tactic: rw [IsBigOWith, eventually_comap] at hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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)‖
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : ℕ) in atTop,
      norm (E := ℂ)
          ((PowerSeries.coeff x : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) : ℂ) ≤
        c * ‖HPow.hPow (α := ℝ) (↑x : ℝ) e‖
have 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‖
Tactic: use (1 / Real.exp (-2 * Real.pi / ↑h)) * C
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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)‖
⊢ ∀ᶠ (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‖
have 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‖
Tactic: filter_upwards [eventually_gt_atTop 0,
    (tendsto_inv_atTop_zero.comp tendsto_natCast_atTop_atTop).eventually hC] with n hn hn'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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)‖
⊢ norm (E := ℂ)
      ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) : ℂ) ≤
    1 / Real.exp (-2 * Real.pi / h) * C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖
have 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 := sorry : ℍ } :
            ℂ)) ≤
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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)‖
⊢ 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‖
have 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 := sorry : ℍ } : ℂ)) ≤
  1 / Real.exp (-2 * Real.pi / h) * C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖
Tactic: simp only [ofReal_div, ofReal_one, ofReal_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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)‖
⊢ 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‖
have 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 := sorry : ℍ } : ℂ)‖ ≤
  1 / Real.exp (-2 * Real.pi / h) * C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖
Tactic: refine intervalIntegral.norm_integral_le_integral_norm (by positivity) |>.trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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 := ⋯ : ℍ } : ℂ)‖
⊢ ∫ (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‖
have hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = HPow.hPow (α := ℝ) (↑n : ℝ) e
Tactic: have hne : ‖(n : ℝ) ^ e‖ = n ^ e := Real.norm_of_nonneg (by positivity)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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)
have 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 := sorry : ℍ } : ℂ)) ≤
  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]