OAI/NumberTheory/JointDickman/Analysis/MellinSieveRegularity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.mellinSieveFunction line 11
2. lemma OAI.JointDickman.mellin_power_phase line 14
3. lemma OAI.JointDickman.mellinSieveFunction_left line 23
4. lemma OAI.JointDickman.mellinSieveFunction_right line 32
5. lemma OAI.JointDickman.norm_mellin_exponent line 42
6. lemma OAI.JointDickman.mellinSieveFunction_left_sub line 47
7. lemma OAI.JointDickman.mellinSieveFunction_right_sub line 76
8. lemma OAI.JointDickman.norm_mellinSieveFunction line 111
9. lemma OAI.JointDickman.mellinSieveFunction_zero line 116
10. lemma OAI.JointDickman.norm_mellinSieveFunction_le line 119
11. lemma OAI.JointDickman.mellinSieveFunction_sub line 133

    Source documentation

    The cusp at the profile's maximum does not affect its global Lipschitz bound on the nonnegative half-line.

    lemma mellinSieveFunction_sub {N a b : ℝ} (hN : 0 < N)
        (ha : 0 ≤ a) (hb : 0 ≤ b) (t : ℝ) :
        ‖mellinSieveFunction N t b-mellinSieveFunction N t a‖ ≤
          ((3+|t|)/N)*|b-a| := by
    …

    Mentions: OAI.JointDickman.mellinSieveFunction

12. lemma OAI.JointDickman.mellinSieveFunction_continuousOn line 165