def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyOf (v : GoldbachG11Label) (k : ℕ) : GoldbachG11SwitchedBody

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyOf v k = ⟨v.fst, ⟨v.snd.fst, ⟨v.snd.snd.snd, k⟩⟩⟩

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_switch_product (v : GoldbachG11Label) (k : ℕ) : v.snd.snd.fst * goldbachG11SwitchedBodyProd (goldbachG11SwitchedBodyOf v k) = goldbachG11LabelProd v * k

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_switch_cutoff_iff {N p n : ℕ} (eps : ℝ) (heq : p + n = N) : ↑p < (1 - eps) * ↑N ↔ eps * ↑N < ↑n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughPair_to_switched {N p k : ℕ} {eps z b : ℝ} {v : GoldbachG11Label} (hv : v ∈ goldbachG11Labels N z b) (hpk : (p, k) ∈ goldbachG11RoughPairs N eps v) : goldbachG11SwitchedBodyOf v k ∈ goldbachG11SwitchedBodies N z b ∧ v.snd.snd.fst ∈ goldbachG11FirstPrimeFiber N eps z (goldbachG11SwitchedBodyOf v k) ∧ p = N - v.snd.snd.fst * goldbachG11SwitchedBodyProd (goldbachG11SwitchedBodyOf v k)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Switched_to_roughPair {N r : ℕ} {eps z b : ℝ} {u : GoldbachG11SwitchedBody} (hu : u ∈ goldbachG11SwitchedBodies N z b) (hr : r ∈ goldbachG11FirstPrimeFiber N eps z u) : ⟨u.fst, ⟨u.snd.fst, ⟨r, u.snd.snd.fst⟩⟩⟩ ∈ goldbachG11Labels N z b ∧ (N - r * goldbachG11SwitchedBodyProd u, u.snd.snd.snd) ∈ goldbachG11RoughPairs N eps ⟨u.fst, ⟨u.snd.fst, ⟨r, u.snd.snd.fst⟩⟩⟩

@[reducible, inline]

abbrev MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11RoughAtom : Type

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11RoughAtom = ((_ : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label) × ℕ × ℕ)

@[reducible, inline]

