Restriction of a function on the upper half-plane to the imaginary axis

The Mellin transform computing the completed L-function of a modular form integrates the form along the positive imaginary axis: Mathlib's CuspForm.Λ_eq_mellin reads Λ hk f = mellin (fun t ↦ f (ofComplex (I * t))) for a cusp form. This file names that restriction, resToImagAxis F t = F (i t) for t > 0 (and 0 otherwise, since i t ∈ ℍ fails for t ≤ 0), for an arbitrary F : ℍ → ℂ.

The three predicates RealOnImagAxis, PosOnImagAxis and EventuallyPosOnImagAxis record that the restriction is real-valued, real and positive, or real and eventually positive along atTop. RealOnImagAxis is closed under constants, negation, addition, subtraction, multiplication, multiplication by a real scalar, and natural powers; the two positivity predicates are closed under the operations that preserve strict positivity — positive constants, addition, multiplication, multiplication by a positive real scalar, and natural powers — but not under negation or subtraction. The closure lemmas are tagged @[fun_prop], except PosOnImagAxis.const and EventuallyPosOnImagAxis.const, whose constant is not determined by the goal.

Main definitions

• UpperHalfPlane.resToImagAxis: the restriction t ↦ F (i t), extended by 0 on t ≤ 0.
• UpperHalfPlane.RealOnImagAxis, PosOnImagAxis, EventuallyPosOnImagAxis: the restriction is real-valued, positive, or eventually positive along atTop.

Main results

• UpperHalfPlane.resToImagAxis_of_pos, resToImagAxis_of_nonpos: the characteristic equations of the restriction.
• UpperHalfPlane.resToImagAxis_zero, _add, _neg, _sub, _mul, _smul: the restriction commutes with the pointwise operations, unconditionally.
• UpperHalfPlane.differentiableAt_resToImagAxis: the restriction is real-differentiable at t > 0 when F ∘ ofComplex is, and differentiableAt_resToImagAxis_of_mDiffAt: the same from manifold differentiability at the corresponding point.
• UpperHalfPlane.tendsto_ofComplex_I_mul_atTop_atImInfty: i t → i∞ as t → ∞, and Asymptotics.IsBigO.resToImagAxis: an asymptotic bound at i∞ restricts to a bound on the imaginary axis at +∞.
• UpperHalfPlane.isBigO_aeval_num_denom: along the imaginary axis, a polynomial in the numerator and denominator of a Möbius transformation grows at most polynomially.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/Modularforms/ResToImagAxis.lean, Chris Birkbeck, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), with the Function.resToImagAxis dot-notation alias dropped in favour of the single definition, the repeated unfolding replaced by resToImagAxis_of_pos, and eventual positivity phrased with the atTop filter. The slash-action behaviour of the restriction, the one modular-forms statement of the source file, lives in TauCeti/NumberTheory/ModularForms/ResToImagAxis.lean.

noncomputable def UpperHalfPlane.resToImagAxis (F : UpperHalfPlane → ℂ) : ℝ → ℂ

The restriction of F : ℍ → ℂ to the positive imaginary axis, t ↦ F (i t). Since i t lies in ℍ only for t > 0, the restriction is extended by 0 on t ≤ 0.

Equations

• UpperHalfPlane.resToImagAxis F t = if ht : 0 < t then F { coe := Complex.I * ↑t, coe_im_pos := ⋯ } else 0

@[simp]

theorem UpperHalfPlane.resToImagAxis_of_pos (F : UpperHalfPlane → ℂ) {t : ℝ} (ht : 0 < t) : resToImagAxis F t = F { coe := Complex.I * ↑t, coe_im_pos := ⋯ }

The characteristic equation of resToImagAxis on its domain of interest.

@[simp]

theorem UpperHalfPlane.resToImagAxis_of_nonpos (F : UpperHalfPlane → ℂ) {t : ℝ} (ht : t ≤ 0) : resToImagAxis F t = 0

Off the positive axis the restriction is 0 by convention.

The restriction commutes with the pointwise operations

Each identity is unconditional in t: off the positive axis both sides are 0.

@[simp]

theorem UpperHalfPlane.resToImagAxis_zero : resToImagAxis 0 = 0

The restriction of 0 is 0.

@[simp]

theorem UpperHalfPlane.resToImagAxis_neg (F : UpperHalfPlane → ℂ) : resToImagAxis (-F) = -resToImagAxis F

The restriction commutes with negation.

@[simp]

theorem UpperHalfPlane.resToImagAxis_add (F G : UpperHalfPlane → ℂ) : resToImagAxis (F + G) = resToImagAxis F + resToImagAxis G

The restriction commutes with addition.

@[simp]

theorem UpperHalfPlane.resToImagAxis_sub (F G : UpperHalfPlane → ℂ) : resToImagAxis (F - G) = resToImagAxis F - resToImagAxis G

The restriction commutes with subtraction.

@[simp]

theorem UpperHalfPlane.resToImagAxis_mul (F G : UpperHalfPlane → ℂ) : resToImagAxis (F * G) = resToImagAxis F * resToImagAxis G

