awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst_1 : FunLike F ℍ ℂ
inst_2 : FunLike F' ℍ ℂ
inst_3 : CuspFormClass F Γ k
inst_4 : ModularFormClass F' Γ k
g : SL(2, ℤ)
this :
  (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))⁻¹ :
        ConjAct (GL (Fin 2) ℝ))
      Γ).IsArithmetic
⊢ Tendsto (β := ℂ)
    (fun (τ : ℍ) ↦
      petersson k (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ))
        (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f' : (a : ℍ) → ℂ)) τ)
    atImInfty (𝓝 0)

Tactic:
(zero_at_infty <| CuspForm.translate f g).petersson_isZeroAtImInfty_left k _
    (ModularForm.translate f' g)

Premises used: Real, CuspForm.translate, ModularForm.translate, CuspFormClass.zero_at_infty, Filter.ZeroAtFilter, UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_left, Matrix.SpecialLinearGroup.map, Int.castRingHom, UpperHalfPlane.IsZeroAtImInfty, DFunLike.coe, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst_1 : FunLike F ℍ ℂ
inst_2 : FunLike F' ℍ ℂ
inst_3 : CuspFormClass F Γ k
inst_4 : ModularFormClass F' Γ k
g : SL(2, ℤ)
this :
  (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))⁻¹ :
        ConjAct (GL (Fin 2) ℝ))
      Γ).IsArithmetic
⊢ Tendsto (β := ℂ)
    (fun (τ : ℍ) ↦
      petersson k (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ))
        (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f' : (a : ℍ) → ℂ)) τ)
    atImInfty (𝓝 0)

Tactic:
exact (zero_at_infty <| CuspForm.translate f g).petersson_isZeroAtImInfty_left k _
    (ModularForm.translate f' g)

Premises used: Real, CuspForm.translate, ModularForm.translate, CuspFormClass.zero_at_infty, UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_left, Matrix.SpecialLinearGroup.map, Int.castRingHom, DFunLike.coe, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst_1 : FunLike F ℍ ℂ
inst_2 : FunLike F' ℍ ℂ
inst_3 : ModularFormClass F Γ k
inst_4 : CuspFormClass F' Γ k
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C

Tactic:
simpa [petersson_norm_symm] using petersson_bounded_left k Γ f' f

Premises used: CuspFormClass.petersson_bounded_left, UpperHalfPlane.petersson_norm_symm
-- 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
obtain :
  ∀ (C : ℝ) (hC : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C),
    ∃ (C : ℝ), ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2

Tactic:
obtain ⟨C, hC⟩ := petersson_bounded_left k Γ f f

Premises used: CuspFormClass.petersson_bounded_left
-- 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 : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2

Tactic:
⟨C.sqrt, fun τ ↦ ?_⟩

Premises used: Exists.intro, Real.sqrt
-- 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 : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
refine : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2

Tactic:
refine ⟨C.sqrt, fun τ ↦ ?_⟩
-- 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 : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
τ : ℍ
⊢ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C

Tactic:
specialize hC τ
-- 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 : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
⊢ 0 ≤ norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)

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 : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
⊢ 0 ≤ √C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2

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 : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
rw :
  HPow.hPow (β := ℕ) (norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    C / HPow.hPow (β := ℕ) (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2) 2
⊢ norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2

Tactic:
rw [← sq_le_sq₀ (by positivity) (by positivity), div_pow, Real.sq_sqrt ((norm_nonneg _).trans hC)]

Premises used: Real.sq_sqrt, sq_le_sq₀, div_pow, LE.le.trans, norm_nonneg
-- 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 : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
grw :
  HPow.hPow (β := ℕ) (norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ / HPow.hPow (β := ℕ) (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2) 2
⊢ HPow.hPow (β := ℕ) (norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    C / HPow.hPow (β := ℕ) (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2) 2

Tactic:
grw [← hC]
-- 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 : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
rw :
  HPow.hPow (β := ℕ) (norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    ‖HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) : ℂ)
            ((f : (a : ℍ) → ℂ) τ : ℂ) *
          (↑τ.im : ℂ) ^ k‖ /
      τ.im ^ (HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 * (↑2 : ℝ))
⊢ HPow.hPow (β := ℕ) (norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ / HPow.hPow (β := ℕ) (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2) 2

Tactic:
rw [petersson, ← Real.rpow_mul_natCast τ.im_pos.le]

Premises used: UpperHalfPlane.im_pos, Real.rpow_mul_natCast, LT.lt.le, UpperHalfPlane.petersson
-- 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 : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
⊢ HPow.hPow (β := ℕ) (norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    ‖HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) : ℂ)
            ((f : (a : ℍ) → ℂ) τ : ℂ) *
          (↑τ.im : ℂ) ^ k‖ /
      τ.im ^ (HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 * (↑2 : ℝ))

Tactic:
simp [abs_of_pos τ.im_pos, field]

Premises used: UpperHalfPlane.im_pos, abs_of_pos
-- 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
obtain :
  ∀ (C : ℝ) (hC : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k),
    ∃ (C : ℝ), ∀ (τ : ℍ), Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)

Tactic:
obtain ⟨C, hC⟩ := ModularFormClass.exists_petersson_le hk Γ f f

Premises used: ModularFormClass.exists_petersson_le
-- 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 : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)

Tactic:
⟨C.sqrt, fun τ ↦ ?_⟩

Premises used: Exists.intro, Real.sqrt
-- 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 : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k
refine : ∀ (τ : ℍ), Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C * max 1 (1 / τ.im ^ k)
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)

