-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
theorem MeasureTheory.volume_sum_rpow_lt [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) (r : ℝ) :
    volume {x : ι → ℝ | (∑ i, |x i| ^ p) ^ (1 / p) < r} = (.ofReal r) ^ card ι *
      .ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (card ι / p + 1))

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : 0 < r
⊢ 0 < p

Tactic:
linarith

Result:
no goals

Proof state:
case inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
this : {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} = ∅
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
rw [this, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow Fin.pos'.ne', zero_mul]

Result:
no goals

Proof state:
case inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have : {x : ι → ℝ | (∑ i, |x i| ^ p) ^ (1 / p) < r} = ∅ := by
  ext x
  refine ⟨fun hx => ?_, fun hx => hx.elim⟩
  exact not_le.mpr (lt_of_lt_of_le (Set.mem_setOf.mp hx) hr) (h₂ x)

Result:
case inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
this : {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} = ∅
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have h₂ : ∀ x : ι → ℝ, 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p) := fun x => rpow_nonneg (h₁ x) _

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Proof state:
case h.e'_2.h.e'_6
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : 0 < r
⊢ {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} = r • {x | ∑ i : ι, |x i| ^ p < 1}

Tactic:
simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
  smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv,
  inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr),
  inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff
  (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul
  (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]

Result:
no goals

Proof state:
case inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : 0 < r
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal (r ^ finrank ℝ (ι → ℝ)) * volume {x | ∑ i : ι, |x i| ^ p < 1}

Tactic:
convert addHaar_smul_of_nonneg volume (le_of_lt hr) {x : ι → ℝ | ∑ i, |x i| ^ p < 1} using 2

Result:
case h.e'_2.h.e'_6
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : 0 < r
⊢ {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} = r • {x | ∑ i : ι, |x i| ^ p < 1}

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have h₁ (x : ι → ℝ) : 0 ≤ ∑ i, |x i| ^ p := by positivity

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
x : ι → ℝ
⊢ 0 ≤ ∑ i : ι, |x i| ^ p

Tactic:
positivity

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
obtain hr | hr := le_or_lt r 0

Result:
case inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

case inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : 0 < r
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Proof state:
case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
x : ι → ℝ
⊢ x ∈ {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} ↔ x ∈ ∅

Tactic:
refine ⟨fun hx => ?_, fun hx => hx.elim⟩

Result:
case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
x : ι → ℝ
hx : x ∈ {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r}
⊢ x ∈ ∅

Proof state:
case inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : 0 < r
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
rw [← volume_sum_rpow_lt_one _ hp, ← ofReal_pow (le_of_lt hr), ← finrank_pi ℝ]

Result:
case inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : 0 < r
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal (r ^ finrank ℝ (ι → ℝ)) * volume {x | ∑ i : ι, |x i| ^ p < 1}