ComplexSphereIntegral.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerStokes.degreeCastEuclidean line 11
Source documentation
The degree equality is explicit; this is transport along that equality, not an arbitrary permutation of the ordered real coordinates.
```
def degreeCastEuclidean {d e : ℕ} (h : d = e) :
    EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin e) := by
…
```
lemma OAI.MahlerStokes.degreeCastEuclidean_apply line 16
def OAI.MahlerStokes.complexSphereCoordinates line 24
Source documentation
Interleaved complex coordinates with the boundary/ambient degree cast shown in the type.
```
def complexSphereCoordinates (d k : ℕ) (h : d+1 = k*2) :
    EuclideanSpace ℝ (Fin (d+1)) ≃ₗᵢ[ℝ] EuclideanSpace ℂ (Fin k) :=
…
```
lemma OAI.MahlerStokes.complexSphereCoordinates_eq_complexCoordinates line 29
Source documentation
The interleaved real-to-complex coordinate map after the explicit Fin cast.
```
lemma complexSphereCoordinates_eq_complexCoordinates (d k : ℕ) (h : d+1 = k*2)
    (x : EuclideanSpace ℝ (Fin (d+1))) :
    complexSphereCoordinates d k h x =
      complexCoordinates k (fun i => x (Fin.cast h.symm i)) := by
…
```
Mentions: OAI.MahlerStokes.complexSphereCoordinates, OAI.MahlerStokes.complexCoordinates

theorem OAI.MahlerStokes.sphereFlux_eq_complexSphereIntegral line 42

Source documentation

Exact positive-radius hemisphere-to-complex-sphere integration equality. The right side uses the same volume.toSphere as Mahler.sphereArea; r^d is the tangential Jacobian in Mahler.radiusSphereArea.

theorem sphereFlux_eq_complexSphereIntegral {d k : ℕ} (h : d+1 = k*2)
    {r : ℝ} (hr : 0 < r)
    (ω : (Fin (d+1) → ℝ) → (Fin (d+1) → ℝ) [⋀^Fin d]→L[ℝ] ℝ)
    (hω : ContinuousOn ω {x | radiusSq x = r^2}) :
    sphereFlux r ω = r^d *
      ∫ z : sphere (0 : EuclideanSpace ℂ (Fin k)) 1,
        coordinateSphereDensity r ω
          (ofLp ((complexSphereCoordinates d k h).symm (z : EuclideanSpace ℂ (Fin k))))
        ∂(volume : Measure (EuclideanSpace ℂ (Fin k))).toSphere := by
…

Mentions: OAI.MahlerStokes.radiusSq, OAI.MahlerStokes.sphereFlux, OAI.MahlerStokes.coordinateSphereDensity, OAI.MahlerStokes.complexSphereCoordinates

theorem OAI.MahlerStokes.sphereFlux_eq_complexSphereIntegral_succ line 63

Source documentation

Boundary degree 2k+1 and ambient complex dimension k+1 in the sphere flux integral.

theorem sphereFlux_eq_complexSphereIntegral_succ (k : ℕ)
    {r : ℝ} (hr : 0 < r)
    (ω : (Fin ((2*k+1)+1) → ℝ) → (Fin ((2*k+1)+1) → ℝ) [⋀^Fin (2*k+1)]→L[ℝ] ℝ)
    (hω : ContinuousOn ω {x | radiusSq x = r^2}) :
    sphereFlux r ω = r^(2*k+1) *
      ∫ z : sphere (0 : EuclideanSpace ℂ (Fin (k+1))) 1,
        coordinateSphereDensity r ω
          (ofLp ((complexSphereCoordinates (2*k+1) (k+1) (by omega)).symm
            (z : EuclideanSpace ℂ (Fin (k+1)))))
        ∂(volume : Measure (EuclideanSpace ℂ (Fin (k+1)))).toSphere :=
…

Mentions: OAI.MahlerStokes.radiusSq, OAI.MahlerStokes.sphereFlux, OAI.MahlerStokes.coordinateSphereDensity, OAI.MahlerStokes.complexSphereCoordinates