-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySum_volume :
    volume (convexBodySum K B) = (convexBodySumFactor K) * (.ofReal B) ^ (finrank ℚ K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ volume (convexBodySum K B) = ENNReal.ofReal B ^ finrank ℚ K * ↑(convexBodySumFactor K)

Tactic:
convert addHaar_smul volume B (convexBodySum K 1)

Result:
case h.e'_2.h.e'_6
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ convexBodySum K B = B • convexBodySum K 1

case h.e'_3.h.e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal |B ^ finrank ℝ (mixedSpace K)|

case h.e'_3.h.e'_6
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ ↑(convexBodySumFactor K) = volume (convexBodySum K 1)

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ENNReal.ofReal
      ((∫ (x : mixedSpace K), rexp (-convexBodySumFun x ^ 1)) / Gamma (↑(finrank ℝ (mixedSpace K)) / 1 + 1)) =
    ↑(convexBodySumFactor K)

Tactic:
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]

Result:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ENNReal.ofReal (∫ (x : mixedSpace K), rexp (-convexBodySumFun x)) / ↑(finrank ℚ K).factorial =
    ↑(convexBodySumFactor K)

Proof state:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : B ≤ 0
⊢ finrank ℚ K ≠ 0

Tactic:
exact finrank_pos.ne'

Result:
no goals

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ volume {x | convexBodySumFun x < 1} = ↑(convexBodySumFactor K)

Tactic:
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]

Result:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ENNReal.ofReal
      ((∫ (x : mixedSpace K), rexp (-convexBodySumFun x ^ 1)) / Gamma (↑(finrank ℝ (mixedSpace K)) / 1 + 1)) =
    ↑(convexBodySumFactor K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) =
    (∫ (x : { w // w.IsReal } → ℝ), ∏ w : { w // w.IsReal }, rexp (-‖x w‖)) *
      ∫ (x : { w // w.IsComplex } → ℂ), ∏ w : { w // w.IsComplex }, rexp (-2 * ‖x w‖)

Tactic:
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]

Result:
no goals

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) = 2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K

Tactic:
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_eq_pow _ (fun x => exp (- ‖x‖)), integral_fintype_prod_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]

Result:
no goals

Proof state:
case h.e'_2.h.e'_6
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ convexBodySum K B = B • convexBodySum K 1

Tactic:
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]

Result:
no goals