Source indexedlemma · leanprover/lean4:v4.32.0

CH2.IsBoundedNoPolesOn.analytic_mul

PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3460 to 3472

Source documentation

Multiplying a bounded-with-no-poles function by an analytic factor that is uniformly bounded on the set preserves IsBoundedNoPolesOn.

Exact Lean statement

lemma IsBoundedNoPolesOn.analytic_mul {g h : ℂ → ℂ} {S : Set ℂ} {C : ℝ}
    (hh : IsBoundedNoPolesOn h S) (hh_mero : ∀ z ∈ S, MeromorphicAt h z)
    (hg_an : ∀ z ∈ S, AnalyticAt ℂ g z) (hg_bd : ∀ z ∈ S, ‖g z‖ ≤ C) :
    IsBoundedNoPolesOn (fun s ↦ g s * h s) S

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma IsBoundedNoPolesOn.analytic_mul {g h : ℂ → ℂ} {S : Set ℂ} {C : ℝ}    (hh : IsBoundedNoPolesOn h S) (hh_mero : ∀ z ∈ S, MeromorphicAt h z)    (hg_an : ∀ z ∈ S, AnalyticAt ℂ g z) (hg_bd : ∀ z ∈ S, ‖g z‖ ≤ C) :    IsBoundedNoPolesOn (fun s ↦ g s * h s) S := by  obtain ⟨M, hM⟩ := hh  refine ⟨C * M, fun z hz ↦ ⟨?_, ?_⟩⟩  · have hCnn : 0 ≤ C := le_trans (norm_nonneg _) (hg_bd z hz)    calc ‖g z * h z‖ = ‖g z‖ * ‖h z‖ := norm_mul _ _      _ ≤ C * ‖h z‖ := mul_le_mul_of_nonneg_right (hg_bd z hz) (norm_nonneg _)      _ ≤ C * M := mul_le_mul_of_nonneg_left (hM z hz).1 hCnn  · rw [show (fun s ↦ g s * h s) = g * h from rfl,      meromorphicOrderAt_mul (hg_an z hz).meromorphicAt (hh_mero z hz)]    exact add_nonneg (hg_an z hz).meromorphicOrderAt_nonneg (hM z hz).2