`LocalMeromorphicWitness`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.MeromorphicCircleOrder
domain: NumberTheory
line: 51 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.MeromorphicCircleOrder on GitHub at line 51.

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

  48
  49/-! ### §1. Local meromorphic factorization -/
  50
  51structure LocalMeromorphicWitness where
  52  center : ℂ
  53  order : ℤ
  54  radius : ℝ
  55  radius_pos : 0 < radius
  56  regularFactor : ℂ → ℂ
  57  regularFactor_analytic : AnalyticAt ℂ regularFactor center
  58  regularFactor_diff : DifferentiableOn ℂ regularFactor (Metric.closedBall center radius)
  59  regularFactor_nz : ∀ z ∈ Metric.closedBall center radius, regularFactor z ≠ 0
  60
  61/-- Restrict a local meromorphic witness to any smaller positive radius. -/
  62def LocalMeromorphicWitness.shrinkRadius
  63    (w : LocalMeromorphicWitness) (r : ℝ) (hr : 0 < r) (hrw : r ≤ w.radius) :
  64    LocalMeromorphicWitness where
  65  center := w.center
  66  order := w.order
  67  radius := r
  68  radius_pos := hr
  69  regularFactor := w.regularFactor
  70  regularFactor_analytic := w.regularFactor_analytic
  71  regularFactor_diff := by
  72    refine w.regularFactor_diff.mono ?_
  73    intro z hz
  74    exact Metric.mem_closedBall.mpr <|
  75      le_trans (Metric.mem_closedBall.mp hz) hrw
  76  regularFactor_nz := by
  77    intro z hz
  78    exact w.regularFactor_nz z <| Metric.mem_closedBall.mpr <|
  79      le_trans (Metric.mem_closedBall.mp hz) hrw
  80
  81/-- Extract a genuine local meromorphic factorization from Mathlib's

papers checked against this theorem

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