English
A variant of the product formula for deriv_expMap_single with a modified decomposition.
Русский
Вариант формулы произведения для deriv_expMap_single с иным разложением.
LaTeX
$$$\prod_w \text{deriv\_expMap\_single } w\big((\text{completeBasis}(K).equivFun.symm x)\,w\big) = \exp(x_{w_0})^{\operatorname{finrank}} \cdot \left(\prod w : { w // IsComplex w }, \expMapBasis x w.1\right)^{-1} \cdot 2^{-nrComplexPlaces K}$$$
Lean4
theorem setLIntegral_expMapBasis_image {s : Set (realSpace K)} (hs : MeasurableSet s) {f : (InfinitePlace K → ℝ) → ℝ≥0∞}
(hf : Measurable f) :
∫⁻ x in expMapBasis '' s, f x =
(2 : ℝ≥0∞)⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * (Module.finrank ℚ K) *
∫⁻ x in s,
ENNReal.ofReal (Real.exp (x w₀ * Module.finrank ℚ K)) *
(∏ i : { w : InfinitePlace K // IsComplex w }, .ofReal (expMapBasis (fun w ↦ x w) i))⁻¹ *
f (expMapBasis x) :=
by
rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume hs
(fun x _ ↦ (hasFDerivAt_expMapBasis K x).hasFDerivWithinAt) (injective_expMapBasis K).injOn]
simp_rw [abs_det_fderiv_expMapBasis]
have : Measurable expMapBasis := (continuous_expMapBasis K).measurable
rw [← lintegral_const_mul _ (by fun_prop)]
congr with x
have : 0 ≤ (∏ w : { w // IsComplex w }, expMapBasis x w.1)⁻¹ :=
inv_nonneg.mpr <| Finset.prod_nonneg fun _ _ ↦ (expMapBasis_pos _ _).le
rw [ofReal_mul (by positivity), ofReal_mul (by positivity), ofReal_mul (by positivity), ofReal_mul (by positivity),
ofReal_pow (by positivity), ofReal_inv_of_pos (Finset.prod_pos fun _ _ ↦ expMapBasis_pos _ _),
ofReal_inv_of_pos zero_lt_two, ofReal_ofNat, ofReal_natCast,
ofReal_prod_of_nonneg (fun _ _ ↦ (expMapBasis_pos _ _).le)]
ring
