OAI/NumberTheory/CubicMoment/Estimates/SmoothLogDenominator.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Smooth, globally defined extensions of the logarithmic denominator weights. The extension equals the literal reciprocal on the application range, so no pole can interfere with parameter-uniform differentiation.

  1. def OAI.CubicFirstMoment.positiveSmoothExtension line 14
  2. lemma OAI.CubicFirstMoment.positiveSmoothExtension_eq line 18
  3. lemma OAI.CubicFirstMoment.positiveSmoothExtension_pos line 25
  4. lemma OAI.CubicFirstMoment.positiveSmoothExtension_smooth line 42
  5. def OAI.CubicFirstMoment.smoothReciprocal line 47
  6. lemma OAI.CubicFirstMoment.smoothReciprocal_smooth line 49
  7. lemma OAI.CubicFirstMoment.smoothReciprocal_eq line 53
  8. def OAI.CubicFirstMoment.smoothLog line 57
  9. lemma OAI.CubicFirstMoment.smoothLog_smooth line 59
  10. lemma OAI.CubicFirstMoment.smoothLog_eq line 63
  11. def OAI.CubicFirstMoment.logDenominatorWeight line 68

    Source documentation

    Parameters are the normalized scale logarithm and inverse logarithm of the outer length. Both range over a compact rectangle.

    def logDenominatorWeight (c : ℝ) (w : ℝ → ℂ) (p : ℝ × ℝ) (x : ℝ) : ℂ :=
…
  12. lemma OAI.CubicFirstMoment.logDenominatorWeight_joint_smooth line 71
  13. lemma OAI.CubicFirstMoment.logDenominatorWeight_eq line 84