awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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⁻¹ • τ)) ⋯
γ : SL(2, ℤ) ⧸ Γ
g : SL(2, ℤ)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x (↑g : SL(2, ℤ) ⧸ Γ)
have simp : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦
  f
    (HSMul.hSMul (α := GL (Fin 2) ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
        GL (Fin 2) ℝ)
      x)
Tactic: simp only [sl_moeb, Quotient.lift_mk, f']
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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⁻¹ • τ)) ⋯
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
have hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
Tactic: have hf'_cont γ : Continuous (f' · γ) := QuotientGroup.induction_on γ fun g ↦ by
    simp only [sl_moeb, Quotient.lift_mk, f']
    fun_prop
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 γ
τ : ℍ
g : SL(2, ℤ)
γ : SL(2, ℤ) ⧸ Γ
⊢ f' (g • τ) (g • γ) = f' τ γ
have H : ∀ (z : SL(2, ℤ)), f' (g • τ) (HSMul.hSMul (β := SL(2, ℤ) ⧸ Γ) g (↑z : SL(2, ℤ) ⧸ Γ)) = f' τ (↑z : SL(2, ℤ) ⧸ Γ)
Tactic: induction γ using QuotientGroup.induction_on
Cleared hypotheses: γ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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 γ
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
have hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
Tactic: have hf'_inv τ (g : SL(2, ℤ)) γ : f' (g • τ) (g • γ) = f' τ γ := by
    induction γ using QuotientGroup.induction_on
    simp [-sl_moeb, f', mul_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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' τ γ
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
have hf'_infty : ∀ (γ : SL(2, ℤ) ⧸ Γ), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (x : ℍ) ↦ f' x γ) fun (z : ℍ) ↦ z.im ^ t
Tactic: have hf'_infty γ : (f' · γ) =O[_] _ := γ.induction_on fun h ↦ hf_infinity h⁻¹
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
have have : ∀ (this : Fintype (SL(2, ℤ) ⧸ Γ)), ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
Tactic: have : Fintype (SL(2, ℤ) ⧸ Γ) := Subgroup.fintypeQuotientOfFiniteIndex
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
have obtain : ∀ (C : ℝ) (hC : ∀ (τ : ℍ), norm (E := ℝ) (∑ i : SL(2, ℤ) ⧸ Γ, ‖f' τ i‖) ≤ 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)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
have refine : ∀ (τ : ℍ), ‖f τ‖ ≤ norm (E := ℝ) (∑ i : SL(2, ℤ) ⧸ Γ, ‖f' τ i‖)
Tactic: refine ⟨C, fun τ ↦ le_trans ?_ (hC τ)⟩
-- 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
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 : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k
have enter : ∀ (C : ℝ) (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖
Tactic: enter [1, C, τ, 1]
-- 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
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 : ℝ
τ : ℍ
| ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖
have rw : ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖
Tactic: rw [← norm_norm]
-- 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
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 : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k
have enter : ∀ (C : ℝ) (τ : ℍ), ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖
Tactic: enter [1, C, τ, 1]; rw [← norm_norm]
-- 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
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 : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k
have conv : ∃ (C : ℝ), ∀ (τ : ℍ), ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖ ≤ C * max τ.im (1 / τ.im) ^ k
Tactic: conv => enter [1, C, τ, 1]; rw [← norm_norm]
-- 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
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 : ℝ), ∀ (τ : ℍ), ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖ ≤ C * max τ.im (1 / τ.im) ^ k
have refine : ∀ (g : SL(2, ℤ)),
  IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖)
    fun (z : ℍ) ↦ HPow.hPow (β := ℝ) z.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)
-- 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
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 (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖)
    fun (z : ℍ) ↦ HPow.hPow (β := ℝ) z.im (↑k : ℝ)
have 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
Tactic: simp_rw [← UpperHalfPlane.petersson_slash_SL, Real.rpow_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C
have enter : ∀ (C : ℝ) (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖
Tactic: enter [1, C, τ, 1]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 : ℝ
τ : ℍ
| ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖
have rw : ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖
Tactic: rw [← norm_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C
have enter : ∀ (C : ℝ) (τ : ℍ), ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖
Tactic: enter [1, C, τ, 1]; rw [← norm_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 : ℝ), ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖ ≤ C
have conv : ∃ (C : ℝ), ∀ (τ : ℍ), ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖ ≤ C
Tactic: conv => enter [1, C, τ, 1]; rw [← norm_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 : ℝ), ∀ (τ : ℍ), ‖‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖‖ ≤ C
have refine : ∀ (g : SL(2, ℤ)), IsBoundedAtImInfty (α := ℝ) fun (τ : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖
Tactic: refine ModularGroup.exists_bound_of_subgroup_invariant (by fun_prop) (fun g ↦ ?_)
    fun g hg τ ↦ SlashInvariantFormClass.norm_petersson_smul hg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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, ℤ)
⊢ IsBoundedAtImInfty (α := ℝ) fun (τ : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖
have hf : IsZeroAtImInfty (α := ℝ) fun (τ : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖
Tactic: apply IsZeroAtImInfty.isBoundedAtImInfty
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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, ℤ)
⊢ IsZeroAtImInfty (α := ℝ) fun (τ : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖
have hf : Tendsto (β := ℂ) (fun (τ : ℍ) ↦ petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)) atImInfty (𝓝 0)
Tactic: rw [IsZeroAtImInfty, ZeroAtFilter, ← tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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, ℤ)
⊢ Tendsto (β := ℂ) (fun (τ : ℍ) ↦ petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)) atImInfty (𝓝 0)
have 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)
Tactic: simp_rw [← UpperHalfPlane.petersson_slash_SL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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, ℤ)
⊢ 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)
have 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
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)⁻¹
-- 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 : ℝ), ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
have obtain : ∀ (C : ℝ) (hC : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C),
  ∃ (C : ℝ), ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
