49structure SampledRing (n : ℕ) where 50 center : ℂ 51 radius : ℝ 52 radius_pos : 0 < radius 53 increments : Fin (8 * n) → ℝ 54 winding : ℤ 55 winding_constraint : ∑ j, increments j = -(2 * Real.pi * winding) 56 winding_from_contour : winding = 0 57 58/-- Convert a `SampledRing` to an `AnnularRingSample`. -/ 59def SampledRing.toAnnularRingSample {n : ℕ} (sr : SampledRing n) : 60 AnnularRingSample n where 61 increments := sr.increments
proof body
Definition body.
62 winding := sr.winding 63 winding_constraint := sr.winding_constraint 64 65/-- The winding of a sampled ring from a zero-winding carrier is 0. -/ 66theorem SampledRing.winding_zero {n : ℕ} (sr : SampledRing n) : 67 sr.winding = 0 := sr.winding_from_contour 68 69/-- The converted `AnnularRingSample` inherits the zero winding. -/ 70theorem SampledRing.toAnnularRingSample_winding_zero {n : ℕ} (sr : SampledRing n) : 71 sr.toAnnularRingSample.winding = 0 := sr.winding_from_contour 72 73/-! ### §2. Constructing sampled rings from a zero-winding cert -/ 74 75/-- Construct a sampled ring from a `ZeroWindingCert` at ring level `n`. 76Uses uniform increments (all zero) since the carrier has zero winding. 77The actual phase values are zero because the net phase change around 78any circle is zero for a zero-winding function. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.