OAI/Analysis/RotationWeights/CoordinateLaws.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CircleCoupling.roundedWidth line 70
  2. def OAI.CircleCoupling.roundedTag line 71
  3. def OAI.CircleCoupling.crossingProbability line 72
  4. lemma OAI.CircleCoupling.width_rounding line 74
  5. lemma OAI.CircleCoupling.tag_rounding line 96
  6. lemma OAI.CircleCoupling.crossingProbability_nonneg line 114
  7. lemma OAI.CircleCoupling.crossingProbability_sq line 117
  8. lemma OAI.CircleCoupling.crossingProbability_div_le line 122
  9. lemma OAI.CircleCoupling.crossingProbability_le_kappa line 133
  10. lemma OAI.CircleCoupling.six_probabilities_le_one line 139
  11. structure OAI.CircleCoupling.CoordinateParameters line 154
  12. instance OAI.CircleCoupling.CoordinateParameters.(instance at line 168) line 168
  13. lemma OAI.CircleCoupling.CoordinateParameters.m_pos line 169
  14. lemma OAI.CircleCoupling.CoordinateParameters.a_pos line 170
  15. lemma OAI.CircleCoupling.CoordinateParameters.b_pos line 171
  16. lemma OAI.CircleCoupling.CoordinateParameters.width_a line 172
  17. lemma OAI.CircleCoupling.CoordinateParameters.width_b line 174
  18. lemma OAI.CircleCoupling.CoordinateParameters.tag_bounds line 176
  19. def OAI.CircleCoupling.CoordinateParameters.ρ line 178
  20. def OAI.CircleCoupling.CoordinateParameters.σ line 179
  21. def OAI.CircleCoupling.CoordinateParameters.τ line 180
  22. lemma OAI.CircleCoupling.CoordinateParameters.ρ_nonneg line 181
  23. lemma OAI.CircleCoupling.CoordinateParameters.σ_nonneg line 182
  24. lemma OAI.CircleCoupling.CoordinateParameters.τ_nonneg line 183
  25. lemma OAI.CircleCoupling.CoordinateParameters.τ_le line 184
  26. lemma OAI.CircleCoupling.CoordinateParameters.ρ_le_one line 185
  27. lemma OAI.CircleCoupling.CoordinateParameters.σ_le_one line 186
  28. lemma OAI.CircleCoupling.CoordinateParameters.probabilities line 187
  29. abbrev OAI.CircleCoupling.CoordinateParameters.Sample line 191
  30. def OAI.CircleCoupling.CoordinateParameters.law line 192
  31. instance OAI.CircleCoupling.CoordinateParameters.(instance at line 196) line 196
  32. lemma OAI.CircleCoupling.CoordinateParameters.rounded_width_a_half line 199
  33. lemma OAI.CircleCoupling.CoordinateParameters.rounded_width_b_half line 204
  34. lemma OAI.CircleCoupling.CoordinateParameters.rounded_tag_half line 209
  35. lemma OAI.CircleCoupling.CoordinateParameters.law_second_moment line 213
  36. lemma OAI.CircleCoupling.CoordinateParameters.law_density_ten line 222
  37. lemma OAI.CircleCoupling.ae_labelled line 230
  38. lemma OAI.CircleCoupling.ae_mixture line 236
  39. def OAI.CircleCoupling.supportCondition line 245
  40. lemma OAI.CircleCoupling.sixLaw_support line 254
  41. lemma OAI.CircleCoupling.CoordinateParameters.law_support line 267
  42. lemma OAI.CircleCoupling.CoordinateParameters.law_order line 271
  43. lemma OAI.CircleCoupling.CoordinateParameters.top_a_failure line 284
  44. lemma OAI.CircleCoupling.CoordinateParameters.bottom_a_failure line 290
  45. lemma OAI.CircleCoupling.CoordinateParameters.top_b_failure line 296
  46. lemma OAI.CircleCoupling.CoordinateParameters.bottom_b_failure line 302