OAI/MathematicalPhysics/Elasticity/Extension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElasticityBoundary.hasFDerivAt_piecewise line 14
2. theorem OAI.ElasticityBoundary.smooth_piecewise_all_jets line 49

   Source documentation

   Matching all actual Fréchet jets gives smooth gluing across an arbitrary interface.

   theorem smooth_piecewise_all_jets (s : Set E) (f g : E → F)
       (hf : ContDiff ℝ (⊤ : ℕ∞) f) (hg : ContDiff ℝ (⊤ : ℕ∞) g)
       (hj : ∀ n : ℕ, ∀ x∈frontier s, iteratedFDeriv ℝ n f x=iteratedFDeriv ℝ n g x) :
       ContDiff ℝ (⊤ : ℕ∞) (s.piecewise f g) := by
   …

3. lemma OAI.ElasticityBoundary.compact_smooth_cutoff line 98
4. lemma OAI.ElasticityBoundary.contDiff_cutoff_mul line 116
5. theorem OAI.ElasticityBoundary.smooth_global_extension line 130

   Source documentation

   A genuine global smooth extension, equal on a neighborhood of the compact set.

   theorem smooth_global_extension {K U : Set E} (hK : IsCompact K) (hU : IsOpen U)
       (hKU : K⊆U) (f : E → ℝ) (hf : ContDiffOn ℝ (⊤ : ℕ∞) f U) :
       ∃ F : E → ℝ, ContDiff ℝ (⊤ : ℕ∞) F ∧ HasCompactSupport F ∧ F =ᶠ[𝓝ˢ K] f := by
   …

6. theorem OAI.ElasticityBoundary.admissible_global_extension line 140

   Source documentation

   Convex interpolation preserves both physical positivity inequalities.

   theorem admissible_global_extension {K U : Set E} (hK : IsCompact K) (hU : IsOpen U)
       (hKU : K⊆U) (lam mu : E → ℝ)
       (hl : ContDiffOn ℝ (⊤ : ℕ∞) lam U) (hm : ContDiffOn ℝ (⊤ : ℕ∞) mu U)
       (hp : ∀ x∈K, 0 < mu x ∧ 0<3*lam x+2*mu x) :
       ∃ L M : E → ℝ, ContDiff ℝ (⊤ : ℕ∞) L ∧ ContDiff ℝ (⊤ : ℕ∞) M ∧
         L =ᶠ[𝓝ˢ K] lam ∧ M =ᶠ[𝓝ˢ K] mu ∧
         (∀ x,0 < M x ∧ 0<3*L x+2*M x) ∧
         HasCompactSupport L ∧ HasCompactSupport (fun x => M x-1) := by
   …