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)
hf : MemSobolev s 2 f
m : E
rw :
  MemSobolev s 2
    (HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
      ((fourierMultiplierCLM F fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F)))
⊢ MemSobolev (s - 1) 2 (∂_{m} f)

Tactic:
rw [SubNegMonoid.sub_eq_add_neg s 1, add_comm, ← memSobolev_besselPotential_iff,
    besselPotential_neg_one_lineDerivOp_eq f]

Premises used: SubNegMonoid.sub_eq_add_neg, TemperedDistribution.memSobolev_besselPotential_iff, TemperedDistribution.besselPotential_neg_one_lineDerivOp_eq, add_comm, OfNat.ofNat
-- 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)
hf : MemSobolev s 2 f
m : E
⊢ Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m : E
apply : ∃ (C : ℝ), ∀ (x : E), ‖(↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)‖ ≤ C
⊢ MemSobolev s 2
    (HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
      ((fourierMultiplierCLM F fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F)))

Tactic:
apply (hf.fourierMultiplierCLM_of_bounded (by fun_prop) ?_).smul

Premises used: TemperedDistribution.MemSobolev.smul, TemperedDistribution.MemSobolev.fourierMultiplierCLM_of_bounded
-- 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)
hf : MemSobolev s 2 f
m : E
h : ∀ (x : E), ‖(↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)‖ ≤ ‖m‖
⊢ ∃ (C : ℝ), ∀ (x : E), ‖(↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)‖ ≤ C

Tactic:
use ‖m‖
-- 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)
hf : MemSobolev s 2 f
m x : E
⊢ 0 ≤ ‖m‖

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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
apply :
  HPow.hPow (β := ℕ) ‖(↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)‖ 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2
⊢ ‖(↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)‖ ≤ ‖m‖

Tactic:
apply le_of_sq_le_sq _ (by positivity)

Premises used: le_of_sq_le_sq
-- 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)
hf : MemSobolev s 2 f
m x : E
simp :
  HPow.hPow (β := ℕ) |inner ℝ x m| 2 * HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 ≤
    HPow.hPow (β := ℕ) ‖m‖ 2
⊢ HPow.hPow (β := ℕ) ‖(↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)‖ 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2

Tactic:
simp only [Complex.ofReal_mul, Complex.norm_mul, Complex.norm_real, Real.norm_eq_abs, mul_pow]

Premises used: Complex.norm_real, mul_pow, Complex.norm_mul, Real.norm_eq_abs, Complex.ofReal_mul
-- 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)
hf : MemSobolev s 2 f
m x : E
field_simp : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) * HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-(1 / 2))| 2 = 1
⊢ HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹

Tactic:
field_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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m 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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
rw :
  (1 + HPow.hPow (β := ℕ) ‖x‖ 2) * (HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ HDiv.hDiv (α := ℝ) 1 2) 2)⁻¹ =
    1
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) * HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-HDiv.hDiv (α := ℝ) 1 2)| 2 = 1

Tactic:
rw [Real.rpow_neg (by positivity), sq_abs, inv_pow]

Premises used: inv_pow, sq_abs, Real.rpow_neg
-- 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)
hf : MemSobolev s 2 f
m x : E
field_simp :
  1 + HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ HDiv.hDiv (α := ℝ) 1 2) 2
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) * (HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ HDiv.hDiv (α := ℝ) 1 2) 2)⁻¹ =
    1

Tactic:
field_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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
rw : 1 + HPow.hPow (β := ℕ) ‖x‖ 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (1 / 2 * 2)
⊢ 1 + HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℝ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (1 / 2)) 2

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

Premises used: Real.rpow_mul
-- 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)
hf : MemSobolev s 2 f
m x : E
⊢ 1 + HPow.hPow (β := ℕ) ‖x‖ 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (1 / 2 * 2)

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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
⊢ HPow.hPow (β := ℝ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (1 / 2)) 2 =
    HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ HDiv.hDiv (α := ℝ) 1 2) 2

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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
_ : 1 + HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℝ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (1 / 2)) 2
_₁ :
  HPow.hPow (β := ℝ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (1 / 2)) 2 =
    HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ HDiv.hDiv (α := ℝ) 1 2) 2
