OAI/Analysis/AncientFlat/Kernel/SymbolDecay.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FlatSimilarity.decayWeight line 10
  2. lemma OAI.FlatSimilarity.decayWeight_pos line 11
  3. lemma OAI.FlatSimilarity.decayWeight_le_one line 12
  4. lemma OAI.FlatSimilarity.symbol_decay_le_weight line 15
  5. lemma OAI.FlatSimilarity.decayWeight_smul line 20
  6. lemma OAI.FlatSimilarity.decayWeight_translate line 26
  7. lemma OAI.FlatSimilarity.SymbolBounds.weighted_deviation_jets line 35
  8. def OAI.FlatSimilarity.movingDeviation line 42
  9. lemma OAI.FlatSimilarity.movingDeviation_smooth line 44
  10. lemma OAI.FlatSimilarity.weighted_scale_jets line 48
  11. lemma OAI.FlatSimilarity.movingDeviation_norm_jet line 62
  12. lemma OAI.FlatSimilarity.SymbolBounds.moving_weighted_jets line 72
  13. lemma OAI.FlatSimilarity.SymbolBounds.moving_four_weighted_jets line 88
  14. lemma OAI.FlatSimilarity.SymbolBounds.movingDeviation_temperate line 97
  15. lemma OAI.FlatSimilarity.SymbolBounds.movingB_temperate line 103