OAI/Geometry/SurfaceImmersion/Correction/UniformLinearChartedMeanData.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual charted mean data with one profile for a nearby family. The positional jet is read on a fixed bounded original-coordinate domain.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.tensorOrder_emptyMetricPolynomial line 17
  2. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_linear_charted_mean_data_all_profiles line 22

    Source documentation

    A bounded original-coordinate domain and explicit weighted jet profiles give one charted-mean profile before the nearby map and both scales.

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

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

  3. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_linear_charted_mean_data line 214

    Source documentation

    A bounded original-coordinate domain and explicit weighted jet profiles give one charted-mean profile before the nearby map and both scales.

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

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