pith. machine review for the scientific record. sign in
def definition def or abbrev

eulerQuantitativeFactorization

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 624noncomputable def eulerQuantitativeFactorization (ρ : ℂ)
 625    (hρ_ne : ρ ≠ 1)
 626    (m : ℤ)
 627    (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m)
 628    (hσ : 1/2 < ρ.re) :
 629    QuantitativeLocalFactorization := by

proof body

Definition body.

 630  let w := (zetaReciprocal_local_factorization ρ hρ_ne m hord).choose
 631  let M : ℝ := carrierDerivBound ρ.re
 632  let r : ℝ := min w.radius (1 / M)
 633  have hM_pos : 0 < M := carrierDerivBound_pos hσ
 634  have hr_pos : 0 < r := by
 635    dsimp [r]
 636    exact lt_min w.radius_pos (one_div_pos.mpr hM_pos)
 637  refine
 638    { toLocalMeromorphicWitness :=
 639        w.shrinkRadius r hr_pos (by
 640          dsimp [r]
 641          exact min_le_left _ _)
 642      logDerivBound := M
 643      logDerivBound_pos := hM_pos
 644      perturbation_regime := by
 645        have hM_nonneg : 0 ≤ M := le_of_lt hM_pos
 646        have hr_le : r ≤ 1 / M := by
 647          dsimp [r]
 648          exact min_le_right _ _
 649        have hM_ne : M ≠ 0 := ne_of_gt hM_pos
 650        calc
 651          M * r ≤ M * (1 / M) := by
 652            exact mul_le_mul_of_nonneg_left hr_le hM_nonneg
 653          _ = 1 := by
 654            simpa [one_div] using mul_inv_cancel₀ hM_ne }
 655
 656/-- The log-derivative bound of the Euler quantitative factorization
 657equals the carrier derivative bound at `σ₀ = Re(ρ)`. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.