Physlib.SpaceAndTime.Space.Derivatives.DerivativeIndex

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.Order.BigOperators.Group.Finset
public import Physlib.SpaceAndTime.Space.Derivatives.MultiIndex

Bounded derivative indices

i. Overview

This module defines bounded derivative indices on Space d, i.e. multi-indices of total order at most k.

These are the finite indexing objects used later for finite-order local jet coordinates, while remaining independent of any specific jet or field-theory construction.

ii. Key results

Physlib.DerivativeIndex

iii. Table of contents

A. Definition and basic instances

iv. References

@[expose] public section

A. Definition and basic instances

The multi-indices on d coordinates of order at most k.

abbrev DerivativeIndex (d k : ℕ) := { I : MultiIndex d // I.order ≤ k }

              instance (d k : ℕ) : DecidableEq (DerivativeIndex d k) := inferInstanceinstance (d k : ℕ) : Zero (DerivativeIndex d k) where
  zero := ⟨0, byd:ℕk:ℕ⊢ MultiIndex.order 0 ≤ k simp [Physlib.MultiIndex.order_zero]All goals completed! 🐙⟩@[simp]
lemma coe_zero (d k : ℕ) :
    ((0 : DerivativeIndex d k) : MultiIndex d) = 0 := rfl@[simp]
lemma zero_apply (d k : ℕ) (i : Fin d) :
    ((0 : DerivativeIndex d k) : MultiIndex d) i = 0 := rfl