Physlib.SpaceAndTime.Space.Derivatives.MultiIndex

Imports

/-
Copyright (c) 2026 Juan Jose Fernandez Morales. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Juan Jose Fernandez Morales
-/

module

public import Mathlib.Algebra.BigOperators.Fin

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.

MultiIndex.toList : the canonical ordered list of directions encoded by a multi-index.

iii. Table of contents

A. The basic type of multi-indices

A.1. Basic operations

A.2. Basic lemmas

A.3. Canonical ordered lists of directions

iv. References

@[expose] public section

A. The basic type of multi-indices

A multi-index on d source coordinates.

The coordinates of the multi-index.

structure MultiIndex (d : ℕ) where

  toFun : Fin d → ℕ
deriving DecidableEq

              instance : CoeFun (MultiIndex d) (fun _ => Fin d → ℕ) := ⟨MultiIndex.toFun⟩instance : Zero (MultiIndex d) := ⟨⟨0⟩⟩instance : Add (MultiIndex d) := ⟨fun I J => ⟨I.toFun + J.toFun⟩⟩

A.1. Basic operations

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

def order (I : MultiIndex d) : Nat := ∑ i, I i

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

def increment (I : MultiIndex d) (i : Fin d) : MultiIndex d := ⟨I.toFun + Pi.single i 1⟩

A.2. Basic lemmas

              @[ext]
lemma ext {I J : MultiIndex d} (h : ∀ i, I i = J i) : I = J := byd:ℕI:MultiIndex dJ:MultiIndex dh:∀ (i : Fin d), I.toFun i = J.toFun i⊢ I = J
  cases Imkd:ℕJ:MultiIndex dtoFun✝:Fin d → ℕh:∀ (i : Fin d), { toFun := toFun✝ }.toFun i = J.toFun i⊢ { toFun := toFun✝ } = J
  cases Jmk.mkd:ℕtoFun✝¹:Fin d → ℕtoFun✝:Fin d → ℕh:∀ (i : Fin d), { toFun := toFun✝¹ }.toFun i = { toFun := toFun✝ }.toFun i⊢ { toFun := toFun✝¹ } = { toFun := toFun✝ }
  simp only at hmk.mkd:ℕtoFun✝¹:Fin d → ℕtoFun✝:Fin d → ℕh:∀ (i : Fin d), toFun✝¹ i = toFun✝ i⊢ { toFun := toFun✝¹ } = { toFun := toFun✝ }
  congrmk.mkd:ℕtoFun✝¹:Fin d → ℕtoFun✝:Fin d → ℕh:∀ (i : Fin d), toFun✝¹ i = toFun✝ i⊢ toFun✝¹ = toFun✝
  funext imk.mkd:ℕtoFun✝¹:Fin d → ℕtoFun✝:Fin d → ℕh:∀ (i : Fin d), toFun✝¹ i = toFun✝ ii:Fin d⊢ toFun✝¹ i = toFun✝ i
  exact h iAll goals completed! 🐙@[simp]
lemma zero_apply (i : Fin d) : (0 : MultiIndex d) i = 0 := rfl@[simp]
lemma add_apply (I J : MultiIndex d) (i : Fin d) : (I + J) i = I i + J i := rfl@[simp]
lemma increment_apply_same (I : MultiIndex d) (i : Fin d) :
    increment I i i = I i + 1 := byd:ℕI:MultiIndex di:Fin d⊢ (I.increment i).toFun i = I.toFun i + 1
  simp [increment]All goals completed! 🐙@[simp]
lemma increment_apply_ne (I : MultiIndex d) {i j : Fin d} (h : j ≠ i) :
    increment I i j = I j := byd:ℕI:MultiIndex di:Fin dj:Fin dh:j ≠ i⊢ (I.increment i).toFun j = I.toFun j
  simp [increment, Pi.single_eq_of_ne h]All goals completed! 🐙@[simp]
