English
Under a norm-stability assumption, the volume of A equals a product of powers of 2π and a polar-space integral.
Русский
При допущении сохраняемости нормы, объём A равен произведению степеней 2π и линейного интеграла по полярному пространству.
LaTeX
$$$volume(A) = 2^{nrRealPlaces(K)} \\cdot (2\\pi)^{nrComplexPlaces(K)} \\cdot \\int^{\\!\\! -}_{normAtAllPlaces(A)} \\prod w : { w // IsComplex w }, ENNReal.ofReal (x w.1)$$$
Lean4
/-- If the measurable set `A` is norm-stable at complex places in the sense that
`normAtComplexPlaces⁻¹ (normAtComplexPlaces '' A) = A`, then its volume can be computed via an
integral over `normAtComplexPlaces '' A`.
-/
theorem volume_eq_two_pi_pow_mul_integral [NumberField K] (hA : normAtComplexPlaces ⁻¹' (normAtComplexPlaces '' A) = A)
(hm : MeasurableSet A) :
volume A =
.ofReal (2 * π) ^ nrComplexPlaces K *
∫⁻ x in normAtComplexPlaces '' A, ∏ w : { w // IsComplex w }, ENNReal.ofReal (x w.1) :=
by
have hA' {x} : (A.indicator 1 x : ℝ≥0∞) = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x) := by
simp_rw [← Set.indicator_comp_right, Function.comp_def, Pi.one_def, hA]
rw [← lintegral_indicator_one hm, ← lintegral_comp_polarSpaceCoord_symm, polarSpaceCoord_target',
Measure.volume_eq_prod, setLIntegral_prod]
· simp_rw [hA', normAtComplexPlaces_polarSpaceCoord_symm, lintegral_const, restrict_apply MeasurableSet.univ,
Set.univ_inter, volume_pi, Measure.pi_pi, volume_Ioo, sub_neg_eq_add, ← two_mul, Finset.prod_const,
Finset.card_univ, ← Set.indicator_const_mul, ← Set.indicator_comp_right, Function.comp_def, Pi.one_apply, mul_one]
rw [lintegral_mul_const' _ _ (ne_of_beq_false rfl).symm, mul_comm]
erw [setLIntegral_indicator (by convert hm.preimage mixedSpaceOfRealSpace.measurable)]
rw [hA, volume_eq_two_pi_pow_mul_integral_aux hA]
congr 1
refine setLIntegral_congr (ae_eq_set_inter (by rfl) (Measure.ae_eq_set_pi fun w _ ↦ ?_))
split_ifs
exacts [ae_eq_rfl, Ioi_ae_eq_Ici]
·
exact
(Measurable.mul (by fun_prop) <|
measurable_const.indicator <| hm.preimage (measurable_polarSpaceCoord_symm K)).aemeasurable
