OAI/Probability/ParisiFinite/YAdd.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Y Add.

  1. theorem OAI.CompactSeedControl.Y_add line 47
  2. theorem OAI.CompactSeedControl.Z_add line 53
  3. theorem OAI.CompactSeedControl.Y_zero line 59
  4. theorem OAI.CompactSeedControl.Z_zero line 65
  5. def OAI.CompactSeedControl.oddEval line 71
  6. theorem OAI.CompactSeedControl.oddEval_add line 75
  7. theorem OAI.CompactSeedControl.oddEval_monomial_even line 82
  8. theorem OAI.CompactSeedControl.oddEval_monomial_odd line 88
  9. theorem OAI.CompactSeedControl.odd_polynomial_mem line 96
  10. theorem OAI.CompactSeedControl.odd_continuous_mem line 112
  11. theorem OAI.CompactSeedControl.odd_continuous_pulse_approximation line 153
  12. def OAI.CompactSeedControl.axisX line 172
  13. def OAI.CompactSeedControl.axisY line 173
  14. def OAI.CompactSeedControl.axisZ line 174
  15. theorem OAI.CompactSeedControl.axisX_skew line 176
  16. theorem OAI.CompactSeedControl.axisY_skew line 179
  17. theorem OAI.CompactSeedControl.axisZ_skew line 182
  18. def OAI.CompactSeedControl.rawGenerator line 186
  19. theorem OAI.CompactSeedControl.rawGenerator_skew line 188
  20. theorem OAI.CompactSeedControl.rawGenerator_continuous line 193
  21. def OAI.CompactSeedControl.localWord line 199
  22. theorem OAI.CompactSeedControl.localWord_unitary line 202
  23. theorem OAI.CompactSeedControl.localWord_continuous line 205
  24. def OAI.CompactSeedControl.fieldEval line 217
  25. theorem OAI.CompactSeedControl.fieldEval_continuous line 225
  26. theorem OAI.CompactSeedControl.field_exp_apply line 229
  27. theorem OAI.CompactSeedControl.field_pulse_apply line 234
  28. theorem OAI.CompactSeedControl.even_localWord_compact line 253
  29. theorem OAI.CompactSeedControl.odd_localWord_compact line 269
  30. theorem OAI.CompactSeedControl.localWord_sequence line 305
  31. theorem OAI.CompactSeedControl.localWord_weighted_L2 line 322
  32. theorem OAI.CompactSeedControl.even_localWord_moment line 353
  33. theorem OAI.CompactSeedControl.odd_localWord_moment line 368
  34. theorem OAI.CompactSeedControl.continuous_sequence_ae line 408
  35. theorem OAI.CompactSeedControl.even_continuous_sequence_ae line 429
  36. theorem OAI.CompactSeedControl.odd_continuous_sequence_ae line 446
  37. theorem OAI.CompactSeedControl.localWord_diagonal line 475
  38. theorem OAI.CompactSeedControl.localWord_weighted_L2_ae line 493
  39. theorem OAI.CompactSeedControl.even_measurable_localWord line 525
  40. theorem OAI.CompactSeedControl.odd_measurable_localWord line 551
  41. def OAI.MaskSign.sign line 599
  42. theorem OAI.MaskSign.sign_sq line 602
  43. def OAI.MaskSign.flipEquiv line 605
  44. theorem OAI.MaskSign.sign_flip_same line 612
  45. theorem OAI.MaskSign.sign_flip_ne line 617
  46. theorem OAI.MaskSign.sum_character line 622
  47. theorem OAI.MaskSign.sum_two line 643
  48. theorem OAI.MaskSign.sum_flip_zero line 646
  49. theorem OAI.MaskSign.sum_four line 655