CommonBranches.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Reparametrizing local branches by their common central component

For local homeomorphisms X,Z on the parameter component, the central parametrizations are X.symm and X.symm.trans Z. Their common source is open, contains the central base point, and inherits both smooth inverses.

def OAI.Problem356.CommonBranches.outer line 23
Source documentation
Reparametrization of the second outer branch by the central coordinate.
```
def outer (X Z : OpenPartialHomeomorph E E) : OpenPartialHomeomorph E E :=
…
```
theorem OAI.Problem356.CommonBranches.outer_apply line 26
theorem OAI.Problem356.CommonBranches.image_mem_outer_source line 31
Source documentation
Both local maps being defined at the parameter base point puts the central image in the source of the reparametrized outer branch.
```
theorem image_mem_outer_source (X Z : OpenPartialHomeomorph E E) {a : E}
    (haX : a ∈ X.source) (haZ : a ∈ Z.source) :
    X a ∈ (outer X Z).source := by
…
```
Mentions: OAI.Problem356.CommonBranches.outer
theorem OAI.Problem356.CommonBranches.outer_source_properties line 42
Source documentation
The common source permits both the inverse branch and the second outer branch, with their expected component containment and inverse identity.
```
theorem outer_source_properties (X Z : OpenPartialHomeomorph E E) {x : E}
    (hx : x ∈ (outer X Z).source) :
    x ∈ X.target ∧ X.symm x ∈ X.source ∧ X.symm x ∈ Z.source ∧
      outer X Z x ∈ Z.target ∧ X (X.symm x) = x := by
…
```
Mentions: OAI.Problem356.CommonBranches.outer
theorem OAI.Problem356.CommonBranches.contact_reparametrize line 52
Source documentation
Every contact predicate on the original graph transfers to the central parametrization. This includes both supporting equality and stationarity.
```
theorem contact_reparametrize (X Z : OpenPartialHomeomorph E E)
    {C : E × (E × E) → Prop}
    (hC : ∀ y ∈ X.source, C (X y, (y, Z y))) {x : E}
    (hx : x ∈ (outer X Z).source) :
    C (x, (X.symm x, outer X Z x)) := by
…
```
Mentions: OAI.Problem356.CommonBranches.outer
def OAI.Problem356.CommonBranches.four line 61
Source documentation
The four ordered outer branches associated with two local families.
```
def four (X Z : Fin 2 → OpenPartialHomeomorph E E) :
    Fin 4 → OpenPartialHomeomorph E E :=
…
```
theorem OAI.Problem356.CommonBranches.subset_four_sources line 67
Source documentation
A common domain for both composed branches is a common domain for all four outer branches, in the indexing used by the smooth marginal construction.
```
theorem subset_four_sources (X Z : Fin 2 → OpenPartialHomeomorph E E)
    {B : Set E} (hB : ∀ i, B ⊆ (outer (X i) (Z i)).source) :
    ∀ j, B ⊆ (four X Z j).source := by
…
```
Mentions: OAI.Problem356.CommonBranches.outer, OAI.Problem356.CommonBranches.four

theorem OAI.Problem356.CommonBranches.four_images_subset line 80

Source documentation

Image containment in the four prescribed outer components.

theorem four_images_subset (X Z : Fin 2 → OpenPartialHomeomorph E E)
    {B : Set E} (hB : ∀ i, B ⊆ (outer (X i) (Z i)).source)
    (P Q : Fin 2 → Set E)
    (hP : ∀ i, (X i).source ⊆ P i) (hQ : ∀ i, (Z i).target ⊆ Q i) :
    ∀ j, four X Z j '' B ⊆ ![P 0, Q 0, P 1, Q 1] j := by
…

Mentions: OAI.Problem356.CommonBranches.outer, OAI.Problem356.CommonBranches.four

theorem OAI.Problem356.CommonBranches.exists_common_central_ball line 100

Source documentation

Finitely many pairs of local branches sharing a central base point admit one positive-radius central ball on which all inverse parametrizations are defined. The ball may also be kept inside any prescribed central neighborhood.

