FuchsianFamily.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SepticProfile.Fuchsian.exists_continuous_fuchsian_disk line 15

Source documentation

Uniform small-radius inversion and contraction constructs a continuously parameterized family. In the source application H is the exact finite-jet remainder map, whose bounds and continuity must be independently supplied.

theorem exists_continuous_fuchsian_disk {A : Type*} [TopologicalSpace A]
    (c : A → ℝ) (hc : Continuous c) (hc1 : ∀ a, 1 ≤ c a)
    {r R M L : ℝ} (hr : 0 ≤ r) (hR : 0 ≤ R)
    (hrM : r*M ≤ R) (hrL : r*L ≤ 1/2)
    (H : A → analyticDisk → analyticDisk)
    (hbound : ∀ a f, ‖f‖ ≤ R → ‖H a f‖ ≤ M)
    (hlip : ∀ a f g, ‖f‖ ≤ R → ‖g‖ ≤ R → ‖H a f-H a g‖ ≤ L*‖f-g‖)
    (hcont : ∀ f, ‖f‖ ≤ R → Continuous (fun a => H a f))
    (P : Set analyticDisk) (hPc : IsClosed P) (hP0 : 0 ∈ P)
    (hP : ∀ a f, f ∈ P → ‖f‖ ≤ R → (r:ℂ) • inverse (c a) (H a f) ∈ P) :
    ∃ f : A → analyticDisk, Continuous f ∧ (∀ a, f a ∈ P ∧ ‖f a‖ ≤ R) ∧
      (∀ a, extend (f a : DiskMap) 0=0) ∧
…

Mentions: OAI.SepticProfile.Fuchsian.analyticDisk, OAI.SepticProfile.Fuchsian.inverse, OAI.SepticProfile.Fuchsian.extend, OAI.SepticProfile.Fuchsian.DiskMap

lemma OAI.SepticProfile.Fuchsian.continuous_nonlinearDisk_family line 89