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

defectSensorCirclePoint_mem_strip

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)

 392theorem defectSensorCirclePoint_mem_strip
 393    (sensor : DefectSensor) {r θ : ℝ}
 394    (hr_nonneg : 0 ≤ r) (hr : r < sensor.realPart - 1 / 2) :
 395    1 / 2 < (defectSensorCirclePoint sensor r θ).re := by

proof body

Term-mode proof.

 396  rw [defectSensorCirclePoint_re]
 397  have hcos : -1 ≤ Real.cos θ := Real.neg_one_le_cos θ
 398  nlinarith
 399
 400/-- Norm of the complex Euler eigenvalue is controlled exactly by the real part
 401of `s`. -/

used by (1)

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

depends on (12)

Lean names referenced from this declaration's body.