Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG12ClippedMass

source
noncomputable def G12ClippedWindow.mass (N : ℕ) (g L U : ℕ → ℝ) :
ℝ

The common mass has no modulus argument.

Equations
Instances For
    Inspect dependencies

    G12ClippedWindow.mass · compiled type and proof/definition references.

    source
    noncomputable def G12ClippedWindow.gateLoss (N : ℕ) (g L U : ℕ → ℝ) (d : ℕ) :
    ℝ
    Equations
    Instances For
      Inspect dependencies

      G12ClippedWindow.gateLoss · compiled type and proof/definition references.

      source
      noncomputable def G12ClippedWindow.divisorResidual (N : ℕ) (g L U : ℕ → ℝ) (d : ℕ) :
      ℝ
      Equations
      Instances For
        Inspect dependencies

        G12ClippedWindow.divisorResidual · compiled type and proof/definition references.

        source
        noncomputable def G12ClippedWindow.commonResidual (N : ℕ) (g L U : ℕ → ℝ) (d : ℕ) :
        ℝ

        Actual full-support divisor count, centered at one modulus-independent mass.

        Equations
        Instances For
          Inspect dependencies

          G12ClippedWindow.commonResidual · compiled type and proof/definition references.

          source
          theorem G12ClippedWindow.mass_nonneg {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) :
          0 ≤ mass N g L U
          Inspect dependencies

          G12ClippedWindow.mass_nonneg · compiled type and proof/definition references.

          source
          theorem G12ClippedWindow.gateLoss_nonneg {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) (d : ℕ) :
          0 ≤ gateLoss N g L U d
          Inspect dependencies

          G12ClippedWindow.gateLoss_nonneg · compiled type and proof/definition references.

          source
          theorem G12ClippedWindow.gateLoss_le {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) (d : ℕ) :
          gateLoss N g L U d ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowGateLoss N ε d

          Both the coefficient and the literal window are dominated by the old gate.

          Inspect dependencies

          G12ClippedWindow.gateLoss_le · compiled type and proof/definition references.

          source
          theorem G12ClippedWindow.mass_eq_gated_add (N d : ℕ) (g L U : ℕ → ℝ) :
          mass N g L U = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N with m.Coprime d, g m * ↑(window N L U m).card + ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N with ¬m.Coprime d, g m * ↑(window N L U m).card
          Inspect dependencies

          G12ClippedWindow.mass_eq_gated_add · compiled type and proof/definition references.

          source
          theorem G12ClippedWindow.apWindow_eq_output_dvd {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) (d : ℕ) {m : ℕ} (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) :
          {r ∈ window N L U m | m * r ≡ N [MOD d]} = {r ∈ window N L U m | d ∣ N - r * m}
          Inspect dependencies

          G12ClippedWindow.apWindow_eq_output_dvd · compiled type and proof/definition references.

          source
          theorem G12ClippedWindow.outputDivisors_empty {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) {m d : ℕ} (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) (hNd : N.Coprime d) (hmd : ¬m.Coprime d) :
          {r ∈ window N L U m | d ∣ N - r * m} = ∅
          Inspect dependencies

          G12ClippedWindow.outputDivisors_empty · compiled type and proof/definition references.

          source
          theorem G12ClippedWindow.divisorResidual_eq {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (hN : 2 ≤ N) (h : Admissible N ε g L U) (d : ℕ) (hNd : N.Coprime d) :
          divisorResidual N g L U d = residual N g L U d N
          Inspect dependencies

          G12ClippedWindow.divisorResidual_eq · compiled type and proof/definition references.

          source
          theorem G12ClippedWindow.commonResidual_eq {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (hN : 2 ≤ N) (h : Admissible N ε g L U) (d : ℕ) :
          commonResidual N g L U d = divisorResidual N g L U d - gateLoss N g L U d
          Inspect dependencies

          G12ClippedWindow.commonResidual_eq · compiled type and proof/definition references.

          source
          theorem G12ClippedWindow.commonResidual_sum_le {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (hN : 2 ≤ N) (h : Admissible N ε g L U) (Q : ℕ) :
          ∑ d ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedModuli N Q, |commonResidual N g L U d| ≤ ∑ d ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedModuli N Q, |residual N g L U d N| + ∑ d ∈ Finset.Icc 1 Q, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeWindowGateLoss N ε d
          Inspect dependencies

          G12ClippedWindow.commonResidual_sum_le · compiled type and proof/definition references.

          source
          theorem G12ClippedWindow.commonResidual_log_saving (A : ℝ) (hA : 0 < A) :
          ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (g L U : ℕ → ℝ) (ε : ℝ) (Q : ℕ), Admissible N ε g L U → ↑Q ≤ √↑N / Real.log ↑N ^ B → ∑ d ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedModuli N Q, |commonResidual N g L U d| ≤ C * ↑N / Real.log ↑N ^ A

          The cutoff precedes every coefficient, endpoint, epsilon and modulus cutoff.

          Inspect dependencies

          G12ClippedWindow.commonResidual_log_saving · compiled type and proof/definition references.