lemma order_zero : order (0 : MultiIndex d) = 0 := byd:ℕ⊢ order 0 = 0
  simp [order]All goals completed! 🐙lemma order_add (I J : MultiIndex d) : order (I + J) = order I + order J := byd:ℕI:MultiIndex dJ:MultiIndex d⊢ (I + J).order = I.order + J.order
  simp [order, Finset.sum_add_distrib]All goals completed! 🐙

@[simp]
lemma order_single (i : Fin d) : order (⟨Pi.single i 1⟩ : MultiIndex d) = 1 := byd:ℕi:Fin d⊢ { toFun := Pi.single i 1 }.order = 1
  classical
  unfold orderd:ℕi:Fin d⊢ ∑ i_1, { toFun := Pi.single i 1 }.toFun i_1 = 1
  rw [Finset.sum_eq_single id:ℕi:Fin d⊢ { toFun := Pi.single i 1 }.toFun i = 1h₀d:ℕi:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ i → { toFun := Pi.single i 1 }.toFun b = 0h₁d:ℕi:Fin d⊢ i ∉ Finset.univ → { toFun := Pi.single i 1 }.toFun i = 0d:ℕi:Fin d⊢ { toFun := Pi.single i 1 }.toFun i = 1h₀d:ℕi:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ i → { toFun := Pi.single i 1 }.toFun b = 0h₁d:ℕi:Fin d⊢ i ∉ Finset.univ → { toFun := Pi.single i 1 }.toFun i = 0]d:ℕi:Fin d⊢ { toFun := Pi.single i 1 }.toFun i = 1h₀d:ℕi:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ i → { toFun := Pi.single i 1 }.toFun b = 0h₁d:ℕi:Fin d⊢ i ∉ Finset.univ → { toFun := Pi.single i 1 }.toFun i = 0
  ·d:ℕi:Fin d⊢ { toFun := Pi.single i 1 }.toFun i = 1 simpAll goals completed! 🐙
  ·h₀d:ℕi:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ i → { toFun := Pi.single i 1 }.toFun b = 0 intro j _ hjh₀d:ℕi:Fin dj:Fin da✝:j ∈ Finset.univhj:j ≠ i⊢ { toFun := Pi.single i 1 }.toFun j = 0
    simp [Pi.single_eq_of_ne hj]All goals completed! 🐙
  ·h₁d:ℕi:Fin d⊢ i ∉ Finset.univ → { toFun := Pi.single i 1 }.toFun i = 0 intro hih₁d:ℕi:Fin dhi:i ∉ Finset.univ⊢ { toFun := Pi.single i 1 }.toFun i = 0
    simp at hiAll goals completed! 🐙@[simp]
lemma order_increment (I : MultiIndex d) (i : Fin d) :
    order (increment I i) = order I + 1 := byd:ℕI:MultiIndex di:Fin d⊢ (I.increment i).order = I.order + 1
  simp [increment, order, Finset.sum_add_distrib]All goals completed! 🐙

A.3. Canonical ordered lists of directions

The tail of a multi-index on d + 1 coordinates, dropping the 0-th coordinate.

def tail (I : MultiIndex d.succ) : MultiIndex d := ⟨fun i => I i.succ⟩

The canonical ordered list of coordinate directions encoded by a multi-index.

def toList : {d : ℕ} → MultiIndex d → List (Fin d)
  | 0, _ => []
  | _ + 1, I => List.replicate (I 0) 0 ++ (toList (tail I)).map Fin.succ

              @[simp]
lemma tail_zero : tail (0 : MultiIndex d.succ) = 0 := byd:ℕ⊢ tail 0 = 0
  ext id:ℕi:Fin d⊢ (tail 0).toFun i = toFun 0 i
  rflAll goals completed! 🐙@[simp]
lemma tail_increment_zero (I : MultiIndex d.succ) : tail (increment I 0) = tail I := byd:ℕI:MultiIndex d.succ⊢ (I.increment 0).tail = I.tail
  ext id:ℕI:MultiIndex d.succi:Fin d⊢ (I.increment 0).tail.toFun i = I.tail.toFun i
  simp [tail, increment]All goals completed! 🐙@[simp]
