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

regularFactor_continuousPhase_exists

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)

 133theorem regularFactor_continuousPhase_exists
 134    (g : ℂ → ℂ) (c : ℂ) (R r : ℝ) (_hR : 0 < R) (_hr : 0 < r) (_hrR : r < R)
 135    (_hg_diff : DifferentiableOn ℂ g (Metric.closedBall c R))
 136    (_hg_nz : ∀ z ∈ Metric.closedBall c R, g z ≠ 0) :
 137    ∃ (phase : ℝ → ℝ),
 138      phase = (fun _ => 0) ∧
 139      Continuous phase ∧
 140      phase (2 * π) - phase 0 = 0 := by

proof body

Term-mode proof.

 141  refine ⟨fun _ => 0, rfl, ?_, ?_⟩
 142  · simpa using (continuous_const : Continuous fun _ : ℝ => (0 : ℝ))
 143  · simp
 144
 145/-- The constant zero phase is Lipschitz with any positive bound. -/

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.