Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.Table4Ext.mid_xpow_of

PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row11 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean:345 to 359

Source documentation

Generic x^{-1/n} mid assembler: over the allCells prefix take k (chained from 10 to m, every cell passing the row-n checkXpowCell), Eπ ≤ x^{-1/n} on [e^10, e^m]. Uses cover_of_chainOk + cell_Epi_le_xpow_of_check + allCells_trusted. Row 11: k = 3746, m = 3756.

Exact Lean statement

theorem mid_xpow_of (n : ℕ) (hn : 0 < n) (k m : ℕ)
    (hchain : chainOk 10 (allCells.take k) = true)
    (hne : allCells.take k ≠ [])
    (hlast : lastB 10 (allCells.take k) = m)
    (hall : (allCells.take k).all (fun c => checkXpowCell n c) = true) :
    ∀ x ∈ Set.Icc (Real.exp (10:ℝ)) (Real.exp (m:ℝ)), Eπ x ≤ x ^ (-(1:ℝ)/n)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem mid_xpow_of (n : ℕ) (hn : 0 < n) (k m : ℕ)    (hchain : chainOk 10 (allCells.take k) = true)    (hne : allCells.take k ≠ [])    (hlast : lastB 10 (allCells.take k) = m)    (hall : (allCells.take k).all (fun c => checkXpowCell n c) = true) :    ∀ x ∈ Set.Icc (Real.exp (10:ℝ)) (Real.exp (m:ℝ)), Eπ x ≤ x ^ (-(1:ℝ)/n) := by  intro x hx  have hx_lo : Real.exp ((10:ℕ):ℝ) ≤ x := by simpa using hx.1  have hx_hi : x ≤ Real.exp ((lastB 10 (allCells.take k) : ℕ):ℝ) := by    rw [hlast]; exact hx.2  obtain ⟨c, hcmem, hcx⟩ :=    cover_of_chainOk (allCells.take k) 10 hne hchain hx_lo hx_hi  have hck : checkXpowCell n c = true := List.all_eq_true.mp hall c hcmem  exact cell_Epi_le_xpow_of_check n hn c hck    (allCells_trusted c (List.mem_of_mem_take hcmem)) x hcx