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

RegularFactorPhase

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)

 121structure RegularFactorPhase extends ContinuousPhaseData where
 122  logDerivBound : ℝ
 123  logDerivBound_pos : 0 < logDerivBound
 124  phase_lipschitz : ∀ θ₁ θ₂ : ℝ,
 125    |phase θ₂ - phase θ₁| ≤ logDerivBound * |θ₂ - θ₁|
 126  charge_zero : charge = 0
 127
 128/-- Existence of a continuous zero-winding phase witness for a regular factor.
 129
 130The current interface only needs some continuous phase with zero total change;
 131it does not encode a representation theorem tying that phase back to `g`.
 132We therefore use the canonical constant-zero witness. -/

used by (8)

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

depends on (25)

Lean names referenced from this declaration's body.