pith. machine review for the scientific record. sign in
theorem proved tactic proof

norm_eulerPrimePowerComplex_lt_one

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)

 422theorem norm_eulerPrimePowerComplex_lt_one {s : ℂ} (hs : 0 < s.re)
 423    (p : Nat.Primes) :
 424    ‖eulerPrimePowerComplex p s‖ < 1 := by

proof body

Tactic-mode proof.

 425  rw [norm_eulerPrimePowerComplex]
 426  have hlog_pos : 0 < primeLog p := by
 427    have hp_one : (1 : ℝ) < p := by
 428      exact_mod_cast p.prop.one_lt
 429    simpa [primeLog] using Real.log_pos hp_one
 430  have hexp_lt : -s.re * primeLog p < 0 := by
 431    nlinarith
 432  have h := Real.exp_lt_exp.mpr hexp_lt
 433  simpa using h
 434
 435/-- The per-prime Euler eigenvalue stays strictly inside the unit disk on any
 436sensor circle contained in the strip. This is the first directly usable strip
 437estimate for building a sampled perturbation witness. -/

used by (3)

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

depends on (9)

Lean names referenced from this declaration's body.