OAI/Combinatorics/BooleanFunctions/FiniteCLT.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareRootDegree.FiniteCLT.normalizedSum line 17

    Source documentation

    The normalized sum uses an actual finite product space at every index.

    def normalizedSum (T : α → ℝ) (n : ℕ) (x : Fin n → α) : ℝ :=
…
  2. theorem OAI.SquareRootDegree.FiniteCLT.measurable_normalizedSum line 20
  3. theorem OAI.SquareRootDegree.FiniteCLT.finite_product_clt line 25
  4. def OAI.SquareRootDegree.UniformFinite.uniformMeasure line 78
  5. instance OAI.SquareRootDegree.UniformFinite.uniformMeasure_probability line 81
  6. theorem OAI.SquareRootDegree.UniformFinite.uniform_singleton line 84
  7. theorem OAI.SquareRootDegree.UniformFinite.integral_uniform line 87
  8. theorem OAI.SquareRootDegree.UniformFinite.uniform_pi line 92
  9. theorem OAI.SquareRootDegree.UniformFinite.average_pi_eval_any line 100
  10. theorem OAI.SquareRootDegree.UniformFinite.centered_sq_any line 107
  11. theorem OAI.SquareRootDegree.UniformFinite.average_normalizedSum line 119
  12. theorem OAI.SquareRootDegree.UniformFinite.average_normalizedSum_sq line 126
  13. theorem OAI.SquareRootDegree.UniformFinite.uniform_clt line 135