OAI/Analysis/Mahler/PuncturedBallStokes.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MahlerStokes.integral_extDeriv_punctured_ball line 12

   Source documentation

   Exact closed-ball puncture. The sign of the inner boundary is negative, while its displayed flux is outward from the inner ball itself.

   theorem integral_extDeriv_punctured_ball {n : ℕ} {a R : ℝ} (haR : a^2 ≤ R^2)
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hω : ∀ x ∈ closedShell (n+1) a R, DifferentiableAt ℝ ω x)
       (hD : ∀ i : Fin (n+1), ContinuousOn (fun x =>
         fderiv ℝ (fun z => ω z (i.removeNth (coordinateBasis (n+1)))) x (coordinateBasis (n+1) i))
         (closedShell (n+1) a R)) :
       (∫ x in coordBall (n+1) R \ coordClosedBall (n+1) a, extDeriv ω x (coordinateBasis (n+1))) =
         (∑ i : Fin (n+1), (-1 : ℝ)^i.val *
           ∫ y in coordBall n R,
             ω (i.insertNth (chord R y) y) (i.removeNth (coordinateBasis (n+1))) -
             ω (i.insertNth (-chord R y) y) (i.removeNth (coordinateBasis (n+1)))) -
         ∑ i : Fin (n+1), (-1 : ℝ)^i.val *
   …

   Mentions: OAI.MahlerStokes.closedShell, OAI.MahlerStokes.coordinateBasis, OAI.MahlerStokes.coordBall, OAI.MahlerStokes.coordClosedBall, OAI.MahlerStokes.chord

2. lemma OAI.MahlerStokes.radiusSq_nonneg line 33
3. lemma OAI.MahlerStokes.coordBall_zero line 36
4. lemma OAI.MahlerStokes.closedShell_zero line 41
5. theorem OAI.MahlerStokes.integral_extDeriv_ball_of_C1 line 46

   Source documentation

   Ball Stokes needs C1 regularity only near the closed ball, not globally.

   theorem integral_extDeriv_ball_of_C1 {n : ℕ} (R : ℝ)
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hω : ∀ x ∈ coordClosedBall (n+1) R, DifferentiableAt ℝ ω x)
       (hD : ∀ i : Fin (n+1), ContinuousOn (fun x =>
         fderiv ℝ (fun z => ω z (i.removeNth (coordinateBasis (n+1)))) x (coordinateBasis (n+1) i)) (coordClosedBall (n+1) R)) :
       (∫ x in coordBall (n+1) R, extDeriv ω x (coordinateBasis (n+1))) =
         ∑ i : Fin (n+1), (-1 : ℝ)^i.val *
           ∫ y in coordBall n R,
             ω (i.insertNth (chord R y) y) (i.removeNth (coordinateBasis (n+1))) -
             ω (i.insertNth (-chord R y) y) (i.removeNth (coordinateBasis (n+1))) := by
   …

   Mentions: OAI.MahlerStokes.coordClosedBall, OAI.MahlerStokes.coordinateBasis, OAI.MahlerStokes.coordBall, OAI.MahlerStokes.chord