awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
h :
  Eq (α := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    ((⇑(LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ E))) :
          (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) ⁻¹'
        ball x r :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (ball
        (((OrthonormalBasis.repr (stdOrthonormalBasis ℝ E) : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
            (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
          x)
        r :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
⊢ (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))

Tactic:
convert! this
-- 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))
⊢ Eq (α := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    ((⇑(LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ E))) :
          (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) ⁻¹'
        ball x r :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (ball
        (((OrthonormalBasis.repr (stdOrthonormalBasis ℝ E) : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
            (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
          x)
        r :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))

Tactic:
simp only [LinearIsometryEquiv.preimage_ball, LinearIsometryEquiv.symm_symm]

Premises used: LinearIsometryEquiv.preimage_ball, LinearIsometryEquiv.symm_symm
-- 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 : 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))
rw₁ rw₂ :
  ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1)) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, InnerProductSpace.volume_ball _]

Premises used: InnerProductSpace.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
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
rw :
  HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 ^ k *
      ENNReal.ofReal (π ^ k / Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k) : ℝ) 2 + 1)) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 ^ k * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))

Tactic:
rw [volume_ball, hk, pow_mul, pow_mul, sq_sqrt pi_nonneg]

Premises used: Real.pi_nonneg, InnerProductSpace.volume_ball, Real.sq_sqrt, pow_mul
-- 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
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
e_a : Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k) : ℝ) 2 + 1) = (↑k ! : ℝ)
⊢ HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 ^ k *
      ENNReal.ofReal (π ^ k / Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k) : ℝ) 2 + 1)) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 ^ k * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))

Tactic:
congr
-- 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
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
⊢ Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k) : ℝ) 2 + 1) = (↑k ! : ℝ)

Tactic:
simp [Gamma_nat_eq_factorial]

Premises used: Real.Gamma_nat_eq_factorial
-- 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
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
rw :
  ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))
rw₁ rw₂ :
  ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / (↑k ! : ℝ)) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_of_dim_even hk x]

Premises used: InnerProductSpace.volume_ball_of_dim_even, 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
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
⊢ Nontrivial E

Tactic:
have : Nontrivial E := Module.nontrivial_of_finrank_pos (R := ℝ) (hk ▸ (2 * k).succ_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
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
rw :
  ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * (√π / Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) 2 + 1))) =
    ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * (HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)))
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ))

Tactic:
rw [volume_ball, hk, pow_succ (√π), pow_mul, sq_sqrt pi_nonneg, mul_div_assoc, mul_div_assoc]

Premises used: Real.pi, Real.pi_nonneg, pow_succ, mul_div_assoc, InnerProductSpace.volume_ball, Real.sq_sqrt, pow_mul, Real.sqrt
-- 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
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
e_a : √π / Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) 2 + 1) = HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)
⊢ ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * (√π / Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) 2 + 1))) =
    ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * (HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)))

Tactic:
congr 3
-- 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
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this_1 : Nontrivial E
this :
  √π / ((↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)) = HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)
⊢ √π / Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) 2 + 1) = HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)

Tactic:
simpa [add_div, add_right_comm, -one_div, Gamma_nat_add_one_add_half]

Premises used: add_right_comm, Real.Gamma_nat_add_one_add_half, one_div, add_div
-- 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
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
e_a :
  √π / ((↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)) = HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)
⊢ √π / Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) 2 + 1) = HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)

Tactic:
suffices √π / (↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)) = 2 ^ (k + 1) / ↑(2 * k + 1)‼ by
    simpa [add_div, add_right_comm, -one_div, Gamma_nat_add_one_add_half]
-- 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
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ √π / ((↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)) = HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)

Tactic:
field
-- 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
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
rw :
  ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ))
rw₁ rw₂ :
  ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ)) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ))
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ))

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_of_dim_odd hk x r]

Premises used: InnerProductSpace.volume_ball_of_dim_odd, MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
x : EuclideanSpace ℝ (Fin 2)
r : ℝ
⊢ Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = HMul.hMul (α := ℕ) 2 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
x : EuclideanSpace ℝ (Fin 2)
r : ℝ
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin 2))) → ℝ≥0∞) (ball x r) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * ENNReal.ofReal π

Tactic:
norm_num [InnerProductSpace.volume_ball_of_dim_even (k := 1) (by simp) x]

Premises used: InnerProductSpace.volume_ball_of_dim_even
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
x : EuclideanSpace ℝ (Fin 2)
r : ℝ
rw :
  (volume : (a : Set (EuclideanSpace ℝ (Fin 2))) → ℝ≥0∞) (ball x r) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * ENNReal.ofReal π
rw₁ rw₂ :
  HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * ENNReal.ofReal π =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * ENNReal.ofReal π
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin 2))) → ℝ≥0∞) (closedBall x r) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * ENNReal.ofReal π

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_fin_two x r]

Premises used: EuclideanSpace.volume_ball_fin_two, MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
x : EuclideanSpace ℝ (Fin 3)
r : ℝ
⊢ Module.finrank ℝ (EuclideanSpace ℝ (Fin 3)) = HMul.hMul (α := ℕ) 2 1 + 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
x : EuclideanSpace ℝ (Fin 3)
r : ℝ
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin 3))) → ℝ≥0∞) (ball x r) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 3 * ENNReal.ofReal (π * 4 / 3)

Tactic:
norm_num [InnerProductSpace.volume_ball_of_dim_odd (k := 1) (by simp) x]

