OAI/Probability/ParisiFinite/SumFinLtNat.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Sum Fin Lt Nat.

  1. lemma OAI.SKCavity.sum_fin_lt_nat line 64
  2. lemma OAI.SKCavity.sum_grid_lt line 74
  3. lemma OAI.SKCavity.grid_covariance_error line 86
  4. def OAI.SKCavity.cavityGrid line 95
  5. def OAI.SKCavity.cavityGridVariance line 96
  6. lemma OAI.SKCavity.cavityGridVariance_nonneg line 98
  7. lemma OAI.SKCavity.cavityGridVariance_sum line 103
  8. lemma OAI.SKCavity.cavityGrid_mono line 108
  9. lemma OAI.SKCavity.cavityGrid_root line 126
  10. lemma OAI.SKCavity.cavityGrid_last line 127
  11. lemma OAI.SKCavity.cavityGrid_error line 132
  12. def OAI.SKCavity.gridCavityMixture line 148
  13. lemma OAI.SKCavity.gridCavityMixture_integral line 154
  14. theorem OAI.SKCavity.gridCavityMixture_error line 168
  15. def OAI.SKCavity.gridCavityPolynomial line 222
  16. lemma OAI.SKCavity.gridCavityPolynomial_continuous line 227
  17. lemma OAI.SKCavity.gridCavityMixture_eq_polynomial line 233
  18. lemma OAI.SKCavity.gridCavityPolynomial_limit line 245
  19. theorem OAI.SKCavity.exists_grid_cavity_pressure_bound line 266
  20. lemma OAI.SKCavity.gaussianLaw_isGaussian line 288
  21. def OAI.SKCavity.fieldCLM line 301
  22. lemma OAI.SKCavity.fieldCLM_apply line 305
  23. lemma OAI.SKCavity.field_hasGaussianLaw line 309
  24. lemma OAI.SKCavity.field_mean_zero line 317
  25. lemma OAI.SKCavity.dual_apply_eq_sum line 331
  26. lemma OAI.SKCavity.dual_field_mean_zero line 344
  27. lemma OAI.SKCavity.dual_field_variance line 354
  28. theorem OAI.SKCavity.field_law_eq_of_kernel line 379
  29. lemma OAI.SKCavity.field_continuous_any line 398
  30. lemma OAI.SKCavity.integral_field_eq_of_kernel line 404
  31. theorem OAI.SKCavity.codeGaussian_marginal line 414
  32. lemma OAI.SKCavity.codeGaussian_integral_marginal line 426
  33. lemma OAI.SKCavity.codeGaussian_law_of_same_partition line 440
  34. def OAI.SKCavity.gaussianQuantizer line 460
  35. abbrev OAI.SKCavity.GaussianQuantizerLabel line 463
  36. def OAI.SKCavity.gaussianQuantizerIndex line 465
  37. lemma OAI.SKCavity.gaussianQuantizerIndex_measurable line 468
  38. lemma OAI.SKCavity.gaussianQuantizer_tendsto line 471
  39. def OAI.SKCavity.gaussianQuantizerLaw line 475
  40. instance OAI.SKCavity.gaussianQuantizerLaw_probability line 478
  41. def OAI.SKCavity.gaussianQuantizerWeight line 482
  42. lemma OAI.SKCavity.gaussianQuantizerWeight_nonneg line 485
  43. lemma OAI.SKCavity.gaussianQuantizerWeight_sum line 488
  44. lemma OAI.SKCavity.gaussianQuantizer_quadrature line 491
  45. theorem OAI.SKCavity.gaussianQuantizer_bounded_continuous line 510
  46. def OAI.SKCavity.TreeNode line 540
  47. instance OAI.SKCavity.treeNodeFintype line 544
  48. instance OAI.SKCavity.treeNodeDecidableEq line 551
  49. def OAI.SKCavity.treeNodePath line 553
  50. lemma OAI.SKCavity.treeNodePath_emb line 559
  51. lemma OAI.SKCavity.treeNodePath_eq_iff line 566
  52. def OAI.SKCavity.treeDrawToNodes line 593
  53. def OAI.SKCavity.treeNodesToDraw line 597
  54. lemma OAI.SKCavity.treeNodesToDraw_toNodes line 601
  55. lemma OAI.SKCavity.treeDrawToNodes_toDraw line 612
  56. def OAI.SKCavity.treeDrawEquivNodes line 623
  57. lemma OAI.SKCavity.treeDrawToNodes_path line 629
  58. lemma OAI.SKCavity.treeDrawToNodes_weight line 642
  59. lemma OAI.SKCavity.treeMarkMoment_node_sum line 653