OAI/Probability/RadialTransition/ScaleSequence.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialTransition.doublePower line 10
  2. lemma OAI.RadialTransition.doublePower_zero line 11
  3. lemma OAI.RadialTransition.doublePower_succ line 12
  4. lemma OAI.RadialTransition.doublePower_pos line 15
  5. lemma OAI.RadialTransition.doublePower_le line 16
  6. lemma OAI.RadialTransition.doublePower_le_geometric line 19
  7. lemma OAI.RadialTransition.summable_doublePower line 21
  8. lemma OAI.RadialTransition.tsum_doublePower_le line 24
  9. lemma OAI.RadialTransition.doublePower_pow line 37
  10. lemma OAI.RadialTransition.doublePower_mul line 40
  11. lemma OAI.RadialTransition.doublePower_inv line 41
  12. def OAI.RadialTransition.scaleRange line 43
  13. def OAI.RadialTransition.scaleTail line 45
  14. lemma OAI.RadialTransition.doublePower_one_le line 47
  15. lemma OAI.RadialTransition.doublePower_le_self line 48
  16. lemma OAI.RadialTransition.scaleRange_pos line 50
  17. lemma OAI.RadialTransition.scaleRange_one_le line 51
  18. lemma OAI.RadialTransition.scaleRange_base_le line 52
  19. lemma OAI.RadialTransition.scaleRange_succ line 56
  20. lemma OAI.RadialTransition.scaleRange_mono line 59
  21. lemma OAI.RadialTransition.scaleTail_pos line 64
  22. lemma OAI.RadialTransition.scaleTail_eq line 65
  23. lemma OAI.RadialTransition.scaleTail_succ line 68
  24. lemma OAI.RadialTransition.scaleTail_le line 70
  25. lemma OAI.RadialTransition.scaleTail_le_one line 73
  26. lemma OAI.RadialTransition.inv_fourth_le_half line 75
  27. lemma OAI.RadialTransition.summable_scaleTail line 81
  28. lemma OAI.RadialTransition.tsum_scaleTail_le line 87
  29. lemma OAI.RadialTransition.sum_scaleTail_le line 89
  30. lemma OAI.RadialTransition.scaleRange_root line 92
  31. lemma OAI.RadialTransition.scaleTail_literal line 96
  32. lemma OAI.RadialTransition.scaleTail_weight line 102
  33. lemma OAI.RadialTransition.summable_scaleTail_weight line 107
  34. lemma OAI.RadialTransition.scale_kac_succ line 117
  35. lemma OAI.RadialTransition.scale_kac_zero line 132