OAI/Probability/ParisiFinite/WeightedSumPos.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Weighted Sum Pos.

  1. lemma OAI.SKCavity.weighted_sum_pos line 65
  2. lemma OAI.SKCavity.hierarchyMark_pos line 76
  3. lemma OAI.SKCavity.hierarchyMark_contDiffAt line 84
  4. lemma OAI.SKCavity.hierarchyLog_contDiffAt line 97
  5. lemma OAI.SKCavity.treeMarkMoment_mem_unit line 105
  6. lemma OAI.SKCavity.hierarchyMarkedMoment_mem_unit line 121
  7. def OAI.SKCavity.hierarchyLogSeries line 142
  8. lemma OAI.SKCavity.hierarchyLog_zero line 146
  9. lemma OAI.SKCavity.hierarchyLogSeries_radius line 150
  10. lemma OAI.SKCavity.GG_hierarchyLog_hasFPowerSeriesAt line 172
  11. theorem OAI.SKCavity.GG_hierarchy_log_identity line 209
  12. lemma OAI.SKCavity.hierarchyMark_one line 245
  13. lemma OAI.SKCavity.hierarchyLog_one line 260
  14. lemma OAI.SKCavity.treeMarkMoment_one line 268
  15. lemma OAI.SKCavity.hierarchy_partition_mass line 276
  16. lemma OAI.SKCavity.hierarchy_partition_cover line 300
  17. def OAI.SKCavity.TreeDraw line 325
  18. instance OAI.SKCavity.treeDrawFintype line 329
  19. def OAI.SKCavity.treeDrawWeight line 337
  20. def OAI.SKCavity.treeDrawPath line 341
  21. lemma OAI.SKCavity.treeDrawPath_emb line 348
  22. lemma OAI.SKCavity.treeDrawWeight_nonneg line 356
  23. lemma OAI.SKCavity.treeDrawWeight_sum line 364
  24. lemma OAI.SKCavity.treeDraw_product line 374
  25. lemma OAI.SKCavity.hierarchy_numerator_mass_nz line 411
  26. lemma OAI.SKCavity.continuous_hierarchyNumerator line 428
  27. lemma OAI.SKCavity.hierarchy_numerator_mass line 433
  28. lemma OAI.SKCavity.hierarchy_partition_mass_all line 464
  29. lemma OAI.SKCavity.hierarchy_partition_cover_all line 485
  30. def OAI.SKCavity.NonnegativeArrays line 505
  31. lemma OAI.SKCavity.isClosed_NonnegativeArrays line 507
  32. lemma OAI.SKCavity.negative_pair_event_zero line 512
  33. theorem OAI.SKCavity.GG_nonnegative_arrays line 539
  34. abbrev OAI.SKCavity.CodeLabel line 571
  35. def OAI.SKCavity.codeGaussianCoeff line 573
  36. lemma OAI.SKCavity.kernel_codeGaussianCoeff line 577
  37. lemma OAI.SKCavity.codeKernel_nonneg line 597
  38. lemma OAI.SKCavity.codeKernel_le_one line 602
  39. lemma OAI.SKCavity.kernel_quadratic_nonneg line 608
  40. def OAI.SKCavity.codeGramBlock line 626
  41. lemma OAI.SKCavity.codeGramBlock_entry line 641
  42. lemma OAI.SKCavity.cavityGramObservable_lipschitz line 645
  43. def OAI.SKCavity.stepCovariance line 656
  44. lemma OAI.SKCavity.codeGramBlock_on_event line 659
  45. lemma OAI.SKCavity.gramBlock_dist_le line 669
  46. lemma OAI.SKCavity.codeCavity_error line 677