Documentation

MathlibNt.AnalyticNumberTheory.Vaughan.VaughanDirectAPNormalizedAssembly

AP-normalized direct Vaughan assembly #

This module is the direct L¹ route with the literal arithmetic-progression weight 1 / φ(q). The historical q / φ(q) unsquared mean remains available only as a compatibility majorant in VaughanDirectL1Physical.

source
noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIIMean (N Q u v : ℕ) :
ℝ

AP-normalized Type-II direct Vaughan mean.

Equations
Instances For
    source
    noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedVaughanSmallMean (N Q v : ℕ) :
    ℝ

    AP-normalized small-range direct Vaughan mean.

    Equations
    Instances For
      source
      theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMean_nonneg (a : ℤ → ℂ) (N Q : ℕ) :
      0 ≤ apNormalizedPrimitiveMean a N Q
      source
      theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMean_sq_le_harmonic_weightedSquare (a : ℤ → ℂ) (N Q : ℕ) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) :
      apNormalizedPrimitiveMean a N Q ^ 2 ≤ conductorHarmonicFactor Q * ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare a 0 N q χ

      Weighted Cauchy in the modulus variable. The reciprocal square roots produce the harmonic factor, while the second factor is exactly the usual q / φ(q) square-large-sieve ledger. Thus q / φ(q) appears only inside the proved square estimate, never as the direct unsquared mean.

      source
      theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMean_vaughan_le (N Q u v : ℕ) :
      apNormalizedPrimitiveMean vonMangoldtIntegerCoeff N Q ≤ 2 * (apNormalizedVaughanTypeIMean N Q u v + apNormalizedVaughanTypeIIMean N Q u v + apNormalizedVaughanSmallMean N Q v)

      Vaughan's exact three-piece identity assembled directly in the AP-normalized primitive L¹ mean.

      source
      theorem AnalyticNumberTheory.LargeSieve.direct_conductor_sum_le_apNormalizedPrimitive (a : ℤ → ℂ) (N Q : ℕ) :
      ∑ d ∈ Finset.Icc 2 Q, directConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, primitivePrefixAmplitude a N d ψ ≤ conductorHarmonicFactor Q ^ 2 * apNormalizedPrimitiveMean a N Q

      Strong conductor transport. The exact reciprocal-totient conductor bound lands on the AP-normalized primitive mean, with no q / φ(q) inflation.

      source
      theorem AnalyticNumberTheory.LargeSieve.directAllCharacterMean_le_apNormalizedPrimitive (a : ℤ → ℂ) (N Q : ℕ) :
      directAllCharacterMean a N Q ≤ 2 * conductorHarmonicFactor Q ^ 2 * apNormalizedPrimitiveMean a N Q + 2 * directConductorCorrectionMean a N Q

      All nonprincipal characters transported to the AP-normalized primitive mean. The change-of-level correction remains explicit.

      source
      def AnalyticNumberTheory.LargeSieve.vaughanTypeIShortScale (u v : ℕ) :
      ℕ

      Largest short-variable scale occurring in the two Type-I lanes.

      Equations
      Instances For
        source
        def AnalyticNumberTheory.LargeSieve.VaughanDirectAPNormalizedTypeIInput (N Q u v : ℕ) (K logPay : ℝ) :
        Prop

        AP-normalized Type-I physical-scale input, retaining the exact Q*sqrt(N*D) dependence of the shell square ledger.

        Equations
        Instances For
          source
          def AnalyticNumberTheory.LargeSieve.VaughanDirectAPNormalizedTypeIIInput (N Q u v : ℕ) (K logPay : ℝ) :
          Prop

          AP-normalized Type-II physical-scale input.

          Equations
          Instances For
            source
            theorem AnalyticNumberTheory.LargeSieve.direct_L1_vaughan_apNormalized_physical_assembly (E : ℕ → ℝ) (N Q u v : ℕ) (K logPay : ℝ) (hK : 0 ≤ K) (hlogPay : 0 ≤ logPay) (hE : ∀ q ∈ Finset.Icc 1 Q, E q ≤ (↑q.totient)⁻¹ * ∑ χ ∈ nonprincipalCharacters q, nonprincipalPrefixAmplitude vonMangoldtIntegerCoeff N q χ) (hI : VaughanDirectAPNormalizedTypeIInput N Q u v K logPay) (hII : VaughanDirectAPNormalizedTypeIIInput N Q u v K logPay) :
            ∑ q ∈ Finset.Icc 1 Q, E q ≤ 4 * conductorHarmonicFactor Q ^ 2 * (2 * vaughanDirectPhysicalMajorant N Q u K logPay + apNormalizedVaughanSmallMean N Q v) + 2 * directConductorCorrectionMean vonMangoldtIntegerCoeff N Q

            Physical direct assembly through the AP-normalized primitive mean. In particular, conductor transport never invokes the compatibility q / φ(q) unsquared mean.