RawClosedProduct.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.raw_wedge_zero_left line 10
lemma OAI.Mahler.raw_wedge_zero_right line 14

def OAI.Mahler.rawPrefix line 19

Source documentation

Adjoin the actual directional derivative as the first raw slot.

def rawPrefix (D : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : ι => E) ℂ) :
    MultilinearMap ℝ (fun _ : Fin 1 ⊕ ι => E) ℂ :=
…

lemma OAI.Mahler.rawPrefix_apply line 24
def OAI.Mahler.rawProductVariation line 28
def OAI.Mahler.rawMoveDerivative line 39
Source documentation
Move a distinguished derivative slot past the left factor without changing the order within either factor.
```
def rawMoveDerivative (ι κ : Type*) : ι ⊕ (Fin 1 ⊕ κ) ≃ Fin 1 ⊕ (ι ⊕ κ) :=
…
```

theorem OAI.Mahler.rawPrefix_productVariation line 46

Source documentation

Every product-rule term, with its explicit slot placement.

theorem rawPrefix_productVariation [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (a : MultilinearMap ℝ (fun _ : ι => E) ℂ)
    (Da : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : ι => E) ℂ)
    (b : MultilinearMap ℝ (fun _ : κ => E) ℂ)
    (Db : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : κ => E) ℂ) :
    rawPrefix (rawProductVariation a Da b Db) =
      (rawProduct (rawPrefix Da) b).domDomCongr (Equiv.sumAssoc (Fin 1) ι κ) +
      (rawProduct a (rawPrefix Db)).domDomCongr (rawMoveDerivative ι κ) := by
…

Mentions: OAI.Mahler.rawPrefix, OAI.Mahler.rawProductVariation, OAI.Mahler.rawProduct, OAI.Mahler.rawMoveDerivative

theorem OAI.Mahler.rawPrefix_productVariation_closed line 58

Source documentation

If both factors are closed after alternation, their full product-rule variation is closed. This retains both placement terms before cancelling.

theorem rawPrefix_productVariation_closed
    (a : MultilinearMap ℝ (fun _ : ι => E) ℂ)
    (Da : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : ι => E) ℂ)
    (b : MultilinearMap ℝ (fun _ : κ => E) ℂ)
    (Db : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : κ => E) ℂ)
    (ha : (rawPrefix Da).alternatization = 0)
    (hb : (rawPrefix Db).alternatization = 0) :
    (rawPrefix (rawProductVariation a Da b Db)).alternatization = 0 := by
…

Mentions: OAI.Mahler.rawPrefix, OAI.Mahler.rawProductVariation

theorem OAI.Mahler.rawPrefix_productVariation_right_closed line 73

Source documentation

If only the right factor is closed, the entire derivative is exactly the left-factor term, with its reassociation shown.

theorem rawPrefix_productVariation_right_closed
    (a : MultilinearMap ℝ (fun _ : ι => E) ℂ)
    (Da : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : ι => E) ℂ)
    (b : MultilinearMap ℝ (fun _ : κ => E) ℂ)
    (Db : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : κ => E) ℂ)
    (hb : (rawPrefix Db).alternatization = 0) :
    (rawPrefix (rawProductVariation a Da b Db)).alternatization =
      (wedge (rawPrefix Da).alternatization b.alternatization).domDomCongr
        (Equiv.sumAssoc (Fin 1) ι κ) := by
…

Mentions: OAI.Mahler.rawPrefix, OAI.Mahler.rawProductVariation, OAI.Mahler.wedge