SphereAreaTransport.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.sphereDilation line 11

Source documentation

Positive dilation sends the unit sphere to the radius-r sphere.

noncomputable def sphereDilation {n : ℕ} (r : ℝ) (hr : 0 < r) :
    sphere (0 : ComplexEuclidean n) 1 → sphere (0 : ComplexEuclidean n) r := fun z =>
…

Mentions: OAI.Mahler.ComplexEuclidean

lemma OAI.Mahler.continuous_sphereDilation line 17
lemma OAI.Mahler.positive_dilation_outward_normal line 24
theorem OAI.Mahler.positive_dilation_surface_determinant line 32
Source documentation
The derivative restricted to an oriented d-dimensional tangent frame has positive determinant r^d. This fixes both the surface Jacobian and its sign.
```
theorem positive_dilation_surface_determinant (d : ℕ) (r : ℝ) (hr : 0 < r) :
    Matrix.det (r • (1 : Matrix (Fin d) (Fin d) ℝ)) = r^d ∧ 0 < r^d := by
…
```
def OAI.Mahler.radiusSphereArea line 40
Source documentation
Euclidean sphere area at radius r, transported from the volume-induced unit sphere measure with its positive tangential Jacobian.
```
noncomputable def radiusSphereArea (n : ℕ) (r : ℝ) (hr : 0 < r) :
    Measure (sphere (0 : ComplexEuclidean n) r) :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean

theorem OAI.Mahler.integral_radiusSphereArea line 45

Source documentation

The surface measure change of variables for an actual Bochner integral.

theorem integral_radiusSphereArea {n : ℕ} (r : ℝ) (hr : 0 < r)
    (g : sphere (0 : ComplexEuclidean n) r → ℂ)
    (hg : AEStronglyMeasurable g ((sphereArea n).map (sphereDilation r hr))) :
    (∫ z, g z ∂radiusSphereArea n r hr) =
      (r^(2*n-1)) • ∫ z : sphere (0 : ComplexEuclidean n) 1,
        g (sphereDilation r hr z) ∂sphereArea n := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.sphereArea, OAI.Mahler.sphereDilation, OAI.Mahler.radiusSphereArea

theorem OAI.Mahler.smallSphereFlux_eq_radiusIntegral line 57

Source documentation

The parameterized flux is also an integral on the actual radius-r sphere, with its outward normal and Euclidean area measure.

theorem smallSphereFlux_eq_radiusIntegral {k : ℕ} (u : ComplexEuclidean (k+1) → ℂ)
    (r : ℝ) (hr : 0 < r)
    (hg : AEStronglyMeasurable
      (fun z : sphere (0 : ComplexEuclidean (k+1)) r =>
        sphereDensity k (r⁻¹ • (z : ComplexEuclidean (k+1))) (boundaryForm u k z))
      ((sphereArea (k+1)).map (sphereDilation r hr))) :
    smallSphereFlux k u r =
      ∫ z : sphere (0 : ComplexEuclidean (k+1)) r,
        sphereDensity k (r⁻¹ • (z : ComplexEuclidean (k+1))) (boundaryForm u k z)
          ∂radiusSphereArea (k+1) r hr := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.sphereDensity, OAI.Mahler.boundaryForm, OAI.Mahler.sphereArea, OAI.Mahler.sphereDilation, OAI.Mahler.smallSphereFlux, OAI.Mahler.radiusSphereArea