theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Pairs_eq_C10Pairs (N : ℕ) : goldbachC9Pairs N = goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9ProductSupport_eq_C10ProductSupport (N : ℕ) : goldbachC9ProductSupport N = goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusAtoms_eq_B10ZeroPrefix (N : ℕ) : goldbachB9PlusAtoms N = goldbachB10Atoms N 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3))

Equality of the entire labelled mother families, not just of their output sets.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusSiftedAtoms_eq_B10ZeroPrefix (N : ℕ) (Z : ℝ) : goldbachB9PlusSiftedAtoms N Z = goldbachB10SiftedAtoms N 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusSifted_card_eq_B10ZeroPrefix (N : ℕ) (Z : ℝ) : ↑(goldbachB9PlusSiftedAtoms N Z).card = goldbachB10SiftedCount N 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z