OAI/GroupTheory/PolycyclicRecognition/Analysis/FiniteSupportInterpolation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.listMass_eq_list_sum line 17
2. theorem OAI.PolycyclicRecognition.listMass_sort line 23
3. theorem OAI.PolycyclicRecognition.filter_sort_support line 30
4. def OAI.PolycyclicRecognition.finiteSupportCenter line 45
5. theorem OAI.PolycyclicRecognition.finiteSupportCenter_eq_on_superset line 48
6. theorem OAI.PolycyclicRecognition.finiteSupportCenter_dist_le line 60

   Source documentation

   A common finite support allows the list stability estimate to compare two probability vectors, even when some coordinates vanish in just one.

   theorem finiteSupportCenter_dist_le (c : ControlledContraction G) {D K : ℝ} {n : ℕ}
       (hK : InterpolationWeightControl (I := I) c D n K) (p₀ : G) (v : I → G)
   …

   Mentions: OAI.PolycyclicRecognition.ControlledContraction, OAI.PolycyclicRecognition.InterpolationWeightControl

7. theorem OAI.PolycyclicRecognition.finiteSupportCenter_dist_anchor_le line 80