awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty :
  ∀ (γ : SL(2, ℤ) ⧸ Γ), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (x : ℍ) ↦ f' x γ) fun (z : ℍ) ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
⊢ Continuous (Y := ℝ) fun (x : ℍ) ↦ ∑ i : SL(2, ℤ) ⧸ Γ, ‖f' x i‖

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty :
  ∀ (γ : SL(2, ℤ) ⧸ Γ), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (x : ℍ) ↦ f' x γ) fun (z : ℍ) ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
g : SL(2, ℤ)
τ : ℍ
⊢ ∀ (x : SL(2, ℤ) ⧸ Γ), ‖f' τ x‖ = ‖f' (g • τ) ((MulAction.toPerm g : (a : SL(2, ℤ) ⧸ Γ) → SL(2, ℤ) ⧸ Γ) x)‖

Tactic:
simp [-sl_moeb, hf'_inv]

Premises used: ModularGroup.sl_moeb
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty :
  ∀ (γ : SL(2, ℤ) ⧸ Γ), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (x : ℍ) ↦ f' x γ) fun (z : ℍ) ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
obtain :
  ∀ (C : ℝ) (hC : ∀ (τ : ℍ), norm (E := ℝ) (∑ i : SL(2, ℤ) ⧸ Γ, ‖f' τ i‖) ≤ C * max τ.im (1 / τ.im) ^ t),
    ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
obtain ⟨C, hC⟩ := exists_bound_of_invariant_of_isBigO (by fun_prop) ht
    (.sum fun i _ ↦ (hf'_infty i).norm_left)
    (fun g τ ↦ (Fintype.sum_equiv (MulAction.toPerm g) _ _ (by simp [-sl_moeb, hf'_inv])).symm)

Premises used: Norm.norm, Asymptotics.IsBigO.norm_left, Asymptotics.IsBigO.sum, MulAction.toPerm, ModularGroup.exists_bound_of_invariant_of_isBigO, HSMul.hSMul, Fintype.sum_equiv, Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty :
  ∀ (γ : SL(2, ℤ) ⧸ Γ), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (x : ℍ) ↦ f' x γ) fun (z : ℍ) ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℝ) (∑ i : SL(2, ℤ) ⧸ Γ, ‖f' τ i‖) ≤ C * max τ.im (1 / τ.im) ^ t
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
⟨C, fun τ ↦ le_trans ?_ (hC τ)⟩

Premises used: Exists.intro, le_trans
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty :
  ∀ (γ : SL(2, ℤ) ⧸ Γ), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (x : ℍ) ↦ f' x γ) fun (z : ℍ) ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℝ) (∑ i : SL(2, ℤ) ⧸ Γ, ‖f' τ i‖) ≤ C * max τ.im (1 / τ.im) ^ t
refine : ∀ (τ : ℍ), ‖f τ‖ ≤ norm (E := ℝ) (∑ i : SL(2, ℤ) ⧸ Γ, ‖f' τ i‖)
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
refine ⟨C, fun τ ↦ le_trans ?_ (hC τ)⟩
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty :
  ∀ (γ : SL(2, ℤ) ⧸ Γ), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (x : ℍ) ↦ f' x γ) fun (z : ℍ) ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℝ) (∑ i : SL(2, ℤ) ⧸ Γ, ‖f' τ i‖) ≤ C * max τ.im (1 / τ.im) ^ t
τ : ℍ
⊢ LE.le (α := ℝ) 0 (∑ γ : SL(2, ℤ) ⧸ Γ, ‖f' τ γ‖)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty :
  ∀ (γ : SL(2, ℤ) ⧸ Γ), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (x : ℍ) ↦ f' x γ) fun (z : ℍ) ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℝ) (∑ i : SL(2, ℤ) ⧸ Γ, ‖f' τ i‖) ≤ C * max τ.im (1 / τ.im) ^ t
τ : ℍ
⊢ ‖f τ‖ ≤ norm (E := ℝ) (∑ i : SL(2, ℤ) ⧸ Γ, ‖f' τ i‖)

Tactic:
simpa [Real.norm_of_nonneg <| show 0 ≤ ∑ γ, ‖f' τ γ‖ by positivity, -sl_moeb, f'] using
    Finset.univ.single_le_sum (fun γ _ ↦ norm_nonneg (f' τ γ)) (Finset.mem_univ ⟦1⟧)

Premises used: Finset.mem_univ, ModularGroup.sl_moeb, Quotient.mk, Finset.single_le_sum, OfNat.ofNat, norm_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup (GL (Fin 2) ℝ)
inst_1 : Γ.IsArithmetic
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
exists_bound_of_subgroup_invariant_of_isBigO hf_cont ht hf_infinity (Γ := Γ.comap (mapGL ℝ))
    (hf_inv ·)

Premises used: Real, ModularGroup.exists_bound_of_subgroup_invariant_of_isBigO, Matrix.SpecialLinearGroup.map, Int.castRingHom, DFunLike.coe, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf_infinity : IsBoundedAtImInfty f
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
⊢ IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ HPow.hPow (β := ℝ) z.im 0

Tactic:
simpa only [Real.rpow_zero] using hf_infinity

Premises used: Real.rpow_zero
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf_infinity : IsBoundedAtImInfty f
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C

Tactic:
simpa using exists_bound_of_invariant_of_isBigO hf_cont le_rfl
    (by simpa only [Real.rpow_zero] using hf_infinity) hf_inv

Premises used: le_rfl, ModularGroup.exists_bound_of_invariant_of_isBigO
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf_infinity : ∀ (g : SL(2, ℤ)), IsBoundedAtImInfty.{u_1} (α := E) fun (τ : ℍ) ↦ f (g • τ)
Γ : Subgroup (GL (Fin 2) ℝ)
inst_1 : Γ.IsArithmetic
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
⊢ ∀ (g : SL(2, ℤ)),
    IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ HPow.hPow (β := ℝ) z.im 0

Tactic:
simpa only [Real.rpow_zero] using hf_infinity

Premises used: Real.rpow_zero
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf_infinity : ∀ (g : SL(2, ℤ)), IsBoundedAtImInfty.{u_1} (α := E) fun (τ : ℍ) ↦ f (g • τ)
Γ : Subgroup (GL (Fin 2) ℝ)
inst_1 : Γ.IsArithmetic
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C

Tactic:
simpa using exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO hf_cont le_rfl
    (by simpa only [Real.rpow_zero] using hf_infinity) hf_inv

Premises used: le_rfl, ModularGroup.exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ 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 : ModularFormClass F' Γ k
enter : ∀ (C : ℝ) (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖
| ∃ (C : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k

Tactic:
enter [1, C, τ, 1]
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ 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 : ModularFormClass F' Γ k
C : ℝ
τ : ℍ
rw : ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖
| ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖

Tactic:
rw [← norm_norm]

Premises used: norm_norm
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ 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 : ModularFormClass F' Γ k
enter : ∀ (C : ℝ) (τ : ℍ), ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖
| ∃ (C : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k

Tactic:
enter [1, C, τ, 1]; rw [← norm_norm]

Premises used: norm_norm
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ 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 : ModularFormClass F' Γ k
conv : ∃ (C : ℝ), ∀ (τ : ℍ), ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖ ≤ C * max τ.im (1 / τ.im) ^ k
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k

Tactic:
conv => enter [1, C, τ, 1]; rw [← norm_norm]

Premises used: norm_norm
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ 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 : ModularFormClass F' Γ k
⊢ Continuous (Y := ℝ) fun (x : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) x‖

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ 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 : ModularFormClass F' Γ k
refine :
  ∀ (g : SL(2, ℤ)),
    IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖)
      fun (z : ℍ) ↦ HPow.hPow (β := ℝ) z.im (↑k : ℝ)
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖ ≤ C * max τ.im (1 / τ.im) ^ k

Tactic:
refine mod_cast ModularGroup.exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO
    (show Continuous (‖petersson k f f' ·‖) by fun_prop) (mod_cast hk : 0 ≤ (k : ℝ))
    (fun g ↦ ?_) (fun g hg τ ↦ SlashInvariantFormClass.norm_petersson_smul hg)

Premises used: Int.cast, congrArg, Int.cast_zero, cast, LE.le, Int.cast_le._simp_1, ModularGroup.exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO, congrFun', SlashInvariantFormClass.norm_petersson_smul, Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ 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 : ModularFormClass F' Γ k
g : SL(2, ℤ)
simp_rw :
  IsBigO (E := ℝ) (F := ℝ) atImInfty
    (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 : ℍ) → ℂ)) τ‖)
    fun (z : ℍ) ↦ z.im ^ k
⊢ IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖)
    fun (z : ℍ) ↦ HPow.hPow (β := ℝ) z.im (↑k : ℝ)

Tactic:
simp_rw [← UpperHalfPlane.petersson_slash_SL, Real.rpow_intCast]

Premises used: UpperHalfPlane.petersson_slash_SL, Real.rpow_intCast
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
hk : 0 ≤ 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 : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ IsBigO (E := ℝ) (F := ℝ) atImInfty
    (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 : ℍ) → ℂ)) τ‖)
    fun (z : ℍ) ↦ z.im ^ k

Tactic:
simpa [petersson, Real.norm_of_nonneg (_ : ℍ).im_pos.le]
    using (bdd_at_infty_slash f g).norm_left.mul (bdd_at_infty_slash f' g).norm_left
      |>.mul (isBigO_refl ..)

Premises used: Asymptotics.IsBigO.norm_left, UpperHalfPlane.im_pos, LT.lt.le, Asymptotics.IsBigO.mul, UpperHalfPlane.petersson, ModularFormClass.bdd_at_infty_slash, Real.norm_of_nonneg, Asymptotics.isBigO_refl
-- 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
enter : ∀ (C : ℝ) (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖
| ∃ (C : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C

Tactic:
enter [1, C, τ, 1]
-- 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
C : ℝ
τ : ℍ
rw : ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖
| ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖

Tactic:
rw [← norm_norm]

Premises used: norm_norm
-- 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
enter : ∀ (C : ℝ) (τ : ℍ), ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖
| ∃ (C : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C

Tactic:
enter [1, C, τ, 1]; rw [← norm_norm]

Premises used: norm_norm
-- 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
conv : ∃ (C : ℝ), ∀ (τ : ℍ), ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C

Tactic:
conv => enter [1, C, τ, 1]; rw [← norm_norm]

Premises used: norm_norm
-- 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
⊢ Continuous (Y := ℝ) fun (τ : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖

Tactic:
fun_prop
-- 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
refine :
  ∀ (g : SL(2, ℤ)),
    IsBoundedAtImInfty (α := ℝ) fun (τ : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖ ≤ C

Tactic:
refine ModularGroup.exists_bound_of_subgroup_invariant (by fun_prop) (fun g ↦ ?_)
    fun g hg τ ↦ SlashInvariantFormClass.norm_petersson_smul hg

Premises used: ModularGroup.exists_bound_of_subgroup_invariant
-- 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, ℤ)
hf : IsZeroAtImInfty (α := ℝ) fun (τ : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖
⊢ IsBoundedAtImInfty (α := ℝ) fun (τ : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖

Tactic:
apply IsZeroAtImInfty.isBoundedAtImInfty

Premises used: UpperHalfPlane.IsZeroAtImInfty.isBoundedAtImInfty
-- 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, ℤ)
hf : Tendsto (β := ℂ) (fun (τ : ℍ) ↦ petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)) atImInfty (𝓝 0)
⊢ IsZeroAtImInfty (α := ℝ) fun (τ : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖

Tactic:
rw [IsZeroAtImInfty, ZeroAtFilter, ← tendsto_zero_iff_norm_tendsto_zero]

Premises used: Filter.ZeroAtFilter, tendsto_zero_iff_norm_tendsto_zero, UpperHalfPlane.IsZeroAtImInfty
-- 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, ℤ)
hf :
  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)
⊢ Tendsto (β := ℂ) (fun (τ : ℍ) ↦ petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)) atImInfty (𝓝 0)

Tactic:
simp_rw [← UpperHalfPlane.petersson_slash_SL]

Premises used: UpperHalfPlane.petersson_slash_SL
-- 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, ℤ)
⊢ Rat.castHom ℝ = algebraMap ℚ ℝ

Tactic:
rfl
-- 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, ℤ)
⊢ (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

Tactic:
simpa [(show Rat.castHom ℝ = algebraMap ℚ ℝ by rfl), map_inv, map_mapGL]
      using Subgroup.IsArithmetic.conj Γ (mapGL ℚ g)⁻¹

Premises used: Matrix.SpecialLinearGroup.map_mapGL, map_inv, Rat, Inv.inv, Matrix.SpecialLinearGroup.mapGL, DFunLike.coe, Subgroup.IsArithmetic.conj
-- 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, ℤ)
⊢ (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

Tactic:
have : ((toConjAct (g : GL (Fin 2) ℝ)⁻¹) • Γ).IsArithmetic := by
    simpa [(show Rat.castHom ℝ = algebraMap ℚ ℝ by rfl), map_inv, map_mapGL]
      using Subgroup.IsArithmetic.conj Γ (mapGL ℚ g)⁻¹