-- 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
⊢ (∫ (x : ℝ), rexp (-|x|)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K =
    (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K * (π * 2 ^ (-2 / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K

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

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (2 * ∫ (x : ℝ) in Set.Ioi 0, rexp (-x)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K =
    (2 * ∫ (x : ℝ) in Set.Ioi 0, rexp (-x ^ 1)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖ ^ 1)) ^ nrComplexPlaces K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (2 * ∫ (x : ℝ) in Set.Ioi 0, rexp (-x)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K =
    (2 * ∫ (x : ℝ) in Set.Ioi 0, rexp (-x ^ 1)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖ ^ 1)) ^ nrComplexPlaces K

Tactic:
simp_rw [Real.rpow_one]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ -2 + 1 = -1

Tactic:
norm_num

Result:
no goals

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) = ↑(convexBodySumFactor K) * ENNReal.ofReal B ^ finrank ℚ K

Tactic:
rw [mul_comm]

Result:
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)

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

Tactic:
rw [integral_fintype_prod_eq_pow _ (fun x => exp (- ‖x‖)), integral_fintype_prod_eq_pow _
  (fun x => exp (- 2 * ‖x‖))]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (∫ (x : ℝ), rexp (-‖x‖)) ^ card { w // w.IsReal } * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ card { w // w.IsComplex } =
    (∫ (x : ℝ), rexp (-|x|)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K

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

Tactic:
simp_rw [norm_eq_abs]

Result:
no goals

Proof state:
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)

Tactic:
exact this.symm

Result:
no goals

Proof state:
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)|

Tactic:
rw [abs_pow, ofReal_pow (abs_nonneg _), abs_eq_self.mpr (le_of_lt hB),
  mixedEmbedding.finrank]

Result:
no goals

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

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

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

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

Tactic:
rw [convexBodySum_volume_eq_zero_of_le_zero K hB, ofReal_eq_zero.mpr hB, zero_pow, mul_zero]

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

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

Tactic:
positivity

Result:
no goals

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

Tactic:
positivity

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) = 2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K
⊢ ENNReal.ofReal (∫ (x : mixedSpace K), rexp (-convexBodySumFun x)) / ↑(finrank ℚ K).factorial =
    ↑(convexBodySumFactor K)

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

Result:
no goals

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

Tactic:
obtain hB | hB := le_or_lt B 0

Result:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : B ≤ 0
⊢ volume (convexBodySum K B) = ↑(convexBodySumFactor K) * ENNReal.ofReal B ^ finrank ℚ K

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

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)) / ↑(finrank ℚ K).factorial =
    ↑(convexBodySumFactor K)

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

Result:
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

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K * (π * 2 ^ (-2 / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K =
    2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K

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