SampledRing

formal source

  46/-- A sampled ring on ring level `n` (with `8n` sample points): phase increments
  47obtained by evaluating a function at equispaced points on a circle. The winding
  48is inherited from the contour winding layer. -/
  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
  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. -/
  79def mkSampledRing (cert : ZeroWindingCert) (n : ℕ) (_hn : 0 < n)