OAI/Combinatorics/BooleanFunctions/Conditioning.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite conditioning, without measure-theoretic assumptions

  1. theorem OAI.SquareRootDegree.average_prod line 13
  2. def OAI.SquareRootDegree.updateSwap line 19
  3. theorem OAI.SquareRootDegree.average_update line 32
  4. def OAI.SquareRootDegree.cell line 40
  5. def OAI.SquareRootDegree.cellMass line 44
  6. def OAI.SquareRootDegree.cellMoment line 47
  7. def OAI.SquareRootDegree.conditionalValue line 50
  8. def OAI.SquareRootDegree.conditionalAverage line 53
  9. theorem OAI.SquareRootDegree.cellMoment_eq_zero_of_mass_eq_zero line 56
  10. theorem OAI.SquareRootDegree.mass_mul_conditionalValue line 68
  11. theorem OAI.SquareRootDegree.average_mul_comp_eq_sum line 75
  12. theorem OAI.SquareRootDegree.cellMoment_conditionalAverage line 84
  13. theorem OAI.SquareRootDegree.conditionalAverage_projection line 97
  14. theorem OAI.SquareRootDegree.average_conditionalAverage line 104
  15. theorem OAI.SquareRootDegree.conditionalAverage_sq line 108
  16. theorem OAI.SquareRootDegree.conditionalAverage_lower_bound line 115