Physlib.Relativity.Tensors.Elab

A syntax category `indexExpr` for the indices of tensor expressions.

A Lean syntax category `indexExpr` for representing the indices of tensor expressions.

This defines the syntax rule specifying that a basic index expression is represented by an identifier.

This defines the syntax rule specifying that an index expression can be a numeric literal, which is used to evaluate the tensor.

This defines the syntax rule for the notation $\tau(x)$ (where $x$ is an identifier) as an index expression, which is used to describe the jiggle of a tensor index.

The syntax notation `[x]`, where `x` is an identifier, is defined as an index expression. It provides a notation to describe the evaluation of a tensor index.

A boolean function that evaluates to `true` if the given syntax object `stx` represents a numerical index in a tensor expression, and `false` otherwise.

A boolean function that evaluates to `true` if the given syntax object `stx` represents an evaluated bracket index in a tensor expression, such as `[μ]`, and `false` otherwise.

This function takes a syntax object representing a tensor index expression and extracts the underlying natural number if the index is a numeric literal. If the provided syntax does not represent a natural number, it throws an error.

This function takes a syntax object representing a tensor index expression and extracts the corresponding identifier when the index is not a numeric literal. Specifically, it can extract the identifier $a$ from syntax patterns such as a plain $a$, $\tau(a)$, or $[a]$. If the provided syntax does not match any of these supported identifier expressions, it throws an error.

This function takes two pairs $a = (s_a, p_a)$ and $b = (s_b, p_b)$, where $s$ represents the syntax of a tensor index expression (such as $\mu$ or $\tau(\mu)$) and $p \in \mathbb{N}$ represents its position. The function extracts the identifiers from both syntax objects; if the identifiers are identical and the position of the first index is strictly less than the position of the second ($p_a < p_b$), it returns the pair of positions $(p_a, p_b)$. Otherwise, it returns `none`. This logic is typically used during tensor elaboration to identify pairs of matching indices that should be contracted.

A function that maps a syntax object representing a tensor index expression to a boolean value. It evaluates to true if the index is of the form $\tau(i)$, indicating that the index is to be dualed, and false otherwise.

A function that maps a list of natural numbers $(x_1, \dots, x_n)$ to a new list $(y_1, \dots, y_n)$, where $y_i = x_i - |\{ j < i \mid x_j < x_i \}|$. It adjusts the sequence by subtracting from each natural number the number of preceding elements in the list that are strictly less than itself. This is used to form a list of pairs which can be used for evaluating indices.

Given a list of tensor index expressions $L$, let $(e_{i_1}, e_{i_2}, \dots, e_{i_k})$ be the subsequence of $L$ consisting of numeric literals, where $i_j$ denotes the original position (0-indexed) of the expression in $L$. Let $v_j$ be the numerical value of the expression $e_{i_j}$. This function returns a list of pairs $((p_1, v_1), (p_2, v_2), \dots, (p_k, v_k))$, where $p_j$ is the "adjusted position" defined as $p_j = i_j - (j - 1)$. This adjusted position represents the index of the numerical value in the list if all preceding numerical indices were sequentially removed. For example, given the index list $[\alpha, 3, \beta, 2, \gamma]$, the function identifies numeric values at positions $i_1=1$ (value $v_1=3$) and $i_2=3$ (value $v_2=2$), and returns the pairs $[(1, 3), (2, 2)]$.

