OAI/Probability/SwitchChain/PairProjectionCell.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.PairResampling.restrictCell line 14
  2. theorem OAI.Problem315.PairResampling.restrictCell_apply line 17
  3. theorem OAI.Problem315.PairResampling.restrictCell_idempotent line 21
  4. theorem OAI.Problem315.PairResampling.restrictCell_sub line 26
  5. def OAI.Problem315.PairResampling.CellInvariant line 31
  6. theorem OAI.Problem315.PairResampling.expectation_restrictCell line 34
  7. theorem OAI.Problem315.PairResampling.fluctuation_restrictCell line 54
  8. theorem OAI.Problem315.PairResampling.restrictCell_eq_self_iff line 60
  9. theorem OAI.Problem315.PairResampling.expectation_preserves_cell_support line 72
  10. theorem OAI.Problem315.PairResampling.fluctuation_preserves_cell_support line 79
  11. theorem OAI.Problem315.PairResampling.restrictCell_inner line 86
  12. theorem OAI.Problem315.PairResampling.sum_restrictCell line 93
  13. theorem OAI.Problem315.PairResampling.inner_eq_sum_cell_inner line 100
  14. theorem OAI.Problem315.PairResampling.norm_sq_eq_sum_cell_norm_sq line 112
  15. theorem OAI.Problem315.PairResampling.fluctuation_interaction_eq_sum_cells line 117