awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
eq_norm :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℂ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
nm_neg :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x)
nm_add :
  ∀ (x y : ι → ℂ),
    ‖HAdd.hAdd (α := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) (toLp (ENNReal.ofReal p) y)‖ ≤
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) +
        Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) y)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℂ),
    ‖HSMul.hSMul (β := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℂ) r (toLp (ENNReal.ofReal p) x)‖ ≤
      ‖r‖ * Norm.norm (E := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℂ) (toLp (ENNReal.ofReal p) x)
eq_zero₁ : ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) = 0 ↔ x = 0
nm_zero₁ : HPow.hPow (α := ℝ) (∑ i : ι, Norm.norm (E := ℂ) (0 i) ^ p) (1 / p) = 0
⊢ ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖(-x) i‖ ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)

Tactic:
simp_rw [← toLp_neg, ← toLp_add, ← toLp_smul, eq_norm] at eq_zero nm_zero nm_neg nm_add nm_smul

Premises used: WithLp.toLp_smul, WithLp.toLp_neg, WithLp.toLp_add
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
eq_norm :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℂ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
nm_neg :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x)
nm_add :
  ∀ (x y : ι → ℂ),
    ‖HAdd.hAdd (α := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) (toLp (ENNReal.ofReal p) y)‖ ≤
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) +
        Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) y)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℂ),
    ‖HSMul.hSMul (β := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℂ) r (toLp (ENNReal.ofReal p) x)‖ ≤
      ‖r‖ * Norm.norm (E := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℂ) (toLp (ENNReal.ofReal p) x)
eq_zero₁ : ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) = 0 ↔ x = 0
nm_zero₁ : HPow.hPow (α := ℝ) (∑ i : ι, Norm.norm (E := ℂ) (0 i) ^ p) (1 / p) = 0
nm_neg₁ :
  ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖(-x) i‖ ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
⊢ ∀ (x y : ι → ℂ),
    HPow.hPow (α := ℝ) (∑ i : ι, ‖(x + y) i‖ ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i : ι, ‖y i‖ ^ p) (1 / p)

Tactic:
simp_rw [← toLp_neg, ← toLp_add, ← toLp_smul, eq_norm] at eq_zero nm_zero nm_neg nm_add nm_smul

Premises used: WithLp.toLp_smul, WithLp.toLp_neg, WithLp.toLp_add
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
eq_norm :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℂ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
nm_neg :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x)
nm_add :
  ∀ (x y : ι → ℂ),
    ‖HAdd.hAdd (α := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) (toLp (ENNReal.ofReal p) y)‖ ≤
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) +
        Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) y)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℂ),
    ‖HSMul.hSMul (β := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℂ) r (toLp (ENNReal.ofReal p) x)‖ ≤
      ‖r‖ * Norm.norm (E := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℂ) (toLp (ENNReal.ofReal p) x)
eq_zero₁ : ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) = 0 ↔ x = 0
nm_zero₁ : HPow.hPow (α := ℝ) (∑ i : ι, Norm.norm (E := ℂ) (0 i) ^ p) (1 / p) = 0
nm_neg₁ :
  ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖(-x) i‖ ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
nm_add₁ :
  ∀ (x y : ι → ℂ),
    HPow.hPow (α := ℝ) (∑ i : ι, ‖(x + y) i‖ ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i : ι, ‖y i‖ ^ p) (1 / p)
⊢ ∀ (r : ℝ) (x : ι → ℂ),
    HPow.hPow (α := ℝ) (∑ i : ι, ‖(r • x) i‖ ^ p) (1 / p) ≤ ‖r‖ * HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)

Tactic:
simp_rw [← toLp_neg, ← toLp_add, ← toLp_smul, eq_norm] at eq_zero nm_zero nm_neg nm_add nm_smul

Premises used: WithLp.toLp_smul, WithLp.toLp_neg, WithLp.toLp_add
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
eq_norm :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) = 0 ↔ x = 0
nm_zero : HPow.hPow (α := ℝ) (∑ i : ι, Norm.norm (E := ℂ) (0 i) ^ p) (1 / p) = 0
nm_neg :
  ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖(-x) i‖ ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
