OAI/Probability/SwitchChain/TripleActualRowBound.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem315.TripleActualRowBound.row_variance_transport line 18
  2. theorem OAI.Problem315.TripleActualRowBound.full_matrix_row_variance_transport line 30
  3. def OAI.Problem315.TripleActualRowBound.finiteCellEquiv line 45
  4. theorem OAI.Problem315.TripleActualRowBound.finiteCell_row_iff line 57
  5. theorem OAI.Problem315.TripleActualRowBound.cell_row_variance line 65
  6. def OAI.Problem315.TripleActualRowBound.exteriorCellEquiv line 76
  7. theorem OAI.Problem315.TripleActualRowBound.exterior_row_variance line 81
  8. theorem OAI.Problem315.TripleActualRowBound.sum_expectation_exterior line 94
  9. theorem OAI.Problem315.TripleActualRowBound.exterior_projection_norm_centered line 112
  10. theorem OAI.Problem315.TripleActualRowBound.triple_square line 138