OAI/Probability/BinarySweep/Mixing/BinaryContraction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.averageOperator_sum line 16
  2. lemma OAI.BinaryCoordinateSweeps.pushLaw_complex_expectation line 22
  3. lemma OAI.BinaryCoordinateSweeps.gridAverage_relabel line 30
  4. theorem OAI.BinaryCoordinateSweeps.binary_contraction line 44
  5. lemma OAI.BinaryCoordinateSweeps.complexAverage_transport line 64
  6. lemma OAI.BinaryCoordinateSweeps.hilbert_norm_of_coordinates line 77
  7. theorem OAI.BinaryCoordinateSweeps.binary_hilbert_contraction line 89
  8. lemma OAI.BinaryCoordinateSweeps.evenMoment_one_norm_bound line 108
  9. lemma OAI.BinaryCoordinateSweeps.complexAverage_uniform_zero line 127
  10. lemma OAI.BinaryCoordinateSweeps.Young.swap_tabloid_eq line 144
  11. lemma OAI.BinaryCoordinateSweeps.Young.swap_poly_coefficient line 176
  12. theorem OAI.BinaryCoordinateSweeps.Young.singleton_column_dimension line 192