OAI/Probability/SwitchChain/VariableBlockVariance.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.VariableBlockVariance.sizes line 16
  2. abbrev OAI.Problem315.VariableBlockVariance.Fiber line 19
  3. abbrev OAI.Problem315.VariableBlockVariance.Family line 22
  4. theorem OAI.Problem315.VariableBlockVariance.sum_sizes line 27
  5. theorem OAI.Problem315.VariableBlockVariance.fiber_nonempty line 31
  6. theorem OAI.Problem315.VariableBlockVariance.pairSizeWeight_eq line 41
  7. theorem OAI.Problem315.VariableBlockVariance.family_average line 53
  8. def OAI.Problem315.VariableBlockVariance.rowFunction line 70
  9. def OAI.Problem315.VariableBlockVariance.rowMean line 75
  10. theorem OAI.Problem315.VariableBlockVariance.average_rowFunction line 80
  11. theorem OAI.Problem315.VariableBlockVariance.marginal_expectation line 88
  12. theorem OAI.Problem315.VariableBlockVariance.centered_row_average_sq line 100
  13. theorem OAI.Problem315.VariableBlockVariance.row_variance_bound line 131