awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
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)
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)
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1} =
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
have 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)
Tactic: simp_rw [← toLp_neg, ← toLp_add, ← toLp_smul, eq_norm] at eq_zero nm_zero nm_neg nm_add nm_smul
Cleared hypotheses: nm_zero, eq_zero, nm_neg, nm_add, nm_smul
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
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)
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)
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1} =
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
have nm_smul₁ : ∀ (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
Cleared hypotheses: nm_zero, eq_zero, nm_neg, nm_add, nm_smul
-- 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 : ι, 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)
⊢ 0 < p
have linarith : p ≤ 0 → -1 + (1 - p) + (p - 0) = 0
Tactic: linarith
-- 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 : ι, 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)
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1} =
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(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 : ι, 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)
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 ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
have h₃ : (π * Real.Gamma (2 / 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 : ι, 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)
h : ∀ (x : ι → ℂ), LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1 ↔ HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < 1
h₃ :
  (π * Real.Gamma (2 / 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 ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
have h₄ : HMul.hMul (α := ℝ) 2 (↑(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 : ι, 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)
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 : ι, 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)
⊢ (π * Real.Gamma (2 / p + 1)) ^ card ι =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℂ) ↦
      rexp (-HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) ^ p)
have h : (π * Real.Gamma (2 / 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, Real.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 : ι, 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)
⊢ (π * Real.Gamma (2 / p + 1)) ^ card ι =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℂ) ↦ ∏ x_1 : ι, rexp (-‖x x_1‖ ^ p)
have h : (π * Real.Gamma (2 / 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 : ℂ => Real.exp (- ‖x‖ ^ p),
      Complex.integral_exp_neg_rpow hp]
-- 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 : ι, 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)
h :
  (π * Real.Gamma (2 / p + 1)) ^ card ι =
    HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-‖x‖ ^ p)) (card ι)
⊢ (π * Real.Gamma (2 / p + 1)) ^ card ι =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℂ) ↦ ∏ x_1 : ι, rexp (-‖x x_1‖ ^ p)
have h₃ : (π * Real.Gamma (2 / p + 1)) ^ card ι = (π * Real.Gamma (2 / p + 1)) ^ card ι
Tactic: rw [integral_fintype_prod_volume_eq_pow fun x : ℂ => Real.exp (- ‖x‖ ^ p),
      Complex.integral_exp_neg_rpow hp]
-- 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 : ι, 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)
⊢ HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℂ)) : ℝ) / p + 1
have h : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, finrank ℝ ℂ) : ℝ) / p + 1
Tactic: rw [finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
      Nat.cast_mul, Nat.cast_ofNat, Fintype.card, mul_comm]
-- 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 : ι, 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)
h : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, finrank ℝ ℂ) : ℝ) / p + 1
⊢ HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℂ)) : ℝ) / p + 1
have h₃ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, 2) : ℝ) / p + 1
Tactic: rw [finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
      Nat.cast_mul, Nat.cast_ofNat, Fintype.card, mul_comm]
-- 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 : ι, 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)
h : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, finrank ℝ ℂ) : ℝ) / p + 1
h₃ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, 2) : ℝ) / p + 1
⊢ HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℂ)) : ℝ) / p + 1
have h₄ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
  (↑(HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := ι) Finset.univ) 2) : ℝ) / p + 1
Tactic: rw [finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
      Nat.cast_mul, Nat.cast_ofNat, Fintype.card, mul_comm]
-- 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 : ι, 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)
h : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, finrank ℝ ℂ) : ℝ) / p + 1
h₃ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, 2) : ℝ) / p + 1
h₄ :
  HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
    (↑(HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := ι) Finset.univ) 2) : ℝ) / p + 1
⊢ HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℂ)) : ℝ) / p + 1
have h₅ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(Finset.card.{u_1} (α := ι) Finset.univ * 2) : ℝ) / p + 1
Tactic: rw [finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
      Nat.cast_mul, Nat.cast_ofNat, Fintype.card, mul_comm]