RegularWorkingChart.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The working chart and a total inverse for the actual patch data

theorem OAI.RegularPointCoordinates.restrict_open_coordinate_chart line 13

Source documentation

Restrict an existing open coordinate chart to a smaller open set.

theorem restrict_open_coordinate_chart {X E : Type*} [TopologicalSpace X]
    [TopologicalSpace E] {A U : Set X} {O : Set E} (hA : IsOpen A) (hO : IsOpen O)
    (hAU : A ⊆ U) (f : X → E) (u : U ≃ₜ O) (hu : ∀ x, (u x).val = f x.val) :
    IsOpen (Set.range (fun x : A => f x.val)) ∧
      ∃ v : A ≃ₜ Set.range (fun x : A => f x.val), ∀ x, (v x).val = f x.val := by
…

theorem OAI.RegularPointCoordinates.RegularBilinearData.patch_region_subset_initial line 29

theorem OAI.RegularPointCoordinates.regular_working_chart line 44

Source documentation

The region used for the finite heat nets is an open subchart of the previously constructed initial coordinate neighborhood.

theorem regular_working_chart {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    {base : X} {a κ B J C A Cχ enlargement zeta eta : ℝ}
    {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    (e : RegularProjectionEnvironment hX base hk a κ B J C A Cχ enlargement zeta eta)
    (hzeta : 0 ≤ zeta) (hzetaSmall : zeta ≤ 1 / 2048)
    (hgramSmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 4 : ℝ) ^ n)⁻¹) * zeta) ≤ 3 / 4) :
    IsOpen (Set.range (fun x : e.heat.patchRegion => e.heat.values x.val)) ∧
      ∃ chart : e.heat.patchRegion ≃ₜ Set.range (fun x : e.heat.patchRegion => e.heat.values x.val),
        ∀ x, (chart x).val = e.heat.values x.val := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment

theorem OAI.RegularPointCoordinates.exists_working_chart_inverse line 61

Source documentation

The inverse of a working chart, extended outside its image, takes values in the same original-space neighborhood as every energy field.

theorem exists_working_chart_inverse {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    [(hausdorff n X).Regular] {base : X} {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    {enlargement zeta : ℝ} (d : RegularBilinearData hX base hk enlargement zeta)
    {Ω : Set (Euclidean n)} (u : d.patchRegion ≃ₜ Ω)
    (hu : ∀ q, (u q).val = d.values q.val) :
    ∃ inverse : Euclidean n → {q : X // q ∈ ball base (d.radius / 32)},
      ∀ x ∈ Ω, (inverse x).val ∈ d.patchRegion ∧ d.values (inverse x).val = x := by
…

theorem OAI.RegularPointCoordinates.working_chart_inverse_left line 83

Source documentation

A right inverse lying in the working region is also a left inverse there, because these are the same open chart coordinates.

theorem working_chart_inverse_left {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    [(hausdorff n X).Regular] {base : X} {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    {enlargement zeta : ℝ} (d : RegularBilinearData hX base hk enlargement zeta)
    {Ω : Set (Euclidean n)} (u : d.patchRegion ≃ₜ Ω)
    (hu : ∀ q, (u q).val = d.values q.val)
    (inverse : Euclidean n → {q : X // q ∈ ball base (d.radius / 32)})
    (hinverse : ∀ x ∈ Ω, (inverse x).val ∈ d.patchRegion ∧ d.values (inverse x).val = x)
    {q : X} (hq : q ∈ d.patchRegion) : (inverse (d.values q)).val = q := by
…