awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ
⊢ 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))
have 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 := sorry : ℍ } : ℂ)) ≤
  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]
-- 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 : ℝ
⊢ 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))
have hbc : -2 * Real.pi / h ≤ (↑n : ℝ) * (-2 * Real.pi * ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I).im / h)
Tactic: gcongr
-- 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 : ℝ
hbc : -2 * Real.pi / h ≤ (↑n : ℝ) * (-2 * Real.pi * ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I).im / h)
⊢ 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))
have hbc₁ : norm (E := ℂ) ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := sorry : ℍ } : ℂ) ≤
  C * HPow.hPow (α := ℝ) (↑n : ℝ) e
Tactic: gcongr
-- 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 : ℝ
⊢ norm (E := ℂ) ((f : (a : ℍ) → ℂ) { coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ) ≤
    C * HPow.hPow (α := ℝ) (↑n : ℝ) e
have hbc : C * ‖{ coe := (↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I, coe_im_pos := sorry : ℍ }.im ^ (-e)‖ ≤
  C * HPow.hPow (α := ℝ) (↑n : ℝ) e
Tactic: grw [hn' _ (by simp [← UpperHalfPlane.coe_im])]
-- 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 := ⋯ : ℍ } : ℂ)‖
hne : ‖HPow.hPow (α := ℝ) (↑n : ℝ) e‖ = 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‖
have this₁ : ∀ (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]
-- 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_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 : ℝ) 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₁ : IntervalIntegrable F MeasureTheory.volume 0 h
Tactic: refine (intervalIntegral.integral_mono (by positivity) ?_ ?_ this).trans (le_of_eq ?_)
-- 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_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
⊢ ∫ (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₂ : IntervalIntegrable (ε := ℝ)
  (fun (i : ℝ) ↦ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * HPow.hPow (α := ℝ) (↑n : ℝ) e)) MeasureTheory.volume 0
  h
Tactic: refine (intervalIntegral.integral_mono (by positivity) ?_ ?_ this).trans (le_of_eq ?_)
-- 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_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
⊢ ∫ (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₃ : ∫ (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: refine (intervalIntegral.integral_mono (by positivity) ?_ ?_ this).trans (le_of_eq ?_)
-- 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_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 F MeasureTheory.volume 0 h
have h₁ : Continuous F
Tactic: apply Continuous.intervalIntegrable
-- 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_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)
⊢ Continuous F
have funProp : ∀ (x : ℝ), 𝕢 h ((↑x : ℂ) + HDiv.hDiv (α := ℂ) 1 (↑n : ℂ) * I) ^ n ≠ 0
Tactic: fun_prop (disch := simp [Function.Periodic.qParam_ne_zero])
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
⊢ IsBigO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k
have simp : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
⊢ IsBigO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (↑k : ℝ)
have hF : IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦
  HPow.hPow (β := ℝ) τ.im (-(↑k : ℝ))
Tactic: apply qExpansion_coeff_isBigO_of_norm_isBigO
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
⊢ IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦
    HPow.hPow (β := ℝ) τ.im (-(↑k : ℝ))
have 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 : ℝ))
Tactic: obtain ⟨C, hC⟩ := exists_bound hk f
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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)
⊢ IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦
    HPow.hPow (β := ℝ) τ.im (-(↑k : ℝ))
have hF : ∃ (c : ℝ), ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ c * ‖a.im ^ (-k)‖
Tactic: simp_rw [IsBigO, ← Int.cast_neg, Real.rpow_intCast, IsBigOWith, eventually_comap]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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)
⊢ ∃ (c : ℝ), ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ c * ‖a.im ^ (-k)‖
have h : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-k)‖
Tactic: use C
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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)
⊢ ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → norm (E := ℂ) ((f : (a : ℍ) → ℂ) a : ℂ) ≤ C * ‖a.im ^ (-k)‖
have h : ∀ (τ : ℍ) (hτ : τ.im ≤ 1), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * ‖τ.im ^ (-k)‖
Tactic: filter_upwards [eventually_le_nhds zero_lt_one] with _ hτ τ rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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)‖
have h : C * max 1 (1 / τ.im ^ k) = C * ‖τ.im ^ (-k)‖
Tactic: refine (hC τ).trans (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
⊢ C * max 1 (1 / τ.im ^ k) = C * ‖τ.im ^ (-k)‖
have h : 1 ≤ 1 / τ.im ^ k
Tactic: rw [max_eq_right, zpow_neg, Real.norm_of_nonneg (by positivity), one_div]
-- 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 : CuspFormClass F Γ k
f : F
⊢ IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦
    τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
have 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)
Tactic: obtain ⟨C, hC⟩ := exists_bound f
-- 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 : 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)
have hF : ∀ (τ : ℍ), C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * ‖τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)‖
Tactic: refine isBigO_of_le' (c := C) _ fun τ ↦ (hC τ).trans (of_eq ?_)
-- 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 : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
τ : ℍ
⊢ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * ‖τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)‖
have hF : C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
Tactic: rw [Real.norm_of_nonneg (by positivity), Real.rpow_neg τ.im_pos.le, div_eq_mul_inv]
-- 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 : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
τ : ℍ
hF : C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
⊢ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * ‖τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)‖
have hF₁ : C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)⁻¹
Tactic: rw [Real.norm_of_nonneg (by positivity), Real.rpow_neg τ.im_pos.le, div_eq_mul_inv]
-- 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 : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
τ : ℍ
hF : C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
hF₁ : C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)⁻¹
⊢ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * ‖τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)‖
have hF₂ : C * (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)⁻¹ = C * (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)⁻¹
Tactic: rw [Real.norm_of_nonneg (by positivity), Real.rpow_neg τ.im_pos.le, div_eq_mul_inv]