lemma tail_increment_succ (I : MultiIndex d.succ) (i : Fin d) :
    tail (increment I i.succ) = increment (tail I) i := byd:ℕI:MultiIndex d.succi:Fin d⊢ (I.increment i.succ).tail = I.tail.increment i
  ext jd:ℕI:MultiIndex d.succi:Fin dj:Fin d⊢ (I.increment i.succ).tail.toFun j = (I.tail.increment i).toFun j
  by_cases h : j = iposd:ℕI:MultiIndex d.succi:Fin dj:Fin dh:j = i⊢ (I.increment i.succ).tail.toFun j = (I.tail.increment i).toFun jnegd:ℕI:MultiIndex d.succi:Fin dj:Fin dh:¬j = i⊢ (I.increment i.succ).tail.toFun j = (I.tail.increment i).toFun j
  ·posd:ℕI:MultiIndex d.succi:Fin dj:Fin dh:j = i⊢ (I.increment i.succ).tail.toFun j = (I.tail.increment i).toFun j subst hposd:ℕI:MultiIndex d.succj:Fin d⊢ (I.increment j.succ).tail.toFun j = (I.tail.increment j).toFun j
    simp [tail, increment]All goals completed! 🐙
  ·negd:ℕI:MultiIndex d.succi:Fin dj:Fin dh:¬j = i⊢ (I.increment i.succ).tail.toFun j = (I.tail.increment i).toFun j simp [tail, increment, h]All goals completed! 🐙@[simp]
lemma toList_zero : toList (0 : MultiIndex d) = [] := byd:ℕ⊢ toList 0 = []
  induction d with
  | zero =>zerod:ℕ⊢ toList 0 = [] rflAll goals completed! 🐙
  | succ d ih =>succd✝:ℕd:ℕih:toList 0 = []⊢ toList 0 = []
      simp [toList, ih]All goals completed! 🐙lemma length_toList (I : MultiIndex d) : I.toList.length = I.order := byd:ℕI:MultiIndex d⊢ I.toList.length = I.order
  induction d with
  | zero =>zerod:ℕI:MultiIndex 0⊢ I.toList.length = I.order
      simp [toList, MultiIndex.order]All goals completed! 🐙
  | succ d ih =>succd✝:ℕd:ℕih:∀ (I : MultiIndex d), I.toList.length = I.orderI:MultiIndex (d + 1)⊢ I.toList.length = I.order
      simp [toList, tail, MultiIndex.order, Fin.sum_univ_succ, ih]All goals completed! 🐙

@[simp]
lemma toList_increment_zero (I : MultiIndex d.succ) :
    toList (increment I 0) = 0 :: toList I := byd:ℕI:MultiIndex d.succ⊢ (I.increment 0).toList = 0 :: I.toList
  simp only [toList, increment_apply_same, tail_increment_zero]d:ℕI:MultiIndex d.succ⊢ List.replicate (I.toFun 0 + 1) 0 ++ List.map Fin.succ I.tail.toList =
  0 :: (List.replicate (I.toFun 0) 0 ++ List.map Fin.succ I.tail.toList)
  rw [show I 0 + 1 = 1 + I 0 byd:ℕI:MultiIndex d.succ⊢ (I.increment 0).toList = 0 :: I.toListd:ℕI:MultiIndex d.succ⊢ List.replicate 1 0 ++ List.replicate (I.toFun 0) 0 ++ List.map Fin.succ I.tail.toList =
  0 :: (List.replicate (I.toFun 0) 0 ++ List.map Fin.succ I.tail.toList) omegaAll goals completed! 🐙d:ℕI:MultiIndex d.succ⊢ List.replicate 1 0 ++ List.replicate (I.toFun 0) 0 ++ List.map Fin.succ I.tail.toList =
  0 :: (List.replicate (I.toFun 0) 0 ++ List.map Fin.succ I.tail.toList), List.replicate_addd:ℕI:MultiIndex d.succ⊢ List.replicate 1 0 ++ List.replicate (I.toFun 0) 0 ++ List.map Fin.succ I.tail.toList =
  0 :: (List.replicate (I.toFun 0) 0 ++ List.map Fin.succ I.tail.toList)d:ℕI:MultiIndex d.succ⊢ List.replicate 1 0 ++ List.replicate (I.toFun 0) 0 ++ List.map Fin.succ I.tail.toList =
  0 :: (List.replicate (I.toFun 0) 0 ++ List.map Fin.succ I.tail.toList)]d:ℕI:MultiIndex d.succ⊢ List.replicate 1 0 ++ List.replicate (I.toFun 0) 0 ++ List.map Fin.succ I.tail.toList =
  0 :: (List.replicate (I.toFun 0) 0 ++ List.map Fin.succ I.tail.toList)
  simpAll goals completed! 🐙

