awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
eq :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume
h : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Iic 0) x), f |x| = f (-x)
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f (-x))

Tactic:
refine setIntegral_congr_fun measurableSet_Iic (fun _ hx => ?_)

Premises used: measurableSet_Iic, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
eq :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iic 0) x
⊢ x ≤ 0

Tactic:
hx

Premises used: Set.Mem, Set.Iic
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
eq :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iic 0) x
⊢ x ≤ 0

Tactic:
exact hx
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
eq :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iic 0) x
h h₁ : f (-x) = f (-x)
⊢ f |x| = f (-x)

Tactic:
rw [abs_eq_neg_self.mpr (by exact hx)]

Premises used: Iff.mpr, abs_eq_neg_self
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
eq :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume
_ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f |x|)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
_₁ :
  HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f |x|)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)

Tactic:
calc
      _ = (∫ x in Iic 0, f |x|) + ∫ x in Ioi 0, f |x| := by
        rw [← setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic hf,
          Iic_union_Ioi, restrict_univ]
      _ = 2 * ∫ x in Ioi 0, f x := by
        rw [two_mul, eq]
        congr! 1
        rw [← neg_zero, ← integral_comp_neg_Iic, neg_zero]
        refine setIntegral_congr_fun measurableSet_Iic (fun _ hx => ?_)
        rw [abs_eq_neg_self.mpr (by exact hx)]

Premises used: Set.Ioi, abs, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, MeasureTheory.integral, Set.Iic, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
eq :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
hf : ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
contrapose :
  ∀ (hf : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume),
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
⊢ ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume

Tactic:
contrapose hf
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
eq :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
hf : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume

Tactic:
hf.integrableOn

Premises used: MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
eq :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
hf : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume

Tactic:
exact hf.integrableOn

Premises used: MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
eq :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
hf : ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
⊢ ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume

Tactic:
have : ¬ Integrable (fun x => f |x|) := by
      contrapose hf
      exact hf.integrableOn
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
eq :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
hf : ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
this : ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume
neg :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
neg₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) = HMul.hMul (α := ℝ) 2 0
neg₂ : 0 = HMul.hMul (α := ℝ) 2 0
neg₃ neg₄ : Eq (α := ℝ) 0 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)

Tactic:
rw [← eq, integral_undef hf, integral_undef this, mul_zero]

Premises used: MeasureTheory.integral_undef, MulZeroClass.mul_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
inl :
  ∀ (hE : Subsingleton E),
    (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
      ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
inr :
  ∀ (hE : Nontrivial E),
    (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
      ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))

Tactic:
obtain hE | hE := subsingleton_or_nontrivial E

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
⊢ LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)

Tactic:
have : (0 : ℝ) < finrank ℝ E := Nat.cast_pos.mpr finrank_pos
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (y : ℝ) ↦
          y ^ HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 * Real.exp (-y ^ p)) /
        Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1) *
      (↑(finrank ℝ E) : ℝ) =
    1
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (y : ℝ) ↦
          y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) /
        Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1) *
      (↑(finrank ℝ E) : ℝ) =
    1

Tactic:
simp_rw [← Real.rpow_natCast _ (finrank ℝ E - 1), smul_eq_mul, Nat.cast_sub finrank_pos,
        Nat.cast_one]

Premises used: Real, Nat.cast_sub, HSub.hSub, smul_eq_mul, OfNat.ofNat, Nat.cast_one, Module.finrank_pos, Module.finrank, Real.rpow_natCast
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
linarith :
  HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 ≤ -1 →
    HSub.hSub (α := ℝ) 0 (↑(finrank ℝ E) : ℝ) + (HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 - -1) = 0
⊢ -1 < HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
⊢ 0 < (↑(finrank ℝ E) : ℝ) / p

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
rw :
  1 / p * Real.Gamma ((↑(finrank ℝ E) : ℝ) / p) / ((↑(finrank ℝ E) : ℝ) / p * Real.Gamma ((↑(finrank ℝ E) : ℝ) / p)) *
      (↑(finrank ℝ E) : ℝ) =
    1
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (y : ℝ) ↦
          y ^ HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 * Real.exp (-y ^ p)) /
        Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1) *
      (↑(finrank ℝ E) : ℝ) =
    1

