SphereFlux.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.sphereFrameSlots line 15
Source documentation
Reassociate the two leading real slots to preserve the interleaved order.
```
def sphereFrameSlots (k : ℕ) :
    Fin 1 ⊕ (Fin 1 ⊕ WedgePowerSlots k) ≃ WedgePowerSlots (k+1) where
…
```
Mentions: OAI.Mahler.WedgePowerSlots
def OAI.Mahler.sphereFluxFrame line 28
Source documentation
The positive frame is exactly x_1,y_1,...,x_n,y_n.
```
noncomputable def sphereFluxFrame (k : ℕ) :
    Fin 1 ⊕ (Fin 1 ⊕ WedgePowerSlots k) → ComplexEuclidean (k+1) :=
…
```
Mentions: OAI.Mahler.WedgePowerSlots, OAI.Mahler.ComplexEuclidean
lemma OAI.Mahler.sphereFluxFrame_positive line 32
def OAI.Mahler.sphereNormal line 38
Source documentation
The real metric dual of the outward unit normal, with complex-valued output.
```
noncomputable def sphereNormal {n : ℕ} (z : ComplexEuclidean n) :
    ComplexEuclidean n [⋀^Fin 1]→ₗ[ℝ] ℂ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean
def OAI.Mahler.sphereDensity line 44
Source documentation
Surface density of a top degree form: evaluate normal^flat wedge omega on the positively oriented Euclidean coordinate frame.
```
noncomputable def sphereDensity (k : ℕ) (z : ComplexEuclidean (k+1))
    (a : ComplexEuclidean (k+1) [⋀^Fin 1 ⊕ WedgePowerSlots k]→ₗ[ℝ] ℂ) : ℂ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.WedgePowerSlots
def OAI.Mahler.sphereJetDensity line 48
lemma OAI.Mahler.continuous_sphereJetDensity line 52
def OAI.Mahler.unitSphereFlux line 62
Source documentation
Actual complex Bochner integral against Euclidean unit-sphere area.
```
noncomputable def unitSphereFlux (k : ℕ) (u : ComplexEuclidean (k+1) → ℂ) : ℂ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean
def OAI.Mahler.smallSphereFlux line 68
Source documentation
Radius-r sphere flux in the positive radial parametrization. The surface Jacobian is r^(2k+1); the normal is z, directed out of the ball.
```
noncomputable def smallSphereFlux (k : ℕ) (u : ComplexEuclidean (k+1) → ℂ) (r : ℝ) : ℂ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean
lemma OAI.Mahler.boundaryForm_pullback_scale line 73

theorem OAI.Mahler.smallSphereFlux_eq_unit line 85

Source documentation

Pointwise pullback proves equality of the actual sphere integrals.

theorem smallSphereFlux_eq_unit {k : ℕ} {u : ComplexEuclidean (k+1) → ℂ} {r : ℝ}
    (hu : ∀ z : sphere (0 : ComplexEuclidean (k+1)) 1,
      ContDiffAt ℝ 2 u (r • (z : ComplexEuclidean (k+1)))) (c : ℂ) :
    smallSphereFlux k u r = unitSphereFlux k (fun y => u (r • y) - c) := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.smallSphereFlux, OAI.Mahler.unitSphereFlux