OAI/Analysis/AncientFlat/Evolution/MovingBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FlatSimilarity.unitClamp line 8
2. lemma OAI.FlatSimilarity.unitClamp_mem line 9
3. lemma OAI.FlatSimilarity.unitClamp_eq line 13
4. lemma OAI.FlatSimilarity.unitClamp_lipschitz line 15
5. lemma OAI.FlatSimilarity.exp_neg_le_one line 17
6. lemma OAI.FlatSimilarity.exp_neg_lip line 19
7. lemma OAI.FlatSimilarity.timeweight_bounds line 29
8. lemma OAI.FlatSimilarity.timeweight_lip line 36
9. lemma OAI.FlatSimilarity.moving_scalar_joint_lip line 43
10. lemma OAI.FlatSimilarity.moving_product_joint_lip line 56