Assembly: Radó's theorem

Step 8 of Rado/PLAN.md: normalize a chart to contain the standard configuration (exists_config_chart), run Perron + barriers to get a nonconstant harmonic function on the connected open configY e, apply the Poincaré–Volterra lemma to the evaluation map on a connected component of the étale space of conjugate germs, descend along the open covering projection (secondCountable_configY), and cover X by that set together with a chart ball (secondCountableTopology_of_riemannSurface).

Assembly

theorem Rado.exists_config_chart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [Nonempty X] : ∃ e ∈ riemannAtlas X, Metric.ball 0 8 ⊆ e.target

Some maximal-atlas chart has target containing the standard configuration ball (affine renormalization of any chart, Rado.affine_trans_mem_riemannAtlas).

theorem Rado.locally_secondCountable_subtype {Z : Type u_2} [TopologicalSpace Z] {C : Set Z} (h : ∀ z ∈ C, ∃ (U : Set Z), z ∈ U ∧ IsOpen U ∧ SecondCountableTopology ↑U) (q : ↑C) : ∃ (W : Set ↑C), q ∈ W ∧ IsOpen W ∧ SecondCountableTopology ↑W

Transfer of local second countability to an open subspace.

theorem Rado.secondCountable_configY {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [T2Space X] [ConnectedSpace X] {e : OpenPartialHomeomorph X ℂ} (he : e ∈ riemannAtlas X) (hb : Metric.ball 0 8 ⊆ e.target) : SecondCountableTopology ↑(configY e)

The heart of the proof: Y = configY e is second countable, via Perron, the étale space of conjugate germs, and Poincaré–Volterra.

theorem Rado.secondCountableTopology_of_riemannSurface {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [T2Space X] [ConnectedSpace X] : SecondCountableTopology X

Radó's theorem, instance form: a connected Hausdorff Riemann surface is second countable. X = configY e ∪ (chart ball), both open and second countable.