theorem exists_common_central_ball {ι : Type uIndex} [Finite ι]
    (X Z : ι → OpenPartialHomeomorph M M) (a : ι → M) (x : M)
    (haX : ∀ i, a i ∈ (X i).source) (haZ : ∀ i, a i ∈ (Z i).source)
    (hcenter : ∀ i, X i (a i) = x)
    {U : Set M} (hU : IsOpen U) (hxU : x ∈ U) :
    ∃ r : ℝ, 0 < r ∧ ball x r ⊆ U ∧
      ∀ i, ball x r ⊆ (outer (X i) (Z i)).source := by
…

Mentions: OAI.Problem356.CommonBranches.outer

theorem OAI.Problem356.CommonBranches.exists_common_central_ball_in_components line 121

Source documentation

The central ball can simultaneously keep the inverse and composed branches inside arbitrary prescribed outer neighborhoods. Thus shrinking the global certificate components does not require changing either local chart.

theorem exists_common_central_ball_in_components {ι : Type uIndex} [Finite ι]
    (X Z : ι → OpenPartialHomeomorph M M) (a : ι → M) (x : M)
    (haX : ∀ i, a i ∈ (X i).source) (haZ : ∀ i, a i ∈ (Z i).source)
    (hcenter : ∀ i, X i (a i) = x)
    (P Q : ι → Set M) (hP : ∀ i, IsOpen (P i)) (hQ : ∀ i, IsOpen (Q i))
    (haP : ∀ i, a i ∈ P i) (haQ : ∀ i, Z i (a i) ∈ Q i)
    {U : Set M} (hU : IsOpen U) (hxU : x ∈ U) :
    ∃ r : ℝ, 0 < r ∧ ball x r ⊆ U ∧
      ∀ i, ∀ y ∈ ball x r,
        y ∈ (outer (X i) (Z i)).source ∧
        (X i).symm y ∈ P i ∧ outer (X i) (Z i) y ∈ Q i := by
…

Mentions: OAI.Problem356.CommonBranches.outer

theorem OAI.Problem356.CommonBranches.contDiffOn_outer line 169
Source documentation
Smoothness of the inverse central branch and original outer branch makes the reparametrized branch smooth on its actual open source.
```
theorem contDiffOn_outer {n : WithTop ENat} (X Z : OpenPartialHomeomorph F F)
    (hX : ContDiffOn ℝ n X.symm X.target)
    (hZ : ContDiffOn ℝ n Z Z.source) :
    ContDiffOn ℝ n (outer X Z) (outer X Z).source := by
…
```
Mentions: OAI.Problem356.CommonBranches.outer

theorem OAI.Problem356.CommonBranches.contDiffOn_outer_symm line 176

Source documentation

The inverse of the reparametrized branch is smooth on its actual target.

theorem contDiffOn_outer_symm {n : WithTop ENat} (X Z : OpenPartialHomeomorph F F)
    (hX : ContDiffOn ℝ n X X.source)
    (hZ : ContDiffOn ℝ n Z.symm Z.target) :
    ContDiffOn ℝ n (outer X Z).symm (outer X Z).target := by
…

Mentions: OAI.Problem356.CommonBranches.outer

theorem OAI.Problem356.CommonBranches.contDiffOn_four line 183

Source documentation

Forward smoothness of all four centrally parametrized branches.

theorem contDiffOn_four {n : WithTop ENat}
    (X Z : Fin 2 → OpenPartialHomeomorph F F)
    (hX : ∀ i, ContDiffOn ℝ n (X i).symm (X i).target)
    (hZ : ∀ i, ContDiffOn ℝ n (Z i) (Z i).source) :
    ∀ j, ContDiffOn ℝ n (four X Z j) (four X Z j).source := by
…

Mentions: OAI.Problem356.CommonBranches.four

theorem OAI.Problem356.CommonBranches.contDiffOn_four_symm line 196

Source documentation

Inverse smoothness of all four centrally parametrized branches.

theorem contDiffOn_four_symm {n : WithTop ENat}
    (X Z : Fin 2 → OpenPartialHomeomorph F F)
    (hX : ∀ i, ContDiffOn ℝ n (X i) (X i).source)
    (hZ : ∀ i, ContDiffOn ℝ n (Z i).symm (Z i).target) :
    ∀ j, ContDiffOn ℝ n (four X Z j).symm (four X Z j).target := by
…

Mentions: OAI.Problem356.CommonBranches.four