Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvryExtractedPhase

The actual extracted exponential kernel in source phase coordinates #

Fouvry (1987), pp. 627--628, (3.11)--(3.13). The negative Fourier phase is -u*h/lcm; a occurs in the CRT phase, not a second time in this Fourier phase. All arithmetic coefficients and carrier restrictions remain outside the smooth weight.

source
noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wReciprocalPhase (v : WGCDData) (a : ℤ) :
UnitAddCircle
Equations
Instances For
    Inspect dependencies

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

    source
    noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticWeight (D D' : ℕ) (a : ℤ) (u h k n r s : ℝ) :
    ℂ

    The reciprocal amplitude and both genuinely smooth phases.

    Equations
    Instances For
      Inspect dependencies

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

      source
      theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fourier_real_eq_fourierChar (h : ℤ) (v : ℝ) :
      (fourier h) ↑v = ↑(Real.fourierChar (↑h * v))
      Inspect dependencies

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

      source
      theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponential_eq_analyticWeight {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) (hc : WCompatible q r N₁ N₂) (a h : ℤ) (u : ℝ) :
      wFourierExponential a q r N₁ N₂ h u = wAnalyticWeight v.D v.D' a u (↑h) (↑v.k₁) (↑v.n₁) (↑v.k₂) 1 * (fourier h) (wSmallRootPhase v.d v.d₁ v.δ v.δ₁ v.δ₂ v.k₁ v.k₂ v.n₁ v.n₂ a) * (fourier h) (wReciprocalPhase v a)

      Pointwise transport uses the already constructed three-phase identity. No coprimality or residue phase is replaced by a bound.

      Inspect dependencies

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

      source
      theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal_valid {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {z : WExtractedTuple} (hz : z ∈ wFactorExtractionTuples N Q a P R S ξ) :
      (wGCDTuple (wExtractedOriginal z)).Valid (wExtractedOriginal z).1.1 (wExtractedOriginal z).1.2 (wExtractedOriginal z).2.1 (wExtractedOriginal z).2.2 ∧ WCompatible (wExtractedOriginal z).1.1 (wExtractedOriginal z).1.2 (wExtractedOriginal z).2.1 (wExtractedOriginal z).2.2

      The arithmetic and positivity facts are derived from actual membership.

      Inspect dependencies

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

      source
      theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtracted_k₂_eq {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {z : WExtractedTuple} (hz : z ∈ wFactorExtractionTuples N Q a P R S ξ) :
      (wGCDTuple (wExtractedOriginal z)).k₂ = z.1.2.1 * z.1.2.2

      The second free canonical modulus is exactly r'*s', not merely a divisor or a factorization supplied by a caller.

      Inspect dependencies

      MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtracted_k₂_eq · compiled type and proof/definition references.

      source
      noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedArithmeticPhase (a h : ℤ) (z : WExtractedTuple) :
      ℂ
      Equations
      Instances For
        Inspect dependencies

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

        source
        theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.norm_wExtractedArithmeticPhase (a h : ℤ) (z : WExtractedTuple) :
        ‖wExtractedArithmeticPhase a h z‖ = 1
        Inspect dependencies

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

        source
        theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyExponential_eq_analyticWeight {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) (H : ℕ → ℕ → ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) (u : ℝ) :
        wExtractedKeyExponential H N Q β c₁ γ ζ a P R S ξ b K u = ∑ t ∈ wExtractedKeyFiber H N Q a P R S ξ b K, have v := wGCDTuple (wExtractedOriginal t.1); ↑(wExtractedCoefficient β c₁ γ ζ t.1) * wExtractedArithmeticPhase a t.2 t.1 * wAnalyticWeight v.D v.D' a u ↑t.2 ↑v.k₁ ↑v.n₁ ↑t.1.1.2.1 ↑t.1.1.2.2

        The fixed-key sum now has only a five-variable analytic weight. The original cutoff, low-omega tests, compatibility, and signed coefficients are still exactly those of wExtractedKeyFiber.

        Inspect dependencies

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

        source
        theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyExponential_zero_or_witness (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) (u : ℝ) :
        wExtractedKeyExponential H N Q β c₁ γ ζ a P R S ξ b K u = 0 ∨ ∃ t ∈ wExtractedKeyFiber H N Q a P R S ξ b K, wExtractedCoefficient β c₁ γ ζ t.1 ≠ 0

        A selected value may be zero. Only the other branch provides an actual member and hence positive canonical parameters.

        Inspect dependencies

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