OAI/Probability/SwitchChain/PairEqualityProjectionFacts.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem315.PairEquality.expectation_centered line 14
  2. theorem OAI.Problem315.PairEquality.expectation_eq_zero_of_mem_equalitySpace line 18
  3. theorem OAI.Problem315.PairEquality.equalitySpace_le_orthogonal line 44
  4. theorem OAI.Problem315.PairEquality.projection_isSymmetric line 50
  5. theorem OAI.Problem315.PairEquality.projection_idempotent line 54
  6. theorem OAI.Problem315.PairEquality.projection_eq_zero_of_mem_fiberSpace line 59
  7. theorem OAI.Problem315.PairEquality.projection_constant line 68
  8. theorem OAI.Problem315.PairEquality.projection_expectation line 72
  9. theorem OAI.Problem315.PairEquality.expectation_projection line 76
  10. theorem OAI.Problem315.PairEquality.projection_fluctuation line 81
  11. theorem OAI.Problem315.PairEquality.fluctuation_projection line 85
  12. theorem OAI.Problem315.PairEquality.gated_rowExtreme_fluctuation_mem line 89
  13. theorem OAI.Problem315.PairEquality.projection_fixes_gated_rowExtreme_fluctuation line 106
  14. theorem OAI.Problem315.PairEquality.gated_affine_rowExtreme_fluctuation_mem line 115
  15. theorem OAI.Problem315.PairEquality.multiply_mem_equalitySpace line 137
  16. theorem OAI.Problem315.PairEquality.multiply_inner line 146
  17. theorem OAI.Problem315.PairEquality.multiply_mem_equalitySpace_orthogonal line 154
  18. theorem OAI.Problem315.PairEquality.projection_multiply line 164
  19. theorem OAI.Problem315.PairEquality.projection_restrict_fiberUnion line 186