awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
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))
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
⊢ Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
        (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution (HSMul.hSMul (α := ↥(Lp ℂ ∞ volume)) (MemLp.toLp (⇑g' : (a : E) → ℂ) ⋯) f') : 𝓢'(E, F))
have h : Eq (α := 𝓢'(E, F))
  ((smulLeftCLM F (g * fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
      (𝓕 f) :
    𝓢'(E, F))
  ((smulLeftCLM F
          (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
            (⇑g' : (a : E) → ℂ)) :
        (a : 𝓢'(E, F)) → 𝓢'(E, F))
      (𝓕 f) :
    𝓢'(E, F))
Tactic: rw [MeasureTheory.Lp.toTemperedDistribution_smul_eq (by apply hg₁), ← hf,
    fourierMultiplierCLM_apply, fourier_fourierInv_eq,
    smulLeftCLM_smulLeftCLM_apply hg₁ (by fun_prop),
    smulLeftCLM_smulLeftCLM_apply (by fun_prop) (by apply hg₁)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
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))
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
⊢ Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F (g * fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
        (𝓕 f) :
      𝓢'(E, F))
    ((smulLeftCLM F
            (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
              (⇑g' : (a : E) → ℂ)) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        (𝓕 f) :
      𝓢'(E, F))
have h : (g * fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) =
  HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) (⇑g' : (a : E) → ℂ)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
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))
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
⊢ (g * fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) =
    HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) (⇑g' : (a : E) → ℂ)
have h : ∀ (x : E),
  HMul.hMul (β := E → ℂ) g (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) x =
    HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
      (⇑g' : (a : E) → ℂ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
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))
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
x : E
⊢ HMul.hMul (β := E → ℂ) g (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) x =
    HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
      (⇑g' : (a : E) → ℂ) x
have h : HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) g x =
  HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
    (⇑g' : (a : E) → ℂ) x
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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 s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ (s' - s) / 2 ≤ 0
have rw : s' - s ≤ HMul.hMul (α := ℝ) 0 2
Tactic: rw [div_le_iff₀ (by norm_num)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (hypothesis)
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 s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ MemSobolev s' 2 f
have h' : (s' - s) / 2 ≤ 0
Tactic: have h' : (s' - s) / 2 ≤ 0 := by
    rw [div_le_iff₀ (by norm_num)]
    simp [h]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (hypothesis)
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 s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
⊢ MemSobolev s' 2 f
have hs : s' = s' - s + s
Tactic: have hs : s' = (s' - s) + s := by ring
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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 s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
⊢ MemSobolev s' 2 f
have rw : MemSobolev.{u_1, u_2} (E := E) (F := F) s 2 ((besselPotential E F (s' - s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f)
Tactic: rw [hs, ← memSobolev_besselPotential_iff]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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 s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
⊢ MemSobolev.{u_1, u_2} (E := E) (F := F) s 2 ((besselPotential E F (s' - s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f)
have apply : ∃ (C : ℝ), ∀ (x : E), ‖(↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2)) : ℂ)‖ ≤ C
Tactic: apply hf.fourierMultiplierCLM_of_bounded (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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 s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
⊢ ∃ (C : ℝ), ∀ (x : E), ‖(↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2)) : ℂ)‖ ≤ C
have h₁ : ∀ (x : E), ‖(↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2)) : ℂ)‖ ≤ 1
Tactic: use 1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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 s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
x : E
⊢ ‖(↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2)) : ℂ)‖ ≤ 1
have h₁ : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s' - s) / 2) ≤ 1
Tactic: rw [Complex.norm_real, Real.norm_eq_abs, abs_eq_self.mpr (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
⊢ MemSobolev (s - 1) 2 (∂_{m} f)
have 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)))
Tactic: rw [SubNegMonoid.sub_eq_add_neg s 1, add_comm, ← memSobolev_besselPotential_iff,
    besselPotential_neg_one_lineDerivOp_eq f]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
⊢ 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)))
have apply : ∃ (C : ℝ), ∀ (x : E), ‖(↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)‖ ≤ C
Tactic: apply (hf.fourierMultiplierCLM_of_bounded (by fun_prop) ?_).smul
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
⊢ ∃ (C : ℝ), ∀ (x : E), ‖(↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)‖ ≤ C
have h : ∀ (x : E), ‖(↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)‖ ≤ ‖m‖
Tactic: use ‖m‖
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
⊢ ‖(↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)‖ ≤ ‖m‖
have apply : HPow.hPow (β := ℕ) ‖(↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)‖ 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2
Tactic: apply le_of_sq_le_sq _ (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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 (β := ℕ) ‖(↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)‖ 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2
have simp : HPow.hPow (β := ℕ) |inner ℝ x m| 2 * HPow.hPow (β := ℕ) |(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]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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)⁻¹
have field_simp : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) * HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-(1 / 2))| 2 = 1
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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) ^ (-HDiv.hDiv (α := ℝ) 1 2)| 2 = 1
have rw : (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]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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) ^ HDiv.hDiv (α := ℝ) 1 2) 2)⁻¹ =
    1
have field_simp : 1 + HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ HDiv.hDiv (α := ℝ) 1 2) 2
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
have rw : 1 + HPow.hPow (β := ℕ) ‖x‖ 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (1 / 2 * 2)
Tactic: rw [← Real.rpow_mul (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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) ^ HDiv.hDiv (α := ℝ) 1 2) 2
have _ : 1 + HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℝ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (1 / 2)) 2
Tactic: calc
      _ = ((1 + ‖x‖ ^ 2) ^ (1 / 2 : ℝ)) ^ (2 : ℝ) := by
        rw [← Real.rpow_mul (by positivity)]; simp
      _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
⊢ 1 + HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ HDiv.hDiv (α := ℝ) 1 2) 2
have _₁ : HPow.hPow (β := ℝ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (1 / 2)) 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
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (hypothesis)
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 (β := ℕ) |inner ℝ x m| 2 * HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 ≤
    HPow.hPow (β := ℕ) ‖m‖ 2
have h₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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)
have grw : HPow.hPow (β := ℕ) (‖x‖ * ‖m‖) 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)
Tactic: grw [abs_real_inner_le_norm]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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‖ * ‖m‖) 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)
have rw : HPow.hPow (β := ℕ) ‖m‖ 2 * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)
Tactic: rw [mul_pow, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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 (β := ℕ) ‖m‖ 2 * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)
have hbc : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ 1 + HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (hypothesis)
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 (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 ≤
    HPow.hPow (β := ℕ) ‖m‖ 2
have h₂ : 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
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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 (β := ℕ) |inner ℝ x m| 2 * HPow.hPow (β := ℕ) |(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)| 2 ≤
    HPow.hPow (β := ℕ) ‖m‖ 2
have grw : HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹ ≤ HPow.hPow (β := ℕ) ‖m‖ 2
Tactic: grw [h₁, h₂]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
have hab : HPow.hPow (β := ℕ) ‖m‖ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)⁻¹ = HPow.hPow (β := ℕ) ‖m‖ 2
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
⊢ MemSobolev (s - 2) 2 (Δ f)
have 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)))
Tactic: rw [SubNegMonoid.sub_eq_add_neg s 2, add_comm, ← memSobolev_besselPotential_iff,
    besselPotential_neg_two_laplacian_eq f]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
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
⊢ Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦
    (↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)
have funProp : HasCompactSupport (β := ℝ) fun (a : E) ↦ ‖a‖
Tactic: fun_prop