OAI/Analysis/Mahler/PunctureCutoff.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MahlerStokes.continuousOn_extDeriv_coefficient line 11
2. theorem OAI.MahlerStokes.integrableOn_extDeriv_compact_closure line 21
3. theorem OAI.MahlerStokes.exists_puncture_regularization line 30

   Source documentation

   An actual smooth cutoff removes the singularity at zero and is exactly one on a neighborhood of every point outside the chosen open ball.

   theorem exists_puncture_regularization {d n : ℕ} {U : Set (Fin d → ℝ)}
       (hU : IsOpen U) {r : ℝ} (hr : 0 < r)
       (ω : (Fin d → ℝ) → (Fin d → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hω : ContDiffOn ℝ 1 ω (U \ {0})) :
       ∃ η : (Fin d → ℝ) → (Fin d → ℝ) [⋀^Fin n]→L[ℝ] ℝ,
         ContDiffOn ℝ 1 η U ∧
         (∀ x ∉ coordBall d r, η =ᶠ[𝓝 x] ω) := by
   …

   Mentions: OAI.MahlerStokes.coordBall

4. def OAI.MahlerStokes.sphereFlux line 65

   Source documentation

   The sphere integral uses the outward orientation from the ball.

   def sphereFlux {n : ℕ} (r : ℝ)
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ) : ℝ :=
   …

5. theorem OAI.MahlerStokes.sphereFlux_congr line 71
6. theorem OAI.MahlerStokes.integral_closedBall_eq_ball line 84
7. theorem OAI.MahlerStokes.integral_extDeriv_ball_local line 94
8. theorem OAI.MahlerStokes.chartBoundaryFlux_congr line 106