ExactSphereFluxBridge.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Mahler.coordinateSphereDensity_fluxPullback line 13
Source documentation
The real coordinate cofactor sum is the actual complex sphereFlux density. The volume of the chosen frame is +1, so no orientation or normalization factor remains.
```
theorem coordinateSphereDensity_fluxPullback {k : ℕ}
    (B : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) [⋀^Fin (2*k+1)]→L[ℝ] ℂ)
    (x : Fin ((2*k+1)+1) → ℝ) :
    MahlerStokes.coordinateSphereDensity 1 (fluxPullback B) x =
      (orientedDensity (sphereFrame k) (sphereVolume k)
        (B (fluxCoordinates k x)).toAlternatingMap (fluxCoordinates k x)).re := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.MahlerStokes.coordinateSphereDensity, OAI.Mahler.fluxPullback, OAI.Mahler.orientedDensity, OAI.Mahler.sphereFrame, OAI.Mahler.sphereVolume, OAI.Mahler.fluxCoordinates
lemma OAI.Mahler.continuousOn_fluxPullback_sphere line 36
theorem OAI.Mahler.sphereFlux_eq_coordinateFlux line 52
Source documentation
The hemisphere-coordinate Stokes flux is exactly Mahler's real flux of a complex form. Only continuity on the sphere is required.
```
theorem sphereFlux_eq_coordinateFlux {k : ℕ}
    (B : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) [⋀^Fin (2*k+1)]→L[ℝ] ℂ)
    (hB : ContinuousOn B (sphere 0 1)) :
    sphereFlux k (fun x => (B x).toAlternatingMap) =
      MahlerStokes.sphereFlux 1 (fluxPullback B) := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.sphereFlux, OAI.MahlerStokes.sphereFlux, OAI.Mahler.fluxPullback