Products involving factorials in ordered semifields

This file evaluates finite products in ordered semifields whose factors stabilize to a simple factorial quotient. Such products occur as accumulated losses in lattice basis estimates.

theorem TauCeti.prod_max_one_add_one_div_two {K : Type u_1} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (n : ℕ) : ∏ i : Fin n, max 1 ((↑↑i + 1) / 2) = ↑n.factorial / 2 ^ (n - 1)

The product of the factors max 1 ((i + 1) / 2), indexed from zero, is the factorial quotient n! / 2^(n - 1).