def
definition
eulerQuantitativeFactorization
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.EulerInstantiation on GitHub at line 624.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
radius -
carrier -
carrier -
of -
of -
of -
of -
carrierDerivBound -
carrierDerivBound_pos -
zetaReciprocal -
zetaReciprocal_local_factorization -
QuantitativeLocalFactorization -
M -
M
used by
formal source
621at a hypothetical zero ρ. The log-derivative bound `M` is taken from
622`carrierDerivBound(Re(ρ))`, which dominates the per-prime log-derivative
623terms by `eulerPrimeLogDerivTermComplex_summable`. -/
624noncomputable def eulerQuantitativeFactorization (ρ : ℂ)
625 (hρ_ne : ρ ≠ 1)
626 (m : ℤ)
627 (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m)
628 (hσ : 1/2 < ρ.re) :
629 QuantitativeLocalFactorization := by
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 }