Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvryGramReindex

Occupied labels for the entire separated Gram energy #

A label retains the common (r,n₁) and both ordered triples (n₂,s,h). It forgets only the common k, which is summed inside its fiber. Labels are images of actual tuple-pairs, not an unrestricted rectangular box.

source
@[reducible, inline]
abbrev MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGramLabel :
Type
Equations
Instances For
    Inspect dependencies

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

    source
    def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramLabel (t u : WExtractedTuple × ℤ) :
    WGramLabel
    Equations
    Instances For
      Inspect dependencies

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

      source
      def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramPairs (V : Finset (WExtractedTuple × ℤ)) :
      Finset ((WExtractedTuple × ℤ) × WExtractedTuple × ℤ)
      Equations
      Instances For
        Inspect dependencies

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

        source
        def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramLabels (V : Finset (WExtractedTuple × ℤ)) :
        Finset WGramLabel
        Equations
        Instances For
          Inspect dependencies

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

          source
          noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramPrefix (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) :
          Finset (WExtractedTuple × ℤ)
          Equations
          Instances For
            Inspect dependencies

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

            source
            theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramPrefix_subset (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) :
            wGramPrefix N a x η R S M Z K b j cap positive ⊆ wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K
            Inspect dependencies

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

            source
            theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wGramPairs {A : Type u_1} [AddCommMonoid A] (V : Finset (WExtractedTuple × ℤ)) (F : WExtractedTuple × ℤ → WExtractedTuple × ℤ → A) :
            ∑ o ∈ Finset.image wCorrelationOuter V, ∑ t ∈ V with wCorrelationOuter t = o, ∑ u ∈ V with wCorrelationOuter u = o, F t u = ∑ p ∈ wGramPairs V, F p.1 p.2

            The initial Gram expansion still counts every ordered original pair.

            Inspect dependencies

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

            source
            theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wGramLabels {A : Type u_1} [AddCommMonoid A] (V : Finset (WExtractedTuple × ℤ)) (F : WExtractedTuple × ℤ → WExtractedTuple × ℤ → A) :
            ∑ p ∈ wGramPairs V, F p.1 p.2 = ∑ L ∈ wGramLabels V, ∑ t ∈ wKSectionSlice V L.1.1 L.1.2 L.2.1.1 L.2.1.2.1 L.2.1.2.2, ∑ u ∈ wKSectionSlice V L.1.1 L.1.2 L.2.2.1 L.2.2.2.1 L.2.2.2.2, if (wGCDTuple (wExtractedOriginal t.1)).k₁ = (wGCDTuple (wExtractedOriginal u.1)).k₁ then F t u else 0

            Fiberwise regrouping forgets no k multiplicity. Each label fiber is exactly the two original slices with their common-k test.

            Inspect dependencies

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

            source
            theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramLabels_eligible {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {V : Finset (WExtractedTuple × ℤ)} (hV : V ⊆ wExtractedKeyFiber H N Q a P R S ξ b K) {L : WGramLabel} (hL : L ∈ wGramLabels V) :
            wKSectionFixedCanonical K L.1.1 L.1.2 L.2.1.1 L.2.1.2.1 ∧ wKSectionFixedCanonical K L.1.1 L.1.2 L.2.2.1 L.2.2.2.1 ∧ 0 < K.2 ∧ 0 < wKSectionDeltaPrime K ∧ K.2 * wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2

            Both canonical sections and both Delta conditions are extracted from actual witnesses for an occupied label. Empty label sets need no witness.

            Inspect dependencies

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