MathlibNt.SieveTheory.LiLiuGoldbachB8LogGrid

@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidablePropB8LogGrid (p : Prop) :

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidablePropB8LogGrid p = Classical.propDecidable p

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridWidth :

ℝ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridWidth = 1 / 12

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridWidth :

ℝ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridWidth = 5 / 44

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridPoint (n i : ℕ) :

ℝ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridPoint n i = 1 / 4 + ↑i / ↑n * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridWidth

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridPoint (n j : ℕ) :

ℝ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridPoint n j = 1 / 4 + ↑j / ↑n * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridWidth

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridStep (n : ℕ) :

ℝ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridStep n = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridWidth / ↑n

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridStep (n : ℕ) :

ℝ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridStep n = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridWidth / ↑n

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridCells (n : ℕ) :

Finset (Fin n × Fin n)

An outer selection sufficient for the closed B8 triangle; not an intersection test.

Equations

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridMajorant (n N : ℕ) :

ℝ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridMajorant n N = ∑ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridCells n, 1 / (1 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridPoint n (↑q.1 + 1) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridPoint n (↑q.2 + 1)) * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridPoint n ↑q.1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridPoint n (↑q.1 + 1)) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridPoint n ↑q.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridPoint n (↑q.2 + 1))

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridUpperSum (n : ℕ) :

ℝ

A named finite upper sum only; no integral or limit assertion is made here.

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridUpperSum n = ∑ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridCells n, 1 / (1 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridPoint n (↑q.1 + 1) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridPoint n (↑q.2 + 1)) * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridPoint n ↑q.1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridPoint n (↑q.1 + 1)) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridPoint n ↑q.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridPoint n (↑q.2 + 1))

Instances For

Inspect dependencies

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

source

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

q ∈ goldbachB8LogGridCells n ↔ goldbachB8Gamma ≤ goldbachB8AlphaGridPoint n (↑q.1 + 1) ∧ goldbachB8AlphaGridPoint n ↑q.1 < goldbachB8BetaGridPoint n (↑q.2 + 1) ∧ goldbachB8AlphaGridPoint n ↑q.1 + 2 * goldbachB8BetaGridPoint n ↑q.2 < 1

Inspect dependencies

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

source

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

0 < goldbachB8AlphaGridStep n

Inspect dependencies

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

source

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

0 < goldbachB8BetaGridStep n

Inspect dependencies

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

source

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

goldbachB8AlphaGridPoint n i = 1 / 4 + ↑i * goldbachB8AlphaGridStep n

Inspect dependencies

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

source

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

goldbachB8BetaGridPoint n i = 1 / 4 + ↑i * goldbachB8BetaGridStep n

Inspect dependencies

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

source

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

goldbachB8AlphaGridPoint n (i + 1) = goldbachB8AlphaGridPoint n i + goldbachB8AlphaGridStep n

Inspect dependencies

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

source

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

goldbachB8BetaGridPoint n (i + 1) = goldbachB8BetaGridPoint n i + goldbachB8BetaGridStep n

Inspect dependencies

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

source

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

0 < goldbachB8AlphaGridPoint n i

Inspect dependencies

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

source

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

0 < goldbachB8BetaGridPoint n i

Inspect dependencies

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

source

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

goldbachB8AlphaGridPoint n i < goldbachB8AlphaGridPoint n (i + 1)

Inspect dependencies

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

source

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

goldbachB8BetaGridPoint n i < goldbachB8BetaGridPoint n (i + 1)

Inspect dependencies

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

source

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

goldbachB8AlphaGridPoint n i ≤ goldbachB8AlphaGridPoint n j

Inspect dependencies

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

source

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

goldbachB8BetaGridPoint n i ≤ goldbachB8BetaGridPoint n j

Inspect dependencies

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

source

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

goldbachB8AlphaGridPoint n n = 1 / 3

Inspect dependencies

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

source

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

goldbachB8BetaGridPoint n n = 4 / 11

Inspect dependencies

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

source

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

goldbachB8AlphaGridPoint n (i + 1) ≤ 1 / 3

Inspect dependencies

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

source

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

goldbachB8BetaGridPoint n (i + 1) ≤ 4 / 11

Inspect dependencies

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

source

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

10 / 33 ≤ 1 - goldbachB8AlphaGridPoint n (↑q.1 + 1) - goldbachB8BetaGridPoint n (↑q.2 + 1)

The gap holds on the entire ambient grid, not just selected cells.

Inspect dependencies

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

source

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

0 < 1 - goldbachB8AlphaGridPoint n (↑q.1 + 1) - goldbachB8BetaGridPoint n (↑q.2 + 1)

Inspect dependencies

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

source

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

goldbachB8AlphaGridPoint n (↑q.1 + 1) + goldbachB8BetaGridPoint n (↑q.2 + 1) < 1

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8Pairs_covered_by_logGrid (n N : ℕ) (hn : 0 < n) (hN : 2 ≤ N) {rs : ℕ × ℕ} (hrs : rs ∈ goldbachS4Pairs N (↑N ^ (3 / 11))) :

∃ q ∈ goldbachB8LogGridCells n, LiuWeight.LiuPairInLogRectangle N (goldbachB8AlphaGridPoint n ↑q.1) (goldbachB8AlphaGridPoint n (↑q.1 + 1)) (goldbachB8BetaGridPoint n ↑q.2) (goldbachB8BetaGridPoint n (↑q.2 + 1)) rs

The two Ioc locations retain grid points and every closed source boundary.

Inspect dependencies

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

source

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

goldbachB8PairLogKernel N ≤ goldbachB8LogGridMajorant n N

The actual finite B8 kernel is bounded by the fixed, closed-boundary grid majorant.

Inspect dependencies

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