Não é necessário plugins medonhos e nem usar jQuery para algo tão trivial, dá pra fazer na mão, aprendendo o básico de verdade, é claro.
Um exemplo de máscara que fiz com JS puro ajuda a entender como fazer de forma simples e até adaptar depois: https://pt.stackoverflow.com/a/419538/3635, o processo é basicamente timeout+expressão regular+replace
Feito isto a questão é a regex que precisará, no caso são quatro numeros após o ponto, sendo assim então se digitar até 4 não tem ponto, creio eu, logo se digitar 5 numeros deve ficar 9.9999, então o regex deve ficar algo como:
/^(\d+)(\d{4})$/
A primeira parte da regex ^(\d+)
pega os digitos que devem vir antes do ponto e o (\d{4})$
pega os 4 últimos dígitos. Note que é necessário .replace(/\D+/, '');
para remover o que não são dígitos.
O código ficou assim:
document.addEventListener('DOMContentLoaded', function () {
console.log('DOM carregou');
var campo1 = document.getElementById('campo1');
if (!campo1) return;
var campo1Timeout;
campo1.addEventListener('input', function () {
if (campo1Timeout) clearTimeout(campo1Timeout);
campo1Timeout = setTimeout(mascara, 200);
});
function mascara()
{
var value = campo1.value.replace(/\D+/, ''); //Remove tudo que não for numero
value = value.replace(/^(\d+)(\d{4})$/, '$1.$2');
campo1.value = value;
}
});
<input type="tel" name="campo1" id="campo1" placeholder="Seu numero">