Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvryActualCorrelation

IV.3 correlation on the actual extracted carrier #

Fouvry (1987), p. 632, (4.7)--(4.8). Lemma 7 supplies the cross coprimalities; the original tuple conditions supply all other inverses. The two terms share k₁, r', and n₁. The small-root factors are retained, and no interval estimate is applied to an arbitrary masked sum.

source
def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wActualCorrelationModulus (t u : WExtractedTuple × ℤ) :
ℕ

The common modulus has only one copy of the shared n₁.

Equations
Instances For
    Inspect dependencies

    MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wActualCorrelationModulus · compiled type and proof/definition references.

    source
    def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wActualCorrelationNumerator (K : WExtractedKey) (a : ℤ) (t u : WExtractedTuple × ℤ) :
    ℤ
    Equations
    Instances For
      Inspect dependencies

      MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wActualCorrelationNumerator · compiled type and proof/definition references.

      source
      noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wActualReciprocalCorrelation (K : WExtractedKey) (a : ℤ) (t u : WExtractedTuple × ℤ) :
      ℂ
      Equations
      Instances For
        Inspect dependencies

        MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wActualReciprocalCorrelation · compiled type and proof/definition references.

        source
        noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wActualSmallRootFactor (a : ℤ) (t : WExtractedTuple × ℤ) :
        ℂ

        Kept as a factor on each original tuple, with no residue-freezing claim.

        Equations
        Instances For
          Inspect dependencies

          MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wActualSmallRootFactor · compiled type and proof/definition references.

          source
          theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.norm_wActualReciprocalCorrelation (K : WExtractedKey) (a : ℤ) (t u : WExtractedTuple × ℤ) :
          ‖wActualReciprocalCorrelation K a t u‖ = 1
          Inspect dependencies

          MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.norm_wActualReciprocalCorrelation · compiled type and proof/definition references.

          source
          theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.norm_wActualSmallRootFactor (a : ℤ) (t : WExtractedTuple × ℤ) :
          ‖wActualSmallRootFactor a t‖ = 1
          Inspect dependencies

          MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.norm_wActualSmallRootFactor · compiled type and proof/definition references.

          source
          theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber_common_inverse_coprime {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {b : ℕ} {K : WExtractedKey} {U : Finset (WExtractedTuple × ℤ)} (hU : U ⊆ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) {c : Finset (ℕ × ℕ)} {t u : WExtractedTuple × ℤ} (ht : t ∈ wCoprimeFiber x N S U c) (hu : u ∈ wCoprimeFiber x N S U c) (hk : (wGCDTuple (wExtractedOriginal t.1)).k₁ = (wGCDTuple (wExtractedOriginal u.1)).k₁) (hr : t.1.1.2.1 = u.1.1.2.1) (hn : (wGCDTuple (wExtractedOriginal t.1)).n₁ = (wGCDTuple (wExtractedOriginal u.1)).n₁) :
          (K.D' * (wGCDTuple (wExtractedOriginal t.1)).n₂ * (wGCDTuple (wExtractedOriginal u.1)).n₂ * (wGCDTuple (wExtractedOriginal t.1)).k₁).Coprime ((wGCDTuple (wExtractedOriginal t.1)).n₁ * t.1.1.2.1 * t.1.1.2.2 * u.1.1.2.2)

          The common inverse in IV.3 is a consequence of actual membership, not an extra coprimality premise. The two s' need not be coprime.

          Inspect dependencies

          MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber_common_inverse_coprime · compiled type and proof/definition references.

          source
          theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber_reciprocal_correlation {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {b : ℕ} {K : WExtractedKey} {U : Finset (WExtractedTuple × ℤ)} (hU : U ⊆ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) {c : Finset (ℕ × ℕ)} {t u : WExtractedTuple × ℤ} (ht : t ∈ wCoprimeFiber x N S U c) (hu : u ∈ wCoprimeFiber x N S U c) (hk : (wGCDTuple (wExtractedOriginal t.1)).k₁ = (wGCDTuple (wExtractedOriginal u.1)).k₁) (hr : t.1.1.2.1 = u.1.1.2.1) (hn : (wGCDTuple (wExtractedOriginal t.1)).n₁ = (wGCDTuple (wExtractedOriginal u.1)).n₁) :
          (fourier t.2) (wReciprocalPhase (wGCDTuple (wExtractedOriginal t.1)) a) * star ((fourier u.2) (wReciprocalPhase (wGCDTuple (wExtractedOriginal u.1)) a)) = wActualReciprocalCorrelation K a t u

          Exact IV.3 phase transport, with both D' and d₁ frozen by the key and all positivity and common-inverse conditions derived from membership.

          Inspect dependencies

          MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber_reciprocal_correlation · compiled type and proof/definition references.

          source
          theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber_arithmetic_correlation {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {b : ℕ} {K : WExtractedKey} {U : Finset (WExtractedTuple × ℤ)} (hU : U ⊆ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) {c : Finset (ℕ × ℕ)} {t u : WExtractedTuple × ℤ} (ht : t ∈ wCoprimeFiber x N S U c) (hu : u ∈ wCoprimeFiber x N S U c) (hk : (wGCDTuple (wExtractedOriginal t.1)).k₁ = (wGCDTuple (wExtractedOriginal u.1)).k₁) (hr : t.1.1.2.1 = u.1.1.2.1) (hn : (wGCDTuple (wExtractedOriginal t.1)).n₁ = (wGCDTuple (wExtractedOriginal u.1)).n₁) :
          wExtractedArithmeticPhase a t.2 t.1 * star (wExtractedArithmeticPhase a u.2 u.1) = wActualSmallRootFactor a t * star (wActualSmallRootFactor a u) * wActualReciprocalCorrelation K a t u

          The complete arithmetic product retains the possibly varying small-root product. Arbitrary signs of a, h, and h' are allowed.

          Inspect dependencies

          MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber_arithmetic_correlation · compiled type and proof/definition references.

          source
          theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber_arithmetic_correlation_zero {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {b : ℕ} {K : WExtractedKey} {U : Finset (WExtractedTuple × ℤ)} (hU : U ⊆ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) {c : Finset (ℕ × ℕ)} {t u : WExtractedTuple × ℤ} (ht : t ∈ wCoprimeFiber x N S U c) (hu : u ∈ wCoprimeFiber x N S U c) (hk : (wGCDTuple (wExtractedOriginal t.1)).k₁ = (wGCDTuple (wExtractedOriginal u.1)).k₁) (hr : t.1.1.2.1 = u.1.1.2.1) (hn : (wGCDTuple (wExtractedOriginal t.1)).n₁ = (wGCDTuple (wExtractedOriginal u.1)).n₁) (hl : wActualCorrelationNumerator K a t u = 0) :
          wExtractedArithmeticPhase a t.2 t.1 * star (wExtractedArithmeticPhase a u.2 u.1) = wActualSmallRootFactor a t * star (wActualSmallRootFactor a u)

          Zero numerator kills the reciprocal factor, not the small-root product.

          Inspect dependencies

          MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber_arithmetic_correlation_zero · compiled type and proof/definition references.

          source
          def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCorrelationOuter (t : WExtractedTuple × ℤ) :
          ℕ × ℕ × ℕ

          These are precisely the coordinates shared in an IV.3 Cauchy pair.

          Equations
          Instances For
            Inspect dependencies

            MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCorrelationOuter · compiled type and proof/definition references.

            source
            noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCorrelationOuterFiber (x : ℝ) (N : Finset ℕ) (S : ℝ) (U : Finset (WExtractedTuple × ℤ)) (c : Finset (ℕ × ℕ)) (o : ℕ × ℕ × ℕ) :
            Finset (WExtractedTuple × ℤ)
            Equations
            Instances For
              Inspect dependencies

              MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCorrelationOuterFiber · compiled type and proof/definition references.

              source
              theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wCorrelationOuterFibers {A : Type u_1} [AddCommMonoid A] (x : ℝ) (N : Finset ℕ) (S : ℝ) (U : Finset (WExtractedTuple × ℤ)) (c : Finset (ℕ × ℕ)) (F : WExtractedTuple × ℤ → A) :
              ∑ t ∈ wCoprimeFiber x N S U c, F t = ∑ o ∈ Finset.image wCorrelationOuter (wCoprimeFiber x N S U c), ∑ t ∈ wCorrelationOuterFiber x N S U c o, F t

              Only the outer labels are imaged; the inner sum still runs over original tuples. Repeated arithmetic coordinates keep their multiplicity.

              Inspect dependencies

              MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wCorrelationOuterFibers · compiled type and proof/definition references.

              source
              theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCorrelationOuterFiber_gram {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {b : ℕ} {K : WExtractedKey} {U : Finset (WExtractedTuple × ℤ)} (hU : U ⊆ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) (c : Finset (ℕ × ℕ)) (o : ℕ × ℕ × ℕ) (A : WExtractedTuple × ℤ → ℂ) :
              ↑(‖∑ t ∈ wCorrelationOuterFiber x N S U c o, A t * wExtractedArithmeticPhase a t.2 t.1‖ ^ 2) = ∑ t ∈ wCorrelationOuterFiber x N S U c o, ∑ u ∈ wCorrelationOuterFiber x N S U c o, A t * star (A u) * (wActualSmallRootFactor a t * star (wActualSmallRootFactor a u)) * wActualReciprocalCorrelation K a t u

              Exact finite Gram expansion on one actual outer-coordinate fiber. A may contain arbitrary complex weights and additional masks. No small-root phase has been discarded, and no positivity of A is used.

              Inspect dependencies

              MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCorrelationOuterFiber_gram · compiled type and proof/definition references.

              source
              theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber_cauchy_correlation {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {b : ℕ} {K : WExtractedKey} {U : Finset (WExtractedTuple × ℤ)} (hU : U ⊆ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) (c : Finset (ℕ × ℕ)) (A : WExtractedTuple × ℤ → ℂ) :
              ‖∑ t ∈ wCoprimeFiber x N S U c, A t * wExtractedArithmeticPhase a t.2 t.1‖ ^ 2 ≤ ↑(Finset.image wCorrelationOuter (wCoprimeFiber x N S U c)).card * ∑ o ∈ Finset.image wCorrelationOuter (wCoprimeFiber x N S U c), (∑ t ∈ wCorrelationOuterFiber x N S U c o, ∑ u ∈ wCorrelationOuterFiber x N S U c o, A t * star (A u) * (wActualSmallRootFactor a t * star (wActualSmallRootFactor a u)) * wActualReciprocalCorrelation K a t u).re

              The finite Cauchy step followed by the exact IV.3 Gram expansion. The outer cost counts occupied triples, not original tuple multiplicities. The right side is an exact nonnegative Gram quantity; its summands need not be nonnegative, and no unweighted interval bound is asserted.

              Inspect dependencies

              MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber_cauchy_correlation · compiled type and proof/definition references.