RawClosedPower.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.rawPowerVariation line 9

theorem OAI.Mahler.rawPowerVariation_closed line 17

Source documentation

All derivative placements in the k-fold product vanish after alternation when the actual two-form derivative is closed.

theorem rawPowerVariation_closed (B : MultilinearMap ℝ (fun _ : Fin 2 => E) ℂ)
    (DB : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : Fin 2 => E) ℂ)
    (hB : (rawPrefix DB).alternatization = 0) (k : ℕ) :
    (rawPrefix (rawPowerVariation B DB k)).alternatization = 0 := by
…

Mentions: OAI.Mahler.rawPrefix, OAI.Mahler.rawPowerVariation

def OAI.Mahler.rawCovectorVariation line 32

Source documentation

The uncurried derivative of a covector field, before alternation.

def rawCovectorVariation (Da : E →ₗ[ℝ] E →ₗ[ℝ] ℂ) :
    E →ₗ[ℝ] MultilinearMap ℝ (fun _ : Fin 1 => E) ℂ where
…

theorem OAI.Mahler.rawBoundaryVariation_closed line 40

Source documentation

Full raw product-rule identity underlying d(alpha wedge B^k), with all right-factor contributions proved zero and the surviving order explicit.

theorem rawBoundaryVariation_closed (a : E →ₗ[ℝ] ℂ)
    (Da : E →ₗ[ℝ] E →ₗ[ℝ] ℂ)
    (B : MultilinearMap ℝ (fun _ : Fin 2 => E) ℂ)
    (DB : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : Fin 2 => E) ℂ)
    (hB : (rawPrefix DB).alternatization = 0) (k : ℕ) :
    (rawPrefix (rawProductVariation (rawCovector a) (rawCovectorVariation Da)
      (rawPower B k) (rawPowerVariation B DB k))).alternatization =
      (wedge (rawPrefix (rawCovectorVariation Da)).alternatization
        (wedgePower B.alternatization k)).domDomCongr
          (Equiv.sumAssoc (Fin 1) (Fin 1) (WedgePowerSlots k)) := by
…

Mentions: OAI.Mahler.rawPrefix, OAI.Mahler.rawProductVariation, OAI.Mahler.rawCovector, OAI.Mahler.rawCovectorVariation, OAI.Mahler.rawPower, OAI.Mahler.rawPowerVariation, OAI.Mahler.wedge, OAI.Mahler.wedgePower, OAI.Mahler.WedgePowerSlots