SphereCoordinateIntegral.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerStokes.coordinateSphereDensity line 12
Source documentation
Outward cofactor density in the fixed ordered coordinate basis. The argument x is the unit normal; r*x is the evaluation point of the form.
```
def coordinateSphereDensity {n : ℕ} (r : ℝ)
    (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
    (x : Fin (n+1) → ℝ) : ℝ :=
…
```
lemma OAI.MahlerStokes.continuousOn_sphere_coefficient line 18

theorem OAI.MahlerStokes.sphereFlux_unit_eq_areaIntegral line 34

Source documentation

Exact equality of the hemisphere-coordinate Stokes integral and the outward cofactor density integrated against volume.toSphere.

theorem sphereFlux_unit_eq_areaIntegral {n : ℕ}
    (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
    (hω : ContinuousOn ω {x | radiusSq x = 1}) :
    sphereFlux 1 ω =
      ∫ z : sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1,
        coordinateSphereDensity 1 ω (ofLp (z : EuclideanSpace ℝ (Fin (n+1))))
        ∂(volume : Measure (EuclideanSpace ℝ (Fin (n+1)))).toSphere := by
…

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

theorem OAI.MahlerStokes.sphereFlux_pos_eq_areaIntegral line 60

Source documentation

Positive-radius coordinate Stokes flux equals the actual unit-sphere area integral with the positive tangential dilation Jacobian r^n. Regularity is required only on the radius-r sphere.

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

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