Documentation

MathlibNt.AnalyticNumberTheory.Vaughan.VaughanDirectTypeIPhysicalScale

Direct Vaughan Type-I: the AP-normalized physical scale #

The unsquared mean arising from character orthogonality has weight 1 / φ(q). This module keeps that weight through row Cauchy and only then invokes the existing variable-length primitive maximal large sieve. It also records why putting the square-large-sieve weight q / φ(q) on the unsquared mean inserts an extra factor q before any analytic estimate is used.

source
noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMean (a : ℤ → ℂ) (N Q : ℕ) :
ℝ

The primitive unsquared mean with the weight produced by AP character orthogonality. This is deliberately distinct from the square-large-sieve weight q / φ(q).

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

    The corrected direct Type-I mean. The Vaughan input itself is not frozen: this is the literal producer quantity.

    Equations
    Instances For
      source
      theorem AnalyticNumberTheory.LargeSieve.directPrimitiveMean_summand_eq_q_mul (a : ℤ → ℂ) (N q : ℕ) (_hq : 0 < q) :
      ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitivePrefixAmplitude a N q χ = ↑q * ((↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, primitivePrefixAmplitude a N q χ)

      The old unsquared weight is exactly q times the AP-normalized summand.

      source
      theorem AnalyticNumberTheory.LargeSieve.directPrimitiveMean_summand_strictly_inflates (a : ℤ → ℂ) (N q : ℕ) (hq : 1 < q) (hA : 0 < ∑ χ : PrimitiveCharacter q, primitivePrefixAmplitude a N q χ) :
      (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, primitivePrefixAmplitude a N q χ < ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitivePrefixAmplitude a N q χ

      Strict one-level scale counterexample: as soon as the primitive amplitude mass is positive and q>1, replacing 1/φ(q) by q/φ(q) strictly enlarges that level. Thus q/φ(q) cannot be called the direct AP-normalized L¹ mean; it is the square-large-sieve weight.

      source
      noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedVariableLengthRowMean {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (c : ι → ℤ → ℂ) (L : ι → ℕ) (Q : ℕ) :
      ℝ

      Rowwise AP-normalized L¹ majorant. For Vaughan's first lane, S is a d-shell; for the middle lane it is a (d,e) shell.

      Equations
      Instances For
        source
        theorem AnalyticNumberTheory.LargeSieve.apNormalizedVariableLengthRowMean_sq_le {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (c : ι → ℤ → ℂ) (L : ι → ℕ) (Q : ℕ) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) :
        apNormalizedVariableLengthRowMean S c L Q ^ 2 ≤ ↑(Finset.Icc 1 Q).card * ↑S.card * ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ∑ r ∈ S, primitiveCharacterPrefixMaxSquare (c r) 0 (L r) q χ

        Cauchy with the correct normalization. The exact number of rows and moduli is visible; no analytic hypothesis is hidden here.

        source
        theorem AnalyticNumberTheory.LargeSieve.apNormalized_variableLength_square_le_budget {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (c : ι → ℤ → ℂ) (L : ι → ℕ) (Q : ℕ) (hQ : 0 < Q) :
        ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ∑ r ∈ S, primitiveCharacterPrefixMaxSquare (c r) 0 (L r) q χ ≤ variableLengthPrimitivePrefixBudget S c L Q

        The AP-normalized square ledger is bounded by the existing variable-length large sieve. This is the precise point where the proved LS theorem is called.

        source
        theorem AnalyticNumberTheory.LargeSieve.apNormalizedVariableLengthRowMean_sq_le_budget {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (c : ι → ℤ → ℂ) (L : ι → ℕ) (Q : ℕ) (hQ : 0 < Q) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) :
        apNormalizedVariableLengthRowMean S c L Q ^ 2 ≤ ↑(Finset.Icc 1 Q).card * ↑S.card * variableLengthPrimitivePrefixBudget S c L Q

        Combined corrected-weight Cauchy + variable-length LS producer.

        source
        theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleShortEnergy_explicitLambda (DS ES : Finset ℕ) :
        vaughanTypeIMiddleShortEnergy DS ES ≤ ↑DS.card * ∑ e ∈ ES, ‖↑(ArithmeticFunction.vonMangoldt e)‖ ^ 2

        The middle μ*Λ lane retains the literal Λ square energy; it is not silently replaced by a row count.

        source
        theorem AnalyticNumberTheory.LargeSieve.corrected_typeI_shell_physical_of_square (shellMean logPay N Q : ℝ) (hmean : 0 ≤ shellMean) (hlog : 0 ≤ logPay) (hN : 0 ≤ N) (_hQ : 0 ≤ Q) (hsq : shellMean ^ 2 ≤ (logPay * (N + Q ^ 2 * √N)) ^ 2) :
        shellMean ≤ logPay * (N + Q ^ 2 * √N)

        Scalar shell optimization. If a corrected-weight shell has a square bound P², then it has the physical unsquared bound P; choosing P = logPay * (N + Q² sqrt N) is the exact producer shape.