FormStokes.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerStokes.coordinateBasis line 11
Source documentation
Ordered coordinate basis for dx_0 wedge ... wedge dx_n.
```
def coordinateBasis (n : ℕ) (i : Fin n) : Fin n → ℝ := Pi.single i 1
```

theorem OAI.MahlerStokes.integral_extDeriv_coordBall line 15

Source documentation

Ball Stokes for alternating differential forms. The boundary is written as explicit oriented hemisphere-coordinate integrals.

theorem integral_extDeriv_coordBall {n : ℕ} (R : ℝ)
    (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
    (hω : Differentiable ℝ ω)
    (hD : ∀ i : Fin (n+1), Continuous (fun x =>
      fderiv ℝ (fun z => ω z (i.removeNth (coordinateBasis (n+1)))) x (coordinateBasis (n+1) i))) :
    (∫ 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.coordinateBasis, OAI.MahlerStokes.coordBall, OAI.MahlerStokes.chord

theorem OAI.MahlerStokes.integral_extDeriv_coordAnnulus line 36

Source documentation

Punctured-ball Stokes for actual differential forms, with no regularity assumption in the interior of the removed inner ball.

theorem integral_extDeriv_coordAnnulus {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 coordAnnulus (n+1) a 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)))) -
      ∑ i : Fin (n+1), (-1 : ℝ)^i.val *
…

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