Source indexedlemma · leanprover/lean4:v4.32.0

CH2.IsBoundedNoPolesOn.linear_mul

PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3492 to 3505

Source documentation

Multiplying a bounded-with-no-poles function h by an analytic factor φ whose growth is controlled by a weight w - ‖φ‖ ≤ C(‖w‖+1) - preserves IsBoundedNoPolesOn, provided the weighted product w · h is itself bounded with no poles. (Used for the Φ^\star = O(|z|) factors: the linear growth is absorbed by the extra decay of w · h = z(s) · F · x₀^s.)

Exact Lean statement

lemma IsBoundedNoPolesOn.linear_mul {φ w h : ℂ → ℂ} {S : Set ℂ} {C : ℝ}
    (hh : IsBoundedNoPolesOn h S) (hwh : IsBoundedNoPolesOn (fun s ↦ w s * h s) S)
    (hh_mero : ∀ z ∈ S, MeromorphicAt h z)
    (hφ_an : ∀ z ∈ S, AnalyticAt ℂ φ z) (hφ_bd : ∀ z ∈ S, ‖φ z‖ ≤ C * (‖w z‖ + 1)) :
    IsBoundedNoPolesOn (fun s ↦ φ s * h s) S

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma IsBoundedNoPolesOn.linear_mul {φ w h : ℂ → ℂ} {S : Set ℂ} {C : ℝ}    (hh : IsBoundedNoPolesOn h S) (hwh : IsBoundedNoPolesOn (fun s ↦ w s * h s) S)    (hh_mero : ∀ z ∈ S, MeromorphicAt h z)    (hφ_an : ∀ z ∈ S, AnalyticAt ℂ φ z) (hφ_bd : ∀ z ∈ S, ‖φ z‖ ≤ C * (‖w z‖ + 1)) :    IsBoundedNoPolesOn (fun s ↦ φ s * h s) S := by  obtain ⟨Mh, hMh⟩ := hh  obtain ⟨Mwh, hMwh⟩ := hwh  refine ⟨|C| * Mwh + |C| * Mh, fun z hz ↦ ⟨?_, ?_⟩⟩  · have hwh_z : ‖w z‖ * ‖h z‖ ≤ Mwh := by      have := (hMwh z hz).1; rwa [norm_mul] at this    exact norm_mul_le_of_linear_growth (hφ_bd z hz) (hMh z hz).1 hwh_z  · rw [show (fun s ↦ φ s * h s) = φ * h from rfl,      meromorphicOrderAt_mul (hφ_an z hz).meromorphicAt (hh_mero z hz)]    exact add_nonneg (hφ_an z hz).meromorphicOrderAt_nonneg (hMh z hz).2