OAI/Analysis/Mahler/ClosedBoundaryStokes.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MahlerStokes.contDiffAt_extDeriv line 11

   Source documentation

   C2 regularity of a form gives C1 regularity of its actual exterior derivative.

   theorem contDiffAt_extDeriv {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
       {n : ℕ} {ω : E → E [⋀^Fin n]→L[ℝ] ℝ} {x : E}
       (hω : ContDiffAt ℝ 2 ω x) : ContDiffAt ℝ 1 (extDeriv ω) x := by
   …

2. theorem OAI.MahlerStokes.exists_closed_set_form_extension line 19

   Source documentation

   Smooth separation extends a C2 form near a closed subset of its open regularity domain, with exact equality on a neighborhood of that subset.

   theorem exists_closed_set_form_extension {d n : ℕ} {U K : Set (Fin d → ℝ)}
       (hU : IsOpen U) (hK : IsClosed K) (hKU : K ⊆ U)
       (ω : (Fin d → ℝ) → (Fin d → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hω : ContDiffOn ℝ 2 ω U) :
       ∃ η : (Fin d → ℝ) → (Fin d → ℝ) [⋀^Fin n]→L[ℝ] ℝ,
         ContDiff ℝ 2 η ∧ (∀ x ∈ K, η =ᶠ[𝓝 x] ω) := by
   …

3. theorem OAI.MahlerStokes.sphereFlux_extDeriv_eq_zero line 47

   Source documentation

   An exact form integrates to zero over the closed sphere. Its primitive need only be C2 on an open neighborhood of the sphere, not inside the ball.

   theorem sphereFlux_extDeriv_eq_zero {n : ℕ} {U : Set (Fin (n+1+1) → ℝ)}
       (r : ℝ) (hU : IsOpen U)
       (hSU : {x | radiusSq x = r^2} ⊆ U)
       (ω : (Fin (n+1+1) → ℝ) → (Fin (n+1+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hω : ContDiffOn ℝ 2 ω U) : sphereFlux r (extDeriv ω) = 0 := by
   …

   Mentions: OAI.MahlerStokes.radiusSq, OAI.MahlerStokes.sphereFlux