OrderedInterpolation.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Ordered interpolation of finitely many nonnegative masses

Zero masses can be omitted. Thus one fixed order on the net gives compatible interpolations on different finite supports without a simplicial-complex API.

def OAI.PolycyclicRecognition.listMass line 17
def OAI.PolycyclicRecognition.listVariation line 21
def OAI.PolycyclicRecognition.orderedCenter line 24
theorem OAI.PolycyclicRecognition.listMass_nonneg line 28
theorem OAI.PolycyclicRecognition.listVariation_nonneg line 34
theorem OAI.PolycyclicRecognition.abs_listMass_sub_le line 37
theorem OAI.PolycyclicRecognition.listMass_filter_zero line 48
theorem OAI.PolycyclicRecognition.orderedCenter_singleton line 62
theorem OAI.PolycyclicRecognition.orderedCenter_zero_cons line 68
Source documentation
Inserting a zero mass at the front does not change a positive-mass interpolation. This is the compatibility needed at a support boundary.
```
theorem orderedCenter_zero_cons (c : ControlledContraction G) (p₀ : G)
    (v : I → G) (a : I → ℝ) (i : I) (l : List I)
    (hi : a i = 0) (hl : listMass a l ≠ 0) :
    orderedCenter c p₀ v a (i :: l) = orderedCenter c p₀ v a l := by
…
```
Mentions: OAI.PolycyclicRecognition.ControlledContraction, OAI.PolycyclicRecognition.listMass, OAI.PolycyclicRecognition.orderedCenter
theorem OAI.PolycyclicRecognition.orderedCenter_filter_zero line 76
Source documentation
Erasing all zero coordinates does not change the interpolated point when the total mass is positive.
```
theorem orderedCenter_filter_zero (c : ControlledContraction G) (p₀ : G)
    (v : I → G) (a : I → ℝ) (l : List I)
    (ha : ∀ i ∈ l, 0 ≤ a i) (hm : 0 < listMass a l) :
    orderedCenter c p₀ v a (l.filter (fun i => a i ≠ 0)) = orderedCenter c p₀ v a l := by
…
```
Mentions: OAI.PolycyclicRecognition.ControlledContraction, OAI.PolycyclicRecognition.listMass, OAI.PolycyclicRecognition.orderedCenter