RetaggedCost.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The auxiliary tuple cost can be removed from an admissible metric's lower bound. This is the retagging step in Section 4 of the manuscript.

def OAI.CircleDomainRigidity.nonTupleCost line 23
theorem OAI.CircleDomainRigidity.pathCostIntegral_sparse line 28
theorem OAI.CircleDomainRigidity.exists_endpointCode_small_tuple line 37
def OAI.CircleDomainRigidity.CostAdmissible line 55
Source documentation
Admissibility for the finite coding-measure family, with the prescribed residual-image null constraint but without any tuple exclusions.
```
def CostAdmissible (d : PathCodeData X Y) (p : D → X) (c : D → ℝ≥0∞)
    (ν : Measure X) (h : PathCostSpace Y D → ℝ≥0∞) : Prop :=
…
```
Mentions: OAI.CircleDomainRigidity.PathCodeData, OAI.CircleDomainRigidity.PathCostSpace
theorem OAI.CircleDomainRigidity.nonTupleCost_ge_one_of_admissible line 60