Lean4
theorem convexBodySum_volume : volume (convexBodySum K B) = (convexBodySumFactor K) * (.ofReal B) ^ (finrank ℚ K) :=
by
obtain hB | hB := le_or_gt B 0
· rw [convexBodySum_volume_eq_zero_of_le_zero K hB, ofReal_eq_zero.mpr hB, zero_pow, mul_zero]
exact finrank_pos.ne'
· suffices volume (convexBodySum K 1) = (convexBodySumFactor K)
by
rw [mul_comm]
convert addHaar_smul volume B (convexBodySum K 1)
·
simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_setOf_eq, convexBodySumFun, normAtPlace_smul,
abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc, ← Finset.mul_sum,
inv_mul_le_iff₀ hB, mul_one]
· rw [abs_pow, ofReal_pow (abs_nonneg _), abs_eq_self.mpr (le_of_lt hB), mixedEmbedding.finrank]
· exact this.symm
rw [MeasureTheory.measure_le_eq_lt _ ((convexBodySumFun_eq_zero_iff 0).mpr rfl) convexBodySumFun_neg
convexBodySumFun_add_le (fun hx => (convexBodySumFun_eq_zero_iff _).mp hx)
(fun r x => le_of_eq (convexBodySumFun_smul r x))]
rw [measure_lt_one_eq_integral_div_gamma (g := fun x : (mixedSpace K) => convexBodySumFun x) volume
((convexBodySumFun_eq_zero_iff 0).mpr rfl) convexBodySumFun_neg convexBodySumFun_add_le
(fun hx => (convexBodySumFun_eq_zero_iff _).mp hx) (fun r x => le_of_eq (convexBodySumFun_smul r x))
zero_lt_one]
simp_rw [mixedEmbedding.finrank, div_one, Gamma_nat_eq_factorial,
ofReal_div_of_pos (Nat.cast_pos.mpr (Nat.factorial_pos _)), Real.rpow_one, ofReal_natCast]
suffices ∫ x : mixedSpace K, exp (-convexBodySumFun x) = (2 : ℝ) ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K by
rw [this, convexBodySumFactor, ofReal_mul (by positivity), ofReal_pow zero_le_two, ofReal_pow (by positivity),
ofReal_div_of_pos zero_lt_two, ofReal_ofNat, ← NNReal.coe_real_pi, ofReal_coe_nnreal,
coe_div (Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)), coe_mul, coe_pow, coe_pow, coe_ofNat,
coe_div two_ne_zero, coe_ofNat, coe_natCast]
calc
_ =
(∫ x : { w : InfinitePlace K // IsReal w } → ℝ, ∏ w, exp (-‖x w‖)) *
(∫ x : { w : InfinitePlace K // IsComplex w } → ℂ, ∏ w, exp (-2 * ‖x w‖)) :=
by
simp_rw [convexBodySumFun_apply', neg_add, ← neg_mul, Finset.mul_sum, ← Finset.sum_neg_distrib, exp_add,
exp_sum, ← integral_prod_mul, volume_eq_prod]
_ = (∫ x : ℝ, exp (-|x|)) ^ nrRealPlaces K * (∫ x : ℂ, Real.exp (-2 * ‖x‖)) ^ nrComplexPlaces K :=
by
rw [integral_fintype_prod_volume_eq_pow (fun x => exp (-‖x‖)),
integral_fintype_prod_volume_eq_pow (fun x => exp (-2 * ‖x‖))]
simp_rw [norm_eq_abs]
_ =
(2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K *
(π * (2 : ℝ) ^ (-(2 : ℝ) / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K :=
by
rw [integral_comp_abs (f := fun x => exp (-x)), ← integral_exp_neg_rpow zero_lt_one, ←
Complex.integral_exp_neg_mul_rpow le_rfl zero_lt_two]
simp_rw [Real.rpow_one]
_ = (2 : ℝ) ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K := by
simp_rw [div_one, one_add_one_eq_two, Gamma_add_one two_ne_zero, Gamma_two, mul_one, mul_assoc, ←
Real.rpow_add_one two_ne_zero, show (-2 : ℝ) + 1 = -1 by norm_num, Real.rpow_neg_one, div_eq_mul_inv]
