OAI/Analysis/Mahler/ExactSphereStokes.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.continuousOn_extDeriv_sphere line 13

   Source documentation

   C1 on an open sphere neighborhood supplies all continuity needed by the area integral. There is no regularity assumption inside the ball.

   lemma continuousOn_extDeriv_sphere {k q : ℕ}
       {eta : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) [⋀^Fin q]→L[ℝ] ℂ}
       {U : Set (ComplexEuclidean (k+1))} (hU : IsOpen U)
       (hSU : sphere 0 1 ⊆ U) (h : ContDiffOn ℝ 1 eta U) :
       ContinuousOn (extDeriv eta) (sphere 0 1) := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean

2. theorem OAI.Mahler.sphereFlux_extDeriv_eq_coordinateFlux line 24

   Source documentation

   Exact C1 transport to the coordinate sphere. This equality does not assert that the flux vanishes.

   theorem sphereFlux_extDeriv_eq_coordinateFlux {k : ℕ}
       (eta : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) [⋀^Fin (2*k)]→L[ℝ] ℂ)
       {U : Set (ComplexEuclidean (k+1))} (hU : IsOpen U)
       (hSU : sphere 0 1 ⊆ U) (h : ContDiffOn ℝ 1 eta U) :
       sphereFlux k (fun x => (extDeriv eta x).toAlternatingMap) =
         MahlerStokes.sphereFlux 1 (extDeriv (fluxPullback eta)) := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.sphereFlux, OAI.MahlerStokes.sphereFlux, OAI.Mahler.fluxPullback

3. theorem OAI.Mahler.sphereFlux_extDeriv_eq_zero_of_C2 line 42

   Source documentation

   The coordinate Stokes theorem for C2 forms.

   theorem sphereFlux_extDeriv_eq_zero_of_C2 {k : ℕ}
       (eta : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) [⋀^Fin (2*k)]→L[ℝ] ℂ)
       {U : Set (ComplexEuclidean (k+1))} (hU : IsOpen U)
       (hSU : sphere 0 1 ⊆ U) (h : ContDiffOn ℝ 2 eta U) :
       sphereFlux k (fun x => (extDeriv eta x).toAlternatingMap) = 0 := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.sphereFlux