Tactic:
refine ⟨C.sqrt, fun τ ↦ ?_⟩
-- 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 : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k
τ : ℍ
⊢ 0 ≤ k

Tactic:
hk
-- 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 : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k
τ : ℍ
lift :
  ∀ (k : ℕ) [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 : ℤ))
⊢ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C * max 1 (1 / τ.im ^ k)

Tactic:
lift k to ℕ using hk
-- 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 :
  ∀ (τ : ℍ),
    ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)
⊢ ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)

Tactic:
specialize hC τ
-- 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 :
  ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)
⊢ 0 ≤ ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ / HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)

Tactic:
positivity
-- 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 :
  ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)
⊢ 0 < HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)

Tactic:
positivity
-- 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 :
  ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)
⊢ 0 ≤ C

Tactic:
have hC' : 0 ≤ C := le_trans (by positivity) <| (div_le_iff₀ (by positivity)).mpr hC
-- 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 :
  ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)
hC' : 0 ≤ C
⊢ 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖

Tactic:
have h : 0 < ‖(τ.im : ℂ) ^ (k : ℤ)‖ := mod_cast norm_pos_iff.mpr (pow_ne_zero _ τ.im_ne_zero)
-- 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 :
  ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)
hC' : 0 ≤ C
h : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
⊢ 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

Premises used: Complex.norm_conj, mul_div_assoc, norm_mul, sq, UpperHalfPlane.petersson, le_div_iff₀
-- 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 :
  ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)
hC' : 0 ≤ C
h : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
hC₁ :
  HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    C * (HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖)
⊢ 0 ≤ C

Tactic:
rw [petersson, norm_mul, norm_mul, Complex.norm_conj, ← sq, ← le_div_iff₀ h, mul_div_assoc] at hC

Premises used: Complex.norm_conj, mul_div_assoc, norm_mul, sq, UpperHalfPlane.petersson, le_div_iff₀
-- 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 :
  ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)
hC' : 0 ≤ C
h : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑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
⊢ 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖

Tactic:
rw [petersson, norm_mul, norm_mul, Complex.norm_conj, ← sq, ← le_div_iff₀ h, mul_div_assoc] at hC

Premises used: Complex.norm_conj, mul_div_assoc, norm_mul, sq, UpperHalfPlane.petersson, le_div_iff₀
-- 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 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
⊢ 0 ≤ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)

Tactic:
positivity
-- 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 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
⊢ 0 ≤ √C * max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))

Tactic:
positivity
-- 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 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
rw :
  HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    C * HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))) 2
⊢ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C * max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))

Tactic:
rw [← sq_le_sq₀ (by positivity) (by positivity), mul_pow, sq_sqrt hC']

Premises used: Real.sq_sqrt, sq_le_sq₀, mul_pow
-- 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 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
⊢ HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    C * HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))) 2

Tactic:
hC.trans (congrArg (C * ·) ?_).le

Premises used: HMul.hMul, congrArg, Eq.le, LE.le.trans
-- 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 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
refine :
  HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖ =
    HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))) 2
⊢ HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    C * HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))) 2

Tactic:
refine hC.trans (congrArg (C * ·) ?_).le

Premises used: HMul.hMul, congrArg, Eq.le, LE.le.trans
-- 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 : 0 < ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖
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
⊢ HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ) / ‖HPow.hPow (β := ℤ) (↑τ.im : ℂ) (↑k : ℤ)‖ =
    HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))) 2

Tactic:
generalize h : τ.im = t

Premises used: UpperHalfPlane.im
-- 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 : ℝ
h : τ.im = t
⊢ 0 < t

Tactic:
have ht : 0 < t := h ▸ τ.im_pos
-- 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 : ℝ
h : τ.im = t
ht : 0 < t
⊢ 0 ≤ t

Tactic:
ht.le

Premises used: LT.lt.le
-- 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 : ℝ
h : τ.im = t
ht : 0 < t
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
⊢ 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

Premises used: LT.lt.le, NNReal
-- 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 : ℝ)
norm_cast : ∀ (ht : 0 < t), max t (1 / t) ^ k / ‖(↑(t ^ k) : ℝ)‖₊ = HPow.hPow (β := ℕ) (max 1 (1 / t ^ k)) 2
⊢ HPow.hPow (β := ℤ) (max (↑t : ℝ) (1 / (↑t : ℝ))) (↑k : ℤ) / (↑‖HPow.hPow (β := ℤ) (↑(↑t : ℝ) : ℂ) (↑k : ℤ)‖₊ : ℝ) =
    HPow.hPow (β := ℕ) (max 1 (1 / HPow.hPow (β := ℤ) (↑t : ℝ) (↑k : ℤ))) 2

Tactic:
norm_cast at ⊢ ht
-- 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
⊢ 0 ≤ ‖(↑(t ^ k) : ℝ)‖₊

Tactic:
positivity