OAI/Analysis/Mahler/RegularStokesAssembly.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MahlerStokes.exists_regular_sublevel_localization line 13

   Source documentation

   Compact regular-sublevel hypotheses yield boundary patches, cutoffs and volume localization with the interior term eliminated. This does not identify the terms as boundary flux.

   theorem exists_regular_sublevel_localization {n : ℕ} {U : Set (Fin (n+1) → ℝ)}
       {g : (Fin (n+1) → ℝ) → ℝ} {R : ℝ}
       (hU : IsOpen U) (hg : ContDiffOn ℝ 2 g U)
       (hc : IsCompact (closure (regularSublevel U g R)))
       (hcl : closure (regularSublevel U g R) ⊆ U)
       (hreg : ∀ x ∈ U, g x = R → fderiv ℝ g x ≠ 0)
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hω : ContDiffOn ℝ 1 ω U) :
       ∃ (a : RegularBoundaryAtlas (n+1) U g (frontier (regularSublevel U g R)))
         (W : Set (Fin (n+1) → ℝ))
         (ρ : SmoothPartitionOfUnity (Option a.Index) 𝓘(ℝ, Fin (n+1) → ℝ)
           (Fin (n+1) → ℝ) (closure W)),
   …

   Mentions: OAI.MahlerStokes.regularSublevel, OAI.MahlerStokes.RegularBoundaryAtlas