`ContinuousPhaseData`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.CirclePhaseLift
domain: NumberTheory
line: 46 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.CirclePhaseLift on GitHub at line 46.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  43Packages a continuous real-valued function Θ : ℝ → ℝ representing the
  44argument of a nonvanishing function f along `circleMap c R`. The integer
  45`charge` is the winding number: Θ(2π) − Θ(0) = −2π·charge. -/
  46structure ContinuousPhaseData where
  47  center : ℂ
  48  radius : ℝ
  49  radius_pos : 0 < radius
  50  phase : ℝ → ℝ
  51  phase_continuous : Continuous phase
  52  charge : ℤ
  53  phase_winding : phase (2 * π) - phase 0 = -(2 * π * (charge : ℝ))
  54
  55/-! ### §2. Sampling into AnnularRingSample -/
  56
  57/-- Sample phase increments at `8n` equispaced angles.
  58Increment k is Θ(2π(k+1)/(8n)) − Θ(2πk/(8n)). -/
  59def ContinuousPhaseData.sampleIncrements
  60    (cpd : ContinuousPhaseData) (n : ℕ) : Fin (8 * n) → ℝ :=
  61  fun k =>
  62    cpd.phase (2 * π * ((k.val : ℝ) + 1) / (8 * (n : ℝ))) -
  63    cpd.phase (2 * π * (k.val : ℝ) / (8 * (n : ℝ)))
  64
  65/-- The sampled increments telescope to the total phase change.
  66
  67**Proof route**: standard Finset telescoping sum. The last sample point
  682π · (8n)/(8n) = 2π coincides with the right endpoint, and the first
  69sample point 2π · 0/(8n) = 0 coincides with the left endpoint, so the
  70sum collapses to Θ(2π) − Θ(0) = −2π · charge. -/
  71theorem ContinuousPhaseData.sample_winding_constraint
  72    (cpd : ContinuousPhaseData) (n : ℕ) (hn : 0 < n) :
  73    ∑ j, cpd.sampleIncrements n j = -(2 * π * (cpd.charge : ℝ)) := by
  74  let f : ℕ → ℝ := fun k => cpd.phase (2 * π * (k : ℝ) / (8 * (n : ℝ)))
  75  have hsum :
  76      (∑ j, cpd.sampleIncrements n j) =

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.