nm_add :
  ∀ (x y : ι → ℂ),
    HPow.hPow (α := ℝ) (∑ i : ι, ‖(x + y) i‖ ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i : ι, ‖y i‖ ^ p) (1 / p)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℂ),
    HPow.hPow (α := ℝ) (∑ i : ι, ‖(r • x) i‖ ^ p) (1 / p) ≤ ‖r‖ * HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
rw :
  ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
rw₁ rw₂ :
  ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal
        ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1)) =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) ≤ r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))

Tactic:
rw [measure_le_eq_lt _ nm_zero (fun x ↦ nm_neg x) (fun x y ↦ nm_add x y) (eq_zero _).mp
    (fun r x => nm_smul r x), Complex.volume_sum_rpow_lt _ hp]

Premises used: Complex.volume_sum_rpow_lt, MeasureTheory.measure_le_eq_lt, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
inl :
  ∀ (hr : r ≤ 0),
    ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
      ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
inr :
  ∀ (hr : 0 ≤ r),
    ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
      ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))

Tactic:
obtain hr | hr := le_total r 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : r ≤ 0
inl :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) ∅ =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
inl₁ : 0 = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
inl₂ :
  0 = HPow.hPow (α := ℝ≥0∞) 0 (card ι) * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
inl₃ : 0 = 0 * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
inl₄ inl₅ : Eq (α := ℝ≥0∞) 0 0
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))

Tactic:
rw [Metric.ball_eq_empty.mpr hr, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow card_ne_zero,
      zero_mul]

Premises used: Iff.mpr, MulZeroClass.zero_mul, MeasureTheory.measure_empty, Fintype.card_ne_zero, Metric.ball_eq_empty, ENNReal.zero_eq_ofReal, zero_pow
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
this :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ Module.finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι)))
      (((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
rw₁ :
  ENNReal.ofReal (r ^ Module.finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι)) *
      ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1)) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
rw₂ :
  ENNReal.ofReal r ^ Module.finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) *
      ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1)) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
rw₃ rw₄ :
  ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1)) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))

Tactic:
rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]

Premises used: finrank_euclideanSpace, MeasureTheory.Measure.addHaar_ball, ENNReal.ofReal_pow
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
inr :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))

Tactic:
suffices volume (Metric.ball (0 : EuclideanSpace ℝ ι) 1) =
        .ofReal (√π ^ card ι / Gamma (card ι / 2 + 1)) by
      rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
inr :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      (Set.preimage (β := WithLp 2 (ι → ℝ)) (WithLp.toLp 2) (Metric.ball 0 1)) =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))

Tactic:
rw [← (PiLp.volume_preserving_toLp ι).measure_preimage
      measurableSet_ball.nullMeasurableSet]

Premises used: MeasurableSet.nullMeasurableSet, PiLp.volume_preserving_toLp, measurableSet_ball, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
inr :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | LT.lt (α := ℝ) (∑ x_1 : ι, HPow.hPow (β := ℕ) (x x_1) 2) 1} =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      (Set.preimage (β := WithLp 2 (ι → ℝ)) (WithLp.toLp 2) (Metric.ball 0 1)) =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))

Tactic:
simp only [Set.preimage, ball_zero_eq _ zero_le_one, one_pow, Set.mem_setOf_eq]

Premises used: one_pow, Set.mem_setOf_eq, zero_le_one, Set.preimage, EuclideanSpace.ball_zero_eq
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, HPow.hPow (β := ℝ) |x i| 2) 1} =
    ENNReal.ofReal ((2 * Gamma (1 / 2 + 1)) ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))

Tactic:
volume_sum_rpow_lt_one ι one_le_two

Premises used: one_le_two, MeasureTheory.volume_sum_rpow_lt_one
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
h :
  ∀ (x : ι → ℝ),
    LT.lt (α := ℝ) (∑ x_1 : ι, HPow.hPow (β := ℕ) (x x_1) 2) 1 ↔ LT.lt (α := ℝ) (∑ i : ι, HPow.hPow (β := ℝ) |x i| 2) 1
