awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
mp :
  MemSobolev s 2 f →
    ∃ (f' : ↥(Lp F 2 volume)),
      Eq (α := 𝓢'(E, F))
        ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
            (𝓕 f) :
          𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))
mpr :
  (∃ (f' : ↥(Lp F 2 volume)),
      Eq (α := 𝓢'(E, F))
        ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
            (𝓕 f) :
          𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))) →
    MemSobolev s 2 f
⊢ MemSobolev s 2 f ↔
    ∃ (f' : ↥(Lp F 2 volume)),
      Eq (α := 𝓢'(E, F))
        ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
            (𝓕 f) :
          𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))

Tactic:
constructor
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
f' : ↥(Lp F 2 volume)
hf' :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
h :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution (𝓕 f') : 𝓢'(E, F))
⊢ ∃ (f' : ↥(Lp F 2 volume)),
    Eq (α := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))

Tactic:
use 𝓕 f'

Premises used: FourierTransform.fourier
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
f' : ↥(Lp F 2 volume)
hf' :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
⊢ 𝓕 (E := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
    𝓕 (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')

Tactic:
apply_fun 𝓕 at hf'
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
f' : ↥(Lp F 2 volume)
hf' :
  𝓕 (E := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
    𝓕 (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')
⊢ (smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) =
    𝓕 (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')

Tactic:
rw [fourier_besselPotential_eq_smulLeftCLM_fourier_apply] at hf'

Premises used: TemperedDistribution.fourier_besselPotential_eq_smulLeftCLM_fourier_apply
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
f' : ↥(Lp F 2 volume)
hf' :
  (smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) =
    𝓕 (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')
h : 𝓕 (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f') = Lp.toTemperedDistribution (𝓕 f')
h₁ h₂ : Eq (α := 𝓢'(E, F)) (Lp.toTemperedDistribution (𝓕 f')) (Lp.toTemperedDistribution (𝓕 f'))
⊢ Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution (𝓕 f') : 𝓢'(E, F))

Tactic:
rw [hf', Lp.fourier_toTemperedDistribution_eq f']

Premises used: MeasureTheory.Lp.fourier_toTemperedDistribution_eq
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
f' : ↥(Lp F 2 volume)
hf' :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
h :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution (𝓕⁻ f') : 𝓢'(E, F))
⊢ MemSobolev s 2 f

Tactic:
use 𝓕⁻ f'

Premises used: FourierTransformInv.fourierInv
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
f' : ↥(Lp F 2 volume)
hf' :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
⊢ 𝓕⁻ (E := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F)) =
    𝓕⁻ (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')

Tactic:
apply_fun 𝓕⁻ at hf'
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
f' : ↥(Lp F 2 volume)
hf' :
  𝓕⁻ (E := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F)) =
    𝓕⁻ (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')
h : 𝓕⁻ (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f') = Lp.toTemperedDistribution (𝓕⁻ f')
h₁ h₂ : Eq (α := 𝓢'(E, F)) (Lp.toTemperedDistribution (𝓕⁻ f')) (Lp.toTemperedDistribution (𝓕⁻ f'))
⊢ 𝓕⁻ (E := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F)) =
    Lp.toTemperedDistribution (𝓕⁻ f')

Tactic:
rw [hf', Lp.fourierInv_toTemperedDistribution_eq f']

Premises used: MeasureTheory.Lp.fourierInv_toTemperedDistribution_eq
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
f : 𝓢'(E, F)
⊢ MemSobolev 0 2 f ↔ ∃ (f' : ↥(Lp F 2 volume)), 𝓕 f = Lp.toTemperedDistribution f'

Tactic:
simp [memSobolev_iff_exists_smulLeftCLM_fourier]

Premises used: TemperedDistribution.memSobolev_iff_exists_smulLeftCLM_fourier
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
obtain :
  ∀ (u : ↥(Lp F 2 volume))
    (hu :
      Eq (α := 𝓢'(E, F))
        ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
            (𝓕 f) :
          𝓢'(E, F))
        (Lp.toTemperedDistribution u : 𝓢'(E, F))),
    ∃ (v : ↥(Lp F 1 volume)), 𝓕 f = Lp.toTemperedDistribution v
⊢ ∃ (v : ↥(Lp F 1 volume)), 𝓕 f = Lp.toTemperedDistribution v

Tactic:
obtain ⟨u, hu⟩ := memSobolev_iff_exists_smulLeftCLM_fourier.mp hf

Premises used: TemperedDistribution.memSobolev_iff_exists_smulLeftCLM_fourier, Iff.mp
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
left :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) volume
right :
  @eLpNorm _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2 volume < ∞
⊢ MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume

Tactic:
constructor
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
⊢ Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
⊢ Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)

Tactic:
have : (fun x : E ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)).HasTemperateGrowth := by
        fun_prop
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
this : Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) volume

Tactic:
this.1.continuous.aestronglyMeasurable

Premises used: ContDiff.continuous, And.left, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
this : Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) volume

Tactic:
exact this.1.continuous.aestronglyMeasurable

Premises used: ContDiff.continuous, And.left, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
⊢ Ne (α := ℝ≥0∞) 2 0

Tactic:
norm_num
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
norm_num
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
right : ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)‖ₑ ^ ENNReal.toReal 2 < ∞
⊢ @eLpNorm _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2 volume < ∞

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (by norm_num) (by norm_num)]

Premises used: MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
h : ∫⁻ (a : E), ENNReal.ofReal ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ < ∞
norm_cast : ∫⁻ (a : E), HPow.hPow (β := ℕ) ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)‖ₑ 2 < ∞
⊢ ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)‖ₑ ^ ENNReal.toReal 2 < ∞

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
h : ∫⁻ (a : E), ENNReal.ofReal ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ < ∞
⊢ ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ₑ < ∞

Tactic:
simp_rw [ofReal_norm] at h

Premises used: ofReal_norm
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
h : ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ₑ < ∞
simp_rw : ∫⁻ (a : E), ‖HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)) 2‖ₑ < ∞
⊢ ∫⁻ (a : E), HPow.hPow (β := ℕ) ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)‖ₑ 2 < ∞

Tactic:
simp_rw [← enorm_pow]

Premises used: enorm_pow
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
h : ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ₑ < ∞
⊢ ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ₑ < ∞

Tactic:
h
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
h : ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ₑ < ∞
h₁ : ∀ (x : E), HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)
⊢ ∫⁻ (a : E), ‖HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)) 2‖ₑ < ∞

Tactic:
convert! h using 4
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
h : ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ₑ < ∞
x : E
⊢ 0 ≤ 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
h : ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ₑ < ∞
x : E
h₁ : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2 * (↑2 : ℝ)) = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)
⊢ HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)

Tactic:
rw [← Real.rpow_mul_natCast (by positivity)]

Premises used: Real.rpow_mul_natCast
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
h : ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ₑ < ∞
x : E
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2 * (↑2 : ℝ)) = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
right : ∫⁻ (a : E), ENNReal.ofReal ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ < ∞
⊢ ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)‖ₑ ^ ENNReal.toReal 2 < ∞

Tactic:
suffices h : ∫⁻ a : E, ENNReal.ofReal ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ < ⊤ from by
        norm_cast
        simp_rw [ofReal_norm] at h
        simp_rw [← enorm_pow]
        convert! h using 4
        rw [← Real.rpow_mul_natCast (by positivity)]
        simp