Tactic: obtain ⟨C, hC⟩ := petersson_bounded_left k Γ f 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 : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
have refine : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
Tactic: refine ⟨C.sqrt, fun τ ↦ ?_⟩
-- 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 : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
τ : ℍ
⊢ norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
have hC₁ : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
Tactic: specialize 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 : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
⊢ norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
have rw : HPow.hPow (β := ℕ) (norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
  C / HPow.hPow (β := ℕ) (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2) 2
Tactic: rw [← sq_le_sq₀ (by positivity) (by positivity), div_pow, Real.sq_sqrt ((norm_nonneg _).trans 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 : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
⊢ HPow.hPow (β := ℕ) (norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    C / HPow.hPow (β := ℕ) (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2) 2
have grw : HPow.hPow (β := ℕ) (norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
  ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ / HPow.hPow (β := ℕ) (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2) 2
Tactic: grw [← 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 : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C
⊢ HPow.hPow (β := ℕ) (norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
    ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ / HPow.hPow (β := ℕ) (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2) 2
have rw : HPow.hPow (β := ℕ) (norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)) 2 ≤
  ‖HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) : ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) *
        (↑τ.im : ℂ) ^ k‖ /
    τ.im ^ (HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 * (↑2 : ℝ))
Tactic: rw [petersson, ← Real.rpow_mul_natCast τ.im_pos.le]
-- 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 : ℝ), ∀ (τ : ℍ), Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)
have 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)
Tactic: obtain ⟨C, hC⟩ := ModularFormClass.exists_petersson_le hk Γ f 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 : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C * max 1 (1 / τ.im ^ k)
have refine : ∀ (τ : ℍ), Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C * max 1 (1 / τ.im ^ k)
Tactic: refine ⟨C.sqrt, fun τ ↦ ?_⟩
-- 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 : ∀ (τ : ℍ), ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * max τ.im (1 / τ.im) ^ k
τ : ℍ
⊢ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C * max 1 (1 / τ.im ^ k)
have 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 : ℤ))
Tactic: lift k to ℕ using hk
Cleared hypotheses: k, hk, inst_2, 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 : ℤ)
⊢ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ √C * max 1 (1 / HPow.hPow (β := ℤ) τ.im (↑k : ℤ))
have hC₁ : ‖petersson (↑k : ℤ) (⇑f : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) τ‖ ≤ C * HPow.hPow (β := ℤ) (max τ.im (1 / τ.im)) (↑k : ℤ)
Tactic: specialize hC τ
Cleared hypotheses: hC