SourceFluxCoordinates.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.powerFinEquiv_interleaved line 11
lemma OAI.Mahler.sourceBoundarySlots_eq_boundaryFinEquiv line 25
lemma OAI.Mahler.sourceTopSlots_eq_ambientFinEquiv line 34
theorem OAI.Mahler.sourceCoordinates_eq_fluxCoordinates line 41
Source documentation
Coordinate Stokes and cofactor sphere integration use the positive interleaved coordinate map, including the ambient degree cast.
```
theorem sourceCoordinates_eq_fluxCoordinates (k : ℕ) :
    sourceCoordinates k = fluxCoordinates k := by
…
```
Mentions: OAI.Mahler.sourceCoordinates, OAI.Mahler.fluxCoordinates

def OAI.Mahler.sourceFluxForm line 55

Source documentation

The bundled complex form, with its specified boundary slot order.

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