awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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
h₅ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(Finset.card.{u_1} (α := ι) Finset.univ * 2) : ℝ) / p + 1
h₆ :
  HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
    HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) (↑2 : ℝ) / p + 1
h₇ :
  HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
    HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) 2 / p + 1
h₈ :
  HMul.hMul (α := ℝ) 2 (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) / p + 1 =
    HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) 2 / p + 1
h₉ h₁₀ :
  HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) 2 / p + 1 =
    HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) 2 / p + 1
⊢ HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℂ)) : ℝ) / 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]

Premises used: Nat.cast_ofNat, Fintype.card, Module.finrank_pi_fintype, Nat.cast_mul, Complex.finrank_real_complex, mul_comm, smul_eq_mul, Finset.sum_const
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
x : ι → ℂ
⊢ LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ p)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
⊢ ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ p)

Tactic:
have h₁ (x : ι → ℂ) : 0 ≤ ∑ i, ‖x i‖ ^ p := by positivity
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ p)
⊢ ∀ (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) _
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 ^ (2 * card ι) *
        ENNReal.ofReal
          ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
inr :
  ∀ (hr : 0 < r),
    ((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))
⊢ ((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:
obtain hr | hr := le_or_gt r 0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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
h :
  ∀ (x : ι → ℂ),
    Membership.mem (γ := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} x ↔
      Membership.mem (γ := Set (ι → ℂ)) ∅ x
⊢ Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} ∅

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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

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

Premises used: False.elim, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι → ℂ
h :
  ∀ (hx : Membership.mem (γ := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} x),
    Membership.mem (γ := Set (ι → ℂ)) ∅ x
⊢ 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⟩
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι → ℂ
hx : Membership.mem (γ := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} x
⊢ Membership.mem (γ := Set (ι → ℂ)) ∅ x

Tactic:
not_le.mpr (lt_of_lt_of_le (Set.mem_setOf.mp hx) hr) (h₂ x)

Premises used: not_le, Iff.mpr, Set.Mem, Set.mem_setOf, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι → ℂ
hx : Membership.mem (γ := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} x
⊢ Membership.mem (γ := Set (ι → ℂ)) ∅ x

Tactic:
exact not_le.mpr (lt_of_lt_of_le (Set.mem_setOf.mp hx) hr) (h₂ x)

Premises used: not_le, Iff.mpr, Set.mem_setOf, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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} ∅

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)
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
inl₁ :
  0 =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
inl₂ :
  0 =
    HPow.hPow (α := ℝ≥0∞) 0 (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
inl₃ :
  0 =
    0 *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
inl₄ inl₅ : Eq (α := ℝ≥0∞) 0 0
⊢ ((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 [this, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow Fin.pos'.ne', zero_mul]

Premises used: Iff.mpr, MulZeroClass.zero_mul, MeasureTheory.measure_empty, LT.lt.ne', Fin.pos', ENNReal.zero_eq_ofReal, zero_pow
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : 0 < r
inr :
  ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ (2 * card ι)))
      (((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1} :
        ℝ≥0∞)
⊢ ((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 [← Complex.volume_sum_rpow_lt_one _ hp, ← ENNReal.ofReal_pow (le_of_lt hr)]

Premises used: le_of_lt, Complex.volume_sum_rpow_lt_one, ENNReal.ofReal_pow
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : 0 < r
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      (HSMul.hSMul (β := Set (ι → ℂ)) r {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1}) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℂ)))
      (((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1} :
        ℝ≥0∞)

Tactic:
addHaar_smul_of_nonneg volume (le_of_lt hr) {x : ι → ℂ | ∑ i, ‖x i‖ ^ p < 1}

Premises used: Norm.norm, Finset.univ, setOf, le_of_lt, HPow.hPow, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.addHaar_smul_of_nonneg, LT.lt, OfNat.ofNat, Finset.sum
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : 0 < r
h :
  {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℂ)) r {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1}
h₃ : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℂ))
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ (2 * card ι)))
      (((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1} :
        ℝ≥0∞)

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

Premises used: Norm.norm, Finset.univ, setOf, le_of_lt, HPow.hPow, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.addHaar_smul_of_nonneg, LT.lt, OfNat.ofNat, Finset.sum
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : 0 < r
linarith : p ≤ 0 → -1 + (1 - p) + (p - 0) = 0
⊢ 0 < p

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : 0 < r
h : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (HPow.hPow (β := ℕ) r (∑ i : ι, finrank ℝ ℂ))
h₃ : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (HPow.hPow (β := ℕ) r (∑ x : ι, 2))
h₄ :
  ENNReal.ofReal (r ^ (2 * card ι)) =
    ENNReal.ofReal (r ^ HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := ι) Finset.univ) 2)
h₅ : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ (Finset.card.{u_1} (α := ι) Finset.univ * 2))
h₆ : ENNReal.ofReal (r ^ (card ι * 2)) = ENNReal.ofReal (r ^ (Finset.card.{u_1} (α := ι) Finset.univ * 2))
⊢ ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℂ))

Tactic:
simp_rw [finrank_pi_fintype ℝ, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
        mul_comm, Fintype.card]

Premises used: Real, Fintype.card, Module.finrank_pi_fintype, Complex.finrank_real_complex, mul_comm, smul_eq_mul, Finset.sum_const
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
x : ι → ℂ
⊢ Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) =
    HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)

Tactic:
simp [PiLp.norm_eq_sum (f := toLp (.ofReal p) x) (this.symm ▸ h₁), this]

Premises used: ENNReal.ofReal, WithLp.toLp, PiLp.norm_eq_sum
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
⊢ ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)

Tactic:
have eq_norm (x : ι → ℂ) : ‖toLp (.ofReal p) x‖ = (∑ i, ‖x i‖ ^ p) ^ (1 / p) := by
    simp [PiLp.norm_eq_sum (f := toLp (.ofReal p) x) (this.symm ▸ h₁), this]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this : (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)
⊢ Fact (1 ≤ ENNReal.ofReal p)

Tactic:
have : Fact (1 ≤ ENNReal.ofReal p) := fact_iff.mpr (ENNReal.ofReal_one ▸ (ofReal_le_ofReal hp))
-- 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)
⊢ Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) 0) = 0

Tactic:
have nm_zero : ‖toLp (.ofReal p) (0 : ι → ℂ)‖ = 0 := norm_zero
-- 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
⊢ ∀ (x : ι → ℂ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0

Tactic:
have eq_zero (x : ι → ℂ) : ‖toLp (.ofReal p) x‖ = 0 ↔ x = 0 :=
    norm_eq_zero.trans (toLp_eq_zero _)
-- 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
⊢ ∀ (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)

Tactic:
have nm_neg := fun x : ι → ℂ => norm_neg (toLp (.ofReal p) x)
-- 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)
⊢ ∀ (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)

Tactic:
have nm_add := fun x y : ι → ℂ => norm_add_le (toLp (.ofReal p) x) (toLp (.ofReal p) y)
-- 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)
⊢ ∀ (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)

Tactic:
have nm_smul := fun (r : ℝ) (x : ι → ℂ) =>
    norm_smul_le (β := PiLp (.ofReal p) (fun _ : ι => ℂ)) r (toLp (.ofReal p) x)
-- 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)
⊢ ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) = 0 ↔ x = 0

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
⊢ HPow.hPow (α := ℝ) (∑ i : ι, Norm.norm (E := ℂ) (0 i) ^ p) (1 / p) = 0

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