OAI/Analysis/Mahler/ReferencePole.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.referencePole line 10
2. lemma OAI.Mahler.referencePole_norm line 13
3. lemma OAI.Mahler.referencePole_inner line 16
4. lemma OAI.Mahler.referencePole_tangent_iff line 24
5. lemma OAI.Mahler.covectorVolume_compLinearMap line 28
6. lemma OAI.Mahler.referencePole_pair_zero line 35
7. lemma OAI.Mahler.referencePole_twoForm line 46
8. lemma OAI.Mahler.oneForm_covectorVolume line 64
9. lemma OAI.Mahler.referencePole_oneForm line 71
10. theorem OAI.Mahler.referencePole_boundary line 83

    Source documentation

    At the standard pole, the reference boundary form is the determinant of the positively ordered tangent covectors, with the exact k!/2 coefficient.

    theorem referencePole_boundary (k : ℕ) :
        wedge (tangentForm (referencePole k)
          (oneForm (dcLinear (normEnergy (k+1))) (referencePole k)).toAlternatingMap)
          (wedgePower (tangentForm (referencePole k)
            (extDeriv (oneForm (dcLinear (normEnergy (k+1)))) (referencePole k)).toAlternatingMap) k) =
        ((k.factorial : ℂ)/2) • covectorVolume
          (Sum.elim
            (fun _ : Fin 1 => (imagCoordinate (0 : Fin (k+1))).comp (sphereTangent (referencePole k)).subtype)
            (pairedCovectors (fun j : Fin k => fun i =>
              (coordinatePair j.succ i).comp (sphereTangent (referencePole k)).subtype))) := by
    …

    Mentions: OAI.Mahler.wedge, OAI.Mahler.tangentForm, OAI.Mahler.referencePole, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.normEnergy, OAI.Mahler.wedgePower, OAI.Mahler.covectorVolume, OAI.Mahler.imagCoordinate, OAI.Mahler.sphereTangent, OAI.Mahler.pairedCovectors, OAI.Mahler.coordinatePair