OAI/Probability/ParisiFinite/SumLeCode.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Sum Le Code.

  1. theorem OAI.FiniteWeightedCode.sum_le_code line 33
  2. def OAI.SKQAOA.SiteHistories.internalEdges line 76
  3. lemma OAI.SKQAOA.SiteHistories.card_internalEdges_le line 79
  4. lemma OAI.SKQAOA.SiteHistories.forestVertices_card_le line 90
  5. lemma OAI.SKQAOA.SiteHistories.sum_powerset_pow line 98
  6. lemma OAI.SKQAOA.SiteHistories.sum_extras_bound line 104
  7. lemma OAI.SKQAOA.SiteHistories.weighted_extras_bound line 126
  8. lemma OAI.SKQAOA.SiteHistories.forest_extra_injective line 143
  9. lemma OAI.SKQAOA.SiteHistories.extras_internal line 150
  10. lemma OAI.SKQAOA.SiteHistories.code_weight line 163
  11. theorem OAI.SKQAOA.SiteHistories.cone_graph_tail line 171
  12. lemma OAI.SKQAOA.SiteHistories.roots_subset_used line 219
  13. lemma OAI.SKQAOA.SiteHistories.used_card_eq_forestSize_add_two line 226
  14. lemma OAI.SKQAOA.SiteHistories.cluster_zero_of_not_cone line 237
  15. lemma OAI.SKQAOA.SiteHistories.cluster_zero_of_edge_deficit line 246
  16. def OAI.SKQAOA.SiteHistories.tailConstant line 256
  17. lemma OAI.SKQAOA.SiteHistories.tailConstant_nonneg line 260
  18. theorem OAI.SKQAOA.SiteHistories.sum_norm_cluster_tail line 266
  19. def OAI.SKQAOA.SiteHistories.clusterEnergy line 303
  20. def OAI.SKQAOA.SiteHistories.complexEnergy line 306
  21. theorem OAI.SKQAOA.SiteHistories.expectedEnergy_eq_complexEnergy line 310
  22. lemma OAI.SKQAOA.SiteHistories.clusterEnergy_eq_scaled line 343
  23. lemma OAI.SKQAOA.SiteHistories.norm_clusterEnergy line 355
  24. lemma OAI.SKQAOA.SiteHistories.sum_norm_clusterEnergy_tail line 361
  25. lemma OAI.FiniteLabelCount.tendsto_choose_inv_pow line 399
  26. lemma OAI.FiniteLabelCount.tendsto_choose_inv_pow_of_le line 415
  27. lemma OAI.FiniteLabelCount.tendsto_choose_inv_pow_complex line 426
  28. def OAI.SKQAOA.SiteHistories.energySlice line 446
  29. def OAI.SKQAOA.SiteHistories.shapeTerm line 449
  30. def OAI.SKQAOA.SiteHistories.shapeTermLimit line 452
  31. theorem OAI.SKQAOA.SiteHistories.energySlice_eq_shapes line 457
  32. def OAI.SKQAOA.SiteHistories.energySliceLimit line 481
  33. theorem OAI.SKQAOA.SiteHistories.tendsto_energySlice line 485
  34. def OAI.SKQAOA.SiteHistories.truncatedEnergy line 501
  35. lemma OAI.SKQAOA.SiteHistories.truncatedEnergy_eq_slices line 504
  36. theorem OAI.SKQAOA.SiteHistories.tendsto_truncatedEnergy line 511
  37. theorem OAI.UniformApproximation.cauchySeq_of_approximants line 528
  38. lemma OAI.SKQAOA.SiteHistories.norm_complexEnergy_sub_truncated line 558
  39. theorem OAI.SKQAOA.SiteHistories.exists_complexEnergy_limit line 576
  40. theorem OAI.SKQAOA.exists_expectedEnergy_limit line 596
  41. theorem OAI.SKQAOA.tendsto_expectedEnergy_value line 604
  42. theorem OAI.SKQAOA.abs_value_le_Pstar line 617
  43. theorem OAI.SKQAOA.value_le_Pstar line 621
  44. theorem OAI.SKQAOA.valueSet_bddAbove line 624
  45. theorem OAI.SKQAOA.value_le_Q line 630
  46. theorem OAI.SKQAOA.Q_le_Pstar line 633
  47. theorem OAI.SKQAOA.monotone_Q line 638
  48. def OAI.SKQAOA.attainableEnergy line 647
  49. theorem OAI.SKQAOA.attainableEnergy_le_Pstar line 649
  50. theorem OAI.SKQAOA.tendsto_Q_attainableEnergy line 654