MRTNearPrefix.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Prefix density controls the centered typical amplitude before the near-frequency square is taken.

lemma OAI.TwoPointCorrelations.mrt_typical_prefix_count line 14
lemma OAI.TwoPointCorrelations.mrt_typical_prefix_difference line 46

theorem OAI.TwoPointCorrelations.mrt_typical_centered_prefix_density line 68

Source documentation

The phase-centered typical prefix differs from the full prefix by linear density, uniformly at all dyadic prefixes and all center phases.

theorem mrt_typical_centered_prefix_density : ∃ C : ℝ, 0<C ∧
    ∀ᶠ N : ℕ in atTop, ∀ P Q : ℝ, ∀ J : ℕ,
      2≤P → P≤Q → 1≤Real.log Q →
      (∀ j∈Icc 1 J, mrtBandUpper Q j ≤ Real.exp (Real.sqrt (Real.log N))) →
      ∀ F : ℕ → ℂ, OneBounded F → ∀ τ : ℝ, ∀ k∈Icc N (2*N),
      ‖halaszPhaseMean (halaszTwistedFunction (mrtTypicalCoefficient (Icc 1 J)
        (fun j => mrtPrimeBand (mrtBandLower P Q j) (mrtBandUpper Q j)) F) τ) 0 k -
        halaszPhaseMean (halaszTwistedFunction F τ) 0 k‖ ≤
        C*(Real.log P/Real.log Q)*k := by
…

Mentions: OAI.TwoPointCorrelations.mrtBandUpper, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.halaszPhaseMean, OAI.TwoPointCorrelations.halaszTwistedFunction, OAI.TwoPointCorrelations.mrtTypicalCoefficient, OAI.TwoPointCorrelations.mrtPrimeBand, OAI.TwoPointCorrelations.mrtBandLower