English
The product over w of deriv_expMap_single w at the inverse basis equals exp(x_{w0})^{finrank} times the inverse of the product expMapBasis(x) over complex w, times 2^{-nrComplexPlaces}.
Русский
Произведение по всем w от deriv_expMap_single w на ((completeBasis K).equivFun.symm x) равно exp(x_{w0})^{finrank} умноженное на обратное к произведению expMapBasis(x) по комплексным местам, умноженное на 2^{−nrComplexPlaces}.
LaTeX
$$$\\prod_w \\text{deriv\_expMap\_single } w((\\text{completeBasis}(K).equivFun.symm x))(w) \\\\ = \\\\exp(x_{w_0})^{\\operatorname{finrank} \\mathbb{Q} K} \\cdot \\left(\\prod w:{w // IsComplex w} \\expMapBasis(x w)\\right)^{-1} \\cdot 2^{-\\mathrm{nrComplexPlaces} K}$$$
Lean4
theorem prod_deriv_expMap_single (x : realSpace K) :
∏ w, deriv_expMap_single w ((completeBasis K).equivFun.symm x w) =
Real.exp (x w₀) ^ Module.finrank ℚ K * (∏ w : { w // IsComplex w }, expMapBasis x w.1)⁻¹ *
(2⁻¹) ^ nrComplexPlaces K :=
by
simp only [deriv_expMap_single, expMap_single_apply]
rw [Finset.prod_mul_distrib]
congr 1
·
simp_rw [← prod_expMapBasis_pow, prod_eq_prod_mul_prod, expMapBasis_apply, expMap_apply, mult_isReal,
mult_isComplex, pow_one, Finset.prod_pow, pow_two, mul_assoc,
mul_inv_cancel₀ (Finset.prod_ne_zero_iff.mpr <| fun _ _ ↦ Real.exp_ne_zero _), mul_one]
· simp [prod_eq_prod_mul_prod, mult_isReal, mult_isComplex]
