Hopf problem: uniformization · special periods 4

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.AnalyticRootCover.exists_holomorphic_square_root_upperHalfPlane (f : UpperHalfPlane → ℂ) (hf : MDiff f) (hzero : ∀ (a : UpperHalfPlane), f a = 0 → ∃ (n : ℕ), analyticOrderAt (f ∘ ↑UpperHalfPlane.ofComplex) ↑a = ↑(2 * n)) : ∃ (r : UpperHalfPlane → ℂ), ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ r ∧ (∀ (a : UpperHalfPlane), r a ^ 2 = f a) ∧ ∀ (a : UpperHalfPlane) (n : ℕ), analyticOrderAt (f ∘ ↑UpperHalfPlane.ofComplex) ↑a = ↑(2 * n) → analyticOrderAt (r ∘ ↑UpperHalfPlane.ofComplex) ↑a = ↑n