Tactic:
rw [integral_rpow_mul_exp_neg_rpow hp (by linarith), sub_add_cancel,
        Real.Gamma_add_one (ne_of_gt (by positivity))]

Premises used: integral_rpow_mul_exp_neg_rpow, ne_of_gt, Real.Gamma_add_one, sub_add_cancel
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
⊢ 1 / p * Real.Gamma ((↑(finrank ℝ E) : ℝ) / p) / ((↑(finrank ℝ E) : ℝ) / p * Real.Gamma ((↑(finrank ℝ E) : ℝ) / p)) *
      (↑(finrank ℝ E) : ℝ) =
    1

Tactic:
field
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (y : ℝ) ↦
          y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) /
        Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1) *
      (↑(finrank ℝ E) : ℝ) =
    1

Tactic:
have : ((∫ y in Set.Ioi (0 : ℝ), y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) /
        Real.Gamma ((finrank ℝ E) / p + 1)) * (finrank ℝ E) = 1 := by
      simp_rw [← Real.rpow_natCast _ (finrank ℝ E - 1), smul_eq_mul, Nat.cast_sub finrank_pos,
        Nat.cast_one]
      rw [integral_rpow_mul_exp_neg_rpow hp (by linarith), sub_add_cancel,
        Real.Gamma_add_one (ne_of_gt (by positivity))]
      field
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this_1 : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (y : ℝ) ↦
          y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) /
        Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1) *
      (↑(finrank ℝ E) : ℝ) =
    1
rw : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))

Tactic:
rw [integral_fun_norm_addHaar μ (fun x => Real.exp (-x ^ p)), nsmul_eq_mul, smul_eq_mul,
      mul_div_assoc, mul_div_assoc, mul_comm, mul_assoc, this, mul_one, ofReal_measureReal _]

Premises used: MeasureTheory.ofReal_measureReal, mul_assoc, mul_div_assoc, Real.exp, MeasureTheory.integral_fun_norm_addHaar, HPow.hPow, mul_comm, nsmul_eq_mul, smul_eq_mul, mul_one, Neg.neg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this_1 : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (y : ℝ) ↦
          y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) /
        Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1) *
      (↑(finrank ℝ E) : ℝ) =
    1
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ne_of_lt measure_ball_lt_top

Premises used: MeasureTheory.measure_ball_lt_top, ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this_1 : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (y : ℝ) ↦
          y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) /
        Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1) *
      (↑(finrank ℝ E) : ℝ) =
    1
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ne_of_lt measure_ball_lt_top

Premises used: MeasureTheory.measure_ball_lt_top, ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this : MeasurableSpace F := borel F
⊢ BorelSpace F

Tactic:
have : BorelSpace F := { measurable_eq := rfl }
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
⊢ (ν : (a : Set F) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : F), Real.exp (-‖x‖ ^ p_1) ∂ν) / Real.Gamma ((↑(finrank ℝ F) : ℝ) / p_1 + 1))

Tactic:
(measure_unitBall_eq_integral_div_gamma ν hp)

Premises used: MeasureTheory.measure_unitBall_eq_integral_div_gamma
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} : ℝ≥0∞) ((ν : (a : Set F) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞)
h₁ :
  ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p_1) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p_1 + 1)) =
    ENNReal.ofReal ((∫ (x : F), Real.exp (-‖x‖ ^ p_1) ∂ν) / Real.Gamma ((↑(finrank ℝ F) : ℝ) / p_1 + 1))
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p_1) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p_1 + 1))

Tactic:
convert! (measure_unitBall_eq_integral_div_gamma ν hp) using 1

Premises used: MeasureTheory.measure_unitBall_eq_integral_div_gamma
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (Set.preimage (β := F) (⇑φ : (a : E) → F) (Metric.ball 0 1)) : ℝ≥0∞)
rw : Measurable (α := E) (β := F) (⇑φ : (a : E) → F)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} : ℝ≥0∞) ((ν : (a : Set F) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞)

Tactic:
rw [@Measure.map_apply E F mE _ μ φ _ _ measurableSet_ball]

Premises used: MeasureTheory.Measure.map_apply, measurableSet_ball
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
h : ∀ (x : E), g x < 1 ↔ Metric.ball 0 1 x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (Set.preimage (β := F) (⇑φ : (a : E) → F) (Metric.ball 0 1)) : ℝ≥0∞)

Tactic:
congr!