MathlibNt.SieveTheory.LiLiuGoldbachB9LogGrid

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB9LogGridCells_iff {n : ℕ} {q : Fin n × Fin n} :

q ∈ goldbachB9LogGridCells n ↔ 4 / 53 ≤ goldbachB9AlphaGridPoint n (↑q.1 + 1) ∧ 1 / 3 ≤ goldbachB9BetaGridPoint n (↑q.2 + 1) ∧ goldbachB9AlphaGridPoint n ↑q.1 + 2 * goldbachB9BetaGridPoint n ↑q.2 < 1

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridStep_pos {n : ℕ} (hn : 0 < n) :

0 < goldbachB9AlphaGridStep n

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridStep_pos {n : ℕ} (hn : 0 < n) :

0 < goldbachB9BetaGridStep n

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint_eq_step (n i : ℕ) :

goldbachB9AlphaGridPoint n i = 1 / 20 + ↑i * goldbachB9AlphaGridStep n

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint_eq_step (n i : ℕ) :

goldbachB9BetaGridPoint n i = 1 / 4 + ↑i * goldbachB9BetaGridStep n

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint_succ (n i : ℕ) :

goldbachB9AlphaGridPoint n (i + 1) = goldbachB9AlphaGridPoint n i + goldbachB9AlphaGridStep n

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint_succ (n i : ℕ) :

goldbachB9BetaGridPoint n (i + 1) = goldbachB9BetaGridPoint n i + goldbachB9BetaGridStep n

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint_pos (n i : ℕ) :

0 < goldbachB9AlphaGridPoint n i

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint_pos (n i : ℕ) :

0 < goldbachB9BetaGridPoint n i

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint_lt_succ {n i : ℕ} (hn : 0 < n) :

goldbachB9AlphaGridPoint n i < goldbachB9AlphaGridPoint n (i + 1)

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint_lt_succ {n i : ℕ} (hn : 0 < n) :

goldbachB9BetaGridPoint n i < goldbachB9BetaGridPoint n (i + 1)

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint_mono {n i j : ℕ} (hn : 0 < n) (hij : i ≤ j) :

goldbachB9AlphaGridPoint n i ≤ goldbachB9AlphaGridPoint n j

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint_mono {n i j : ℕ} (hn : 0 < n) (hij : i ≤ j) :

goldbachB9BetaGridPoint n i ≤ goldbachB9BetaGridPoint n j

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint_end {n : ℕ} (hn : 0 < n) :

goldbachB9AlphaGridPoint n n = 1 / 3

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint_end {n : ℕ} (hn : 0 < n) :

goldbachB9BetaGridPoint n n = 1 / 2

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint_succ_le_end {n i : ℕ} (hn : 0 < n) (hi : i < n) :

goldbachB9AlphaGridPoint n (i + 1) ≤ 1 / 3

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint_succ_le_end {n i : ℕ} (hn : 0 < n) (hi : i < n) :

goldbachB9BetaGridPoint n (i + 1) ≤ 1 / 2

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCell_cornerGap_ge {n : ℕ} (hn : 0 < n) (q : Fin n × Fin n) :

1 / 6 ≤ 1 - goldbachB9AlphaGridPoint n (↑q.1 + 1) - goldbachB9BetaGridPoint n (↑q.2 + 1)

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCell_cornerGap_pos {n : ℕ} (hn : 0 < n) (q : Fin n × Fin n) :

0 < 1 - goldbachB9AlphaGridPoint n (↑q.1 + 1) - goldbachB9BetaGridPoint n (↑q.2 + 1)

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCell_upperCorner_lt_one {n : ℕ} (hn : 0 < n) (q : Fin n × Fin n) :

goldbachB9AlphaGridPoint n (↑q.1 + 1) + goldbachB9BetaGridPoint n (↑q.2 + 1) < 1

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9Pairs_covered_by_logGrid (n N : ℕ) (hn : 0 < n) (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) :

∃ q ∈ goldbachB9LogGridCells n, LiuWeight.LiuPairInLogRectangle N (goldbachB9AlphaGridPoint n ↑q.1) (goldbachB9AlphaGridPoint n (↑q.1 + 1)) (goldbachB9BetaGridPoint n ↑q.2) (goldbachB9BetaGridPoint n (↑q.2 + 1)) rs

The larger ambient box retains all three closed source boundaries.

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PairLogKernel_le_logGridMajorant (n N : ℕ) (hn : 0 < n) (hN : 2 ≤ N) :

goldbachB9PairLogKernel N ≤ goldbachB9LogGridMajorant n N

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachB9LogGridMajorant (n : ℕ) (hn : 0 < n) :

Filter.Tendsto (goldbachB9LogGridMajorant n) Filter.atTop (nhds (goldbachB9LogGridUpperSum n))

Only N tends to infinity here; its threshold may depend on n.

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PairLogKernel_le_gridUpperSum_eventually (n : ℕ) (hn : 0 < n) (η : ℝ) (hη : 0 < η) :

∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachB9PairLogKernel N ≤ goldbachB9LogGridUpperSum n + η

Inspect dependencies

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