Is there a full and precise formulation of Theorem 1 in the Integrated Gradients paper?

Question

Theorem 1 (page 5) in the paper about Integrated Gradients states that

Integrated gradients is the unique path method that is symmetry-preserving.

What I miss is

1. A precise formulation of the theorem: in particular, the exact properties that must be satisfied by the function $f$ used in the proof (continuity, differentiability, etc.). Also, should the paths be assumed to be monotonic?

2. A consistent definition of function $f$ in the proof - note that $f$ is defined inconsistently, e.g. in the region where $x_i<a$ and $x_j>b$, where it is not clear whether its value should be $0$ or $(b-a)^2$.

Point 2 is easy to fix with an appropriate redefinition (e.g. replacing "if $\text{max}(x_i,x_j)\geq 0$" with "else if $\text{max}(x_i,x_j)\geq 0$"). What it is not clear if whether there is a redefinition that:

1. preserves the properties that have been assumed in the rest of the paper, in particular in Proposition 1 (proving completeness), where the function is assumed to be continuous everywhere, and the set of discontinuous points of each of its partial derivatives along each input dimension has measure zero, and

2. the function is a constant for $t \notin [t_1,t_2]$.

Does anybody have a precise formulation and full proof of the theorem?

Answer 1

After working on it for a while this is what I got.

Concerning proposition 1 in the paper, a rigorous statement could be the following version of the Gradient Theorem for line integrals:

Proposition 1. (Gradient Theorem for Lipschitz Continuous Functions). Let $U$ be an open subset of $\mathbb{R}^n$. If $F : U \to \mathbb{R}$ is Lipschitz continuous, and $\gamma : [0,1] \to U$ is a smooth path such that $F$ is differentiable at $\gamma(t)$ for almost every $t\in [0,1]$, then $$ \int_{\gamma} \nabla F(\mathbf{x}) \cdot d\mathbf{x} = F(\gamma(1)) - F(\gamma(0)) \,. $$

I found theorem 1 about symmetry-preserving harder to state rigurously while still fully capturing its intended meaning - this is the best I got:

Theorem 1. Given $i,j\in \{1,\dots,n\}$, $i\neq j$, real numbers $a<b$, and a strictly monotonic smooth path $\gamma : [0,1] \to (a,b)^n$ such that $\gamma_i(0)=\gamma_j(0)$ and $\gamma_i(1)=\gamma_j(1)$, then the following statements are equivalent:

(1) For every $t\in [0,1]$, $\gamma_i(t) = \gamma_j(t)$.

(2) For every function $F : [a,b]^n \to \mathbb{R}$ symmetric in $x_i$ and $x_j$ and verifying the premises of proposition 1 with $U=(a,b)^n$ we have $\int_{\gamma} \frac{\partial F(\mathbf{x})}{\partial x_i} \, dx_i = \int_{\gamma} \frac{\partial F(\mathbf{x})}{\partial x_j} \, dx_j$.

Further details and proofs: Symmetry-Preserving Paths in Integrated Gradients