English
The modified convex body LT' has a computable volume given by a product formula similar to LT.
Русский
У модифицированного выпуклого тела LT' вычисимый объем задаётся по формуле произведения, сходной с LT.
LaTeX
$$$$ \operatorname{vol}(\operatorname{convexBodyLT'}(K,f,w_0)) = \text{(product formula similar to LT)} $$$$
Lean4
/-- The volume of `(ConvexBodyLt K f)` where `convexBodyLT K f` is the set of points `x`
such that `‖x w‖ < f w` for all infinite places `w`. -/
theorem convexBodyLT_volume : volume (convexBodyLT K f) = (convexBodyLTFactor K) * ∏ w, (f w) ^ (mult w) := by
calc
_ =
(∏ x : { w // InfinitePlace.IsReal w }, ENNReal.ofReal (2 * (f x.val))) *
∏ x : { w // InfinitePlace.IsComplex w }, ENNReal.ofReal (f x.val) ^ 2 * NNReal.pi :=
by simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]
_ =
((2 : ℝ≥0) ^ nrRealPlaces K * (∏ x : { w // InfinitePlace.IsReal w }, ENNReal.ofReal (f x.val))) *
((∏ x : { w // IsComplex w }, ENNReal.ofReal (f x.val) ^ 2) * NNReal.pi ^ nrComplexPlaces K) :=
by
simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const, Finset.card_univ,
ofReal_ofNat, ofReal_coe_nnreal, coe_ofNat]
_ =
(convexBodyLTFactor K) *
((∏ x : { w // InfinitePlace.IsReal w }, .ofReal (f x.val)) *
(∏ x : { w // IsComplex w }, ENNReal.ofReal (f x.val) ^ 2)) :=
by
simp_rw [convexBodyLTFactor, coe_mul, ENNReal.coe_pow]
ring
_ = (convexBodyLTFactor K) * ∏ w, (f w) ^ (mult w) := by
simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finset_prod, mult_isReal, mult_isComplex, pow_one, ENNReal.coe_pow,
ofReal_coe_nnreal]
