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

WitnessedDefectSensor

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)

 581structure WitnessedDefectSensor where
 582  rho : ℂ
 583  charge : ℤ
 584  in_strip : 1/2 < rho.re ∧ rho.re < 1
 585  order_witness : meromorphicOrderAt zetaReciprocal rho = ↑(-charge)
 586
 587/-- Forget the complex witness and retain only the abstract charge/real-part
 588sensor data used by the annular-cost framework. -/
 589def WitnessedDefectSensor.toDefectSensor (sensor : WitnessedDefectSensor) : DefectSensor where
 590  charge := sensor.charge

proof body

Definition body.

 591  realPart := sensor.rho.re
 592  in_strip := sensor.in_strip
 593
 594@[simp] theorem WitnessedDefectSensor.toDefectSensor_charge
 595    (sensor : WitnessedDefectSensor) :
 596    sensor.toDefectSensor.charge = sensor.charge := rfl
 597
 598@[simp] theorem WitnessedDefectSensor.toDefectSensor_realPart
 599    (sensor : WitnessedDefectSensor) :
 600    sensor.toDefectSensor.realPart = sensor.rho.re := rfl
 601
 602/-- A witnessed strip sensor is automatically away from the pole `s = 1`. -/
 603theorem WitnessedDefectSensor.rho_ne_one (sensor : WitnessedDefectSensor) :
 604    sensor.rho ≠ 1 := by
 605  intro h
 606  have hre : sensor.rho.re = 1 := by simpa [h]
 607  linarith [sensor.in_strip.2]
 608
 609/-- A local meromorphic factorization of `zetaReciprocal` at a hypothetical
 610zero ρ of ζ in the strip. The regular factor `g` is analytic and nonvanishing
 611on a closed disk, extracted from Mathlib's `meromorphicOrderAt_eq_int_iff`. -/

used by (27)

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

depends on (29)

Lean names referenced from this declaration's body.