For manifolds without boundary one defines the injectivity radius as the maximal radius where the exponential map is a diffeomorphism. One can then show that the injectivity radius is the maximum number that such any two points with distance less than that number have a unique geodesic length minimizer between them.

If one looks at a (smooth complete compact) manifold with boundary, using the exponential map definition, points close to the boundary have small injectivity radius and the injectivity radius of the entire manifold would be zero. Using the interpretation about unique length minimizer instead would give a nontrivial notion of injectivity radius for manifolds with boundary.

My question is mostly a reference request, is it written down somewhere how to define the injectivity radius of a manifold with boundary?

My question came from papers that have general statements of the form: Let $(M,g)$ be a manifold with boundary, such that some curvature bounds hold and the injectivity radius is bounded from below. Then bla bla bla. I assume these are not theorems about the empty set.

Edit: Maybe this is more complicated than I thought. It seems we have three alternative proposals: 1. my original idea: there exists a unique length minimizer 2. Thomas Rot's idea: use the injectivity radius of the double of the manifold 3. Schick's paper, referenced by user44172: using a collar near the boundary

I think 1. and 2. are equivalent. Whether these two are equivalent to 3. looks nontrivial. Additionally, all these definitions are usually only used in combination with some curvature bounds, so the definitions might be distinct in full generality but equivalent under some suitable curvature bounds.