theorem MathlibNt.SieveTheory.SuzukiPowerCoordinates.log_upper_endpoint {D s z : ℝ} (hD : 1 < D) (_hs : 0 < s) (hz : z = D ^ (1 / s)) : Real.log z = Real.log D / s

Logarithm of the upper power-coordinate endpoint.

theorem MathlibNt.SieveTheory.SuzukiPowerCoordinates.log_lower_endpoint {D σ w : ℝ} (hD : 1 < D) (_hσ : 0 < σ) (hw : w = D ^ (1 / σ)) : Real.log w = Real.log D / σ

Logarithm of the lower power-coordinate endpoint.

theorem MathlibNt.SieveTheory.SuzukiPowerCoordinates.endpoints_order {D s σ w z : ℝ} (hD : 1 < D) (hs : 0 < s) (hsσ : s ≤ σ) (hz : z = D ^ (1 / s)) (hw : w = D ^ (1 / σ)) : 1 < w ∧ w ≤ z

The power-coordinate endpoints satisfy 1 < w ≤ z.

theorem MathlibNt.SieveTheory.SuzukiPowerCoordinates.log_div_log_mem_Icc {D s σ w z x : ℝ} (hD : 1 < D) (hs : 0 < s) (hsσ : s ≤ σ) (hz : z = D ^ (1 / s)) (hw : w = D ^ (1 / σ)) (hx : x ∈ Set.Icc w z) : Real.log D / Real.log x ∈ Set.Icc s σ

Every point between the power-coordinate endpoints maps back into [s, σ] under Suzuki's coordinate x ↦ log D / log x.

theorem MathlibNt.SieveTheory.SuzukiPowerCoordinates.coordinate_at_upper {D s z : ℝ} (hD : 1 < D) (hs : 0 < s) (hz : z = D ^ (1 / s)) : Real.log D / Real.log z = s

Suzuki's coordinate takes the upper endpoint z to s.

theorem MathlibNt.SieveTheory.SuzukiPowerCoordinates.coordinate_at_lower {D σ w : ℝ} (hD : 1 < D) (hσ : 0 < σ) (hw : w = D ^ (1 / σ)) : Real.log D / Real.log w = σ

Suzuki's coordinate takes the lower endpoint w to σ.

theorem MathlibNt.SieveTheory.SuzukiPowerCoordinates.apply_coordinate_at_upper {D s z : ℝ} (H : ℝ → ℝ) (hD : 1 < D) (hs : 0 < s) (hz : z = D ^ (1 / s)) : H (Real.log D / Real.log z) = H s

Applying H at the upper endpoint gives exactly H s.

theorem MathlibNt.SieveTheory.SuzukiPowerCoordinates.apply_coordinate_at_lower {D σ w : ℝ} (H : ℝ → ℝ) (hD : 1 < D) (hσ : 0 < σ) (hw : w = D ^ (1 / σ)) : H (Real.log D / Real.log w) = H σ

Applying H at the lower endpoint gives exactly H σ.

theorem MathlibNt.SieveTheory.SuzukiPowerCoordinates.apply_coordinate_endpoints {D s σ w z : ℝ} (H : ℝ → ℝ) (hD : 1 < D) (hs : 0 < s) (hsσ : s ≤ σ) (hz : z = D ^ (1 / s)) (hw : w = D ^ (1 / σ)) : H (Real.log D / Real.log z) = H s ∧ H (Real.log D / Real.log w) = H σ

Endpoint normalization after applying an arbitrary function H.

theorem MathlibNt.SieveTheory.SuzukiPowerCoordinates.reciprocal_log_endpoint_normalization {D s σ w z : ℝ} (hD : 1 < D) (hs : 0 < s) (hsσ : s ≤ σ) (hz : z = D ^ (1 / s)) (hw : w = D ^ (1 / σ)) : 1 / Real.log z * (σ / s) = 1 / Real.log w

The endpoint logarithms give the exact normalization factor used in Suzuki's main term.