SourceTopCoordinates.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Mahler.sourceTopSlots_interleaved line 11
Source documentation
The calculated top-slot order is the positive interleaved real/imaginary order.
```
theorem sourceTopSlots_interleaved (k : ℕ) (s : WedgePowerSlots (k+1)) :
    (sourceTopSlots k s).val = (finProdFinEquiv (pairSlotEquiv (k+1) s)).val := by
…
```
Mentions: OAI.Mahler.WedgePowerSlots, OAI.Mahler.sourceTopSlots, OAI.Mahler.pairSlotEquiv
def OAI.Mahler.coordinateCast line 20
lemma OAI.Mahler.coordinateCast_basis line 24
def OAI.Mahler.sourceCoordinates line 30
theorem OAI.Mahler.sourceCoordinates_top_basis line 35
Source documentation
No unproved orientation factor remains in the coordinate frame.
```
theorem sourceCoordinates_top_basis (k : ℕ) (s : WedgePowerSlots (k+1)) :
    sourceCoordinates k (MahlerStokes.coordinateBasis ((2*k+1)+1) (sourceTopSlots k s)) =
      interleavedBasis s := by
…
```
Mentions: OAI.Mahler.WedgePowerSlots, OAI.Mahler.sourceCoordinates, OAI.MahlerStokes.coordinateBasis, OAI.Mahler.sourceTopSlots, OAI.Mahler.interleavedBasis