OAI/NumberTheory/JointDickman/Analysis/MultiscaleMellinEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual multiscale prime partition in the Mellin convention

The costs below are the proved Ramaré extraction and amplified cofactor costs. The integral over the class with no small prime polynomial remains explicit; no estimate for that exceptional class is assumed here.

  1. structure OAI.JointDickman.MellinPrimeBands line 18
  2. def OAI.JointDickman.MellinPrimeBands.polynomial line 28
  3. structure OAI.JointDickman.MellinPrimeBands.Valid line 33
  4. def OAI.JointDickman.MellinPrimeBands.extractionCost line 45
  5. def OAI.JointDickman.MellinPrimeBands.initialCost line 50
  6. def OAI.JointDickman.MellinPrimeBands.laterCost line 54
  7. lemma OAI.JointDickman.MellinPrimeBands.angular_eq_dyadic line 63
  8. lemma OAI.JointDickman.MellinPrimeBands.polynomial_continuous line 66
  9. theorem OAI.JointDickman.MellinPrimeBands.firstSmallBand_energy_le line 69
  10. theorem OAI.JointDickman.MellinPrimeBands.laterSmallBand_energy_le line 85
  11. theorem OAI.JointDickman.MellinPrimeBands.partition_energy_le line 119

    Source documentation

    Every nonexceptional class is bounded by its actual small-prime or amplified cofactor estimate. Only the no-small-band integral is left.

    theorem partition_energy_le (D : MellinPrimeBands) {J N : ℕ}
    (hD : D.Valid J N) (hN : 0 < N)
    (f : ℕ → ℂ) (hf : Multiplicative f) (hb : OneBounded f)
    {T : ℝ} (hT : 0 < T) {S : Set ℝ} (hSm : MeasurableSet S)
    (hS : S ⊆ Set.Ioc (-T) T) :
    (∫ t in S, ‖angularMellinPolynomial (Ioc N (2*N))
      (mrtTypicalCoefficient (range J) D.primes f) t‖^2) ≤
    (∫ t in S ∩ mrtNoSmallBand D.bins (D.polynomial f) D.threshold J,
      ‖angularMellinPolynomial (Ioc N (2*N))
        (mrtTypicalCoefficient (range J) D.primes f) t‖^2) +
    ∑ j ∈ range J, (D.extractionCost j N T +
      if j = 0 then D.initialCost N T else D.laterCost j N T) := by
…

    Mentions: OAI.JointDickman.MellinPrimeBands, OAI.JointDickman.angularMellinPolynomial