Premises used: InnerProductSpace.volume_ball_of_dim_odd
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
x : EuclideanSpace ℝ (Fin 3)
r : ℝ
rw :
  (volume : (a : Set (EuclideanSpace ℝ (Fin 3))) → ℝ≥0∞) (ball x r) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 3 * ENNReal.ofReal (π * 4 / 3)
rw₁ rw₂ :
  HPow.hPow (β := ℕ) (ENNReal.ofReal r) 3 * ENNReal.ofReal (π * 4 / 3) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 3 * ENNReal.ofReal (π * 4 / 3)
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin 3))) → ℝ≥0∞) (closedBall x r) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 3 * ENNReal.ofReal (π * 4 / 3)

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_fin_three x]

Premises used: EuclideanSpace.volume_ball_fin_three, MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
a : ℂ
r : ℝ
⊢ Module.finrank ℝ ℂ = HMul.hMul (α := ℕ) 2 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
a : ℂ
r : ℝ
⊢ (volume : (a : Set ℂ) → ℝ≥0∞) (Metric.ball a r) = HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * (↑NNReal.pi : ℝ≥0∞)

Tactic:
simp [InnerProductSpace.volume_ball_of_dim_even (k := 1) (by simp) a,
    ← NNReal.coe_real_pi, ofReal_coe_nnreal]

Premises used: NNReal.coe_real_pi, ENNReal.ofReal_coe_nnreal, InnerProductSpace.volume_ball_of_dim_even
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
a : ℂ
r : ℝ
rw : (volume : (a : Set ℂ) → ℝ≥0∞) (Metric.ball a r) = HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * (↑NNReal.pi : ℝ≥0∞)
rw₁ rw₂ :
  HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * (↑NNReal.pi : ℝ≥0∞) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * (↑NNReal.pi : ℝ≥0∞)
⊢ (volume : (a : Set ℂ) → ℝ≥0∞) (Metric.closedBall a r) = HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * (↑NNReal.pi : ℝ≥0∞)

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, Complex.volume_ball]

Premises used: Complex.volume_ball, MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
x : ℕ
⊢ (μ x : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑1 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
refine :
  ∀ (z : E) (hz : ‖z‖ = 1),
    Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪z, x⟫‖}) atTop) atTop (𝓝 0)
⊢ IsTightMeasureSet (Set.range μ)

Tactic:
refine isTightMeasureSet_range_of_tendsto_limsup_measureReal_inner_of_norm_eq_one ℝ
    (fun z hz ↦ ?_) 1 (.of_forall fun _ ↦ by simp)

Premises used: MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_measureReal_inner_of_norm_eq_one, Real, Filter.Eventually.of_forall, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
rw : 0 ≤ 2 * r⁻¹
⊢ -(2 * r⁻¹) ≤ 2 * r⁻¹

Tactic:
rw [neg_le_self_iff]

Premises used: neg_le_self_iff
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
⊢ 0 ≤ 2 * r⁻¹

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
⊢ -(2 * r⁻¹) ≤ 2 * r⁻¹

Tactic:
have hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹ := by rw [neg_le_self_iff]; positivity
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
grw :
  2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤
    2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - charFun (μ n) (t • z)‖
grw₁ grw₂ :
  2⁻¹ * r * ∫ (x : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - charFun (μ n) (x • z)‖ ≤
    2⁻¹ * r * ∫ (x : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - charFun (μ n) (x • z)‖
⊢ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤
    2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - charFun (μ n) (t • z)‖

Tactic:
grw [neg_mul, intervalIntegral.norm_integral_le_integral_norm hr']

Premises used: intervalIntegral.norm_integral_le_integral_norm, neg_mul
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
hbc :
  LE.le (α := ℝ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - charFun (μ n) (t • z)‖) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 2)
⊢ 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - charFun (μ n) (t • z)‖ ≤
    2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 2

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
hbc :
  LE.le (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (x : ℝ) ↦
      ‖1 - charFun (μ n) (x • z)‖)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (x : ℝ) ↦ 2)
⊢ LE.le (α := ℝ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - charFun (μ n) (t • z)‖) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 2)

Tactic:
rw [intervalIntegral.integral_of_le hr', intervalIntegral.integral_of_le hr']

Premises used: intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
funProp : enorm (E := ℝ) 2 ≠ ∞
⊢ @Integrable ℝ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ 2) (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
hbc :
  (ae (F := Measure ℝ) (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    ‖1 - charFun (μ n) (x • z)‖
hbc₁ :
  (ae (F := Measure ℝ) (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))).EventuallyLE (β := ℝ)
    (fun (x : ℝ) ↦ ‖1 - charFun (μ n) (x • z)‖) fun (x : ℝ) ↦ 2
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (x : ℝ) ↦
      ‖1 - charFun (μ n) (x • z)‖)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (x : ℝ) ↦ 2)

Tactic:
refine integral_mono_of_nonneg ?_ (by fun_prop) ?_

Premises used: MeasureTheory.integral_mono_of_nonneg
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
x : ℝ
⊢ LE.le (α := ℝ) (0 x) ((fun (x : ℝ) ↦ ‖1 - charFun (μ n) (x • z)‖) x)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    ‖1 - charFun (μ n) (x • z)‖

Tactic:
exact ae_of_all _ fun _ ↦ by positivity

Premises used: MeasureTheory.ae_of_all