Documentation

MathlibNt.AnalyticNumberTheory.Vaughan.VaughanTypeIActualDyadic

Actual dyadic partition for the AP-normalized Vaughan Type-I mean #

source
def AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstDyadicShell (u k : ℕ) :
Finset ℕ

Dyadic first-lane shell: positive d ≤ u with log₂ d = k.

Equations
Instances For
    source
    def AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleProductDyadicShell (u v k : ℕ) :
    Finset (ℕ × ℕ)

    Dyadic product shell in the middle lane. It partitions by the actual short product d*e, rather than by an ambient rectangle.

    Equations
    Instances For
      source
      @[simp]
      theorem AnalyticNumberTheory.LargeSieve.mem_vaughanTypeIFirstDyadicShell {u k d : ℕ} :
      d ∈ vaughanTypeIFirstDyadicShell u k ↔ 0 < d ∧ d ≤ u ∧ d.log2 = k
      source
      @[simp]
      theorem AnalyticNumberTheory.LargeSieve.mem_vaughanTypeIMiddleProductDyadicShell {u v k d e : ℕ} :
      (d, e) ∈ vaughanTypeIMiddleProductDyadicShell u v k ↔ 0 < d ∧ d ≤ u ∧ 0 < e ∧ e ≤ v ∧ (d * e).log2 = k
      source
      theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstDyadicShell_bounds {u k d : ℕ} (hd : d ∈ vaughanTypeIFirstDyadicShell u k) :
      2 ^ k ≤ d ∧ d < 2 ^ (k + 1)

      A first shell really is contained in [2^k,2^(k+1)).

      source
      theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleProductDyadicShell_bounds {u v k d e : ℕ} (hde : (d, e) ∈ vaughanTypeIMiddleProductDyadicShell u v k) :
      2 ^ k ≤ d * e ∧ d * e < 2 ^ (k + 1)

      A middle shell has the corresponding bounds on the actual product.

      source
      theorem AnalyticNumberTheory.LargeSieve.mem_own_vaughanTypeIFirstDyadicShell {u d : ℕ} (hd : 0 < d) (hdu : d ≤ u) :
      d ∈ vaughanTypeIFirstDyadicShell u d.log2

      Every positive d ≤ u occurs in its actual dyadic shell.

      source
      theorem AnalyticNumberTheory.LargeSieve.mem_own_vaughanTypeIMiddleProductDyadicShell {u v d e : ℕ} (hd : 0 < d) (hdu : d ≤ u) (he : 0 < e) (hev : e ≤ v) :
      (d, e) ∈ vaughanTypeIMiddleProductDyadicShell u v (d * e).log2

      Every positive pair in the Vaughan rectangle occurs in its product shell.

      source
      theorem AnalyticNumberTheory.LargeSieve.firstDyadicShell_index_lt {u k d : ℕ} (hd : d ∈ vaughanTypeIFirstDyadicShell u k) :
      k < u.log2 + 1

      The shell index of a nonempty first shell lies in the advertised range.

      source
      theorem AnalyticNumberTheory.LargeSieve.middleProductDyadicShell_index_lt {u v k d e : ℕ} (hde : (d, e) ∈ vaughanTypeIMiddleProductDyadicShell u v k) :
      k < (u * v).log2 + 1

      The shell index of a nonempty product shell lies in the advertised range.

      source
      noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIMiddleProductShellMean (S : Finset (ℕ × ℕ)) (N Q : ℕ) :
      ℝ

      Literal AP-normalized mean of one middle product shell.

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

        The exact physical payment attached to a first shell. This deliberately spells out the two literal ledgers; no global length-N moment is substituted.

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

          The analogous honest product-shell payment.

          Equations
          Instances For
            source
            theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIFirstDyadicShell_physical (u k N Q : ℕ) (hN : 0 < N) (hQ : 0 < Q) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) :
            apNormalizedVaughanTypeIFirstShellMean (vaughanTypeIFirstDyadicShell u k) N Q ≤ vaughanTypeIFirstDyadicLogPay u k N Q * (↑N + ↑Q * √(↑N * ↑(2 ^ k)))

            Every first shell meets the existing physical lemma with its literal energy and variable-length budget.

            source
            theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIMiddleProductDyadicShell_physical (u v k N Q : ℕ) (hN : 0 < N) (hQ : 0 < Q) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) :
            apNormalizedVaughanTypeIMiddleProductShellMean (vaughanTypeIMiddleProductDyadicShell u v k) N Q ≤ vaughanTypeIMiddleProductDyadicLogPay u v k N Q * (↑N + ↑Q * √(↑N * ↑(2 ^ k)))

            Every middle product shell meets the same physical lemma.

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

            Explicit common payment used by the finite shell assembler.

            Equations
            Instances For
              source
              theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstDyadicLogPay_nonneg (u k N Q : ℕ) :
              0 ≤ vaughanTypeIFirstDyadicLogPay u k N Q
              source
              theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleProductDyadicLogPay_nonneg (u v k N Q : ℕ) :
              0 ≤ vaughanTypeIMiddleProductDyadicLogPay u v k N Q
              source
              theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIActualDyadicLogPay_nonneg (N Q u v : ℕ) :
              0 ≤ vaughanTypeIActualDyadicLogPay N Q u v