OAI/Probability/SwitchChain/FiniteKernelTV.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.Analytic.zeroSumSpace line 14
  2. theorem OAI.Problem315.Analytic.mem_zeroSumSpace line 29
  3. lemma OAI.Problem315.Analytic.euclidean_inner_eq_sum line 32
  4. lemma OAI.Problem315.Analytic.euclidean_norm_sq_eq_sum line 36
  5. lemma OAI.Problem315.Analytic.matrix_preserves_zeroSum line 43
  6. theorem OAI.Problem315.Analytic.matrix_centered_norm_decay line 52
  7. lemma OAI.Problem315.Analytic.sum_abs_le_sqrt_card_mul_norm line 95
  8. def OAI.Problem315.Analytic.centeredPoint line 102
  9. lemma OAI.Problem315.Analytic.centeredPoint_sum line 105
  10. lemma OAI.Problem315.Analytic.centeredPoint_norm_sq line 110
  11. lemma OAI.Problem315.Analytic.centeredPoint_norm_le_one line 123
  12. lemma OAI.Problem315.Analytic.matrix_pow_row_sum line 128
  13. lemma OAI.Problem315.Analytic.matrix_iterate_centeredPoint line 139
  14. theorem OAI.Problem315.Analytic.matrix_tv_bound_of_gap line 151