Multi-indices

i. Overview

This module defines the basic type of multi-indices used to index iterated partial derivatives.

A multi-index on d source coordinates is represented as a structure with an underlying function Fin d → ℕ, together with the first basic operations needed later in the local Classical Field Theory development.

ii. Key results

• Physlib.MultiIndex : multi-indices on d coordinates.
• MultiIndex.order : the order |I| of a multi-index.
• MultiIndex.increment : increment a single coordinate of a multi-index.

iii. Table of contents

• A. The basic type of multi-indices
  • A.1. Basic operations
  • A.2. Basic lemmas

iv. References

A. The basic type of multi-indices

structure Physlib.MultiIndex (d : ℕ) : Type

A multi-index on d source coordinates.

• toFun : Fin d → ℕ

  The coordinates of the multi-index.

def Physlib.instDecidableEqMultiIndex.decEq {d✝ : ℕ} (x✝ x✝¹ : MultiIndex d✝) : Decidable (x✝ = x✝¹)

Equations

• Physlib.instDecidableEqMultiIndex.decEq { toFun := a } { toFun := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Physlib.instDecidableEqMultiIndex {d✝ : ℕ} : DecidableEq (MultiIndex d✝)

Equations

• Physlib.instDecidableEqMultiIndex = Physlib.instDecidableEqMultiIndex.decEq

instance Physlib.MultiIndex.instCoeFunForallFinNat {d : ℕ} : CoeFun (MultiIndex d) fun (x : MultiIndex d) => Fin d → ℕ

Equations

• Physlib.MultiIndex.instCoeFunForallFinNat = { coe := Physlib.MultiIndex.toFun }

instance Physlib.MultiIndex.instZero {d : ℕ} : Zero (MultiIndex d)

Equations

• Physlib.MultiIndex.instZero = { zero := { toFun := 0 } }

instance Physlib.MultiIndex.instAdd {d : ℕ} : Add (MultiIndex d)

Equations

• Physlib.MultiIndex.instAdd = { add := fun (I J : Physlib.MultiIndex d) => { toFun := I.toFun + J.toFun } }

A.1. Basic operations

def Physlib.MultiIndex.order {d : ℕ} (I : MultiIndex d) : ℕ

The order |I| of a multi-index I, defined as the sum of its components.

Equations

• I.order = ∑ i : Fin d, I.toFun i

def Physlib.MultiIndex.increment {d : ℕ} (I : MultiIndex d) (i : Fin d) : MultiIndex d

Increment the i-th coordinate of a multi-index by one.

Equations

• I.increment i = { toFun := I.toFun + Pi.single i 1 }

A.2. Basic lemmas

theorem Physlib.MultiIndex.ext {d : ℕ} {I J : MultiIndex d} (h : ∀ (i : Fin d), I.toFun i = J.toFun i) : I = J

theorem Physlib.MultiIndex.ext_iff {d : ℕ} {I J : MultiIndex d} : I = J ↔ ∀ (i : Fin d), I.toFun i = J.toFun i

@[simp]

theorem Physlib.MultiIndex.zero_apply {d : ℕ} (i : Fin d) : toFun 0 i = 0

@[simp]

theorem Physlib.MultiIndex.add_apply {d : ℕ} (I J : MultiIndex d) (i : Fin d) : (I + J).toFun i = I.toFun i + J.toFun i

@[simp]

theorem Physlib.MultiIndex.increment_apply_same {d : ℕ} (I : MultiIndex d) (i : Fin d) : (I.increment i).toFun i = I.toFun i + 1

@[simp]

theorem Physlib.MultiIndex.increment_apply_ne {d : ℕ} (I : MultiIndex d) {i j : Fin d} (h : j ≠ i) : (I.increment i).toFun j = I.toFun j

@[simp]

theorem Physlib.MultiIndex.order_zero {d : ℕ} : order 0 = 0

theorem Physlib.MultiIndex.order_add {d : ℕ} (I J : MultiIndex d) : (I + J).order = I.order + J.order

@[simp]

theorem Physlib.MultiIndex.order_single {d : ℕ} (i : Fin d) : { toFun := Pi.single i 1 }.order = 1

@[simp]

theorem Physlib.MultiIndex.order_increment {d : ℕ} (I : MultiIndex d) (i : Fin d) : (I.increment i).order = I.order + 1