Simplified0.4
\[\leadsto \color{blue}{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(0.5 - \frac{k}{2}\right)}}{\sqrt{k}}}
\]
Proof
(/.f64 (pow.f64 (*.f64 2 (*.f64 (PI.f64) n)) (-.f64 1/2 (/.f64 k 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 (PI.f64)) n)) (-.f64 1/2 (/.f64 k 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (-.f64 (Rewrite<= metadata-eval (/.f64 1 2)) (/.f64 k 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= div-sub_binary64 (/.f64 (-.f64 1 k) 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= /-rgt-identity_binary64 (/.f64 (/.f64 (-.f64 1 k) 2) 1))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (/.f64 (-.f64 1 k) 2) (Rewrite<= metadata-eval (/.f64 2 2)))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (/.f64 (-.f64 1 k) 2) 2) 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (/.f64 (-.f64 1 k) 2) 2) 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= *-commutative_binary64 (*.f64 2 (/.f64 (/.f64 (-.f64 1 k) 2) 2)))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (/.f64 (-.f64 1 k) 2) 2)) (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (/.f64 (-.f64 1 k) 2) 2)))) (sqrt.f64 k)): 48 points increase in error, 24 points decrease in error
(/.f64 (Rewrite<= sqr-pow_binary64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (-.f64 1 k) 2))) (sqrt.f64 k)): 24 points increase in error, 48 points decrease in error
(/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (-.f64 1 k) 2)))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (-.f64 1 k) 2)))): 22 points increase in error, 14 points decrease in error