English
The volume of normLeOne(K) is given by a product of powers of 2, π, and the regulator.
Русский
Объем normLeOne(K) равен произведению степеней 2 и π и регулятора поля.
LaTeX
$$$\\operatorname{vol}(\\operatorname{normLeOne}(K)) = 2^{\\operatorname{nrRealPlaces}} \\cdot \\pi^{\\operatorname{nrComplexPlaces}} \\cdot \\operatorname{regulator}(K).$$$
Lean4
theorem volume_normLeOne :
volume (normLeOne K) = 2 ^ nrRealPlaces K * NNReal.pi ^ nrComplexPlaces K * .ofReal (regulator K) :=
by
rw [volume_eq_two_pow_mul_two_pi_pow_mul_integral (normLeOne_eq_preimage_image K).symm (measurableSet_normLeOne K),
normLeOne_eq_preimage, normAtAllPlaces_image_preimage_expMapBasis,
setLIntegral_expMapBasis_image (measurableSet_paramSet K) (by fun_prop)]
simp_rw [ENNReal.inv_mul_cancel_right
(Finset.prod_ne_zero_iff.mpr fun _ _ ↦ ofReal_ne_zero_iff.mpr (expMapBasis_pos _ _))
(prod_ne_top fun _ _ ↦ ofReal_ne_top)]
rw [setLIntegral_paramSet_exp K Module.finrank_pos, ofReal_mul zero_le_two, mul_pow, ofReal_ofNat,
ENNReal.mul_inv_cancel_right (Nat.cast_ne_zero.mpr Module.finrank_pos.ne') (natCast_ne_top _), coe_nnreal_eq,
NNReal.coe_real_pi, mul_mul_mul_comm, ← ENNReal.inv_pow, ← mul_assoc, ← mul_assoc,
ENNReal.inv_mul_cancel_right (pow_ne_zero _ two_ne_zero) (pow_ne_top ENNReal.ofNat_ne_top)]
