OAI/Analysis/RotationWeights/CouplingMoments.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CircleCoupling.sum_sq_le_card_mul line 68
  2. lemma OAI.CircleCoupling.centered_density_squares line 72
  3. lemma OAI.CircleCoupling.mixture_density_squares line 92
  4. lemma OAI.CircleCoupling.probability_sum_singleton_real line 127
  5. lemma OAI.CircleCoupling.uniform_l2_set_bound line 132
  6. lemma OAI.CircleCoupling.pi_second_moment line 163
  7. lemma OAI.CircleCoupling.pi_uniform_singleton_real line 174
  8. lemma OAI.CircleCoupling.mixture_endpoint_second_moment line 184
  9. def OAI.CircleCoupling.digitEndpoint line 228
  10. lemma OAI.CircleCoupling.digitEndpoint_measurable line 229
  11. lemma OAI.CircleCoupling.diagonal_endpoint_real line 235
  12. lemma OAI.CircleCoupling.rectangle_endpoint_density_bound line 243
  13. lemma OAI.CircleCoupling.sixComponents_density_bound line 255
  14. lemma OAI.CircleCoupling.sixLaw_second_moment line 287
  15. lemma OAI.CircleCoupling.fiber_failure_bound line 328
  16. lemma OAI.CircleCoupling.fiber_failure_of_density_bounds line 341
  17. lemma OAI.CircleCoupling.fiber_failure_tenth line 351
  18. lemma OAI.CircleCoupling.sixLaw_density_ten line 362
  19. lemma OAI.CircleCoupling.sixLaw_top_t_failure line 392
  20. lemma OAI.CircleCoupling.sixLaw_bottom_t_failure line 413
  21. lemma OAI.CircleCoupling.sixLaw_top_u_failure line 434
  22. lemma OAI.CircleCoupling.sixLaw_bottom_u_failure line 455