OAI/Analysis/Mahler/MatrixExteriorPower.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.pairSplitEquiv line 11
2. def OAI.Mahler.hessianCovectorMatrix line 19

   Source documentation

   The complex-coordinate coefficient matrix, in split real/imaginary order.

   noncomputable def hessianCovectorMatrix {n : ℕ} (H : Matrix (Fin n) (Fin n) ℂ) :
       Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℂ :=
   …

3. lemma OAI.Mahler.hessianCovectorMatrix_det line 23
4. def OAI.Mahler.splitCoordinates line 33
5. lemma OAI.Mahler.pairedCoordinates_split line 36
6. def OAI.Mahler.hessianPair line 44

   Source documentation

   Coordinate two-form associated with a complex Hessian. This is the standard (i/2) sum H_ij dz_i wedge dbar(z_j), represented by covectors.

   noncomputable def hessianPair {n : ℕ} (H : Matrix (Fin n) (Fin n) ℂ) (i : Fin n) :
       Fin 2 → ComplexEuclidean n →ₗ[ℝ] ℂ :=
   …

   Mentions: OAI.Mahler.ComplexEuclidean

7. def OAI.Mahler.matrixTwoForm line 49
8. lemma OAI.Mahler.hessianPair_split line 53
9. lemma OAI.Mahler.hessianPair_volume line 63
10. theorem OAI.Mahler.matrixTwoForm_top line 75

    Source documentation

    The full n! det(H) normalization, with the i/2 convention and the positively oriented interleaved real volume form.

    theorem matrixTwoForm_top {n : ℕ} (H : Matrix (Fin n) (Fin n) ℂ) :
        wedgePower (matrixTwoForm H) n =
          ((n.factorial : ℂ) * H.det) • interleavedVolume n := by
    …

    Mentions: OAI.Mahler.wedgePower, OAI.Mahler.matrixTwoForm, OAI.Mahler.interleavedVolume

11. def OAI.Mahler.matrixPairing line 87
12. lemma OAI.Mahler.hessianPair_zero line 90
13. lemma OAI.Mahler.hessianPair_one line 95
14. lemma OAI.Mahler.matrixTwoForm_apply line 105