SphereFluxIntegral.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.powerFinEquiv line 12

Source documentation

The order is recursive and interleaved, not an arbitrary finite equivalence.

def powerFinEquiv : (k : ℕ) → WedgePowerSlots k ≃ Fin (2*k)
  | 0 => Equiv.refl _
  | k+1 => (Equiv.sumCongr (Equiv.refl (Fin 2)) (powerFinEquiv k)).trans
      (finSumFinEquiv.trans (finCongr (by omega)))

Mentions: OAI.Mahler.WedgePowerSlots

def OAI.Mahler.boundaryFinEquiv line 17
def OAI.Mahler.ambientFinEquiv line 21
def OAI.Mahler.sphereVolume line 24
def OAI.Mahler.sphereFrame line 28
lemma OAI.Mahler.topForm_basis_ne_zero line 34
lemma OAI.Mahler.sphereVolume_frame_ne_zero line 46

def OAI.Mahler.boundaryFormFin line 58

Source documentation

Actual boundary form, in its standard ordered slots.

noncomputable def boundaryFormFin {k : ℕ}
    (a : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) →L[ℝ] ℂ)
    (x : ComplexEuclidean (k+1)) :
    ComplexEuclidean (k+1) [⋀^Fin (2*k+1)]→ₗ[ℝ] ℂ :=
…

Mentions: OAI.Mahler.ComplexEuclidean

def OAI.Mahler.sphereFlux line 67
Source documentation
The integral uses Euclidean area and the cofactor surface density with outward normal x on the unit sphere.
```
noncomputable def sphereFlux (k : ℕ)
    (B : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) [⋀^Fin (2*k+1)]→ₗ[ℝ] ℂ) : ℝ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean
theorem OAI.Mahler.sphereFlux_normalized_contraction line 75
Source documentation
The coefficient for contraction of the normalized top volume. Equality with the Liouville boundary form is not assumed.
```
theorem sphereFlux_normalized_contraction (k : ℕ) :
    sphereFlux k (fun x => ((k.factorial : ℂ) / 2) • (sphereVolume k).curryLeft x) =
      Real.pi^(k+1) := by
…
```
Mentions: OAI.Mahler.sphereFlux, OAI.Mahler.sphereVolume