OAI/Geometry/SurfaceImmersion/Correction/UniformLinearChartedMeanFamily.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData.atRadius line 15
2. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanProfile.Fits.atRadius line 37
3. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_linear_charted_mean_family_all_profiles line 50

   Source documentation

   Three local linear phases have one common perturbation radius and fixed mean profiles. The maps, slow scale, frequency and smaller trial radius are supplied only after those profiles have been chosen.

   theorem uniform_linear_charted_mean_family_all_profiles
       {F : Base → Space} (hF : ContDiff ℝ ∞ F)
       (Ω U K : Fin 3 → Set SmallModes.Base)
       (hΩ : ∀ j, IsOpen (Ω j)) (hU : ∀ j, IsOpen (U j))
       (hK : ∀ j, IsCompact (K j))
       (hUK : ∀ j, U j ⊆ K j) (hKΩ : ∀ j, K j ⊆ Ω j)
       (ξ : Fin 3 → SmallModes.Base) (hξ : ∀ j, ξ j ≠ 0)
       (hImm : ∀ j x, x ∈ Ω j → Function.Injective
         (fderiv ℝ (F ∘ planeCoordinateIsometry.symm) x))
       (hgood : ∀ j x, x ∈ Ω j →
         Good (realSecondTensor (F ∘ planeCoordinateIsometry.symm) x) (ξ j))
       (S : Fin 3 → Compacts Base)
   …

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

4. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_linear_charted_mean_family line 127

   Source documentation

   Three local linear phases have one common perturbation radius and fixed mean profiles. The maps, slow scale, frequency and smaller trial radius are supplied only after those profiles have been chosen.

   theorem uniform_linear_charted_mean_family
       {F : Base → Space} (hF : ContDiff ℝ ∞ F)
       (Ω U K : Fin 3 → Set SmallModes.Base)
       (hΩ : ∀ j, IsOpen (Ω j)) (hU : ∀ j, IsOpen (U j))
       (hK : ∀ j, IsCompact (K j))
       (hUK : ∀ j, U j ⊆ K j) (hKΩ : ∀ j, K j ⊆ Ω j)
       (ξ : Fin 3 → SmallModes.Base) (hξ : ∀ j, ξ j ≠ 0)
       (hImm : ∀ j x, x ∈ Ω j → Function.Injective
         (fderiv ℝ (F ∘ planeCoordinateIsometry.symm) x))
       (hgood : ∀ j x, x ∈ Ω j →
         Good (realSecondTensor (F ∘ planeCoordinateIsometry.symm) x) (ξ j))
       (S : Fin 3 → Compacts Base)
   …

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