MathlibNt.SieveTheory.LiLiuGoldbachG10BuchstabBridge

@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachG10BuchstabBridge (P : Prop) :

Decidable P

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachG10BuchstabBridge P = Classical.propDecidable P

Instances For

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachG10BuchstabBridge · compiled type and proof/definition references.

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT16 (A : Finset ℕ) (N : ℕ) (b c : ℝ) :

ℤ

The genuine triple layer attached to the corrected closed G10 carrier.

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT16 A N b c = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N b c, ∑ t ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N (↑rs.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Cutoff N rs), MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A (N * rs.1) (rs.1 * rs.2 * t) ↑rs.2

Instances For

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT16 · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT16_nonneg (A : Finset ℕ) (N : ℕ) (b c : ℝ) :

0 ≤ goldbachWeightT16 A N b c

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT16_nonneg · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed_eq_sum_goldbachC10Pairs (A : Finset ℕ) (N : ℕ) (b c : ℝ) :

goldbachS5Closed A N b c = ∑ rs ∈ goldbachC10Pairs N b c, literalH A (N * rs.1) (rs.1 * rs.2) ↑rs.2

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed_eq_sum_goldbachC10Pairs · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pair_cell_le_goldbachG10CorrectedCell_add_t16Slice (A : Finset ℕ) {N : ℕ} {b c : ℝ} {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N b c) :

literalH A (N * rs.1) (rs.1 * rs.2) ↑rs.2 ≤ literalH A (N * goldbachC10Prod rs) (goldbachC10Prod rs) (goldbachC10Cutoff N rs) + ∑ t ∈ goldbachClosedPrimes N (↑rs.2) (goldbachC10Cutoff N rs), literalH A (N * rs.1) (rs.1 * rs.2 * t) ↑rs.2

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pair_cell_le_goldbachG10CorrectedCell_add_t16Slice · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed_le_goldbachG10Corrected_add_goldbachWeightT16 (A : Finset ℕ) (N : ℕ) (b c : ℝ) (_hb : 2 ≤ b) (_hbc : b ≤ c) :

goldbachS5Closed A N b c ≤ goldbachG10Corrected A N b c + goldbachWeightT16 A N b c

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed_le_goldbachG10Corrected_add_goldbachWeightT16 · compiled type and proof/definition references.