OAI/NumberTheory/JointDickman/Analysis/CanonicalMellinEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.canonical_initialCost_nonneg line 9
2. theorem OAI.JointDickman.canonical_small_cost_sum_le line 14
3. theorem OAI.JointDickman.canonical_mellin_energy_bound line 61

   Source documentation

   This is the actual Dirichlet energy estimate away from the residual class: all selected-band costs have been summed, independently of their number. The no-small-band integral is retained verbatim.

   theorem canonical_mellin_energy_bound {P Q η : ℝ} {J N : ℕ} (hJ : 0 < J)
       (hPbig : 2*Real.exp 1 ≤ P) (hP : 2 ≤ Real.log P) (hPQ : P ≤ Q)
       (hη : 0 < η) (hη' : η ≤ 1/12)
       (hbudget : 8192*(Real.log (Real.log Q)+1) ≤ η*Real.log P)
       (hH : 2 ≤ mrtBaseResolution P Q η) (hN : 0 < N)
       (hupper : ∀ j ∈ range J, 2*mrtBandUpper Q (j+1) ≤ 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) (canonicalMellinBands P Q η).primes f) t‖^2) ≤
       (∫ t in S ∩ mrtNoSmallBand (canonicalMellinBands P Q η).bins
   …

   Mentions: OAI.JointDickman.angularMellinPolynomial, OAI.JointDickman.canonicalMellinBands