OAI/Probability/SwitchChain/TripleCellVarianceGluing.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.CellVarianceGluing.restrict line 13
  2. theorem OAI.Problem315.CellVarianceGluing.restrict_apply line 20
  3. theorem OAI.Problem315.CellVarianceGluing.norm_sq_eq_sum_restrict line 27
  4. theorem OAI.Problem315.CellVarianceGluing.norm_sum_sq_le_of_cells line 33
  5. def OAI.Problem315.CellVarianceGluing.cellSpace line 49
  6. def OAI.Problem315.CellVarianceGluing.center line 61
  7. theorem OAI.Problem315.CellVarianceGluing.center_mem line 65
  8. theorem OAI.Problem315.CellVarianceGluing.sum_restrict_sub_center_eq_zero line 71
  9. theorem OAI.Problem315.CellVarianceGluing.centered_row_variance_of_cells line 95
  10. theorem OAI.Problem315.PairResampling.expectation_center_of_key_invariant line 116
  11. theorem OAI.Problem315.PairResampling.vertex_triple_square_of_cellwise_row_variance line 125
  12. def OAI.Problem315.PairResampling.tripleExteriorKey line 155
  13. theorem OAI.Problem315.PairResampling.tripleExteriorKey_eq_of_sameFiber line 159
  14. theorem OAI.Problem315.PairResampling.expectation_tripleExterior_center line 166
  15. theorem OAI.Problem315.PairResampling.vertex_triple_square_of_exterior_cellwise_row_variance line 173