OAI/Probability/SwitchChain/WeightedConditionalVariance.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.WeightedConditional.conditionalSum line 13
  2. theorem OAI.Problem315.WeightedConditional.sum_mul_conditionalSum line 18
  3. theorem OAI.Problem315.WeightedConditional.sum_conditionalSum line 34
  4. theorem OAI.Problem315.WeightedConditional.conditionalSum_add line 40
  5. theorem OAI.Problem315.WeightedConditional.conditionalSum_smul line 53
  6. abbrev OAI.Problem315.WeightedConditional.Space line 65
  7. def OAI.Problem315.WeightedConditional.decode line 68
  8. def OAI.Problem315.WeightedConditional.rowSum line 71
  9. def OAI.Problem315.WeightedConditional.gram line 74
  10. theorem OAI.Problem315.WeightedConditional.gram_apply line 98
  11. theorem OAI.Problem315.WeightedConditional.inner_gram line 103
  12. theorem OAI.Problem315.WeightedConditional.gram_symmetric line 127
  13. theorem OAI.Problem315.WeightedConditional.gram_nonneg line 135
  14. def OAI.Problem315.WeightedConditional.centered line 143
  15. theorem OAI.Problem315.WeightedConditional.mem_centered line 158
  16. theorem OAI.Problem315.WeightedConditional.marginal_mul_decode line 164
  17. theorem OAI.Problem315.WeightedConditional.weighted_rowSum line 177
  18. theorem OAI.Problem315.WeightedConditional.gram_preserves_centered line 196
  19. theorem OAI.Problem315.WeightedConditional.conditional_eigen_equation line 217
  20. def OAI.Problem315.WeightedConditional.encode line 236
  21. theorem OAI.Problem315.WeightedConditional.decode_encode line 240
  22. theorem OAI.Problem315.WeightedConditional.encode_mem_centered line 248
  23. theorem OAI.Problem315.WeightedConditional.norm_encode_sq line 260
  24. theorem OAI.Problem315.WeightedConditional.centered_variance_le_of_eigenvalue_bound line 272