OAI/Analysis/Mahler/WedgeOne.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.prependFinEquiv line 11
2. lemma OAI.Mahler.covectorVolume_cons_apply line 23
3. lemma OAI.Mahler.covectorVolume_prepend line 34
4. lemma OAI.Mahler.alternating_sum_eval line 45
5. theorem OAI.Mahler.wedge_one_eval line 56

   Source documentation

   One-form wedge evaluation in standard Fin order, with the unnormalized exterior-derivative signs.

   theorem wedge_one_eval (basis : Module.Basis J ℝ T) {n : ℕ}
       (a : T →ₗ[ℝ] ℂ) (B : T [⋀^Fin n]→ₗ[ℝ] ℂ) (v : Fin (n+1) → T) :
       (wedge (covectorVolume (fun _ : Fin 1 => a)) B).domDomCongr (prependFinEquiv n) v =
         ∑ i : Fin (n+1), (-1 : ℂ)^i.val * a (v i) * B (i.removeNth v) := by
   …

   Mentions: OAI.Mahler.wedge, OAI.Mahler.covectorVolume, OAI.Mahler.prependFinEquiv