awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ 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 : ι, HPow.hPow (α := ℝ) |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)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1} =
    ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have h : ∀ (x : ι → ℝ), LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1 ↔ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < 1
Tactic: convert!
    (measure_lt_one_eq_integral_div_gamma (volume : Measure (ι → ℝ)) (g := fun x =>
      (∑ i, |x i| ^ p) ^ (1 / p)) nm_zero nm_neg nm_add (eq_zero _).mp (fun r x => nm_smul r x)
      (by linarith : 0 < p)) using 4
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ 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 : ι, HPow.hPow (α := ℝ) |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)
h : ∀ (x : ι → ℝ), LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1 ↔ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < 1
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1} =
    ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have h₃ : (2 * Gamma (1 / p + 1)) ^ card ι =
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℝ) ↦
    rexp (-HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) ^ p)
Tactic: convert!
    (measure_lt_one_eq_integral_div_gamma (volume : Measure (ι → ℝ)) (g := fun x =>
      (∑ i, |x i| ^ p) ^ (1 / p)) nm_zero nm_neg nm_add (eq_zero _).mp (fun r x => nm_smul r x)
      (by linarith : 0 < p)) using 4
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ 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 : ι, HPow.hPow (α := ℝ) |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)
h : ∀ (x : ι → ℝ), LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1 ↔ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < 1
h₃ :
  (2 * Gamma (1 / p + 1)) ^ card ι =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℝ) ↦
      rexp (-HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) ^ p)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1} =
    ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have h₄ : (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℝ)) : ℝ) / p + 1
Tactic: convert!
    (measure_lt_one_eq_integral_div_gamma (volume : Measure (ι → ℝ)) (g := fun x =>
      (∑ i, |x i| ^ p) ^ (1 / p)) nm_zero nm_neg nm_add (eq_zero _).mp (fun r x => nm_smul r x)
      (by linarith : 0 < p)) using 4
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ 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 : ι, HPow.hPow (α := ℝ) |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)
x : ι → ℝ
⊢ LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1 ↔ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < 1
have rw : LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
Tactic: rw [rpow_lt_one_iff' _ (one_div_pos.mpr h₁)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ 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 : ι, HPow.hPow (α := ℝ) |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)
⊢ (2 * Gamma (1 / p + 1)) ^ card ι =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℝ) ↦
      rexp (-HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) ^ p)
have h : (2 * Gamma (1 / p + 1)) ^ card ι =
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℝ) ↦ ∏ x_1 : ι, rexp (-|x x_1| ^ p)
Tactic: simp_rw [← rpow_mul (h₂ _), div_mul_cancel₀ _ (ne_of_gt h₁), Real.rpow_one,
      ← Finset.sum_neg_distrib, exp_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ 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 : ι, HPow.hPow (α := ℝ) |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)
⊢ (2 * Gamma (1 / p + 1)) ^ card ι =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℝ) ↦ ∏ x_1 : ι, rexp (-|x x_1| ^ p)
have h : (2 * Gamma (1 / p + 1)) ^ card ι =
  HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-|x| ^ p)) (card ι)
Tactic: rw [integral_fintype_prod_volume_eq_pow fun x : ℝ => exp (- |x| ^ p), integral_comp_abs
      (f := fun x => exp (- x ^ p)), integral_exp_neg_rpow h₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ 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 : ι, HPow.hPow (α := ℝ) |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)
h :
  (2 * Gamma (1 / p + 1)) ^ card ι =
    HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-|x| ^ p)) (card ι)
⊢ (2 * Gamma (1 / p + 1)) ^ card ι =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℝ) ↦ ∏ x_1 : ι, rexp (-|x x_1| ^ p)
have h₃ : (2 * Gamma (1 / p + 1)) ^ card ι =
  HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (x : ℝ) ↦ rexp (-x ^ p)) ^
    card ι
Tactic: rw [integral_fintype_prod_volume_eq_pow fun x : ℝ => exp (- |x| ^ p), integral_comp_abs
      (f := fun x => exp (- x ^ p)), integral_exp_neg_rpow h₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ 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 : ι, HPow.hPow (α := ℝ) |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)
h :
  (2 * Gamma (1 / p + 1)) ^ card ι =
    HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-|x| ^ p)) (card ι)
h₃ :
  (2 * Gamma (1 / p + 1)) ^ card ι =
    HMul.hMul (α := ℝ) 2
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (x : ℝ) ↦ rexp (-x ^ p)) ^
      card ι
⊢ (2 * Gamma (1 / p + 1)) ^ card ι =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℝ) ↦ ∏ x_1 : ι, rexp (-|x x_1| ^ p)
have h₄ : (2 * Gamma (1 / p + 1)) ^ card ι = (2 * Gamma (1 / p + 1)) ^ card ι
Tactic: rw [integral_fintype_prod_volume_eq_pow fun x : ℝ => exp (- |x| ^ p), integral_comp_abs
      (f := fun x => exp (- x ^ p)), integral_exp_neg_rpow h₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ 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 : ι, HPow.hPow (α := ℝ) |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)
⊢ (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℝ)) : ℝ) / p + 1
have h : (↑(card ι) : ℝ) / p + 1 = (↑(card ι) : ℝ) / p + 1
Tactic: rw [finrank_fintype_fun_eq_card]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
Tactic: have h₁ (x : ι → ℝ) : 0 ≤ ∑ i, |x i| ^ p := by positivity
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
Tactic: have h₂ : ∀ x : ι → ℝ, 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p) := fun x => rpow_nonneg (h₁ x) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have inl : ∀ (hr : r ≤ 0),
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ 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_gt r 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
inl :
  ∀ (hr : r ≤ 0),
    ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
        {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
      ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have inr : ∀ (hr : 0 < r),
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ 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_gt r 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : r ≤ 0
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} ∅
have h : ∀ (x : ι → ℝ),
  Membership.mem (γ := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} x ↔
    Membership.mem (γ := Set (ι → ℝ)) ∅ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : r ≤ 0
x : ι → ℝ
⊢ Membership.mem (γ := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} x ↔
    Membership.mem (γ := Set (ι → ℝ)) ∅ x
have h : ∀ (hx : Membership.mem (γ := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} x),
  Membership.mem (γ := Set (ι → ℝ)) ∅ x
Tactic: refine ⟨fun hx => ?_, fun hx => hx.elim⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : r ≤ 0
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have this : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} ∅
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : r ≤ 0
this : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} ∅
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have inl : ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) ∅ =
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : r ≤ 0
this : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} ∅
inl :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) ∅ =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have inl₁ : 0 = 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : r ≤ 0
this : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} ∅
inl :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) ∅ =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
inl₁ :
  0 = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have inl₂ : 0 =
  HPow.hPow (α := ℝ≥0∞) 0 (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : r ≤ 0
this : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} ∅
inl :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) ∅ =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
inl₁ :
  0 = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
inl₂ :
  0 =
    HPow.hPow (α := ℝ≥0∞) 0 (card ι) *
      ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have inl₃ : 0 = 0 * 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]