OAI/NumberTheory/DirichletL/Fourier/FrequencyTwists.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.JointLogSeparation.logPhase_temperate line 80
  2. def OAI.JointLogSeparation.frequencyTwist line 85
  3. lemma OAI.JointLogSeparation.frequencyTwist_apply line 88
  4. lemma OAI.JointLogSeparation.logPhase_add_frequency line 92
  5. lemma OAI.JointLogSeparation.frequencyTwist_twice line 100
  6. lemma OAI.JointLogSeparation.frequencyTwist_norm line 106
  7. lemma OAI.JointLogSeparation.frequencyTwist_tsupport line 109
  8. def OAI.JointLogSeparation.phaseDerivative line 120
  9. lemma OAI.JointLogSeparation.logPhase_hasDerivAt line 122
  10. lemma OAI.JointLogSeparation.logPhase_iteratedDeriv line 134
  11. lemma OAI.JointLogSeparation.phaseDerivative_norm line 147
  12. lemma OAI.JointLogSeparation.logPhase_iteratedFDeriv_norm line 151
  13. def OAI.JointLogSeparation.derivativeSeminormSum line 156
  14. lemma OAI.JointLogSeparation.derivativeSeminormSum_nonneg line 159
  15. lemma OAI.JointLogSeparation.seminorm_le_derivativeSeminormSum line 162
  16. theorem OAI.JointLogSeparation.frequencyTwist_seminorm_bound line 169
  17. theorem OAI.JointLogSeparation.frequencyTwist_seminorm_polynomial line 209
  18. def OAI.JointLogSeparation.twistSourceBound line 222
  19. lemma OAI.JointLogSeparation.twistSourceBound_nonneg line 227
  20. theorem OAI.JointLogSeparation.profileSourceBound_frequencyTwist line 233
  21. lemma OAI.JointLogSeparation.fourierPointBound_mono line 252
  22. lemma OAI.JointLogSeparation.fourierPointBound_mul line 257
  23. theorem OAI.JointLogSeparation.twisted_profile_fourier_envelope line 262
  24. lemma OAI.JointLogSeparation.integrable_phase_schwartz line 284
  25. theorem OAI.JointLogSeparation.finite_triple_phase_integral line 291
  26. def OAI.SecondPassArithmetic.postCommonSmoothPair line 332
  27. def OAI.SecondPassArithmetic.fixedSecondTest line 343
  28. theorem OAI.SecondPassArithmetic.postCommonSmoothPair_fixed_tests line 347
  29. def OAI.SecondPassArithmetic.separatedPostCommon line 457
  30. theorem OAI.SecondPassArithmetic.postCommonSmoothPair_uniform_fixed_tests line 468
  31. theorem OAI.SecondPassArithmetic.labeled_child_second_energy_pushforward line 506
  32. theorem OAI.SecondPassArithmetic.support_child_label_span line 539
  33. lemma OAI.SecondPassArithmetic.rayMonoid_norm_le_one line 552
  34. lemma OAI.SecondPassArithmetic.secondRayMinus_norm_le line 555
  35. lemma OAI.SecondPassArithmetic.secondRayPlus_norm_le line 563
  36. theorem OAI.SecondPassArithmetic.secondPreColumn_norm_le line 577
  37. theorem OAI.SecondPassArithmetic.secondCommonWeight_norm_le line 591
  38. theorem OAI.SecondPassArithmetic.secondTotalWeight_norm_le line 607
  39. theorem OAI.SecondPassArithmetic.secondRayCoefficient_mass line 626