Order, canonical value, and holoRepr on germ classes (CC3, D3/D5)

Unit: meromorphic-and-divisors (docs/design/meromorphic-and-divisors.md §4.4, proof plans §6.4/6.5).

• MeroGermOn.ord φ x : WithTop ℤ: the order of a class at a point (junk 0 off IsOpen U ∧ x ∈ U); descends from ordAtX (meromorphy-free congr).
• MeroGermOn.evalAt φ x : ℂ: the canonical value (D5) — the limit along 𝓝[≠] x when 0 ≤ ord, junk 0 else.
• MeroGermOn.holoRepr φ : X → ℂ := fun x => φ.evalAt x: the canonical repaired representative. holoRepr_contMDiffAt shows it is honestly holomorphic wherever 0 ≤ ord; mk_holoRepr shows it recovers φ as a class. This is the rigidified normal form the blueprint needs for Čech.

theorem RS.limUnder_congr {α : Type u_2} {l : Filter α} {g g' : α → ℂ} (h : g =ᶠ[l] g') : l.limUnder g = l.limUnder g'

limUnder respects EventuallyEq (via Filter.map_congr, since limUnder l f = lim (map f l)).

ord

noncomputable def RS.MeroGermOn.ord {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (φ : MeroGermOn X U) (x : X) : WithTop ℤ

Order of a germ class at a point; junk 0 unless IsOpen U ∧ x ∈ U (D3).

Equations

• φ.ord x = (↑φ).liftOn (fun (f : X → ℂ) => if IsOpen U ∧ x ∈ U then RS.ordAtX f x else 0) ⋯

theorem RS.MeroGermOn.ord_apply_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (f : X → ℂ) (hf : MeromorphicOnX f U) (x : X) : (mk f hf).ord x = if IsOpen U ∧ x ∈ U then ordAtX f x else 0

@[simp]

theorem RS.MeroGermOn.ord_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} (hU : IsOpen U) (hx : x ∈ U) {f : X → ℂ} {hf : MeromorphicOnX f U} : (mk f hf).ord x = ordAtX f x

theorem RS.MeroGermOn.ord_restrict {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U V : Set X} (h : V ⊆ U) (hV : IsOpen V) (hU : IsOpen U) {x : X} (hx : x ∈ V) (φ : MeroGermOn X U) : ((restrict h) φ).ord x = φ.ord x

theorem RS.MeroGermOn.ord_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} : ord 0 x = if IsOpen U ∧ x ∈ U then ⊤ else 0

theorem RS.MeroGermOn.ord_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} (hU : IsOpen U) (hx : x ∈ U) : ord 1 x = 0

theorem RS.MeroGermOn.ord_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} (hU : IsOpen U) (hx : x ∈ U) (φ ψ : MeroGermOn X U) : min (φ.ord x) (ψ.ord x) ≤ (φ + ψ).ord x

theorem RS.MeroGermOn.ord_add_of_ne {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} (hU : IsOpen U) (hx : x ∈ U) {φ ψ : MeroGermOn X U} (h : φ.ord x ≠ ψ.ord x) : (φ + ψ).ord x = min (φ.ord x) (ψ.ord x)

theorem RS.MeroGermOn.ord_mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} (hU : IsOpen U) (hx : x ∈ U) (φ ψ : MeroGermOn X U) : (φ * ψ).ord x = φ.ord x + ψ.ord x

theorem RS.MeroGermOn.ord_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} (φ : MeroGermOn X U) : (-φ).ord x = φ.ord x

theorem RS.MeroGermOn.ord_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} {c : ℂ} (hU : IsOpen U) (hx : x ∈ U) (hc : c ≠ 0) (φ : MeroGermOn X U) : (c • φ).ord x = φ.ord x

theorem RS.MeroGermOn.ord_algebraMap {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} {c : ℂ} (hU : IsOpen U) (hx : x ∈ U) (hc : c ≠ 0) : ((algebraMap ℂ (MeroGermOn X U)) c).ord x = 0

evalAt (D5)

noncomputable def RS.MeroGermOn.evalAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (φ : MeroGermOn X U) (x : X) : ℂ

Canonical value (D5): the limit along 𝓝[≠] x when 0 ≤ ord, junk 0 else.

Equations

• φ.evalAt x = (↑φ).liftOn (fun (f : X → ℂ) => if (IsOpen U ∧ x ∈ U) ∧ 0 ≤ RS.ordAtX f x then (nhdsWithin x {x}ᶜ).limUnder f else 0) ⋯

theorem RS.MeroGermOn.evalAt_apply_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (f : X → ℂ) (hf : MeromorphicOnX f U) (x : X) : (mk f hf).evalAt x = if (IsOpen U ∧ x ∈ U) ∧ 0 ≤ ordAtX f x then (nhdsWithin x {x}ᶜ).limUnder f else 0

