MRTNearMaskSum.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Summing the phase-shaped near-center approximation over missing-band masks. The error is summed before integration; the centered typical prefix is retained, so its density contribution will be squared in energy.

lemma OAI.TwoPointCorrelations.mrt_typical_phase_mean_expansion line 16
lemma OAI.TwoPointCorrelations.mrt_typical_phase_error line 31

theorem OAI.TwoPointCorrelations.mrt_missing_near_prefix line 60

Source documentation

A missing-prime mask is allowed uniformly at each prefix, while the small-distance hypothesis stays at the single original cutoff 2*N.

theorem mrt_missing_near_prefix :
    ∀ᶠ N : ℕ in atTop, ∀ (F : ℕ → ℂ), F 1 = 1 → Multiplicative F → OneBounded F →
      ∀ Q : Finset ℕ, (∀ p ∈ Q, p.Prime) →
      (∀ p ∈ Q, (p : ℝ) ≤ Real.exp (Real.sqrt (Real.log N))) →
      ∀ t : ℝ, squaredDistance F (mrtArchimedeanTwist t) (2*N) ≤
        Real.log (Real.log (2*N : ℕ))/10 →
      ∀ u : ℝ, |u| ≤ (Real.log N)^(1/(16:ℝ)) →
      ∀ k ∈ Icc N (2*N),
      ‖halaszPhaseMean (halaszTwistedFunction (mrtMissingCoefficient F Q) t) u k -
        (halaszPowerPhase u k / (1 + (-u : ℂ)*Complex.I)) *
          halaszPhaseMean (halaszTwistedFunction (mrtMissingCoefficient F Q) t) 0 k‖ ≤
        (36*(halaszPrimePowerLogConstant+1)*Real.exp 8) *
…

Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.halaszPhaseMean, OAI.TwoPointCorrelations.halaszTwistedFunction, OAI.TwoPointCorrelations.mrtMissingCoefficient, OAI.TwoPointCorrelations.halaszPowerPhase, OAI.TwoPointCorrelations.halaszPrimePowerLogConstant

theorem OAI.TwoPointCorrelations.mrt_typical_near_renormalization line 112

Source documentation

Finite inclusion-exclusion preserves the centered typical prefix.

theorem mrt_typical_near_renormalization :
    ∀ᶠ N : ℕ in atTop, ∀ {ι : Type*} (J : Finset ι) (P : ι → Finset ℕ),
      (∀ j ∈ J, ∀ p ∈ P j, p.Prime) →
      (∀ j ∈ J, ∀ p ∈ P j, (p:ℝ) ≤ Real.exp (Real.sqrt (Real.log N))) →
      ∀ (F : ℕ → ℂ), F 1 = 1 → Multiplicative F → OneBounded F →
      ∀ t : ℝ, squaredDistance F (mrtArchimedeanTwist t) (2*N) ≤
        Real.log (Real.log (2*N : ℕ))/10 →
      ∀ u : ℝ, |u| ≤ (Real.log N)^(1/(16:ℝ)) →
      ∀ k ∈ Icc N (2*N),
      ‖halaszPhaseMean (halaszTwistedFunction (mrtTypicalCoefficient J P F) t) u k -
        (halaszPowerPhase u k / (1 + (-u : ℂ)*Complex.I)) *
          halaszPhaseMean (halaszTwistedFunction (mrtTypicalCoefficient J P F) t) 0 k‖ ≤
…

Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.halaszPhaseMean, OAI.TwoPointCorrelations.halaszTwistedFunction, OAI.TwoPointCorrelations.mrtTypicalCoefficient, OAI.TwoPointCorrelations.halaszPowerPhase