English
For any suitable K, f, and w0 with IsComplex w, the volume of the LT' convex body is given by the product formula:
Русский
Для подходящего K, функции f и w0 с IsComplex w коэффициент объёма выпуклого тела LT' задаётся формулой произведения:
LaTeX
$$$\\operatorname{volume}(\\mathrm{convexBodyLT'}\\,K\\,f\\,w_0) = \\operatorname{convexBodyLT'Factor}\\,K \\\\; \\cdot \\prod_w f(w)^{\\operatorname{mult}(w)}$$$
Lean4
theorem convexBodyLT'_volume : volume (convexBodyLT' K f w₀) = convexBodyLT'Factor K * ∏ w, (f w) ^ (mult w) :=
by
have vol_box : ∀ B : ℝ≥0, volume {x : ℂ | |x.re| < 1 ∧ |x.im| < B ^ 2} = 4 * B ^ 2 :=
by
intro B
rw [← (Complex.volume_preserving_equiv_real_prod.symm).measure_preimage]
· simp_rw [Set.preimage_setOf_eq, Complex.measurableEquivRealProd_symm_apply]
rw [show
{a : ℝ × ℝ | |a.1| < 1 ∧ |a.2| < B ^ 2} = Set.Ioo (-1 : ℝ) (1 : ℝ) ×ˢ Set.Ioo (-(B : ℝ) ^ 2) ((B : ℝ) ^ 2) by
ext; simp_rw [Set.mem_setOf_eq, Set.mem_prod, Set.mem_Ioo, abs_lt]]
simp_rw [volume_eq_prod, prod_prod, Real.volume_Ioo, sub_neg_eq_add, one_add_one_eq_two, ← two_mul,
ofReal_mul zero_le_two, ofReal_pow (coe_nonneg B), ofReal_ofNat, ofReal_coe_nnreal, ← mul_assoc,
show (2 : ℝ≥0∞) * 2 = 4 by norm_num]
· refine (MeasurableSet.inter ?_ ?_).nullMeasurableSet
· exact measurableSet_lt (measurable_norm.comp Complex.measurable_re) measurable_const
· exact measurableSet_lt (measurable_norm.comp Complex.measurable_im) measurable_const
calc
_ =
(∏ x : { w // InfinitePlace.IsReal w }, ENNReal.ofReal (2 * (f x.val))) *
((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal (f x.val) ^ 2 * pi) * (4 * (f w₀) ^ 2)) :=
by
simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball]
rw [← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
congr 2
· refine Finset.prod_congr rfl (fun w' hw' ↦ ?_)
rw [if_neg (Finset.ne_of_mem_erase hw'), Complex.volume_ball]
· simpa only [ite_true] using vol_box (f w₀)
_ =
((2 : ℝ≥0) ^ nrRealPlaces K * (∏ x : { w // InfinitePlace.IsReal w }, ENNReal.ofReal (f x.val))) *
((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal (f x.val) ^ 2) * ↑pi ^ (nrComplexPlaces K - 1) *
(4 * (f w₀) ^ 2)) :=
by
simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ, ofReal_ofNat, ofReal_coe_nnreal, coe_ofNat]
_ =
convexBodyLT'Factor K * (∏ x : { w // InfinitePlace.IsReal w }, ENNReal.ofReal (f x.val)) *
(∏ x : { w // IsComplex w }, ENNReal.ofReal (f x.val) ^ 2) :=
by
rw [show (4 : ℝ≥0∞) = (2 : ℝ≥0) ^ 2 by norm_num, convexBodyLT'Factor, pow_add, ←
Finset.prod_erase_mul _ _ (Finset.mem_univ w₀), ofReal_coe_nnreal]
simp_rw [coe_mul, ENNReal.coe_pow]
ring
_ = convexBodyLT'Factor 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, mul_assoc]
