OAI/NumberTheory/JointDickman/Probability/GeometricSquareKernel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The squared geometric kernel in the smoothed bilinear estimate

  1. def OAI.JointDickman.geometricSquareKernel line 10
  2. lemma OAI.JointDickman.additivePhase_nat_mul line 13
  3. lemma OAI.JointDickman.geometricSquareKernel_nonneg line 20
  4. lemma OAI.JointDickman.geometricSquareKernel_neg line 23
  5. lemma OAI.JointDickman.geometricSquareKernel_zero line 34
  6. lemma OAI.JointDickman.geometricSquareKernel_le line 38
  7. lemma OAI.JointDickman.geometricSquareKernel_decay line 45
  8. lemma OAI.JointDickman.geometricSquareKernel_le_div line 56
  9. lemma OAI.JointDickman.geometricSquareKernel_int_Ico line 61