OAI/Analysis/Mahler/RegularSublevel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MahlerStokes.regularSublevel line 12
2. lemma OAI.MahlerStokes.isOpen_regularSublevel line 15
3. theorem OAI.MahlerStokes.level_mem_closure_sublevel line 21

   Source documentation

   Regularity forces a point on the level to be approached from below: otherwise it would be a local minimum with zero derivative.

   theorem level_mem_closure_sublevel {d : ℕ} {U : Set (Fin d → ℝ)}
       {g : (Fin d → ℝ) → ℝ} {R : ℝ} {x : Fin d → ℝ}
       (hU : IsOpen U) (hx : x ∈ U) (heq : g x = R) (hreg : fderiv ℝ g x ≠ 0) :
       x ∈ closure (regularSublevel U g R) := by
   …

   Mentions: OAI.MahlerStokes.regularSublevel

4. theorem OAI.MahlerStokes.frontier_regularSublevel line 35

   Source documentation

   The boundary of the actual relatively defined sublevel is exactly the regular level, provided its closure stays inside U.

   theorem frontier_regularSublevel {d : ℕ} {U : Set (Fin d → ℝ)}
       {g : (Fin d → ℝ) → ℝ} {R : ℝ} (hU : IsOpen U) (hg : ContinuousOn g U)
       (hcl : closure (regularSublevel U g R) ⊆ U)
       (hreg : ∀ x ∈ U, g x = R → fderiv ℝ g x ≠ 0) :
       frontier (regularSublevel U g R) = U ∩ {x | g x = R} := by
   …

   Mentions: OAI.MahlerStokes.regularSublevel

5. theorem OAI.MahlerStokes.isCompact_regularLevel line 57