⊢ 1 + HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ HDiv.hDiv (α := ℝ) 1 2) 2

Tactic:
calc
      _ = ((1 + ‖x‖ ^ 2) ^ (1 / 2 : ℝ)) ^ (2 : ℝ) := by
        rw [← Real.rpow_mul (by positivity)]; simp
      _ = _ := by simp

Premises used: Norm.norm, HDiv.hDiv, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- 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)
hf : MemSobolev s 2 f
m x : E
⊢ HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹

Tactic:
have h₁ : |(1 + ‖x‖ ^ 2) ^ (-1 / 2 : ℝ)| ^ 2 = (1 + ‖x‖ ^ 2)⁻¹ := by
    field_simp
    norm_cast
    rw [Real.rpow_neg (by positivity), sq_abs, inv_pow]
    field_simp
    calc
      _ = ((1 + ‖x‖ ^ 2) ^ (1 / 2 : ℝ)) ^ (2 : ℝ) := by
        rw [← Real.rpow_mul (by positivity)]; simp
      _ = _ := by 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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
h₁ : HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
grw : HPow.hPow (β := ℕ) (‖x‖ * ‖m‖) 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ HPow.hPow (β := ℕ) |inner ℝ x m| 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)

Tactic:
grw [abs_real_inner_le_norm]

Premises used: abs_real_inner_le_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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
h₁ : HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
rw : HPow.hPow (β := ℕ) ‖m‖ 2 * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ HPow.hPow (β := ℕ) (‖x‖ * ‖m‖) 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)

Tactic:
rw [mul_pow, mul_comm]

Premises used: mul_comm, mul_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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
h₁ : HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
hbc : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ 1 + HPow.hPow (β := ℕ) ‖x‖ 2
⊢ HPow.hPow (β := ℕ) ‖m‖ 2 * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)

Tactic:
gcongr
-- 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)
hf : MemSobolev s 2 f
m x : E
h₁ : HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ 1 + HPow.hPow (β := ℕ) ‖x‖ 2

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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
h₁ : HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
⊢ HPow.hPow (β := ℕ) |inner ℝ x m| 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)

Tactic:
have h₂ : |inner ℝ x m| ^ 2 ≤ ‖m‖ ^ 2 * (1 + ‖x‖ ^ 2) := by
    grw [abs_real_inner_le_norm]
    rw [mul_pow, mul_comm]
    gcongr
    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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
h₁ : HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
h₂ : HPow.hPow (β := ℕ) |inner ℝ x m| 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)
grw :
  HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹ ≤
    HPow.hPow (β := ℕ) ‖m‖ 2
⊢ HPow.hPow (β := ℕ) |inner ℝ x m| 2 * HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 ≤
    HPow.hPow (β := ℕ) ‖m‖ 2

Tactic:
grw [h₁, 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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
h₁ : HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
h₂ : HPow.hPow (β := ℕ) |inner ℝ x m| 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)
hab :
  HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹ =
    HPow.hPow (β := ℕ) ‖m‖ 2
⊢ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹ ≤
    HPow.hPow (β := ℕ) ‖m‖ 2

Tactic:
apply le_of_eq

Premises used: le_of_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)
hf : MemSobolev s 2 f
m x : E
h₁ : HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹
h₂ : HPow.hPow (β := ℕ) |inner ℝ x m| 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹ =
    HPow.hPow (β := ℕ) ‖m‖ 2

