WedgeCalculus.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.wedge_summand_eval line 13

theorem OAI.Mahler.hasDerivAt_wedge_eval line 25

Source documentation

Differentiating the actual finite shuffle sum, at each vector tuple.

theorem hasDerivAt_wedge_eval {a : ℝ → T [⋀^ι]→ₗ[ℝ] ℂ}
    {b : ℝ → T [⋀^κ]→ₗ[ℝ] ℂ} {da : T [⋀^ι]→ₗ[ℝ] ℂ}
    {db : T [⋀^κ]→ₗ[ℝ] ℂ} {t : ℝ}
    (ha : ∀ v, HasDerivAt (fun s => a s v) (da v) t)
    (hb : ∀ v, HasDerivAt (fun s => b s v) (db v) t) (v : ι ⊕ κ → T) :
    HasDerivAt (fun s => wedge (a s) (b s) v)
      ((wedge da (b t) + wedge (a t) db) v) t := by
…

Mentions: OAI.Mahler.wedge

def OAI.Mahler.wedgePowerVariation line 49
Source documentation
The exact variation of an iterated shuffle power, without suppressing any terms by a formal commutativity or integration-by-parts assumption.
```
noncomputable def wedgePowerVariation (a da : T [⋀^Fin 2]→ₗ[ℝ] ℂ) :
    (k : ℕ) → T [⋀^WedgePowerSlots k]→ₗ[ℝ] ℂ
  | 0 => 0
  | k + 1 => wedge da (wedgePower a k) + wedge a (wedgePowerVariation a da k)
```
Mentions: OAI.Mahler.WedgePowerSlots, OAI.Mahler.wedge, OAI.Mahler.wedgePower
theorem OAI.Mahler.hasDerivAt_wedgePower_eval line 54