OAI/Combinatorics/BooleanFunctions/Rounding.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareRootDegree.FiniteRounding.productWeight line 16

    Source documentation

    Real-valued finite probabilities; used only to select a deterministic finite table.

    def productWeight {ι α : Type*} [Fintype ι] (p : ι → α → ℝ) (x : ι → α) : ℝ :=
…
  2. theorem OAI.SquareRootDegree.FiniteRounding.sum_productWeight line 19
  3. theorem OAI.SquareRootDegree.FiniteRounding.productWeight_nonneg line 27
  4. theorem OAI.SquareRootDegree.FiniteRounding.weighted_product line 31
  5. theorem OAI.SquareRootDegree.FiniteRounding.weighted_evaluation line 38
  6. def OAI.SquareRootDegree.FiniteRounding.bernoulliWeight line 45
  7. theorem OAI.SquareRootDegree.FiniteRounding.bernoulli_sum line 47
  8. theorem OAI.SquareRootDegree.FiniteRounding.bernoulli_nonneg line 50
  9. theorem OAI.SquareRootDegree.FiniteRounding.bernoulli_expect line 53
  10. def OAI.SquareRootDegree.FiniteRounding.leafWeight line 58

    Source documentation

    A distribution over entire leaf-test tables, not random bits added to the cube.

    def leafWeight {α : Type*} [Fintype α] (p : α → ℝ) (t : α → Bool) : ℝ :=
…
  11. theorem OAI.SquareRootDegree.FiniteRounding.leafWeight_sum line 61
  12. theorem OAI.SquareRootDegree.FiniteRounding.leafWeight_nonneg line 64
  13. theorem OAI.SquareRootDegree.FiniteRounding.leafWeight_eval line 68
  14. theorem OAI.SquareRootDegree.FiniteRounding.exists_ge_weighted_sum line 74
  15. def OAI.SquareRootDegree.TableRounding.tableWeight line 94
  16. def OAI.SquareRootDegree.TableRounding.bit line 97
  17. def OAI.SquareRootDegree.TableRounding.tableEvent line 99
  18. theorem OAI.SquareRootDegree.TableRounding.event_indicator line 103
  19. theorem OAI.SquareRootDegree.TableRounding.tableWeight_nonneg line 132
  20. theorem OAI.SquareRootDegree.TableRounding.tableWeight_sum line 137
  21. theorem OAI.SquareRootDegree.TableRounding.weighted_leaf_prod line 143
  22. theorem OAI.SquareRootDegree.TableRounding.weighted_indicator line 156
  23. theorem OAI.SquareRootDegree.TableRounding.weighted_deficit line 185
  24. theorem OAI.SquareRootDegree.TableRounding.exists_event_deficit line 196