noncomputable def ResToImagAxis (F : UpperHalfPlane → ℂ) : ℝ → ℂ

Restrict a function F : ℍ → ℂ to the positive imaginary axis, i.e. t ↦ F (I * t). If $t \le 0$, then F (I * t) is not defined, so we return 0 in that case.

Equations

• ResToImagAxis F t = if ht : 0 < t then F ⟨Complex.I * ↑t, ⋯⟩ else 0

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

Dot notation alias for ResToImagAxis.

Equations

• Function.resToImagAxis F = ResToImagAxis F

@[simp]

theorem Function.resToImagAxis_eq_resToImagAxis (F : UpperHalfPlane → ℂ) : resToImagAxis F = ResToImagAxis F

@[simp]

theorem Function.resToImagAxis_apply (F : UpperHalfPlane → ℂ) (t : ℝ) : resToImagAxis F t = ResToImagAxis F t

noncomputable def ResToImagAxis.Real (F : UpperHalfPlane → ℂ) : Prop

Function $F : \mathbb{H} \to \mathbb{C}$ whose restriction to the imaginary axis is real-valued.

Equations

• ResToImagAxis.Real F = ∃ (f : ℝ → ℝ), ∀ (t : ℝ) (ht : 0 < t), F ⟨Complex.I * ↑t, ⋯⟩ = ↑(f t)

noncomputable def ResToImagAxis.Pos (F : UpperHalfPlane → ℂ) : Prop

Function $F : \mathbb{H} \to \mathbb{C}$ is postive on the imaginary axis.

Equations

• ResToImagAxis.Pos F = ∀ (t : ℝ), 0 < t → ∃ (r : ℝ), 0 < r ∧ Function.resToImagAxis F t = ↑r

noncomputable def ResToImagAxis.EventuallyPos (F : UpperHalfPlane → ℂ) : Prop

Function $F : \mathbb{H} \to \mathbb{C}$ whose restriction to the imaginary axis is eventually positive, i.e. there exists $t_0 > 0$ such that for all $t \ge t_0$, $F(it)$ is positive.

Equations

• ResToImagAxis.EventuallyPos F = ∃ (t₀ : ℝ), 0 < t₀ ∧ ∀ (t : ℝ), t₀ ≤ t → ∃ (r : ℝ), 0 < r ∧ Function.resToImagAxis F t = ↑r

theorem ResToImagAxis.Differentiable (F : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) (t : ℝ) (ht : 0 < t) : DifferentiableAt ℝ (Function.resToImagAxis F) t

theorem ResToImagAxis.SlashActionS (F : UpperHalfPlane → ℂ) (k : ℤ) (t : ℝ) (ht : 0 < t) : Function.resToImagAxis (SlashAction.map k ModularGroup.S F) t = Complex.I ^ k * ↑t ^ (-k) * Function.resToImagAxis F (1 / t)

Restriction and slash action under S: $(F |_k S) (it) = t^{-k} * F(it)$