OAI/Combinatorics/HoneycombBridges/LengthTransform.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Renewal transforms and irreducible length kernels.

  1. def OAI.HoneycombActual.discountedWeight line 14
  2. def OAI.HoneycombActual.bridgePartition line 17
  3. def OAI.HoneycombActual.irreducibleLaplace line 20
  4. def OAI.HoneycombActual.UnnormalizedRenewalIdentity line 23
  5. abbrev OAI.HoneycombActual.IrreducibleBridge line 29
  6. def OAI.HoneycombActual.irreducibleProduct line 31
  7. theorem OAI.HoneycombActual.irreducibleProduct_injective line 34
  8. theorem OAI.HoneycombActual.irreducibleProduct_surjective line 45
  9. def OAI.HoneycombActual.irreducibleProductEquiv line 54
  10. theorem OAI.HoneycombActual.discountedWeight_concat line 58
  11. def OAI.HoneycombActual.optionWeight line 67
  12. theorem OAI.HoneycombActual.optionWeight_bridgeProduct line 71
  13. theorem OAI.HoneycombActual.optionWeight_irreducibleProduct line 85
  14. def OAI.HoneycombActual.RenewalList.lengthSuccEquiv line 95
  15. theorem OAI.HoneycombActual.RenewalList.sum_prod_length line 110
  16. theorem OAI.HoneycombActual.RenewalList.sum_prod line 127
  17. theorem OAI.HoneycombActual.optionWeight_tsum line 138
  18. theorem OAI.HoneycombActual.bridgePartition_geometric line 144
  19. theorem OAI.HoneycombActual.unnormalizedRenewalIdentity line 157
  20. def OAI.HoneycombActual.lengthPartition line 163
  21. def OAI.HoneycombActual.irreducibleLengthPartition line 166
  22. def OAI.HoneycombActual.LengthRewardTransformIdentity line 169
  23. abbrev OAI.HoneycombActual.RenewalList.Marked line 177
  24. def OAI.HoneycombActual.RenewalList.mark line 179
  25. def OAI.HoneycombActual.RenewalList.unmark line 182
  26. theorem OAI.HoneycombActual.RenewalList.unmark_mark line 185
  27. theorem OAI.HoneycombActual.RenewalList.mark_unmark line 189
  28. def OAI.HoneycombActual.RenewalList.markedEquiv line 198
  29. def OAI.HoneycombActual.RenewalList.markedWeight line 204
  30. theorem OAI.HoneycombActual.RenewalList.sum_map_eq_sum_fin line 207
  31. theorem OAI.HoneycombActual.RenewalList.sum_markedWeight line 214
  32. theorem OAI.HoneycombActual.RenewalList.markedWeight_mark line 223
  33. theorem OAI.HoneycombActual.RenewalList.sum_prod_reward line 230
  34. def OAI.HoneycombActual.optionLength line 254
  35. theorem OAI.HoneycombActual.optionLength_bridgeProduct line 258
  36. theorem OAI.HoneycombActual.optionLength_irreducibleProduct line 272
  37. theorem OAI.HoneycombActual.optionLengthWeight_tsum line 277
  38. theorem OAI.HoneycombActual.listWeight_tsum line 285
  39. theorem OAI.HoneycombActual.lengthPartition_marked line 293
  40. theorem OAI.HoneycombActual.lengthRewardTransformIdentity line 316
  41. theorem OAI.HoneycombActual.tsum_by_halfLength line 322
  42. def OAI.HoneycombActual.truncatedIrreducibleLength line 337
  43. def OAI.HoneycombActual.ActualTruncatedLengthLower line 342
  44. theorem OAI.HoneycombActual.half_min_le_length_kernel line 346
  45. theorem OAI.HoneycombActual.length_kernel_le_min line 363
  46. theorem OAI.HoneycombActual.lengthLaplaceReward_le_truncated line 371
  47. theorem OAI.HoneycombActual.truncated_le_lengthLaplaceReward line 395
  48. theorem OAI.HoneycombActual.exponent_balance line 423
  49. theorem OAI.HoneycombActual.actualLengthLaplaceLower_iff_truncated line 432
  50. def OAI.HoneycombActual.irreducibleCount line 476
  51. theorem OAI.HoneycombActual.truncatedIrreducibleLength_eq_count_series line 479
  52. def OAI.HoneycombActual.ActualCoefficientLower line 497
  53. theorem OAI.HoneycombActual.actualLengthLaplaceLower_iff_coefficients line 503