The restriction commutes with pointwise multiplication.

@[simp]

theorem UpperHalfPlane.resToImagAxis_smul (c : ℂ) (F : UpperHalfPlane → ℂ) : resToImagAxis (c • F) = c • resToImagAxis F

The restriction commutes with scalar multiplication.

Behaviour at i∞

theorem UpperHalfPlane.tendsto_ofComplex_I_mul_atTop_atImInfty : Filter.Tendsto (fun (t : ℝ) => ↑ofComplex (Complex.I * ↑t)) Filter.atTop atImInfty

Along the imaginary axis, i t tends to i∞ as t → ∞.

theorem Asymptotics.IsBigO.resToImagAxis {E : Type u_1} [Norm E] {F : UpperHalfPlane → ℂ} {G : UpperHalfPlane → E} (h : F =O[UpperHalfPlane.atImInfty] G) : UpperHalfPlane.resToImagAxis F =O[Filter.atTop] fun (t : ℝ) => G (↑UpperHalfPlane.ofComplex (Complex.I * ↑t))

An asymptotic bound at i∞ restricts to the imaginary axis: if F = O(G) along atImInfty, then resToImagAxis F = O(t ↦ G (i t)) along atTop.

theorem UpperHalfPlane.isBigO_aeval_num_denom {R : Type u_1} [CommSemiring R] [Algebra R ℂ] {P : MvPolynomial (Fin 2) R} {n : ℕ} (hP : P.totalDegree ≤ n) (g : GL (Fin 2) ℝ) : (fun (t : ℝ) => (MvPolynomial.aeval ![num g (Complex.I * ↑t), denom g (Complex.I * ↑t)]) P) =O[Filter.atTop] fun (t : ℝ) => t ^ n

Along the imaginary axis, a polynomial P in the numerator a i t + b and denominator c i t + d of the Möbius transformation of a real matrix grows at most like t ^ n for n ≥ P.totalDegree.

Real-valuedness, positivity, and eventual positivity

def UpperHalfPlane.RealOnImagAxis (F : UpperHalfPlane → ℂ) : Prop

F is real-valued on the positive imaginary axis.

Equations

• UpperHalfPlane.RealOnImagAxis F = ∀ (t : ℝ), 0 < t → (UpperHalfPlane.resToImagAxis F t).im = 0

def UpperHalfPlane.PosOnImagAxis (F : UpperHalfPlane → ℂ) : Prop

F is real and strictly positive on the positive imaginary axis.

Equations

• UpperHalfPlane.PosOnImagAxis F = (UpperHalfPlane.RealOnImagAxis F ∧ ∀ (t : ℝ), 0 < t → 0 < (UpperHalfPlane.resToImagAxis F t).re)

def UpperHalfPlane.EventuallyPosOnImagAxis (F : UpperHalfPlane → ℂ) : Prop

F is real on the positive imaginary axis and strictly positive far out along it.

Equations

• UpperHalfPlane.EventuallyPosOnImagAxis F = (UpperHalfPlane.RealOnImagAxis F ∧ ∀ᶠ (t : ℝ) in Filter.atTop, 0 < (UpperHalfPlane.resToImagAxis F t).re)

Differentiability

theorem UpperHalfPlane.differentiableAt_resToImagAxis (F : UpperHalfPlane → ℂ) {t : ℝ} (ht : 0 < t) (hF : DifferentiableAt ℝ (fun (z : ℂ) => F (↑ofComplex z)) (Complex.I * ↑t)) : DifferentiableAt ℝ (resToImagAxis F) t

The restriction is real-differentiable at t > 0 whenever F ∘ ofComplex is: the restriction is its composite with t ↦ i t, so only real differentiability at the corresponding point is used — holomorphy is not needed.

theorem UpperHalfPlane.differentiableAt_resToImagAxis_of_mDiffAt (F : UpperHalfPlane → ℂ) {t : ℝ} (ht : 0 < t) (hF : MDiffAt F { coe := Complex.I * ↑t, coe_im_pos := ⋯ }) : DifferentiableAt ℝ (resToImagAxis F) t

The manifold-differentiable case, which is how modular forms supply the hypothesis.

Real-valuedness is preserved by the algebraic operations

theorem UpperHalfPlane.RealOnImagAxis.const (c : ℝ) : RealOnImagAxis fun (x : UpperHalfPlane) => ↑c

A real constant is real-valued on the imaginary axis.

theorem UpperHalfPlane.RealOnImagAxis.zero : RealOnImagAxis fun (x : UpperHalfPlane) => 0

The zero function is real-valued on the imaginary axis.

theorem UpperHalfPlane.RealOnImagAxis.one : RealOnImagAxis fun (x : UpperHalfPlane) => 1

The constant function 1 is real-valued on the imaginary axis.

theorem UpperHalfPlane.RealOnImagAxis.neg {F : UpperHalfPlane → ℂ} (hF : RealOnImagAxis F) : RealOnImagAxis (-F)

Negation preserves real-valuedness on the imaginary axis.

