OAI/Analysis/Mahler/PowerTransgression.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.wedge_triple_power_order line 12
2. def OAI.Mahler.powerTransgressionPrimitive line 38

   Source documentation

   The ordered primitive alpha wedge beta wedge (d alpha)^k.

   noncomputable def powerTransgressionPrimitive (basis : Module.Basis J ℝ E)
       (a b : E → E →L[ℝ] ℂ) (k : ℕ) (x : E) : E [⋀^Fin (2*(k+1))]→L[ℝ] ℂ :=
   …

3. def OAI.Mahler.primitiveFinEquiv line 44
4. lemma OAI.Mahler.powerTransgressionPrimitive_is_wedge line 51

   Source documentation

   The continuous primitive is the ordered shuffle product.

   lemma powerTransgressionPrimitive_is_wedge (basis : Module.Basis J ℝ E)
       (a b : E → E →L[ℝ] ℂ) (k : ℕ) (x : E) :
       (powerTransgressionPrimitive basis a b k x).toAlternatingMap =
         (wedge (oneForm a x).toAlternatingMap
           (wedge (oneForm b x).toAlternatingMap
             (wedgePower (extDeriv (oneForm a) x).toAlternatingMap k))).domDomCongr
           (primitiveFinEquiv k) := by
   …

   Mentions: OAI.Mahler.powerTransgressionPrimitive, OAI.Mahler.wedge, OAI.Mahler.oneForm, OAI.Mahler.wedgePower, OAI.Mahler.primitiveFinEquiv

5. theorem OAI.Mahler.extDeriv_powerTransgressionPrimitive line 70

   Source documentation

   Full ambient transgression identity in every degree. The hypotheses are actual differentiability and d squared alpha = 0, not a formal product law.

   theorem extDeriv_powerTransgressionPrimitive (basis : Module.Basis J ℝ E)
       {a b : E → E →L[ℝ] ℂ} {x : E} (k : ℕ)
       (ha : DifferentiableAt ℝ a x) (hb : DifferentiableAt ℝ b x)
       (hda : DifferentiableAt ℝ (extDeriv (oneForm a)) x)
       (hclosed : extDeriv (extDeriv (oneForm a)) x = 0) :
       (extDeriv (powerTransgressionPrimitive basis a b k) x).toAlternatingMap =
         (wedge (oneForm b x).toAlternatingMap
           (wedgePower (extDeriv (oneForm a) x).toAlternatingMap (k+1))).domDomCongr
           (boundaryFinEquiv (k+1)) -
         (wedge (oneForm a x).toAlternatingMap
           (wedge (extDeriv (oneForm b) x).toAlternatingMap
             (wedgePower (extDeriv (oneForm a) x).toAlternatingMap k))).domDomCongr
   …

   Mentions: OAI.Mahler.oneForm, OAI.Mahler.powerTransgressionPrimitive, OAI.Mahler.wedge, OAI.Mahler.wedgePower, OAI.Mahler.boundaryFinEquiv

6. lemma OAI.Mahler.contDiffAt_powerTransgressionPrimitive line 108