UniformInputAtlasMeanData.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed atlas mean profiles from the global norms of the actual input map.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.uniform_input_atlas_mean_data_all_profiles line 22

Source documentation

The fixed local geometry determines all mean profiles and one global C2 radius before the nearby map, the scales, and the smaller trial radius.

theorem uniform_input_atlas_mean_data_all_profiles
    (F : M → Space) (hF : ContMDiff planeModel spaceModel ∞ F)
    (Ω U K : A.centers → Fin 3 → Set SmallModes.Base)
    (hΩ : ∀ i j, IsOpen (Ω i j)) (hU : ∀ i j, IsOpen (U i j))
    (hK : ∀ i j, IsCompact (K i j))
    (hUK : ∀ i j, U i j ⊆ K i j) (hKΩ : ∀ i j, K i j ⊆ Ω i j)
    (ξ : A.centers → Fin 3 → SmallModes.Base) (hξ : ∀ i j, ξ i j ≠ 0)
    (hImm : ∀ i j x, x ∈ Ω i j → Function.Injective
      (fderiv ℝ (spaceCoordinates ∘ A.vectorPlaneRead i F) x))
    (hgood : ∀ i j x, x ∈ Ω i j →
      Good (realSecondTensor (spaceCoordinates ∘ A.vectorPlaneRead i F) x) (ξ i j))
    (S : A.centers → Fin 3 → Compacts JetPolynomial.Base)
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.spaceCoordinates, OAI.ClosedSurfaceR4.JetPolynomial.Base

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.uniform_input_atlas_mean_data line 151

Source documentation

The fixed local geometry determines all mean profiles and one global C2 radius before the nearby map, the scales, and the smaller trial radius.

theorem uniform_input_atlas_mean_data
    (F : M → Space) (hF : ContMDiff planeModel spaceModel ∞ F)
    (Ω U K : A.centers → Fin 3 → Set SmallModes.Base)
    (hΩ : ∀ i j, IsOpen (Ω i j)) (hU : ∀ i j, IsOpen (U i j))
    (hK : ∀ i j, IsCompact (K i j))
    (hUK : ∀ i j, U i j ⊆ K i j) (hKΩ : ∀ i j, K i j ⊆ Ω i j)
    (ξ : A.centers → Fin 3 → SmallModes.Base) (hξ : ∀ i j, ξ i j ≠ 0)
    (hImm : ∀ i j x, x ∈ Ω i j → Function.Injective
      (fderiv ℝ (spaceCoordinates ∘ A.vectorPlaneRead i F) x))
    (hgood : ∀ i j x, x ∈ Ω i j →
      Good (realSecondTensor (spaceCoordinates ∘ A.vectorPlaneRead i F) x) (ξ i j))
    (S : A.centers → Fin 3 → Compacts JetPolynomial.Base)
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.spaceCoordinates, OAI.ClosedSurfaceR4.JetPolynomial.Base