Given a list of tensor index expressions $I = (e_0, e_1, \dots, e_n)$, the function identifies all indices of the form $[x]$ (referred to as bracketed evaluation indices). For each such index occurring at an original position $i$ in the list, it extracts the term $x$ and calculates an adjusted position $i'$. This adjusted position is defined as $i' = i - k$, where $k$ is the number of preceding indices in the list $I$ that are also bracketed evaluation indices. The function returns a list of pairs $(i', x)$ containing these adjusted positions and their corresponding terms.

Given a list of tensor index expressions $I$, let $I'$ be the sublist consisting of all symbolic indices, formed by removing numerical indices (e.g., $3$) and bracketed evaluation indices (e.g., $[x]$). This function identifies pairs of positions $(a, b)$ in $I'$ such that $a < b$ and the index symbol at position $a$ is identical to the index symbol at position $b$, corresponding to a contraction under the Einstein summation convention. The function returns a list of these position pairs $[(a_1, b_1), (a_2, b_2), \dots]$. It also verifies that no position appears in more than one pair, ensuring that each index symbol appears at most twice in $I'$; if an index symbol appears more than twice, the function throws an error.

Given a list of tensor index expressions $I$, the function `withoutContrEval` returns the sublist consisting of the "free" indices. This is achieved by first removing all numerical indices (which denote evaluation at a specific coordinate) and then removing any index that appears more than once in the remaining list (which denotes a contraction according to the Einstein summation convention).

The function maps a list of natural numbers $l$ to a list of pairs of natural numbers by grouping consecutive elements of $l$ together. Specifically, it transforms a list $[x_1, x_2, x_3, x_4, \dots]$ into $[(x_1, x_2), (x_3, x_4), \dots]$. If the length of $l$ is odd, the last element $x$ of the list is paired with $0$ to form the final pair $(x, 0)$.

The function maps a list of pairs of natural numbers $l$ to a new list of pairs of natural numbers. It adjusts the list by subtracting from each natural number the number of elements before it in the list which are strictly less than itself. This is used to form a list of pairs which can be used for contracting tensor indices.

Given two lists of tensor index expressions $l_1$ and $l_2$, where each expression represents an identifier (such as $\mu$ or $\nu$), this function computes the permutation that transforms $l_1$ into $l_2$. Specifically, it returns a list of natural numbers $[p_0, p_1, \dots, p_n]$ such that the $i$-th element of $l_2$ corresponds to the $p_i$-th element of $l_1$. The computation is performed within the `TermElabM` monad.

A function that constructs a term expression corresponding to a given string once parsed within the term elaboration monad.

Given two lists of tensor index expressions $l_1$ and $l_2$, this function identifies the permutation that maps the elements of $l_1$ to those of $l_2$. It returns a Lean syntax term representing an array literal $![p_0, p_1, \dots, p_n]$, where each $p_i$ is the natural number index in $l_1$ corresponding to the $i$-th element in $l_2$. This term is typically used to construct equivalence mappings for tensor indices (such as `finMapToEquiv`) during the elaboration of tensor expressions. The function operates within the `TermElabM` monad.

Defines the quotation parser description for the syntax category `tensorExpr`, which is used for parsing tensor expressions.

Defines the syntax category `tensorExpr` for parsing tensor expressions.

Defines the parsing syntax for a tensor node, consisting of a tensor term followed by a vertical bar `|` and a sequence of index expressions.

Defines the parsing syntax for the equality of two tensor expressions, denoted by `=`.

Defines the parsing syntax for the tensor product of two tensor expressions, denoted by $\otimes$.

Defines the parsing syntax for the addition of two tensor expressions, denoted by $+$.

This is a parser descriptor defining the syntax for using parentheses `(...)` in tensor expressions. It allows brackets to be used to group subexpressions within a tensor expression.

This is a parser descriptor defining the syntax for the scalar multiplication of a tensor expression, using the notation `•ₜ`.

This is a parser descriptor defining the syntax for the group action on tensor expressions, using the notation `•ₐ`.

This is a parser descriptor defining the syntax for the negation of a tensor expression, using the notation `-`.

For a given syntax `stx` representing a tensor $T$ of the form `S.F.obj (OverColor.mk c)`, this function evaluates and returns the exact number of indices associated with $T$. The result is a natural number returned within the `TermElabM` monad.

For a given syntax `stx` representing a tensor expression, this function evaluates and returns a list of all its index expressions within the `TermElabM` monad. For instance, given a syntax of the form $T \mid \alpha \, \beta \, 2 \, \beta$, it returns the list $[\alpha, \beta, 2, \beta]$ containing all the `indexExpr` elements.

The function `getProdIndices` evaluates the syntax `stx` of a tensor expression and returns a list of all uncontracted and unevaluated indices. Specifically, it operates on the syntax as follows: 1. For a single tensor expression, e.g., $T \mid \alpha \beta 2 \beta$, it returns all uncontracted and unevaluated indices, such as $[\alpha]$. 2. For a tensor product, e.g., $T_1 \mid \alpha \beta 2 \beta \otimes T_2 \mid \alpha \gamma \delta \delta$, it returns all unevaluated indices which are not contracted in either tensor, such as $[\alpha, \alpha, \gamma]$. 3. For nested tensor products, e.g., $(T_1 \mid \alpha \beta 2 \beta \otimes T_2 \mid \alpha \gamma \delta \delta) \otimes T_3 \mid \gamma$, it evaluates the indices recursively, such as $[\gamma, \gamma]$.

The function `getIndicesFull` evaluates the syntax `stx` of a tensor expression and returns a list of the remaining indices after contraction and evaluation. Thus, every index in the output is an identifier and there are no duplicates. Examples of its operation are as follows: 1. $T \mid \alpha \beta 2 \beta$ gives $[\alpha]$ 2. $T_1 \mid \alpha \beta 2 \beta \otimes T_2 \mid \alpha \gamma \delta \delta$ gives $[\gamma]$ 3. $(T_1 \mid \alpha \beta 2 \beta \otimes T_2 \mid \alpha \gamma \delta \delta) \otimes T_3 \mid \gamma$ gives $[]$ 4. $T_1 \mid \alpha \beta 2 \beta + T_2 \mid \alpha 4 \delta \delta$ gives $[\alpha]$

The function `getIndicesLeft` evaluates the syntax `stx` of a tensor addition expression, typically of the form $A + B$. It extracts and returns the list of uncontracted and unevaluated indices of the left-hand summand $A$ by calling `getIndicesFull`. If the provided syntax does not match an addition pattern, the function throws an error.

Given a syntax object representing the sum of two tensor expressions $A + B$, this function extracts the list of free indices associated with the right-hand summand $B$. The function specifically processes the syntax tree to isolate $B$ and then identifies all unique identifier indices that remain after any internal contractions or constant evaluations have been performed within that expression.

The function `getIndicesLeftEq` takes a syntax term representing a tensor equality of the form $A = B$ and returns a list of the free indices associated with the left-hand side expression $A$. These free indices are the identifiers that remain after all internal contractions and evaluations within the expression $A$ have been performed.

Given a syntax object representing a tensor equality of the form $T_1 = T_2$, this function extracts the list of free indices from the right-hand side expression $T_2$. These free indices are those that remain after all internal contractions and evaluations within $T_2$ have been performed (as determined by the `getIndicesFull` function). If the provided syntax does not match the pattern of an equality, the function returns an error.

For a syntax term $T$ representing a tensor of type `S.F.obj (OverColor.mk c)`, this function returns the syntax term corresponding to the tensor node of $T$.

Given a list $l$ of pairs $(a, b) \in \mathbb{N} \times \mathbb{N}$ and a term $T$ corresponding to a tensor tree, this function returns a new term by recursively applying the evaluation operation to $T$ for each pair in $l$. Here, $a$ is the position of the index to be evaluated, and $b$ is the value it is evaluated to.

Given a list $l$ of pairs $(a, b) \in \mathbb{N} \times \text{Term}$ and a syntax term $T$ corresponding to a tensor tree, this function returns a new syntax term by recursively applying the evaluation operation to $T$ for each pair in $l$. Here, $a$ is the position of the index to be evaluated, and $b$ is the term it is evaluated to from the bracket syntax. For example, if $l = [(1, \mu), (1, \nu)]$ and $T$ is a tensor tree, the result represents the term `TensorTree.eval 1 ν (TensorTree.eval 1 μ T)`.

The function `contrTermMap` generates a syntax term representing the repeated contraction of a tensor term $T$. Given a natural number $n$, a list of pairs of indices $l = [(i_1, j_1), (i_2, j_2), \dots]$, and a term $T$ (representing a tensor tree), the function first adjusts the indices using `contrListAdjust` to account for the reduction in the number of available indices after each successive contraction. It then constructs a new term by iteratively applying the contraction operator `Tensor.contrT` to $T$ for each pair in the adjusted list.

A function that constructs the syntax associated with the product of tensors. It maps two syntax terms $T_1$ and $T_2$ to the term representing their product, typically denoted as $T_1 \otimes T_2$.

A function that constructs the syntax associated with the negation of tensors. It maps a syntax term $T_1$ to the term representing its negation $-T_1$.

A function that constructs the syntax associated with the scalar multiplication of tensors. It maps a syntax term $c$ representing a scalar and a syntax term $T$ representing a tensor to the syntax term representing their scalar multiplication $c \cdot T$.

A function that constructs the syntax associated with the group action of tensors. It maps a syntax term $c$ representing a group element and a syntax term $T$ representing a tensor to the syntax term representing the group action of $c$ on $T$.

The function takes a permutation term $P$ and two tensor tree terms $T_1$ and $T_2$, and constructs the syntax term representing the addition of $T_1$ and the permutation of $T_2$ by $P$, effectively computing $T_1 + P(T_2)$. It is used to elaborate the syntax for an addition of tensor trees where the indices of the second tensor are permuted to match the first.

This function constructs the syntax for an equality of tensor trees. Given syntax terms $P$, $T_1$, and $T_2$, it returns the syntax term representing the equality $T_1 = P(T_2)$, where $P$ acts as a permutation on the indices of $T_2$.

The function `syntaxFull` takes a syntax `stx` corresponding to a tensor expression and turns it into a term corresponding to a tensor tree.

Given a syntax input `stx` representing a tensor expression (for instance, $\{T \mid \mu \nu\}^T$), this function elaborates it into a Lean expression `Expr` that represents the underlying tensor tree structure. This process transforms the high-level index notation into a formal representation of tensor operations such as contractions, permutations, and products.

The syntax `{E}ᵀ` denotes the tensor tree corresponding to the tensor expression $E$.