Parameters for the six-point transfer

The approximate-root ratio and the sibling-density parameter are chosen strictly between the finite endpoint and the target density.

theorem LeanPool.Besicovitch.exists_transfer_parameters {s β : ℝ} (hs : 0 < s) (hsβ : s < β) : ∃ (q : ℝ) (γ : ℝ), 0 < q ∧ q < 1 ∧ s / β < q ∧ 0 < γ ∧ γ < β ∧ s < γ * q

Between positive parameters s < β, choose an approximate-root ratio q and a sibling parameter γ with s < γq.