MathlibNt.SieveTheory.LiLiuGoldbachG12OutsideBudget

source

noncomputable def G12OutsideBudget.fibre (N : ℕ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) (n : ℕ) :

ℝ

The actual normalized output fibre, restricted to any submother.

Equations

G12OutsideBudget.fibre N A n = ∑ x ∈ A with MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutput N x = n, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N x.fst

Instances For

Inspect dependencies

G12OutsideBudget.fibre · compiled type and proof/definition references.

source

theorem G12OutsideBudget.fibre_le_twenty {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) (hA : A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) (n : ℕ) :

fibre N A n ≤ 20

Inspect dependencies

G12OutsideBudget.fibre_le_twenty · compiled type and proof/definition references.

source

theorem G12OutsideBudget.output_mem {N : ℕ} {ε : ℝ} {x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom} (hx : x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) :

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutput N x ∈ Finset.Icc 1 N

All genuine outputs are positive and at most N.

Inspect dependencies

G12OutsideBudget.output_mem · compiled type and proof/definition references.

source

theorem G12OutsideBudget.test_le {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) (hA : A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) (B : Finset ℕ) :

∑ x ∈ A with MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutput N x ∈ B, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N x.fst ≤ 20 * ↑B.card

Finite tests are paid after output pushforward, never tuplewise.

Inspect dependencies

G12OutsideBudget.test_le · compiled type and proof/definition references.

source

noncomputable def G12OutsideBudget.mass (N : ℕ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) :

ℝ

Equations

G12OutsideBudget.mass N A = ∑ x ∈ A, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N x.fst

Instances For

Inspect dependencies

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

source

noncomputable def G12OutsideBudget.divisibility (N : ℕ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) (d : ℕ) :

ℝ

Equations

G12OutsideBudget.divisibility N A d = ∑ x ∈ A, if d ∣ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutput N x then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N x.fst else 0

Instances For

Inspect dependencies

G12OutsideBudget.divisibility · compiled type and proof/definition references.

source

noncomputable def G12OutsideBudget.residue (N : ℕ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) (d : ℕ) :

ℝ

Equations

G12OutsideBudget.residue N A d = G12OutsideBudget.divisibility N A d - G12OutsideBudget.mass N A / ↑d.totient

Instances For

Inspect dependencies

G12OutsideBudget.residue · compiled type and proof/definition references.

source

theorem G12OutsideBudget.mass_le {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) (hA : A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) :

mass N A ≤ 20 * ↑N

Inspect dependencies

G12OutsideBudget.mass_le · compiled type and proof/definition references.

source

theorem G12OutsideBudget.multiples_card_le (N d : ℕ) :

{n ∈ Finset.Icc 1 N | d ∣ n}.card ≤ N / d

Inspect dependencies

G12OutsideBudget.multiples_card_le · compiled type and proof/definition references.

source

theorem G12OutsideBudget.divisibility_le {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) (hA : A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) (d : ℕ) :

divisibility N A d ≤ 20 * ↑(N / d)

Inspect dependencies

G12OutsideBudget.divisibility_le · compiled type and proof/definition references.

source

theorem G12OutsideBudget.residue_majorant {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) (hA : A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) {d : ℕ} (hd : 1 ≤ d) :

|residue N A d| ≤ 20 * ↑N / ↑d.totient

An unconditional majorant for the real normalized G12 residue.

Inspect dependencies

G12OutsideBudget.residue_majorant · compiled type and proof/definition references.