OAI/Probability/ParisiFinite/OrderedCode.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Ordered Code.

  1. def OAI.SKCavity.orderedCode line 64
  2. lemma OAI.SKCavity.orderedIndex_emb line 66
  3. lemma OAI.SKCavity.codeLabels_orderedCode line 70
  4. lemma OAI.SKCavity.labelCount_orderedCode line 83
  5. lemma OAI.SKCavity.partitionNumerator_ordered line 93
  6. lemma OAI.SKCavity.tableFactor_explicit line 100
  7. theorem OAI.SKCavity.GG_ordered_partition_probability line 118
  8. lemma OAI.SKCavity.iteratedDeriv_log_succ line 137
  9. lemma OAI.SKCavity.iteratedDeriv_log_one line 156
  10. lemma OAI.SKCavity.signed_log_factor line 162
  11. lemma OAI.SKCavity.log_mark_derivative line 178
  12. def OAI.SKCavity.orderedMarkedMoment line 207
  13. theorem OAI.SKCavity.GG_marked_log_derivative line 214
  14. def OAI.SKCavity.branchFactor line 244
  15. lemma OAI.SKCavity.branchFactor_one line 247
  16. lemma OAI.SKCavity.branchFactor_zero line 248
  17. lemma OAI.SKCavity.branchFactor_succ line 250
  18. lemma OAI.SKCavity.signed_power_factor line 258
  19. lemma OAI.SKCavity.iteratedDeriv_rpow_one line 276
  20. lemma OAI.SKCavity.power_mark_derivative line 290
  21. theorem OAI.SKCavity.GG_join_on_block line 329
  22. def OAI.SKCavity.ParentReps line 370
  23. lemma OAI.SKCavity.sum_parent_clusterCount line 373
  24. theorem OAI.SKCavity.GG_nested_innovation line 407
  25. lemma OAI.SKCavity.log_power_affine_derivative line 493
  26. lemma OAI.SKCavity.ordered_partition_mass line 511
  27. lemma OAI.SKCavity.ordered_partSize_sum line 528
  28. lemma OAI.SKCavity.finiteMarkMoment_nonneg line 533
  29. lemma OAI.SKCavity.finiteMarkMoment_le line 536
  30. lemma OAI.SKCavity.orderedMarkedMoment_nonneg line 543
  31. lemma OAI.SKCavity.orderedMarkedMoment_le line 550
  32. def OAI.SKCavity.markedLogSeries line 577
  33. lemma OAI.SKCavity.markedLog_hasFPowerSeriesAt line 581
  34. lemma OAI.SKCavity.markedLogSeries_radius line 613
  35. lemma OAI.SKCavity.affine_mark_pos line 652
  36. lemma OAI.SKCavity.finiteMarkTransform_pos line 659
  37. lemma OAI.SKCavity.contDiffAt_mark_of_abs_lt line 673
  38. theorem OAI.SKCavity.GG_marked_log_identity line 685