OAI/Analysis/Mahler/WedgeDecomposition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.complexCoord line 11
2. lemma OAI.Mahler.complexCoord_apply line 15
3. lemma OAI.Mahler.multilinear_basis_expansion line 18
4. theorem OAI.Mahler.alternating_basis_expansion line 41

   Source documentation

   Every finite-dimensional form is an explicit finite sum of simple forms. The factorial is retained, matching the unnormalized alternatization.

   theorem alternating_basis_expansion (b : Module.Basis J ℝ T)
       (a : T [⋀^ι]→ₗ[ℝ] ℂ) :
       (Fintype.card ι).factorial • a =
         ∑ q : ι → J, a (b ∘ q) • covectorVolume (complexCoord b ∘ q) := by
   …

   Mentions: OAI.Mahler.covectorVolume, OAI.Mahler.complexCoord

5. theorem OAI.Mahler.alternating_basis_expansion_normalized line 58
6. theorem OAI.Mahler.alternating_induction line 70

   Source documentation

   Induction on simple forms, justified by a finite basis expansion.

   theorem alternating_induction (b : Module.Basis J ℝ T)
       (P : (T [⋀^ι]→ₗ[ℝ] ℂ) → Prop)
       (hz : P 0) (ha : ∀ A B, P A → P B → P (A+B))
       (hs : ∀ (c : ℂ) A, P A → P (c • A))
       (hv : ∀ l : ι → T →ₗ[ℝ] ℂ, P (covectorVolume l))
       (a : T [⋀^ι]→ₗ[ℝ] ℂ) : P a := by
   …

   Mentions: OAI.Mahler.covectorVolume