OAI/Analysis/Mahler/UnitaryReference.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.normEnergy_twoForm_inner line 10
2. lemma OAI.Mahler.unitary_real_inner line 23
3. lemma OAI.Mahler.normEnergy_oneForm_unitary line 30
4. lemma OAI.Mahler.normEnergy_twoForm_unitary line 40
5. theorem OAI.Mahler.interleavedVolume_unitary line 58

   Source documentation

   Unitary maps preserve the actual positive coordinate volume. The proof uses the normalized symplectic top power, so no determinant sign is assumed.

   theorem interleavedVolume_unitary {n : ℕ}
       (L : ComplexEuclidean n ≃ₗᵢ[ℂ] ComplexEuclidean n) :
       (interleavedVolume n).compLinearMap (L.toLinearEquiv.toLinearMap.restrictScalars ℝ) =
         interleavedVolume n := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.interleavedVolume

6. lemma OAI.Mahler.normEnergy_boundary_unitary line 70