CircleLifts.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Real lifts of circle coordinates near filling disks

The quotient ℝ → ℝ/ℤ is a covering map in Mathlib. Its lifting theorem therefore gives actual continuous real branches on simply connected open sets. Smoothness is expressed in the ordinary real quotient charts AddCircle.equivIco; a continuous lift is locally one of these charts plus an integer, so the lift is smooth. No external lifting axiom is used.

def OAI.CircleDomainRigidity.FiniteTransfer.SmoothCircleOn line 27
Source documentation
Smoothness in every real quotient chart whose cut point is absent. This uses the actual ℝ/ℤ charts, without requiring a separate manifold instance for AddCircle.
```
def SmoothCircleOn {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : E → UnitAddCircle) (U : Set E) : Prop :=
…
```
theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothCircleOn_coe line 34
Source documentation
Ordinary smooth real coordinates project to smooth circle coordinates in the explicit quotient-chart definition.
```
theorem smoothCircleOn_coe
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {U : Set E} (hU : IsOpen U) {u : E → ℝ} (hu : ContDiffOn ℝ ∞ u U) :
    SmoothCircleOn (fun x => (u x : UnitAddCircle)) U := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.SmoothCircleOn
theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_continuous_circle_lift line 52

theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiffOn_circle_lift line 79

Source documentation

Smooth circle charts automatically make any continuous real lift smooth, by local injectivity of the quotient on an interval of length one.

theorem contDiffOn_circle_lift
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {U : Set E} (hU : IsOpen U) {f : E → UnitAddCircle} {u : E → ℝ}
    (hu : ContinuousOn u U) (hlift : ∀ x ∈ U, (u x : UnitAddCircle) = f x)
    (hf : SmoothCircleOn f U) : ContDiffOn ℝ ∞ u U := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.SmoothCircleOn

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_smooth_circle_lift line 102
theorem OAI.CircleDomainRigidity.FiniteTransfer.isSimplyConnected_homeomorph_ball line 113

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_smooth_circle_lift_near_jordan_disk line 123

Source documentation

The entire closed filling disk has one slightly larger simply connected neighborhood avoiding the singular set. The real branch is smooth on this whole neighborhood, hence on all sufficiently small collars.

theorem exists_smooth_circle_lift_near_jordan_disk
    (H : ℂ ≃ₜ ℂ) {S : Set ℂ} (hS : IsClosed S)
    (havoid : Disjoint (closure (jordanInterior H)) S)
    (f : ℂ → UnitAddCircle) (hf : ContinuousOn f Sᶜ) (hfs : SmoothCircleOn f Sᶜ) :
    ∃ (V : Set ℂ) (u : ℂ → ℝ), IsOpen V ∧ closure (jordanInterior H) ⊆ V ∧
      V ⊆ Sᶜ ∧ ContDiffOn ℝ ∞ u V ∧ ∀ x ∈ V, (u x : UnitAddCircle) = f x := by
…

Mentions: OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.SmoothCircleOn

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_simultaneous_smooth_circle_lifts line 154

Source documentation

The finite coordinate family has a common open branch neighborhood around each closed filling disk.

theorem exists_simultaneous_smooth_circle_lifts
    {I L : Type*} [Fintype L]
    (H : I → ℂ ≃ₜ ℂ) (S : L → Set ℂ) (hS : ∀ l, IsClosed (S l))
    (havoid : ∀ i l, Disjoint (closure (jordanInterior (H i))) (S l))
    (f : L → ℂ → UnitAddCircle)
    (hf : ∀ l, ContinuousOn (f l) (S l)ᶜ) (hfs : ∀ l, SmoothCircleOn (f l) (S l)ᶜ) :
    ∃ (O : I → Set ℂ) (u : I → L → ℂ → ℝ),
      (∀ i, IsOpen (O i) ∧ closure (jordanInterior (H i)) ⊆ O i) ∧
      ∀ i l, O i ⊆ (S l)ᶜ ∧ ContDiffOn ℝ ∞ (u i l) (O i) ∧
        ∀ x ∈ O i, (u i l x : UnitAddCircle) = f l x := by
…

Mentions: OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.SmoothCircleOn

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_smooth_circle_lift_of_projected_avoidance line 177

Source documentation

Closed quotient singularities pull back to exactly the obstacle used in the physical lifting theorem.

theorem exists_smooth_circle_lift_of_projected_avoidance
    {X : Type*} [TopologicalSpace X] (q : ℂ → X) (hq : Continuous q)
    (H : ℂ ≃ₜ ℂ) {S : Set X} (hS : IsClosed S)
    (havoid : Disjoint (q '' closure (jordanInterior H)) S)
    (f : ℂ → UnitAddCircle) (hf : ContinuousOn f (q ⁻¹' S)ᶜ)
    (hfs : SmoothCircleOn f (q ⁻¹' S)ᶜ) :
    ∃ (V : Set ℂ) (u : ℂ → ℝ), IsOpen V ∧ closure (jordanInterior H) ⊆ V ∧
      V ⊆ q ⁻¹' Sᶜ ∧ ContDiffOn ℝ ∞ u V ∧ ∀ x ∈ V, (u x : UnitAddCircle) = f x := by
…

Mentions: OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.SmoothCircleOn