Boundedness and vanishing at cusps

We define the notions of "bounded at c" and "vanishing at c" for functions on ℍ, where c is an element of OnePoint ℝ.

theorem UpperHalfPlane.IsZeroAtImInfty.slash {g : GL (Fin 2) ℝ} {f : UpperHalfPlane → ℂ} (k : ℤ) (hg : ↑g 1 0 = 0) (hf : IsZeroAtImInfty f) : IsZeroAtImInfty (SlashAction.map k g f)

theorem UpperHalfPlane.IsBoundedAtImInfty.slash {g : GL (Fin 2) ℝ} {f : UpperHalfPlane → ℂ} (k : ℤ) (hg : ↑g 1 0 = 0) (hf : IsBoundedAtImInfty f) : IsBoundedAtImInfty (SlashAction.map k g f)

def OnePoint.IsBoundedAt (c : OnePoint ℝ) (f : UpperHalfPlane → ℂ) (k : ℤ) : Prop

We say f is bounded at c if, for all g with g • ∞ = c, the function f ∣[k] g is bounded at ∞.

def OnePoint.IsZeroAt (c : OnePoint ℝ) (f : UpperHalfPlane → ℂ) (k : ℤ) : Prop

We say f is zero at c if, for all g with g • ∞ = c, the function f ∣[k] g is zero at ∞.

theorem OnePoint.IsBoundedAt.smul_iff {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} {g : GL (Fin 2) ℝ} : (g • c).IsBoundedAt f k ↔ c.IsBoundedAt (SlashAction.map k g f) k

theorem OnePoint.IsZeroAt.smul_iff {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} {g : GL (Fin 2) ℝ} : (g • c).IsZeroAt f k ↔ c.IsZeroAt (SlashAction.map k g f) k

theorem OnePoint.IsBoundedAt.add {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} {f' : UpperHalfPlane → ℂ} (hf : c.IsBoundedAt f k) (hf' : c.IsBoundedAt f' k) : c.IsBoundedAt (f + f') k

theorem OnePoint.IsZeroAt.add {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} {f' : UpperHalfPlane → ℂ} (hf : c.IsZeroAt f k) (hf' : c.IsZeroAt f' k) : c.IsZeroAt (f + f') k

theorem OnePoint.isBoundedAt_infty_iff {f : UpperHalfPlane → ℂ} {k : ℤ} : infty.IsBoundedAt f k ↔ UpperHalfPlane.IsBoundedAtImInfty f

theorem OnePoint.isZeroAt_infty_iff {f : UpperHalfPlane → ℂ} {k : ℤ} : infty.IsZeroAt f k ↔ UpperHalfPlane.IsZeroAtImInfty f

theorem OnePoint.isBoundedAt_iff {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} {g : GL (Fin 2) ℝ} (hg : g • infty = c) : c.IsBoundedAt f k ↔ UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k g f)

To check that f is bounded at c, it suffices for f ∣[k] g to be bounded at ∞ for any single g with g • ∞ = c.

theorem OnePoint.isZeroAt_iff {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} {g : GL (Fin 2) ℝ} (hg : g • infty = c) : c.IsZeroAt f k ↔ UpperHalfPlane.IsZeroAtImInfty (SlashAction.map k g f)

To check that f is zero at c, it suffices for f ∣[k] g to be zero at ∞ for any single g with g • ∞ = c.

theorem OnePoint.isBoundedAt_iff_exists_SL2Z {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} (hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range) : c.IsBoundedAt f k ↔ ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), (Matrix.SpecialLinearGroup.mapGL ℝ) γ • infty = c ∧ UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k γ f)

theorem OnePoint.isZeroAt_iff_exists_SL2Z {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} (hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range) : c.IsZeroAt f k ↔ ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), (Matrix.SpecialLinearGroup.mapGL ℝ) γ • infty = c ∧ UpperHalfPlane.IsZeroAtImInfty (SlashAction.map k γ f)

theorem OnePoint.isBoundedAt_iff_forall_SL2Z {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} (hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range) : c.IsBoundedAt f k ↔ ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), (Matrix.SpecialLinearGroup.mapGL ℝ) γ • infty = c → UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k γ f)

theorem OnePoint.isZeroAt_iff_forall_SL2Z {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} (hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range) : c.IsZeroAt f k ↔ ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), (Matrix.SpecialLinearGroup.mapGL ℝ) γ • infty = c → UpperHalfPlane.IsZeroAtImInfty (SlashAction.map k γ f)