Roadmap area
ConformalMapping
Items in scope
Rouché, for the disc, from the ConformalMapping roadmap's L0 layer: if ‖f z - g z‖ < ‖f z‖ on sphere c R, then f and g have equal zero counts in ball c R.
Only this one target. The rest of L0 (Hurwitz, the open-mapping degree) and all of L1–L6 are left open for others.
Notes
Per the roadmap README's Coordination with upstream Mathlib: this is L0 material that mathlib4#33505 proves internally as private lemmas, so the PR will cite it and be declared a temporary shim, to be deleted and refactored onto Mathlib's version once it lands. The value added is named, discoverable API, not first proof.
Depends on the ContourIntegration argument principle; a prerequisite restating it against Mathlib's MeromorphicOn.divisor is open as TauCetiProject/TauCeti#1167.
Worked on by @JeremyKahn, with an AI implementor.
Roadmap area
ConformalMapping
Items in scope
Rouché, for the disc, from the ConformalMapping roadmap's L0 layer: if
‖f z - g z‖ < ‖f z‖onsphere c R, thenfandghave equal zero counts inball c R.Only this one target. The rest of L0 (Hurwitz, the open-mapping degree) and all of L1–L6 are left open for others.
Notes
Per the roadmap README's Coordination with upstream Mathlib: this is L0 material that mathlib4#33505 proves internally as private lemmas, so the PR will cite it and be declared a temporary shim, to be deleted and refactored onto Mathlib's version once it lands. The value added is named, discoverable API, not first proof.
Depends on the ContourIntegration argument principle; a prerequisite restating it against Mathlib's
MeromorphicOn.divisoris open as TauCetiProject/TauCeti#1167.Worked on by @JeremyKahn, with an AI implementor.