theorem UpperHalfPlane.RealOnImagAxis.add {F G : UpperHalfPlane → ℂ} (hF : RealOnImagAxis F) (hG : RealOnImagAxis G) : RealOnImagAxis (F + G)

Addition preserves real-valuedness on the imaginary axis.

theorem UpperHalfPlane.RealOnImagAxis.sub {F G : UpperHalfPlane → ℂ} (hF : RealOnImagAxis F) (hG : RealOnImagAxis G) : RealOnImagAxis (F - G)

Subtraction preserves real-valuedness on the imaginary axis.

theorem UpperHalfPlane.RealOnImagAxis.mul {F G : UpperHalfPlane → ℂ} (hF : RealOnImagAxis F) (hG : RealOnImagAxis G) : RealOnImagAxis (F * G)

Multiplication preserves real-valuedness on the imaginary axis.

theorem UpperHalfPlane.RealOnImagAxis.const_smul {F : UpperHalfPlane → ℂ} {c : ℝ} (hF : RealOnImagAxis F) : RealOnImagAxis (c • F)

Real scalar multiplication preserves real-valuedness on the imaginary axis.

theorem UpperHalfPlane.RealOnImagAxis.pow {F : UpperHalfPlane → ℂ} (hF : RealOnImagAxis F) (n : ℕ) : RealOnImagAxis (F ^ n)

Natural powers preserve real-valuedness on the imaginary axis.

Positivity is preserved by the algebraic operations

theorem UpperHalfPlane.PosOnImagAxis.const {c : ℝ} (hc : 0 < c) : PosOnImagAxis fun (x : UpperHalfPlane) => ↑c

A positive real constant is positive on the imaginary axis.

theorem UpperHalfPlane.PosOnImagAxis.one : PosOnImagAxis fun (x : UpperHalfPlane) => 1

The constant function 1 is positive on the imaginary axis.

theorem UpperHalfPlane.PosOnImagAxis.add {F G : UpperHalfPlane → ℂ} (hF : PosOnImagAxis F) (hG : PosOnImagAxis G) : PosOnImagAxis (F + G)

Addition preserves positivity on the imaginary axis.

theorem UpperHalfPlane.PosOnImagAxis.mul {F G : UpperHalfPlane → ℂ} (hF : PosOnImagAxis F) (hG : PosOnImagAxis G) : PosOnImagAxis (F * G)

Multiplication preserves positivity on the imaginary axis: the two restrictions are real there, so the real part of the product is the product of the real parts.

theorem UpperHalfPlane.PosOnImagAxis.const_smul {F : UpperHalfPlane → ℂ} {c : ℝ} (hF : PosOnImagAxis F) (hc : 0 < c) : PosOnImagAxis (c • F)

Positive scalar multiplication preserves positivity on the imaginary axis.

theorem UpperHalfPlane.PosOnImagAxis.pow {F : UpperHalfPlane → ℂ} (hF : PosOnImagAxis F) (n : ℕ) : PosOnImagAxis (F ^ n)

Natural powers preserve positivity on the imaginary axis.

Eventual positivity is preserved by the algebraic operations

theorem UpperHalfPlane.PosOnImagAxis.eventuallyPos {F : UpperHalfPlane → ℂ} (hF : PosOnImagAxis F) : EventuallyPosOnImagAxis F

Positivity everywhere implies positivity far out.

theorem UpperHalfPlane.EventuallyPosOnImagAxis.one : EventuallyPosOnImagAxis fun (x : UpperHalfPlane) => 1

The constant function 1 is eventually positive on the imaginary axis.

theorem UpperHalfPlane.EventuallyPosOnImagAxis.const {c : ℝ} (hc : 0 < c) : EventuallyPosOnImagAxis fun (x : UpperHalfPlane) => ↑c

A positive real constant is eventually positive on the imaginary axis.

theorem UpperHalfPlane.EventuallyPosOnImagAxis.add {F G : UpperHalfPlane → ℂ} (hF : EventuallyPosOnImagAxis F) (hG : EventuallyPosOnImagAxis G) : EventuallyPosOnImagAxis (F + G)

Addition preserves eventual positivity on the imaginary axis.

theorem UpperHalfPlane.EventuallyPosOnImagAxis.mul {F G : UpperHalfPlane → ℂ} (hF : EventuallyPosOnImagAxis F) (hG : EventuallyPosOnImagAxis G) : EventuallyPosOnImagAxis (F * G)

Multiplication preserves eventual positivity on the imaginary axis.

theorem UpperHalfPlane.EventuallyPosOnImagAxis.const_smul {F : UpperHalfPlane → ℂ} {c : ℝ} (hF : EventuallyPosOnImagAxis F) (hc : 0 < c) : EventuallyPosOnImagAxis (c • F)

Positive scalar multiplication preserves eventual positivity on the imaginary axis.

theorem UpperHalfPlane.EventuallyPosOnImagAxis.pow {F : UpperHalfPlane → ℂ} (hF : EventuallyPosOnImagAxis F) (n : ℕ) : EventuallyPosOnImagAxis (F ^ n)

Natural powers preserve eventual positivity on the imaginary axis.