OAI/Analysis/Mahler/ContinuousWedge.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.continuousWedge line 20

   Source documentation

   The shuffle product bundled with its actual joint-vector continuity.

   def continuousWedge (a : E [⋀^ι]→L[ℝ] ℂ) (b : E [⋀^κ]→L[ℝ] ℂ) :
       E [⋀^ι ⊕ κ]→L[ℝ] ℂ :=
   …

2. lemma OAI.Mahler.continuousWedge_apply line 38
3. instance OAI.Mahler.finiteDimensional_continuousAlternatingMap line 42
4. lemma OAI.Mahler.continuousWedge_add_left line 52
5. lemma OAI.Mahler.continuousWedge_add_right line 61
6. lemma OAI.Mahler.continuousWedge_smul_left line 70
7. lemma OAI.Mahler.continuousWedge_smul_right line 78
8. def OAI.Mahler.continuousWedgeCLM line 87

   Source documentation

   Exterior multiplication is an actual continuous bilinear map.

   def continuousWedgeCLM [FiniteDimensional ℝ E] :
       (E [⋀^ι]→L[ℝ] ℂ) →L[ℝ] (E [⋀^κ]→L[ℝ] ℂ) →L[ℝ] E [⋀^ι ⊕ κ]→L[ℝ] ℂ :=
   …

9. lemma OAI.Mahler.contDiffAt_continuousWedge line 97