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 : ℝ
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
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-(2 * s) / 2) = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)
have h : -(2 * s) / 2 = -s
Tactic: congr
-- 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 : ℝ
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))
⊢ ∃ (v : ↥(Lp F 1 volume)), 𝓕 f = Lp.toTemperedDistribution v
have this : 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
-- 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 : ℝ
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
⊢ ∃ (v : ↥(Lp F 1 volume)), 𝓕 f = Lp.toTemperedDistribution v
have this₁ : 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
-- 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 : ℝ
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
⊢ ∃ (v : ↥(Lp F 1 volume)), 𝓕 f = Lp.toTemperedDistribution v
have h : 𝓕 f = Lp.toTemperedDistribution (MemLp.toLp (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) this • u)
Tactic: use this.toLp • u
-- 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 : ℝ
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 =
    Lp.toTemperedDistribution (MemLp.toLp (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) this • u)
have h : 𝓕 f =
  (smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
    (Lp.toTemperedDistribution u)
Tactic: rw [MeasureTheory.Lp.toTemperedDistribution_smul_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 : ℝ
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)
⊢ 𝓕 f =
    Lp.toTemperedDistribution (MemLp.toLp (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)) this • u)
have h₁ : Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ)
Tactic: rw [MeasureTheory.Lp.toTemperedDistribution_smul_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 : ℝ
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 =
    (smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
      (Lp.toTemperedDistribution u)
have 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)
Tactic: rw [← hu, smulLeftCLM_smulLeftCLM_apply (by fun_prop) (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 : ℝ
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 =
    (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)
have h : 𝓕 f = HSMul.hSMul (α := ℂ) 1 (𝓕 f)
Tactic: convert! (smulLeftCLM_const 1 (𝓕 f)).symm using 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 : ℝ
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)
⊢ 𝓕 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)
have 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))
Tactic: convert! (smulLeftCLM_const 1 (𝓕 f)).symm using 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 : ℝ
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
⊢ 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))
have 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
Tactic: congr
-- 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 : ℝ
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
⊢ (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
have 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
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 : ℝ
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
⊢ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) * (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) : ℂ) = 1
have h : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2) = 1
Tactic: norm_cast
-- 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 : ℝ
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
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2) = 1
have h : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + -s / 2) = 1
Tactic: rw [← Real.rpow_add (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 : ℝ
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
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + -s / 2) = 1
have h : HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 0 = 1
Tactic: ring_nf
-- 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
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : ∃ (C : ℝ), ∀ (x : E), ‖g x‖ ≤ C
⊢ MemSobolev.{u_1, u_2} (E := E) (F := F) s 2 ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f)
have rw : ∀
  (hf :
    ∃ (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)))
  {g : E → ℂ} (hg₁ : Function.HasTemperateGrowth g) (hg₂ : ∃ (C : ℝ), ∀ (x : E), ‖g x‖ ≤ C),
  ∃ (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))
          (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))
Tactic: rw [memSobolev_iff_exists_smulLeftCLM_fourier] at hf ⊢
Cleared hypotheses: hf, g, hg₁, 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)
hf :
  ∃ (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))
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : ∃ (C : ℝ), ∀ (x : E), ‖g x‖ ≤ C
⊢ ∃ (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))
          (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))
have obtain : ∀ (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))),
  ∃ (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))
          (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))
Tactic: obtain ⟨f', hf⟩ := hf
Cleared hypotheses: hf
-- 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
hg₂ : ∃ (C : ℝ), ∀ (x : E), ‖g x‖ ≤ C
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))
⊢ ∃ (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))
          (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))
have obtain : ∀ (C : ℝ) (hC : ∀ (x : E), ‖g x‖ ≤ C),
  ∃ (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))
          (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))
Tactic: obtain ⟨C, hC⟩ := hg₂
Cleared hypotheses: 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
⊢ ∃ (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))
          (𝓕 (E := 𝓢'(E, F)) ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))
have h : 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) → ℂ) sorry) f') : 𝓢'(E, F))
Tactic: use (g'.memLp_top.toLp _ (μ := volume)) • f'