OAI/Analysis/Littlewood/BinaryPacket.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.integral_circle_fourier line 18
  2. def OAI.AsymptoticallyMinimalLittlewood.Auxiliary.cosine line 23
  3. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.cosine_continuous line 25
  4. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.cosine_abs_le line 27
  5. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.cosine_cast line 30
  6. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.integral_cosine line 35
  7. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.integral_cosine_sq line 43
  8. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.integral_pi_cons line 69
  9. def OAI.AsymptoticallyMinimalLittlewood.Auxiliary.binary line 88
  10. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.binary_continuous line 92
  11. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.binary_abs_le line 100
  12. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.binary_cons line 116
  13. def OAI.AsymptoticallyMinimalLittlewood.Auxiliary.energy line 120
  14. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.energy_bounds line 122
  15. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.integrable_cont line 131
  16. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.integral_pi_cons_rev line 136
  17. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.integral_cosine_linear line 144
  18. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.integral_cosine_square line 150
  19. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.binary_mean_zero line 159
  20. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.energy_succ line 167
  21. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.energy_increment line 177
  22. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.energy_monotone line 191
  23. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.exists_binary_energy line 196
  24. def OAI.AsymptoticallyMinimalLittlewood.Auxiliary.primitive line 223
  25. def OAI.AsymptoticallyMinimalLittlewood.Auxiliary.spectrumSpan line 227
  26. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.spectrumSpan_mono line 231
  27. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.character_mem line 237
  28. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.character_cons line 241
  29. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.spectrumSpan_lift line 245
  30. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.allSpectrum_mul line 267
  31. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.allSpectrum_one line 286
  32. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.binary_spectrum line 290
  33. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.primitive_ne_zero line 313
  34. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.primitive_neg line 324
  35. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.primitive_parallel_scalar line 333
  36. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.exists_binary_coefficients line 368
  37. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.integral_character line 379
  38. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.coeff_finite_sum line 391
  39. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.coeff_real_neg line 411
  40. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.parseval_continuous line 420
  41. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.binary_coefficients_energy line 429
  42. def OAI.AsymptoticallyMinimalLittlewood.Auxiliary.positive line 449
  43. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.positive_primitive line 453
  44. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.positive_not_neg line 462
  45. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.primitive_positive_or_neg line 474
  46. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.positive_parallel_eq line 486
  47. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.binary_coefficients_conj line 498
  48. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.binary_support_neg line 506
  49. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.coefficient_support_pairs line 511