OAI/Geometry/SurfaceImmersion/Primitive/LocalPeriodicGlobalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported local periodic coefficients extend smoothly by zero.

  1. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.contDiff_of_zero_off_closed line 21

    Source documentation

    Closed support lying inside the admissible domain suffices for smooth extension; there is no regularity requirement on the domain boundary.

    lemma contDiff_of_zero_off_closed {F : A × ℝ → E} {O K : Set A}
    (hO : IsOpen O) (hF : ContDiffOn ℝ ∞ F (O ×ˢ Set.univ))
    (hK : IsClosed K) (hKO : K ⊆ O) (hz : ∀ p ∉ K, ∀ t, F (p, t) = 0) :
    ContDiff ℝ ∞ F := by
…
  2. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.smooth_global line 38
  3. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.global line 49
  4. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.global_apply line 53
  5. theorem OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.exists_supported_coefficients line 64

    Source documentation

    The local recursion gives globally smooth coefficients when its initial input is supported in a closed subset of the admissible domain.

    theorem Geometry.exists_supported_coefficients {v : A} (g : Geometry (E := E) O v)
…

    Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry

  6. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.finiteAnsatz_smooth_global line 90
  7. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.finiteAnsatz_eq_off_support line 102