OAI/Analysis/Mahler/PrimitiveRegularity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.basisVolumeContinuous line 16

   Source documentation

   Continuous form for a fixed basis covector determinant.

   def basisVolumeContinuous (b : Module.Basis J ℝ E) (q : ι → J) :
       E [⋀^ι]→L[ℝ] ℂ :=
   …

2. lemma OAI.Mahler.basisVolumeContinuous_eq line 23
3. def OAI.Mahler.bundleFiniteForm line 31

   Source documentation

   Bundle an actual finite-dimensional form using its exact normalized basis expansion. Forgetting continuity returns the original form.

   def bundleFiniteForm (b : Module.Basis J ℝ E) (a : E [⋀^ι]→ₗ[ℝ] ℂ) :
       E [⋀^ι]→L[ℝ] ℂ :=
   …

4. lemma OAI.Mahler.bundleFiniteForm_eq line 35
5. lemma OAI.Mahler.contDiffAt_bundleFiniteForm line 48
6. lemma OAI.Mahler.contDiffAt_wedge_eval line 57
7. lemma OAI.Mahler.contDiffAt_wedgePower_eval line 73