EndpointRowScale.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A coefficient box chosen from the fixed endpoint alone

def OAI.JointDickman.endpointRowScale line 10
def OAI.JointDickman.EndpointCoefficientWindow line 12

theorem OAI.JointDickman.endpointRowScale_window line 18

Source documentation

One box, determined solely by the first coefficient, contains every possible quotient in its support window.

theorem endpointRowScale_window {B T b c : ℕ} (hB : 2 ≤ B) (hT : 0 < T)
    (hc : 0 < c) (hlog : (B : ℝ) ≤ Real.log c)
    (hlo : T*c ≤ b) (hhi : b ≤ 2*T*c) :
    Real.exp ((1/2 : ℝ)*B) ≤ (endpointRowScale T b : ℝ) ∧
      c ∈ Ico (endpointRowScale T b) (4*endpointRowScale T b) ∧
      T*endpointRowScale T b ≤ b := by
…

Mentions: OAI.JointDickman.endpointRowScale

theorem OAI.JointDickman.endpointCoefficientWindow_size line 51
Source documentation
All possible endpoint coefficients are in the fixed range needed for the previously proved prime-product domination.
```
theorem endpointCoefficientWindow_size {B T b : ℕ} (hB : 10 ≤ B)
    (hT : (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B))
    (hw : EndpointCoefficientWindow B T b) :
    (b : ℝ) ≤ Real.exp ((16/5 : ℝ)*B) := by
…
```
Mentions: OAI.JointDickman.EndpointCoefficientWindow