UniformPolynomialAtlasMeanData.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual perturbed polynomial mean families on a fixed smoothing atlas. The common geometric radius precedes the derivative profiles, the nearby map, and both scales.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.uniform_polynomial_input_atlas_mean_data_all_profiles line 24

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_polynomial_input_atlas_mean_data_all_profiles {n : A.centers → ℕ}
    (P : ∀ i : A.centers, Fin 3 → Fin (n i) → Expression)
    (hP : ∀ i k j, (P i k j).SmoothCoeffs univ)
    (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 →
…

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

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.uniform_polynomial_atlas_phase_mean_data_all_profiles line 156

Source documentation

The supported cutoff, phase, and coefficient form are constructed from the fixed atlas weights and phase bases. No solver or cutoff is supplied for the varying map.

theorem uniform_polynomial_atlas_phase_mean_data_all_profiles {n : A.centers → ℕ}
    (P : ∀ i : A.centers, Fin 3 → Fin (n i) → Expression)
    (hP : ∀ i k j, (P i k j).SmoothCoeffs univ)
    (F : M → Space) (hF : ContMDiff planeModel spaceModel ∞ F)
    (Q : A.centers → PhaseBasis) (w : A.centers → Fin 3 → ℝ)
    (hw : ∀ i j, w i j ≠ 0)
    (Ω 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)
    (hImm : ∀ i j x, x ∈ Ω i j → Function.Injective
      (fderiv ℝ (spaceCoordinates ∘ A.vectorPlaneRead i F) x))
…

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