OAI/Combinatorics/UniformKServer/PositiveSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Removing zero atoms of a finite nonnegative law does not change any weighted observable or conditional law on its support. This justifies the positive-law presentation, without an assertion on impossible histories.

  1. abbrev OAI.UniformKServer.PositiveSupport.Support line 18
  2. theorem OAI.UniformKServer.PositiveSupport.sum_support line 20
  3. theorem OAI.UniformKServer.PositiveSupport.weighted_sum line 28
  4. theorem OAI.UniformKServer.PositiveSupport.total line 35
  5. def OAI.UniformKServer.PositiveSupport.filtration line 40
  6. theorem OAI.UniformKServer.PositiveSupport.mass_eq line 42
  7. theorem OAI.UniformKServer.PositiveSupport.kernel_eq line 50
  8. theorem OAI.UniformKServer.PositiveSupport.posterior_eq line 56