OAI/Analysis/AffineBernstein/CapPerturbation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.isOpen_graphSublevel line 14
2. lemma OAI.AffineBernstein.isCompact_lower_graphSublevel line 22
3. theorem OAI.AffineBernstein.exists_cap_perturbation line 35

   Source documentation

   A genuine compact smooth convex-cap replacement, with no stationarity or area conclusion assumed.

   theorem exists_cap_perturbation {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
       {u q : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω) (hq : ContDiffOn ℝ ∞ q Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef) {b ε : ℝ} (hε : 0 < ε)
       (hK : IsCompact {x | x ∈ Ω ∧ u x ≤ b})
       (hqtop : ∀ x, x ∈ Ω → u x < b → q x ≤ b-2*ε)
       (hqp : ∀ x, x ∈ Ω → u x < b → (hessian q x).PosDef) :
       ∃ η : Space n → ℝ, ContDiff ℝ ∞ η ∧ HasCompactSupport η ∧
         tsupport η ⊆ {x | x ∈ Ω ∧ u x < b} ∧
         (∀ x ∈ Ω, (hessian (fun y => u y+η y) x).PosDef) ∧
         ∀ x, x ∈ Ω → u x < b → ε ≤ q x-u x → u x+η x = q x := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian