HorizontalForms.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.Horizontal line 16
Source documentation
A form annihilates a vector in every slot.
```
def Horizontal {ι : Type*} (a : T [⋀^ι]→ₗ[ℝ] ℂ) (V : T) : Prop :=
…
```

theorem OAI.Mahler.horizontal_top_eq_zero line 20

Source documentation

A horizontal top-degree form vanishes when the contracting vector is nonzero.

theorem horizontal_top_eq_zero [FiniteDimensional ℝ T]
    {ι : Type*} [Fintype ι] {a : T [⋀^ι]→ₗ[ℝ] ℂ} {V : T}
    (hdim : Fintype.card ι = Module.finrank ℝ T) (hV : V ≠ 0)
    (ha : Horizontal a V) : a = 0 := by
…

Mentions: OAI.Mahler.Horizontal

def OAI.Mahler.wedge line 54

Source documentation

The exterior product uses the shuffle convention, with scalar multiplication after the tensor-valued alternating product.

noncomputable def wedge {ι κ : Type*} [Fintype ι] [Fintype κ]
    [DecidableEq ι] [DecidableEq κ]
    (a : T [⋀^ι]→ₗ[ℝ] ℂ) (b : T [⋀^κ]→ₗ[ℝ] ℂ) : T [⋀^ι ⊕ κ]→ₗ[ℝ] ℂ :=
…

theorem OAI.Mahler.Horizontal.wedge line 60

Source documentation

Exterior products of horizontal forms are horizontal.

theorem Horizontal.wedge {ι κ : Type*} [Fintype ι] [Fintype κ]
    [DecidableEq ι] [DecidableEq κ]
    {a : T [⋀^ι]→ₗ[ℝ] ℂ} {b : T [⋀^κ]→ₗ[ℝ] ℂ} {V : T}
    (ha : Horizontal a V) (hb : Horizontal b V) : Horizontal (wedge a b) V := by
…

Mentions: OAI.Mahler.Horizontal

def OAI.Mahler.WedgePowerSlots line 87
Source documentation
Slot types retain the order of each two-form factor.
```
def WedgePowerSlots : ℕ → Type
  | 0 => Fin 0
  | n + 1 => Fin 2 ⊕ WedgePowerSlots n
```
instance OAI.Mahler.wedgePowerSlotsFintype line 91
instance OAI.Mahler.wedgePowerSlotsDecidableEq line 98
lemma OAI.Mahler.card_wedgePowerSlots line 101

def OAI.Mahler.wedgePower line 110

Source documentation

Iterated shuffle exterior power of an actual alternating two-form.

noncomputable def wedgePower (a : T [⋀^Fin 2]→ₗ[ℝ] ℂ) :
    (n : ℕ) → T [⋀^WedgePowerSlots n]→ₗ[ℝ] ℂ
  | 0 => AlternatingMap.constOfIsEmpty ℝ T (Fin 0) 1
  | n + 1 => wedge a (wedgePower a n)

Mentions: OAI.Mahler.WedgePowerSlots, OAI.Mahler.wedge

lemma OAI.Mahler.Horizontal.wedgePower line 115

theorem OAI.Mahler.beta_wedge_power_eq_zero line 123

Source documentation

The form beta wedge (d alpha_t)^(n-1) vanishes in top degree. Here k = n-1 and T is the sphere tangent space, of dimension 2k+1.

theorem beta_wedge_power_eq_zero [FiniteDimensional ℝ T]
    (k : ℕ) {b : T [⋀^Fin 1]→ₗ[ℝ] ℂ} {a : T [⋀^Fin 2]→ₗ[ℝ] ℂ} {V : T}
    (hdim : Module.finrank ℝ T = 2 * k + 1) (hV : V ≠ 0)
    (hb : Horizontal b V) (ha : Horizontal a V) : wedge b (wedgePower a k) = 0 := by
…

Mentions: OAI.Mahler.Horizontal, OAI.Mahler.wedge, OAI.Mahler.wedgePower