ExteriorPower.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.pairSlotEquiv line 13
Source documentation
The recursive wedge slots list each coordinate's real slot before its imaginary slot. This equivalence records that interleaved order.
```
def pairSlotEquiv : (k : ℕ) → WedgePowerSlots k ≃ Fin k × Fin 2
  | 0 => by
    change Fin 0 ≃ Fin 0 × Fin 2
    exact Equiv.equivOfIsEmpty _ _
  | k+1 =>
    { toFun := Sum.elim (fun j => (0,j))
…
```
Mentions: OAI.Mahler.WedgePowerSlots
def OAI.Mahler.pairedCovectors line 39
lemma OAI.Mahler.pairedCovectors_succ line 43
theorem OAI.Mahler.wedgePower_sum_pairs line 50
Source documentation
Expand the actual shuffle power as a sum of determinants of selected covector pairs. This identity includes every term, also repeated selections.
```
theorem wedgePower_sum_pairs {J : Type*} [Fintype J]
    (p : J → Fin 2 → T →ₗ[ℝ] ℂ) (k : ℕ) :
    wedgePower (∑ j, covectorVolume (p j)) k =
      ∑ q : Fin k → J, covectorVolume (pairedCovectors (fun i => p (q i))) := by
…
```
Mentions: OAI.Mahler.wedgePower, OAI.Mahler.covectorVolume, OAI.Mahler.pairedCovectors
def OAI.Mahler.pairPermutation line 78
lemma OAI.Mahler.pairPermutation_sign line 82
lemma OAI.Mahler.pairedCovectors_perm line 86
lemma OAI.Mahler.covectorVolume_pairs_perm line 92
lemma OAI.Mahler.covectorVolume_pairs_noninjective line 102
theorem OAI.Mahler.wedgePower_sum_pairs_top line 121
Source documentation
The n-fold shuffle power of n simple two-forms is n! times their interleaved covector volume. Repeated choices vanish; pair permutations have positive sign. This yields the factorial in the normalization.
```
theorem wedgePower_sum_pairs_top (k : ℕ) (p : Fin k → Fin 2 → T →ₗ[ℝ] ℂ) :
    wedgePower (∑ j, covectorVolume (p j)) k =
      (k.factorial : ℂ) • covectorVolume (pairedCovectors p) := by
…
```
Mentions: OAI.Mahler.wedgePower, OAI.Mahler.covectorVolume, OAI.Mahler.pairedCovectors