Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.mid_of

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean:82 to 98

Source documentation

Generic mid-range: every row's [e^10, e^20000] segment via the allCells envelope transported by cell_Epi_le_admissible_gen. Rows supply P, the curve params (A,B,C), the cell-param numeric witnesses, and the native_decide check. Shared by every row's mid_row (the cover_of_chainOk plumbing was identical).

Exact Lean statement

theorem mid_of (P : CellParams) (A B C : ℝ)
    (hk : (P.k : ℝ) = 2 * B) (hB : 0 ≤ B) (hAnn : 0 ≤ A)
    (hAq : ((P.Aq : ℚ) : ℝ) = A)
    (hCge : C / Real.sqrt 5.5666305 ≤ ((P.c64 * 64 : ℚ) : ℝ))
    (hrB : (5.5666305:ℝ) ^ B ≤ ((P.rB : ℚ) : ℝ))
    (hchecked : allCells.all (fun c => checkCellGen P c) = true) :
    ∀ x ∈ Set.Icc (exp (10:ℝ)) (exp (20000:ℝ)),
      Eπ x ≤ admissible_bound A B C 5.5666305 x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem mid_of (P : CellParams) (A B C : ℝ)    (hk : (P.k : ℝ) = 2 * B) (hB : 0 ≤ B) (hAnn : 0 ≤ A)    (hAq : ((P.Aq : ℚ) : ℝ) = A)    (hCge : C / Real.sqrt 5.5666305 ≤ ((P.c64 * 64 : ℚ) : ℝ))    (hrB : (5.5666305:ℝ) ^ B ≤ ((P.rB : ℚ) : ℝ))    (hchecked : allCells.all (fun c => checkCellGen P c) = true) :    ∀ x ∈ Set.Icc (exp (10:ℝ)) (exp (20000:ℝ)),      Eπ x ≤ admissible_bound A B C 5.5666305 x := by  intro x hx  have hx_lo : exp ((10:ℕ):ℝ) ≤ x := by simpa using hx.1  have hx_hi : x ≤ exp ((lastB 10 allCells : ℕ):ℝ) := by    rw [allCells_last]; simpa using hx.2  obtain ⟨c, hcmem, hcx⟩ :=    cover_of_chainOk allCells 10 allCells_ne_nil allCells_chain hx_lo hx_hi  have hck : checkCellGen P c = true := List.all_eq_true.mp hchecked c hcmem  exact cell_Epi_le_admissible_gen P A B C 5.5666305 hk hB (by norm_num) hAnn hAq hCge hrB    c hck (allCells_trusted c hcmem) x hcx