OAI/Geometry/SurfaceImmersion/Correction/CompactSmoothCutoffs.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.CollarVelocity.compact_open_thickening line 15
2. theorem OAI.ClosedSurfaceR4.CollarVelocity.compact_cutoff line 25
3. theorem OAI.ClosedSurfaceR4.CollarVelocity.nested_compact_cutoffs line 45

   Source documentation

   The inner cutoff is one on an open collar, and the outer one is one on the whole closed support of the inner cutoff.

   theorem nested_compact_cutoffs {K U : Set E} (hK : IsCompact K)
       (hU : IsOpen U) (hKU : K ⊆ U) :
       ∃ W : Set E, IsOpen W ∧ K ⊆ W ∧ W ⊆ U ∧
         ∃ φ χ : E → ℝ, ContDiff ℝ ∞ φ ∧ ContDiff ℝ ∞ χ ∧
           HasCompactSupport φ ∧ HasCompactSupport χ ∧
           (∀ x, φ x ∈ Icc (0 : ℝ) 1) ∧ (∀ x, χ x ∈ Icc (0 : ℝ) 1) ∧
           tsupport χ ⊆ U ∧ tsupport φ ⊆ U ∧
           (∀ x ∈ W, φ x = 1) ∧ (∀ x ∈ tsupport φ, χ x = 1) := by
   …

4. lemma OAI.ClosedSurfaceR4.CollarVelocity.supported_local_mul line 64
5. lemma OAI.ClosedSurfaceR4.CollarVelocity.supported_local_smul line 79
6. theorem OAI.ClosedSurfaceR4.CollarVelocity.compact_smooth_extension line 94