NormExteriorPower.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.alternatingMap_sum_apply line 11
def OAI.Mahler.realCoordinate line 22
def OAI.Mahler.imagCoordinate line 24
lemma OAI.Mahler.realCoordinate_apply line 27
lemma OAI.Mahler.imagCoordinate_apply line 29
def OAI.Mahler.coordinatePair line 32
def OAI.Mahler.interleavedVolume line 36
Source documentation
The actual positive coordinate volume form, ordered dx_1,dy_1,... .
```
noncomputable def interleavedVolume (n : ℕ) :
    ComplexEuclidean n [⋀^WedgePowerSlots n]→ₗ[ℝ] ℂ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.WedgePowerSlots
lemma OAI.Mahler.extDeriv_normEnergy_covectors line 40
theorem OAI.Mahler.extDeriv_normEnergy_top line 57
Source documentation
Full squared-norm exterior normalization, in arbitrary dimension, for the actual exterior derivative and standard shuffle powers.
```
theorem extDeriv_normEnergy_top (n : ℕ) (x : ComplexEuclidean n) :
    wedgePower (extDeriv (oneForm (dcLinear (normEnergy n))) x).toAlternatingMap n =
      (n.factorial : ℂ) • interleavedVolume n := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.wedgePower, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.normEnergy, OAI.Mahler.interleavedVolume
def OAI.Mahler.interleavedBasis line 65
Source documentation
The positively ordered real coordinate basis, using the same recursive slots as the exterior power.
```
noncomputable def interleavedBasis {n : ℕ} (s : WedgePowerSlots n) : ComplexEuclidean n :=
…
```
Mentions: OAI.Mahler.WedgePowerSlots, OAI.Mahler.ComplexEuclidean
theorem OAI.Mahler.interleavedVolume_basis line 70
Source documentation
The normalization is positive on dx_1,dy_1,..., not just determined up to an unspecified orientation sign.
```
theorem interleavedVolume_basis (n : ℕ) : interleavedVolume n interleavedBasis = 1 := by
…
```
Mentions: OAI.Mahler.interleavedVolume, OAI.Mahler.interleavedBasis