theorem Section10CanonicalXi.xi_monotone : Monotone xi

theorem Section10CanonicalXi.xi_sub_two_log_antitone : AntitoneOn (fun (s : ℝ) => xi s - 2 * Real.log s) (Set.Ici Section10CanonicalXi.phaseThreshold✝)

theorem Section10CanonicalXi.xi_le_two_log_add {s : ℝ} (hs : Section10CanonicalXi.phaseThreshold✝ ≤ s) : xi s ≤ xi Section10CanonicalXi.phaseThreshold✝ + 2 * Real.log s

theorem Section10CanonicalXi.phaseLogConstant_gt_one : 1 < Section10CanonicalXi.phaseLogConstant✝

theorem Section10CanonicalXi.xi_le_coarse_phase {s : ℝ} (hs : Section10CanonicalXi.phaseThreshold✝ ≤ s) : xi s ≤ Real.log s + Real.log (Real.log (3 * s)) + Real.log Section10CanonicalXi.phaseLogConstant✝

Pointwise coarse phase estimate obtained from the canonical equation, not assumed.

theorem Section10CanonicalXi.coarse_phase_uniform_on_Icc {s t : ℝ} (hs : Section10CanonicalXi.phaseThreshold✝ ≤ s) (ht : t ∈ Set.Icc 1 s) : xi t ≤ Real.log s + Real.log (Real.log (3 * s)) + Section10CanonicalXi.phaseConstant✝

theorem Section10CanonicalXi.proposition1023_coarse_phase : ∀ᶠ (s : ℝ) in Filter.atTop, ∫ (t : ℝ) in 1..s, xi t ≤ s * Real.log s + s * Real.log (Real.log (3 * s)) + Section10CanonicalXi.phaseConstant✝ * s

Proposition 10.23, coarse phase-integral upper bound for κ=b=1. The bound is proved for the canonical xi; no phase estimate is a premise.