diff --git a/Physlib.lean b/Physlib.lean index 750da9136..616caa334 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -350,6 +350,7 @@ public import Physlib.SpaceAndTime.Space.Derivatives.Curl public import Physlib.SpaceAndTime.Space.Derivatives.Div public import Physlib.SpaceAndTime.Space.Derivatives.Grad public import Physlib.SpaceAndTime.Space.Derivatives.Laplacian +public import Physlib.SpaceAndTime.Space.Derivatives.MultiIndex public import Physlib.SpaceAndTime.Space.DistConst public import Physlib.SpaceAndTime.Space.DistOfFunction public import Physlib.SpaceAndTime.Space.Integrals.Basic diff --git a/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean b/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean new file mode 100644 index 000000000..f76657402 --- /dev/null +++ b/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean @@ -0,0 +1,131 @@ +/- +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.Pi + +/-! +# 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 + +-/ + +@[expose] public section + +open scoped BigOperators + +namespace Physlib + +/-! +## A. The basic type of multi-indices + +-/ + +/-- A multi-index on `d` source coordinates. -/ +structure MultiIndex (d : ℕ) where + /-- The coordinates of the multi-index. -/ + toFun : Fin d → ℕ +deriving DecidableEq + +namespace MultiIndex + +variable {d : ℕ} + +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 := by + cases I + cases J + simp only at h + congr + funext i + exact h i + +@[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 := by + simp [increment] + +@[simp] +lemma increment_apply_ne (I : MultiIndex d) {i j : Fin d} (h : j ≠ i) : + increment I i j = I j := by + simp [increment, Pi.single_eq_of_ne h] + +@[simp] +lemma order_zero : order (0 : MultiIndex d) = 0 := by + simp [order] + +lemma order_add (I J : MultiIndex d) : order (I + J) = order I + order J := by + simp [order, Finset.sum_add_distrib] + +@[simp] +lemma order_single (i : Fin d) : order (⟨Pi.single i 1⟩ : MultiIndex d) = 1 := by + classical + unfold order + rw [Finset.sum_eq_single i] + · simp + · intro j _ hj + simp [Pi.single_eq_of_ne hj] + · intro hi + simp at hi + +@[simp] +lemma order_increment (I : MultiIndex d) (i : Fin d) : + order (increment I i) = order I + 1 := by + simp [increment, order, Finset.sum_add_distrib] + +end MultiIndex + +end Physlib