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 : ℝ
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))
apply :
  (ae (F := Measure E) (volume : Measure E)).EventuallyEq (β := ℝ)
    (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-(2 * s) / 2)) fun (x : E) ↦
    ‖(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)‖
⊢ ∫⁻ (a : E), ENNReal.ofReal ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ < ∞

Tactic:
apply ((integrable_rpow_neg_one_add_norm_sq hs).congr _).lintegral_lt_top

Premises used: integrable_rpow_neg_one_add_norm_sq, MeasureTheory.Integrable.lintegral_lt_top, MeasureTheory.Integrable.congr
-- 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 : ∀ (x : E), (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-(2 * s) / 2) = ‖(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)‖
⊢ (ae (F := Measure E) (volume : Measure E)).EventuallyEq (β := ℝ)
    (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-(2 * s) / 2)) fun (x : E) ↦
    ‖(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)‖

Tactic:
filter_upwards with x
-- 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))
x : E
⊢ 0 ≤ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)

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))
x : E
h : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-(2 * s) / 2) = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-(2 * s) / 2) = ‖(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)‖

Tactic:
rw [Real.norm_eq_abs, abs_eq_self.mpr (by positivity)]

Premises used: Iff.mpr, abs_eq_self, Real.norm_eq_abs
-- 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))
x : E
h : -(2 * s) / 2 = -s
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-(2 * s) / 2) = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)

Tactic:
congr
-- 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))
x : E
⊢ -(2 * s) / 2 = -s

Tactic:
ring
-- 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))
⊢ MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume

Tactic:
have : MemLp (fun x : E ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 := by
    constructor
    · have : (fun x : E ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)).HasTemperateGrowth := by
        fun_prop
      exact this.1.continuous.aestronglyMeasurable
    · rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (by norm_num) (by norm_num)]
      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
      apply ((integrable_rpow_neg_one_add_norm_sq hs).congr _).lintegral_lt_top
      filter_upwards with x
      rw [Real.norm_eq_abs, abs_eq_self.mpr (by positivity)]
      congr
      ring
-- 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 :
  MemLp (ε := ℝ) (m0 := 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:
have : MemLp (fun x : E ↦ Complex.ofReal ((1 + ‖x‖ ^ 2) ^ (-s / 2) : ℝ)) 2 := this.ofReal
-- 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_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
h :
  𝓕 f =
    Lp.toTemperedDistribution (MemLp.toLp (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) this • u)
⊢ ∃ (v : ↥(Lp F 1 volume)), 𝓕 f = Lp.toTemperedDistribution v

Tactic:
use this.toLp • u

Premises used: MeasureTheory.MemLp.toLp
-- 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_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
h :
  𝓕 f =
    (smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
      (Lp.toTemperedDistribution u)
h₁ : Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)
⊢ 𝓕 f =
    Lp.toTemperedDistribution (MemLp.toLp (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) this • u)

Tactic:
rw [MeasureTheory.Lp.toTemperedDistribution_smul_eq]

Premises used: MeasureTheory.Lp.toTemperedDistribution_smul_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 : ℝ
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_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
⊢ 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))
this_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
⊢ 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))
this_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
h :
  𝓕 f =
    (smulLeftCLM F
          (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
            (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) :
        (a : 𝓢'(E, F)) → 𝓢'(E, F))
      (𝓕 f)
⊢ 𝓕 f =
    (smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
      (Lp.toTemperedDistribution u)

Tactic:
rw [← hu, smulLeftCLM_smulLeftCLM_apply (by fun_prop) (by fun_prop)]

Premises used: TemperedDistribution.smulLeftCLM_smulLeftCLM_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 : ℝ
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_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
⊢ HSMul.hSMul (α := ℂ) 1 (𝓕 f) = (smulLeftCLM F fun (x : E) ↦ 1 : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f)

Tactic:
(smulLeftCLM_const 1 (𝓕 f)).symm

Premises used: FourierTransform.fourier, TemperedDistribution.smulLeftCLM_const, OfNat.ofNat, Eq.symm
-- 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_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
h : 𝓕 f = HSMul.hSMul (α := ℂ) 1 (𝓕 f)
h₁ :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F
            (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
              (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        (𝓕 f) :
      𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ 1 : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) : 𝓢'(E, F))
⊢ 𝓕 f =
    (smulLeftCLM F
          (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
            (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) :
        (a : 𝓢'(E, F)) → 𝓢'(E, F))
      (𝓕 f)

Tactic:
convert! (smulLeftCLM_const 1 (𝓕 f)).symm using 1

Premises used: FourierTransform.fourier, TemperedDistribution.smulLeftCLM_const, OfNat.ofNat, Eq.symm
-- 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_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
⊢ 𝓕 f = HSMul.hSMul (α := ℂ) 1 (𝓕 f)

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))
this_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
h :
  (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
      (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) =
    fun (x : E) ↦ 1
⊢ Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F
            (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
              (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        (𝓕 f) :
      𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ 1 : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) : 𝓢'(E, F))

Tactic:
congr
-- 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_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
h :
  ∀ (x : E),
    HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
        (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) x =
      1
⊢ (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
      (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) =
    fun (x : E) ↦ 1

Tactic:
ext x
-- 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_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
x : E
h : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2) = 1
⊢ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) * (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ) = 1

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))
this_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
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))
this_1 :
  MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
this :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) 2 volume
x : E
h : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + -s / 2) = 1
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2) = 1

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

Premises used: Real.rpow_add