abbrev MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11SwitchedAtom : Type

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11SwitchedAtom = ((_ : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11SwitchedBody) × ℕ)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughFamily (N : ℕ) (eps z b : ℝ) : Finset GoldbachG11RoughAtom

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughFamily N eps z b = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Labels N z b).sigma (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughPairs N eps)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedFamily (N : ℕ) (eps z b : ℝ) : Finset GoldbachG11SwitchedAtom

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedFamily N eps z b = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodies N z b).sigma (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FirstPrimeFiber N eps z)

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchForward (x : GoldbachG11RoughAtom) : GoldbachG11SwitchedAtom

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchForward x = ⟨MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyOf x.fst x.snd.2, x.fst.snd.snd.fst⟩

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchBackward (N : ℕ) (y : GoldbachG11SwitchedAtom) : GoldbachG11RoughAtom

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchBackward N y = ⟨⟨y.fst.fst, ⟨y.fst.snd.fst, ⟨y.snd, y.fst.snd.snd.fst⟩⟩⟩, (N - y.snd * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd y.fst, y.fst.snd.snd.snd)⟩

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchForward_mem {N : ℕ} {eps z b : ℝ} {x : GoldbachG11RoughAtom} (hx : x ∈ goldbachG11RoughFamily N eps z b) : goldbachG11SwitchForward x ∈ goldbachG11SwitchedFamily N eps z b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchBackward_mem {N : ℕ} {eps z b : ℝ} {y : GoldbachG11SwitchedAtom} (hy : y ∈ goldbachG11SwitchedFamily N eps z b) : goldbachG11SwitchBackward N y ∈ goldbachG11RoughFamily N eps z b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchBackward_forward {N : ℕ} {eps z b : ℝ} {x : GoldbachG11RoughAtom} (hx : x ∈ goldbachG11RoughFamily N eps z b) : goldbachG11SwitchBackward N (goldbachG11SwitchForward x) = x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchForward_backward (N : ℕ) (y : GoldbachG11SwitchedAtom) : goldbachG11SwitchForward (goldbachG11SwitchBackward N y) = y

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchEquiv (N : ℕ) (eps z b : ℝ) : ↥(goldbachG11RoughFamily N eps z b) ≃ ↥(goldbachG11SwitchedFamily N eps z b)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchEquiv N eps z b = { toFun := fun (x : ↥(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughFamily N eps z b)) => ⟨MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchForward ↑x, ⋯⟩, invFun := fun (y : ↥(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedFamily N eps z b)) => ⟨MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchBackward N ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Switch_card (N : ℕ) (eps z b : ℝ) : (goldbachG11RoughFamily N eps z b).card = (goldbachG11SwitchedFamily N eps z b).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Switch_sum (N : ℕ) (eps z b : ℝ) (w : GoldbachG11SwitchedBody → ℤ) : ∑ v ∈ goldbachG11Labels N z b, ∑ pk ∈ goldbachG11RoughPairs N eps v, w (goldbachG11SwitchedBodyOf v pk.2) = ∑ u ∈ goldbachG11SwitchedBodies N z b, ∑ _r ∈ goldbachG11FirstPrimeFiber N eps z u, w u

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughCount_sum_eq_switchedTotal (N : ℕ) (eps z b : ℝ) : ∑ v ∈ goldbachG11Labels N z b, goldbachG11RoughCount N eps v = goldbachG11SwitchedTotal N eps z b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Switch_filter_count (N : ℕ) (eps z b : ℝ) (C : GoldbachG11SwitchedBody → Prop) : ∑ v ∈ goldbachG11Labels N z b, ↑{pk ∈ goldbachG11RoughPairs N eps v | C (goldbachG11SwitchedBodyOf v pk.2)}.card = ∑ u ∈ goldbachG11SwitchedBodies N z b with C u, ↑(goldbachG11FirstPrimeFiber N eps z u).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BadRoughPair_mem_NException {N : ℕ} {eps z b : ℝ} {v : GoldbachG11Label} {pk : ℕ × ℕ} (heps : 0 ≤ eps) (hv : v ∈ goldbachG11Labels N z b) (hpk : pk ∈ goldbachG11RoughPairs N eps v) (hbad : ¬(goldbachG11SwitchedBodyProd (goldbachG11SwitchedBodyOf v pk.2)).Coprime N) : goldbachG11LabelProd v * pk.2 ∈ goldbachG11NException (goldbachDifferenceCarrier N eps) N v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughPair_output_injective (N : ℕ) (eps : ℝ) (v : GoldbachG11Label) (hv : 0 < goldbachG11LabelProd v) : Set.InjOn (fun (pk : ℕ × ℕ) => goldbachG11LabelProd v * pk.2) ↑(goldbachG11RoughPairs N eps v)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BadRoughCount_le_NCount {N : ℕ} {eps z b : ℝ} (heps : 0 ≤ eps) {v : GoldbachG11Label} (hv : v ∈ goldbachG11Labels N z b) : ↑{pk ∈ goldbachG11RoughPairs N eps v | ¬(goldbachG11SwitchedBodyProd (goldbachG11SwitchedBodyOf v pk.2)).Coprime N}.card ≤ goldbachG11NCount (goldbachDifferenceCarrier N eps) N v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BadSwitchedTotal_le_NCount_sum (N : ℕ) (eps z b : ℝ) (heps : 0 ≤ eps) : goldbachG11BadSwitchedTotal N eps z b ≤ ∑ v ∈ goldbachG11Labels N z b, goldbachG11NCount (goldbachDifferenceCarrier N eps) N v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedTotal_le_good_add_NCount (N : ℕ) (eps z b : ℝ) (heps : 0 ≤ eps) : goldbachG11SwitchedTotal N eps z b ≤ goldbachG11GoodSwitchedTotal N eps z b + ∑ v ∈ goldbachG11Labels N z b, goldbachG11NCount (goldbachDifferenceCarrier N eps) N v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughTotal_eq_switchedTotal (N : ℕ) (eps : ℝ) : goldbachG11RoughTotal N eps = goldbachG11SwitchedTotal N eps (↑N ^ (4 / 53)) (↑N ^ (4 / 33))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughTotal_good_comparison (N : ℕ) (eps : ℝ) (heps : 0 ≤ eps) : 0 ≤ goldbachG11RoughTotal N eps - goldbachG11GoodSwitchedTotal N eps (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) ∧ goldbachG11RoughTotal N eps ≤ goldbachG11GoodSwitchedTotal N eps (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) + ∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), goldbachG11NCount (goldbachDifferenceCarrier N eps) N v