OAI/Analysis/BernoulliCone/SmoothLocalizedExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.LocalExtension.exists_cutoff line 14
2. lemma OAI.Bernoulli.LocalExtension.exists_contDiff_extension line 34

   Source documentation

   A compact part of a genuinely smooth open domain admits a global smooth representative. This permits use of global calculus only after verifying the actual local hypotheses.

   lemma exists_contDiff_extension {n:ℕ∞} {F:E→G} {K D:Set E}
       (hK:IsCompact K) (hD:IsOpen D) (hKD:K⊆D) (hF:ContDiffOn ℝ n F D) :
       ∃B:E→G,ContDiff ℝ n B ∧ B =ᶠ[𝓝ˢ K] F := by
   …