Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvrySeparatedCorrelation

Removing the actual outer coefficients before the IV.3 Gram expansion #

The first modulus coefficient, gamma and first beta depend only on the shared outer triple. Their exact L2 cost is outside the correlation sum. The remaining signed coefficient depends only on (n₂,s'), not on k₁. The small-root phase and all carrier restrictions are still retained.

source
def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCorrelationOuterWeight (K : WExtractedKey) (β c₁ γ : ℕ → ℝ) (o : ℕ × ℕ × ℕ) :
ℝ
Equations
Instances For
    Inspect dependencies

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

    source
    def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCorrelationInnerWeight (K : WExtractedKey) (β ζ : ℕ → ℝ) (t : WExtractedTuple × ℤ) :
    ℝ
    Equations
    Instances For
      Inspect dependencies

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

      source
      theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCorrelationInnerWeight_eq (K : WExtractedKey) (β ζ : ℕ → ℝ) {t u : WExtractedTuple × ℤ} (hn : (wGCDTuple (wExtractedOriginal t.1)).n₂ = (wGCDTuple (wExtractedOriginal u.1)).n₂) (hs : t.1.1.2.2 = u.1.1.2.2) :
      wCorrelationInnerWeight K β ζ t = wCorrelationInnerWeight K β ζ u

      Equality of the two inner arithmetic coordinates suffices. Neither the first modulus nor its coefficient is concealed in this weight.

      Inspect dependencies

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

      source
      theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedCoefficient_eq_outer_inner {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K) (β c₁ γ ζ : ℕ → ℝ) :
      wExtractedCoefficient β c₁ γ ζ t.1 = wCorrelationOuterWeight K β c₁ γ (wCorrelationOuter t) * wCorrelationInnerWeight K β ζ t
      Inspect dependencies

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

      source
      noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSeparatedCorrelationEnergy (x : ℝ) (N : Finset ℕ) (S : ℝ) (U : Finset (WExtractedTuple × ℤ)) (c : Finset (ℕ × ℕ)) (K : WExtractedKey) (β ζ : ℕ → ℝ) (a : ℤ) :
      ℝ
      Equations
      Instances For
        Inspect dependencies

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

        source
        noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCorrelationOuterMass (x : ℝ) (N : Finset ℕ) (S : ℝ) (U : Finset (WExtractedTuple × ℤ)) (c : Finset (ℕ × ℕ)) (K : WExtractedKey) (β c₁ γ : ℕ → ℝ) :
        ℝ
        Equations
        Instances For
          Inspect dependencies

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

          source
          theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSeparatedCorrelationEnergy_nonneg {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 (ℕ × ℕ)) (β ζ : ℕ → ℝ) :
          0 ≤ wSeparatedCorrelationEnergy x N S U c K β ζ a
          Inspect dependencies

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

          source
          theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber_separated_cauchy {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 (ℕ × ℕ)) (β c₁ γ ζ : ℕ → ℝ) :
          ‖∑ t ∈ wCoprimeFiber x N S U c, ↑(wExtractedCoefficient β c₁ γ ζ t.1) * wExtractedArithmeticPhase a t.2 t.1‖ ^ 2 ≤ wCorrelationOuterMass x N S U c K β c₁ γ * wSeparatedCorrelationEnergy x N S U c K β ζ a
          Inspect dependencies

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

          source
          theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePrefixMax_sq_le_separated_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 (ℕ × ℕ)) (j : Fin 5 → ℕ) (β c₁ γ ζ : ℕ → ℝ) :
          ∃ cap ∈ LiLiuPrereqFouvry.Rectangle.box (wAnalyticBoxLo j) (wAnalyticBoxHi j), wAnalyticBlockPrefixMax (wCoprimeFiber x N S U c) j β c₁ γ ζ a ^ 2 ≤ wCorrelationOuterMass x N S (wAnalyticPrefix U cap) c K β c₁ γ * wSeparatedCorrelationEnergy x N S (wAnalyticPrefix U cap) c K β ζ a

          The selected prefix of a cell is a real original tuple carrier, not an arbitrary family of weights inserted into an interval theorem.

          Inspect dependencies

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