@[simp]
lemma toList_single (i : Fin d) : toList (increment 0 i : MultiIndex d) = [i] := byd:ℕi:Fin d⊢ (increment 0 i).toList = [i]
  induction d with
  | zero =>zerod:ℕi:Fin 0⊢ (increment 0 i).toList = [i]
      exact Fin.elim0 iAll goals completed! 🐙
  | succ d ih =>succd✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)⊢ (increment 0 i).toList = [i]
      refine Fin.cases ?_ ?_ isucc.refine_1d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)⊢ (increment 0 0).toList = [0]succ.refine_2d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)⊢ ∀ (i : Fin d), (increment 0 i.succ).toList = [i.succ]
      ·succ.refine_1d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)⊢ (increment 0 0).toList = [0] simp [toList_increment_zero]All goals completed! 🐙
      ·succ.refine_2d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)⊢ ∀ (i : Fin d), (increment 0 i.succ).toList = [i.succ] intro jsucc.refine_2d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)j:Fin d⊢ (increment 0 j.succ).toList = [j.succ]
        have htail :
            tail (increment (0 : MultiIndex d.succ) j.succ) = increment (0 : MultiIndex d) j := byd:ℕi:Fin d⊢ (increment 0 i).toList = [i]succ.refine_2d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)j:Fin dhtail:(increment 0 j.succ).tail = increment 0 j⊢ (increment 0 j.succ).toList = [j.succ]
          rw [tail_increment_succ,d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)j:Fin d⊢ (tail 0).increment j = increment 0 jsucc.refine_2d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)j:Fin dhtail:(increment 0 j.succ).tail = increment 0 j⊢ (increment 0 j.succ).toList = [j.succ] tail_zerod✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)j:Fin d⊢ increment 0 j = increment 0 jsucc.refine_2d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)j:Fin dhtail:(increment 0 j.succ).tail = increment 0 j⊢ (increment 0 j.succ).toList = [j.succ]]succ.refine_2d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)j:Fin dhtail:(increment 0 j.succ).tail = increment 0 j⊢ (increment 0 j.succ).toList = [j.succ]succ.refine_2d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)j:Fin dhtail:(increment 0 j.succ).tail = increment 0 j⊢ (increment 0 j.succ).toList = [j.succ]
        have hzero : increment (0 : MultiIndex d.succ) j.succ 0 = 0 := byd:ℕi:Fin d⊢ (increment 0 i).toList = [i]succ.refine_2d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)j:Fin dhtail:(increment 0 j.succ).tail = increment 0 jhzero:(increment 0 j.succ).toFun 0 = 0⊢ (increment 0 j.succ).toList = [j.succ]
          simp [increment]succ.refine_2d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)j:Fin dhtail:(increment 0 j.succ).tail = increment 0 jhzero:(increment 0 j.succ).toFun 0 = 0⊢ (increment 0 j.succ).toList = [j.succ]succ.refine_2d✝:ℕd:ℕih:∀ (i : Fin d), (increment 0 i).toList = [i]i:Fin (d + 1)j:Fin dhtail:(increment 0 j.succ).tail = increment 0 jhzero:(increment 0 j.succ).toFun 0 = 0⊢ (increment 0 j.succ).toList = [j.succ]
        simp [toList, hzero, htail, ih j]All goals completed! 🐙