theorem RS.MeroGermOn.tendsto_evalAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} (hU : IsOpen U) (hx : x ∈ U) (φ : MeroGermOn X U) (h : 0 ≤ φ.ord x) {f : X → ℂ} {hf : MeromorphicOnX f U} (hrep : mk f hf = φ) : Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds (φ.evalAt x))

@[simp]

theorem RS.MeroGermOn.evalAt_of_not_nonneg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {φ : MeroGermOn X U} {x : X} (h : ¬0 ≤ φ.ord x) : φ.evalAt x = 0

From here on, chart invariance is needed (ContMDiffAt/AnalyticAt bridges).

theorem RS.MeroGermOn.evalAt_mk_of_contMDiffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hU : IsOpen U) (hx : x ∈ U) {f : X → ℂ} {hf : MeromorphicOnX f U} (hc : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x) : (mk f hf).evalAt x = f x

theorem RS.MeroGermOn.evalAt_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} (hU : IsOpen U) (hx : x ∈ U) {φ ψ : MeroGermOn X U} (h1 : 0 ≤ φ.ord x) (h2 : 0 ≤ ψ.ord x) : (φ + ψ).evalAt x = φ.evalAt x + ψ.evalAt x

theorem RS.MeroGermOn.evalAt_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} {c : ℂ} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hU : IsOpen U) (hx : x ∈ U) {φ : MeroGermOn X U} (h : 0 ≤ φ.ord x) : (c • φ).evalAt x = c * φ.evalAt x

theorem RS.MeroGermOn.evalAt_mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} (hU : IsOpen U) (hx : x ∈ U) {φ ψ : MeroGermOn X U} (h1 : 0 ≤ φ.ord x) (h2 : 0 ≤ ψ.ord x) : (φ * ψ).evalAt x = φ.evalAt x * ψ.evalAt x

theorem RS.MeroGermOn.evalAt_restrict {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U V : Set X} (h : V ⊆ U) (hV : IsOpen V) (hU : IsOpen U) {x : X} (hx : x ∈ V) (φ : MeroGermOn X U) : ((restrict h) φ).evalAt x = φ.evalAt x

holoRepr (D5)

noncomputable def RS.MeroGermOn.holoRepr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (φ : MeroGermOn X U) : X → ℂ

CC3's holoRepr (D5): the canonical repaired representative.

Equations

• φ.holoRepr x = φ.evalAt x

theorem RS.MeroGermOn.holoRepr_eventuallyEq_nhdsNE {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hU : IsOpen U) (hx : x ∈ U) (φ : MeroGermOn X U) {f : X → ℂ} {hf : MeromorphicOnX f U} (hrep : mk f hf = φ) : φ.holoRepr =ᶠ[nhdsWithin x {x}ᶜ] f

holoRepr agrees with any representative off x (unconditionally on ord: near x the representative is automatically chart-analytic, MeromorphicAt.eventually_analyticAt).

theorem RS.MeroGermOn.holoRepr_contMDiffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hU : IsOpen U) (hx : x ∈ U) {φ : MeroGermOn X U} (h : 0 ≤ φ.ord x) : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ φ.holoRepr x

theorem RS.MeroGermOn.holoRepr_contMDiffOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hU : IsOpen U) {φ : MeroGermOn X U} (h : ∀ x ∈ U, 0 ≤ φ.ord x) : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ φ.holoRepr U

theorem RS.MeroGermOn.holoRepr_contMDiff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {φ : Mero X} (h : ∀ (x : X), 0 ≤ ord φ x) : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (holoRepr φ)

theorem RS.MeroGermOn.meromorphicOnX_holoRepr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hU : IsOpen U) (φ : MeroGermOn X U) : MeromorphicOnX φ.holoRepr U

theorem RS.MeroGermOn.mk_holoRepr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hU : IsOpen U) (φ : MeroGermOn X U) : mk φ.holoRepr ⋯ = φ

theorem RS.MeroGermOn.holoRepr_restrict {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U V : Set X} (h : V ⊆ U) (hV : IsOpen V) (hU : IsOpen U) (φ : MeroGermOn X U) : Set.EqOn ((restrict h) φ).holoRepr φ.holoRepr V

theorem RS.MeroGermOn.continuousAt_holoRepr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hU : IsOpen U) (hx : x ∈ U) {φ : MeroGermOn X U} (h : 0 ≤ φ.ord x) : ContinuousAt φ.holoRepr x

theorem RS.MeroGermOn.tendsto_holoRepr_cobounded_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hU : IsOpen U) (hx : x ∈ U) (φ : MeroGermOn X U) : Filter.Tendsto φ.holoRepr (nhdsWithin x {x}ᶜ) (Bornology.cobounded ℂ) ↔ φ.ord x < 0