h₁ : √π = 2 * Gamma (1 / 2 + 1)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | LT.lt (α := ℝ) (∑ x_1 : ι, HPow.hPow (β := ℕ) (x x_1) 2) 1} =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))

Tactic:
convert! volume_sum_rpow_lt_one ι one_le_two using 4

Premises used: one_le_two, MeasureTheory.volume_sum_rpow_lt_one
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
x_1 : ι → ℝ
⊢ LT.lt (α := ℝ) (∑ x : ι, HPow.hPow (β := ℕ) (x_1 x) 2) 1 ↔ LT.lt (α := ℝ) (∑ i : ι, HPow.hPow (β := ℝ) |x_1 i| 2) 1

Tactic:
simp [sq_abs]

Premises used: sq_abs
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ 1 / 2 ≠ 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
h : √π = 2 * (1 / 2 * Gamma (1 / 2))
h₁ : √π = 2 * (1 / 2 * √π)
h₂ : √π = 2 * (1 / 2) * √π
h₃ : √π = 1 * √π
h₄ h₅ : √π = √π
⊢ √π = 2 * Gamma (1 / 2 + 1)

Tactic:
rw [Gamma_add_one (by simp), Gamma_one_half_eq, ← mul_assoc, mul_div_cancel₀ _
        two_ne_zero, one_mul]

Premises used: mul_assoc, Real.Gamma_one_half_eq, Real.Gamma_add_one, mul_div_cancel₀, two_ne_zero, one_mul
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
rw :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
rw₁ rw₂ :
  ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1)) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.closedBall x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, EuclideanSpace.volume_ball]

Premises used: EuclideanSpace.volume_ball, MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
x : E
r : ℝ
rw :
  (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
      ((⇑(LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ E))) :
          (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) ⁻¹'
        ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))

Tactic:
rw [← ((stdOrthonormalBasis ℝ E).measurePreserving_repr_symm).measure_preimage
      measurableSet_ball.nullMeasurableSet]

Premises used: Real, MeasurableSet.nullMeasurableSet, OrthonormalBasis.measurePreserving_repr_symm, measurableSet_ball, MeasureTheory.MeasurePreserving.measure_preimage, stdOrthonormalBasis
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
x : E
r : ℝ
⊢ Nonempty (Fin (finrank ℝ E))

Tactic:
have : Nonempty (Fin (finrank ℝ E)) := Fin.pos_iff_nonempty.mp finrank_pos
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
x : E
r : ℝ
this : Nonempty (Fin (finrank ℝ E))
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
      (ball
          (((OrthonormalBasis.repr (stdOrthonormalBasis ℝ E) : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) =
    ENNReal.ofReal r ^ Fintype.card (Fin (finrank ℝ E)) *
      ENNReal.ofReal
        (√π ^ Fintype.card (Fin (finrank ℝ E)) /
          Gamma (HDiv.hDiv (α := ℝ) (↑(Fintype.card (Fin (finrank ℝ E))) : ℝ) 2 + 1))

Tactic:
have := EuclideanSpace.volume_ball (Fin (finrank ℝ E)) ((stdOrthonormalBasis ℝ E).repr x) r
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
x : E
r : ℝ
this_1 : Nonempty (Fin (finrank ℝ E))
this :
  (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
      (ball
          (((OrthonormalBasis.repr (stdOrthonormalBasis ℝ E) : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) =
    ENNReal.ofReal r ^ Fintype.card (Fin (finrank ℝ E)) *
      ENNReal.ofReal
        (√π ^ Fintype.card (Fin (finrank ℝ E)) /
          Gamma (HDiv.hDiv (α := ℝ) (↑(Fintype.card (Fin (finrank ℝ E))) : ℝ) 2 + 1))
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
      (ball
          (((OrthonormalBasis.repr (stdOrthonormalBasis ℝ E) : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))

Tactic:
simp_rw [Fintype.card_fin] at this

Premises used: Fintype.card_fin
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
x : E
r : ℝ
this_1 : Nonempty (Fin (finrank ℝ E))
this :
  (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
      (ball
          (((OrthonormalBasis.repr (stdOrthonormalBasis ℝ E) : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
      (ball
          (((OrthonormalBasis.repr (stdOrthonormalBasis ℝ E) : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))

Tactic:
this