OAI/Computability/PerfectCompleteness/Foundations/QuarterBalanceLemmas.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.QuarterBalance.F2 line 21
  2. def OAI.PerfectCompleteness.QuarterBalance.sign line 23
  3. theorem OAI.PerfectCompleteness.QuarterBalance.scalar_cases line 25
  4. theorem OAI.PerfectCompleteness.QuarterBalance.sign_zero line 27
  5. theorem OAI.PerfectCompleteness.QuarterBalance.sign_one line 28
  6. theorem OAI.PerfectCompleteness.QuarterBalance.abs_sign line 29
  7. theorem OAI.PerfectCompleteness.QuarterBalance.sign_add line 31
  8. theorem OAI.PerfectCompleteness.QuarterBalance.sign_sum line 36
  9. theorem OAI.PerfectCompleteness.QuarterBalance.bit_probabilities line 45
  10. theorem OAI.PerfectCompleteness.QuarterBalance.expectation_sign line 55
  11. theorem OAI.PerfectCompleteness.QuarterBalance.bias_of_balanced_bits line 66
  12. def OAI.PerfectCompleteness.QuarterBalance.Balanced line 78
  13. theorem OAI.PerfectCompleteness.QuarterBalance.balanced_of_bias_le_half line 82
  14. theorem OAI.PerfectCompleteness.QuarterBalance.bilinear_bit_lower line 91
  15. theorem OAI.PerfectCompleteness.QuarterBalance.bilinear_bias line 138
  16. theorem OAI.PerfectCompleteness.SelectedSources.expectation_product_selected line 165
  17. theorem OAI.PerfectCompleteness.SelectedSources.pushforward_law_selected line 188
  18. theorem OAI.PerfectCompleteness.SelectedSources.selected_sources_conditioned line 216
  19. def OAI.PerfectCompleteness.SelectedSources.childObservation line 239
  20. theorem OAI.PerfectCompleteness.SelectedSources.clean_observation_event line 243
  21. theorem OAI.PerfectCompleteness.SelectedSources.clean_record_sources line 258
  22. theorem OAI.PerfectCompleteness.SourceCoordinateSplit.coordinate_split line 310
  23. theorem OAI.PerfectCompleteness.SourceCoordinateSplit.coordinate_split_pushforward line 330
  24. theorem OAI.PerfectCompleteness.SourceCoordinateSplit.iid_coordinate_split line 338
  25. abbrev OAI.PerfectCompleteness.FiniteProductSplit.Others line 362
  26. def OAI.PerfectCompleteness.FiniteProductSplit.others line 364
  27. def OAI.PerfectCompleteness.FiniteProductSplit.otherLaw line 366
  28. theorem OAI.PerfectCompleteness.FiniteProductSplit.split_law line 370
  29. theorem OAI.PerfectCompleteness.FiniteProductSplit.expectation_split line 375
  30. theorem OAI.PerfectCompleteness.FiniteProductSplit.expectation_background_first line 384
  31. theorem OAI.PerfectCompleteness.FiniteProductSplit.resampling_expectation line 391