OAI/Geometry/SurfaceImmersion/Correction/SmoothingLocalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize line 16
2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize_chart line 19
3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize_zero_off_image line 24
4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize_tsupport line 36
5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize_compact line 45
6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize_tsupport_inter line 51

   Source documentation

   Both scalar localization and input support are retained in coordinates.

   lemma localize_tsupport_inter (p : M) {ψ : M → ℝ}
       (hψ : tsupport ψ ⊆ (chart p).source) (f : M → V) :
       tsupport (localize p ψ f) ⊆ (chart p) '' (tsupport ψ ∩ tsupport f) := by
   …

   Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize

7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize_smooth line 76

   Source documentation

   Extension by zero is smooth because the localization support lies in a compact subset of the chart target.

   lemma localize_smooth (p : M) {ψ : M → ℝ} (hψ : ContMDiff planeModel 𝓘(ℝ) ∞ ψ)
       (hsupp : tsupport ψ ⊆ (chart p).source) {f : M → V}
       (hf : ContMDiff planeModel 𝓘(ℝ, V) ∞ f) : ContDiff ℝ ∞ (localize p ψ f) := by
   …

   Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize