OAI/NumberTheory/CubicMoment/Estimates/LogDenominatorWeights.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform weights for the literal factor Λ(a)/log(Na).

  1. def OAI.CubicFirstMoment.logWeightParameters line 13
  2. lemma OAI.CubicFirstMoment.logWeightParameters_compact line 15
  3. def OAI.CubicFirstMoment.logDenominatorWeight_uniform line 18
  4. def OAI.CubicFirstMoment.coordinateLogDenominatorWeights line 28
  5. lemma OAI.CubicFirstMoment.logWeightParameters_mem line 42
  6. lemma OAI.CubicFirstMoment.logDenominatorWeight_scale line 57

    Source documentation

    On the support range the smooth extension is precisely the factor log(Y)/log(Xx), with no approximation.

    lemma logDenominatorWeight_scale {c Y X x : ℝ} (hc : 0 < c)
    (hY0 : 0 < Y) (hY : 1 ≤ Real.log Y) (hlo : Y^c ≤ X) (hhi : X ≤ Y) (hx : 1 ≤ x)
    (w : ℝ → ℂ) :
    logDenominatorWeight c w (Real.log X/Real.log Y,1/Real.log Y) x =
      (Real.log Y:ℂ)*w x/(Real.log (X*x):ℂ) := by
…

    Mentions: OAI.CubicFirstMoment.logDenominatorWeight