OAI/Probability/Contingency/ConcreteKernel.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Concrete Kernel.

  1. abbrev OAI.Contingency.PaddedGraph.SmallSlot line 16
  2. abbrev OAI.Contingency.PaddedGraph.LargeSlot line 18
  3. abbrev OAI.Contingency.PaddedGraph.SmallCoord line 20
  4. def OAI.Contingency.PaddedGraph.largeIndex line 23
  5. def OAI.Contingency.PaddedGraph.wholeCoordinates line 28
  6. theorem OAI.Contingency.PaddedGraph.wholeCoordinates_small line 48
  7. theorem OAI.Contingency.PaddedGraph.wholeCoordinates_large line 53
  8. theorem OAI.Contingency.PaddedGraph.capacity_box line 59
  9. theorem OAI.Contingency.PaddedGraph.capacity_total line 67
  10. def OAI.Contingency.PaddedGraph.smallKernel line 80
  11. theorem OAI.Contingency.PaddedGraph.smallKernel_signature line 88
  12. def OAI.Contingency.PaddedGraph.stateCoordinates line 106
  13. def OAI.Contingency.PaddedGraph.coordinatesState line 110
  14. theorem OAI.Contingency.PaddedGraph.coordinatesState_x line 115
  15. theorem OAI.Contingency.PaddedGraph.coordinatesState_q line 118
  16. theorem OAI.Contingency.PaddedGraph.stateCoordinates_coordinatesState line 122
  17. def OAI.Contingency.PaddedGraph.largeChoicesEquiv line 128
  18. def OAI.Contingency.PaddedGraph.largeProfileEquiv line 152
  19. theorem OAI.Contingency.PaddedGraph.balanced_fullCoordinates line 156
  20. theorem OAI.Contingency.PaddedGraph.smallKernel_zero_count line 178
  21. theorem OAI.Contingency.PaddedGraph.full_zero_feasible line 188
  22. theorem OAI.Contingency.PaddedGraph.coordinatesState_supported line 236
  23. theorem OAI.Contingency.PaddedGraph.smallKernel_zero_infeasible line 244
  24. theorem OAI.Contingency.PaddedGraph.smallKernel_continuous line 260
  25. theorem OAI.Contingency.PaddedGraph.smallKernel_nonneg line 267
  26. theorem OAI.Contingency.weight_zero_of_total_zero line 291
  27. theorem OAI.Contingency.mass_mul_mean line 296
  28. theorem OAI.Contingency.centered_sum_nonneg line 304
  29. theorem OAI.Contingency.variance_translate_nonneg line 310
  30. theorem OAI.Contingency.variance_le_deviation line 321
  31. theorem OAI.Contingency.variance_decompose line 334
  32. def OAI.Contingency.Profiles line 360
  33. instance OAI.Contingency.profilesFintype line 364
  34. def OAI.Contingency.ExposureEnergies line 371
  35. def OAI.Contingency.exposureEnergy line 375
  36. def OAI.Contingency.ChildVarianceBounds line 381
  37. theorem OAI.Contingency.exposure_variance_bound line 391
  38. def OAI.Contingency.exposureLevel line 419
  39. theorem OAI.Contingency.exposureEnergy_levels line 424
  40. theorem OAI.Contingency.exposure_variance_level_bound line 435
  41. def OAI.Contingency.nodeMass line 460
  42. def OAI.Contingency.nodeMean line 463
  43. def OAI.Contingency.adjacentDisplay line 466
  44. theorem OAI.Contingency.adjacent_minus line 468
  45. theorem OAI.Contingency.adjacent_plus line 472
  46. theorem OAI.Contingency.nodeMass_min line 477
  47. theorem OAI.Contingency.node_adjacent_bound line 497
  48. theorem OAI.Contingency.node_variance_bound line 533