OAI/Analysis/Mahler/PuncturedSublevelStokes.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MahlerStokes.punctured_sublevel_stokes_of_partition line 12

   Source documentation

   Punctured Stokes for a fixed atlas and partition, allowing comparison with another form on the very same oriented boundary representation.

   theorem punctured_sublevel_stokes_of_partition {n : ℕ} {U : Set (Fin (n+1) → ℝ)}
       {g : (Fin (n+1) → ℝ) → ℝ} {R r : ℝ}
       (hU : IsOpen U) (hg : ContinuousOn g U)
       (hc : IsCompact (closure (regularSublevel U g R)))
       (hcl : closure (regularSublevel U g R) ⊆ U)
       (hr : 0 < r) (hB : coordClosedBall (n+1) r ⊆ regularSublevel U g R)
       (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))
       (hWo : IsOpen W) (hCW : closure (regularSublevel U g R) ⊆ W)
       (hρc : ∀ i, HasCompactSupport (ρ i)) (hρsub : ρ.IsSubordinate (sublevelPatchDomain a))
   …

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

2. theorem OAI.MahlerStokes.exists_punctured_sublevel_stokes line 81

   Source documentation

   General punctured regular-sublevel Stokes. The original form is C1 only away from zero. The inner sphere is oriented outward from the ball and is subtracted exactly once. All terms are actual Lebesgue chart integrals.

   theorem exists_punctured_sublevel_stokes {n : ℕ} {U : Set (Fin (n+1) → ℝ)}
       {g : (Fin (n+1) → ℝ) → ℝ} {R 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)
       (hr : 0 < r) (hB : coordClosedBall (n+1) r ⊆ regularSublevel U g R)
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hω : ContDiffOn ℝ 1 ω (U \ {0})) :
       ∃ (a : RegularBoundaryAtlas (n+1) U g (frontier (regularSublevel U g R)))
         (W : Set (Fin (n+1) → ℝ))
         (ρ : SmoothPartitionOfUnity (Option a.Index) 𝓘(ℝ, Fin (n+1) → ℝ)
   …

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