Tactic:
field_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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
rw :
  MemSobolev s 2
    (HSMul.hSMul (β := 𝓢'(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
      ((fourierMultiplierCLM F fun (x : E) ↦
              (↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F)))
⊢ MemSobolev (s - 2) 2 (Δ f)

Tactic:
rw [SubNegMonoid.sub_eq_add_neg s 2, add_comm, ← memSobolev_besselPotential_iff,
    besselPotential_neg_two_laplacian_eq f]

Premises used: SubNegMonoid.sub_eq_add_neg, TemperedDistribution.memSobolev_besselPotential_iff, add_comm, TemperedDistribution.besselPotential_neg_two_laplacian_eq, OfNat.ofNat
-- 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)
hf : MemSobolev s 2 f
funProp : HasCompactSupport (β := ℝ) fun (a : E) ↦ ‖a‖
⊢ Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦
    (↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)

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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
apply :
  ∃ (C : ℝ), ∀ (x : E), ‖(↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)‖ ≤ C
⊢ MemSobolev s 2
    (HSMul.hSMul (β := 𝓢'(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
      ((fourierMultiplierCLM F fun (x : E) ↦
              (↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F)))

Tactic:
apply (hf.fourierMultiplierCLM_of_bounded (by fun_prop) ?_).smul

Premises used: TemperedDistribution.MemSobolev.smul, TemperedDistribution.MemSobolev.fourierMultiplierCLM_of_bounded
-- 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)
hf : MemSobolev s 2 f
h : ∀ (x : E), ‖(↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)‖ ≤ 1
⊢ ∃ (C : ℝ), ∀ (x : E), ‖(↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)‖ ≤ C

Tactic:
use 1
-- 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)
hf : MemSobolev s 2 f
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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
h : ‖(↑(HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 1)⁻¹) : ℂ)‖ ≤ 1
⊢ ‖(↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)‖ ≤ 1

Tactic:
rw [Real.rpow_neg (by positivity)]

Premises used: Real.rpow_neg
-- 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)
hf : MemSobolev s 2 f
x : E
h : ‖HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 1)⁻¹‖ ≤ 1
⊢ ‖(↑(HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 1)⁻¹) : ℂ)‖ ≤ 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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
h : HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) |1 + HPow.hPow (β := ℕ) ‖x‖ 2| 1)⁻¹ ≤ 1
⊢ ‖HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 1)⁻¹‖ ≤ 1

Tactic:
simp only [norm_mul, norm_pow, abs_norm, norm_inv, Real.norm_eq_abs]

Premises used: norm_pow, norm_mul, norm_inv, abs_norm, 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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
⊢ 0 < HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 1

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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
h : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ 1 * HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 1
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) |1 + HPow.hPow (β := ℕ) ‖x‖ 2| 1)⁻¹ ≤ 1

Tactic:
rw [abs_of_nonneg (by positivity), mul_inv_le_iff₀ (by positivity)]

Premises used: mul_inv_le_iff₀, abs_of_nonneg
-- 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)
hf : MemSobolev s 2 f
x : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ 1 * HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 1

Tactic:
grind
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst : FunLike F α β
inst_1 : TopologicalSpace α
inst_2 : Zero β
f : F → V
inst_3 : Zero V
s₁ s₂ : Set α
hs : s₂ ⊆ s₁
hf : IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f s₁
⊢ IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f s₂

Tactic:
(hf · <| ·.trans hs)

Premises used: HasSubset.Subset.trans, Distribution.IsVanishingOn
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst : FunLike F α β
inst_1 : TopologicalSpace α
inst_2 : Zero β
f : F → V
inst_3 : Zero V
s₁ s₂ : Set α
hs : s₁ ⊆ s₂
hf : ¬IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f s₁
⊢ ¬IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f s₂

Tactic:
(hf <| ·.mono hs)

Premises used: Distribution.IsVanishingOn.mono, Not
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst : FunLike F α β
inst_1 : TopologicalSpace α
inst_2 : Zero β
f : F → V
s : Set α
inst_3 : Zero V
⊢ ¬IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f s ↔
    ∃ (u : F), tsupport.{u_2, u_3} (α := β) (⇑u : (a : α) → β) ⊆ s ∧ f u ≠ 0

Tactic:
simp [IsVanishingOn]

Premises used: Distribution.IsVanishingOn