OAI/Probability/Contingency/ChildLogConcavity.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Child Log Concavity.

  1. theorem OAI.Contingency.bool_signature_determinant line 19
  2. def OAI.Contingency.childProfile line 40
  3. theorem OAI.Contingency.signature_child_logconcave line 44
  4. theorem OAI.Contingency.positive_logconcave_min line 69
  5. theorem OAI.Contingency.signature_child_min line 112
  6. theorem OAI.Contingency.zero_child_min line 128
  7. def OAI.Contingency.totalWeight line 153
  8. def OAI.Contingency.weightedMean line 154
  9. def OAI.Contingency.weightedVariance line 155
  10. theorem OAI.Contingency.centered_sum line 158
  11. theorem OAI.Contingency.variance_translate line 165
  12. theorem OAI.Contingency.variance_secondMoment line 176
  13. theorem OAI.Contingency.variance_pair_formula line 187
  14. theorem OAI.Contingency.variance_nonneg line 199
  15. theorem OAI.Contingency.variance_le_card_sq line 205
  16. theorem OAI.Contingency.interval_square_bound line 227
  17. theorem OAI.Contingency.child_pair_bound line 247
  18. structure OAI.Contingency.FiniteChain.Chain line 298
  19. def OAI.Contingency.FiniteChain.Chain.mean line 313
  20. def OAI.Contingency.FiniteChain.Chain.inner line 314
  21. def OAI.Contingency.FiniteChain.Chain.normSq line 315
  22. def OAI.Contingency.FiniteChain.Chain.step line 316
  23. def OAI.Contingency.FiniteChain.Chain.energy line 317
  24. theorem OAI.Contingency.FiniteChain.Chain.stationary line 319
  25. theorem OAI.Contingency.FiniteChain.Chain.normSq_nonneg line 323
  26. theorem OAI.Contingency.FiniteChain.Chain.inner_self line 326
  27. theorem OAI.Contingency.FiniteChain.Chain.step_mean line 329
  28. theorem OAI.Contingency.FiniteChain.Chain.step_selfadjoint line 334
  29. theorem OAI.Contingency.FiniteChain.Chain.inner_comm line 343
  30. theorem OAI.Contingency.FiniteChain.Chain.edge_sums_left line 347
  31. theorem OAI.Contingency.FiniteChain.Chain.edge_sums_right line 351
  32. theorem OAI.Contingency.FiniteChain.Chain.edge_cross line 356
  33. theorem OAI.Contingency.FiniteChain.Chain.energy_identity line 362
  34. theorem OAI.Contingency.FiniteChain.Chain.step_positive line 371
  35. theorem OAI.Contingency.FiniteChain.Chain.step_cauchy line 400
  36. def OAI.Contingency.FiniteChain.Chain.variance line 433
  37. theorem OAI.Contingency.FiniteChain.Chain.variance_centered line 435
  38. theorem OAI.Contingency.FiniteChain.Chain.gap_inner line 438
  39. theorem OAI.Contingency.FiniteChain.Chain.gap_normSq line 452
  40. def OAI.Contingency.FiniteChain.Chain.iterate line 471
  41. theorem OAI.Contingency.FiniteChain.Chain.iterate_mean line 475
  42. theorem OAI.Contingency.FiniteChain.Chain.iterate_normSq line 480
  43. def OAI.Contingency.FiniteChain.Chain.law line 496
  44. def OAI.Contingency.FiniteChain.Chain.initialDensity line 500
  45. theorem OAI.Contingency.FiniteChain.Chain.density_mean line 503
  46. theorem OAI.Contingency.FiniteChain.Chain.density_normSq line 511
  47. theorem OAI.Contingency.FiniteChain.Chain.density_law line 525
  48. def OAI.Contingency.FiniteChain.Chain.tv line 545
  49. theorem OAI.Contingency.FiniteChain.Chain.tv_density line 548
  50. theorem OAI.Contingency.FiniteChain.Chain.weighted_abs_sq line 558
  51. theorem OAI.Contingency.FiniteChain.Chain.tv_sq line 568
  52. theorem OAI.Contingency.FiniteChain.Chain.mixing_bound line 576
  53. theorem OAI.Contingency.FiniteChain.Chain.mixing_bound_min line 610