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)
⊢ MemSobolev s 2 f ↔
    ∃ (f' : ↥(Lp F 2 volume)),
      Eq (α := 𝓢'(E, F))
        ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
            (𝓕 f) :
          𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))
have mp : MemSobolev s 2 f →
  ∃ (f' : ↥(Lp F 2 volume)),
    Eq (α := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))
Tactic: constructor
-- 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)
mp :
  MemSobolev s 2 f →
    ∃ (f' : ↥(Lp F 2 volume)),
      Eq (α := 𝓢'(E, F))
        ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
            (𝓕 f) :
          𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))
⊢ MemSobolev s 2 f ↔
    ∃ (f' : ↥(Lp F 2 volume)),
      Eq (α := 𝓢'(E, F))
        ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
            (𝓕 f) :
          𝓢'(E, F))
        (Lp.toTemperedDistribution f' : 𝓢'(E, F))
have mpr : (∃ (f' : ↥(Lp F 2 volume)),
    Eq (α := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution f' : 𝓢'(E, F))) →
  MemSobolev s 2 f
Tactic: constructor
-- 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)
f' : ↥(Lp F 2 volume)
hf' :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
⊢ ∃ (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))
have h : Eq (α := 𝓢'(E, F))
  ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
    𝓢'(E, F))
  (Lp.toTemperedDistribution (𝓕 f') : 𝓢'(E, F))
Tactic: use 𝓕 f'
-- 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)
f' : ↥(Lp F 2 volume)
hf' :
  Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
⊢ 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))
have hf'₁ : 𝓕 (E := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
  𝓕 (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')
Tactic: apply_fun 𝓕 at hf'
Cleared hypotheses: hf'
-- 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)
f' : ↥(Lp F 2 volume)
hf' :
  𝓕 (E := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
    𝓕 (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')
⊢ 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))
have hf'₁ : (smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) =
  𝓕 (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')
Tactic: rw [fourier_besselPotential_eq_smulLeftCLM_fourier_apply] at 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)
f' : ↥(Lp F 2 volume)
hf' :
  (smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) =
    𝓕 (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')
⊢ 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))
have h : 𝓕 (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f') = Lp.toTemperedDistribution (𝓕 f')
Tactic: rw [hf', Lp.fourier_toTemperedDistribution_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)
f' : ↥(Lp F 2 volume)
hf' :
  (smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) =
    𝓕 (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')
h : 𝓕 (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f') = Lp.toTemperedDistribution (𝓕 f')
⊢ 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))
have h₁ : Eq (α := 𝓢'(E, F)) (Lp.toTemperedDistribution (𝓕 f')) (Lp.toTemperedDistribution (𝓕 f'))
Tactic: rw [hf', Lp.fourier_toTemperedDistribution_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)
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))
⊢ MemSobolev s 2 f
have h : Eq (α := 𝓢'(E, F)) ((besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
  (Lp.toTemperedDistribution (𝓕⁻ f') : 𝓢'(E, F))
Tactic: use 𝓕⁻ f'
-- 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)
f' : ↥(Lp F 2 volume)
hf' :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution f' : 𝓢'(E, F))
⊢ 𝓕⁻ (E := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F)) =
    Lp.toTemperedDistribution (𝓕⁻ f')
have hf'₁ : 𝓕⁻ (E := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F)) =
  𝓕⁻ (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')
Tactic: apply_fun 𝓕⁻ at 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)
f' : ↥(Lp F 2 volume)
hf' :
  𝓕⁻ (E := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F)) =
    𝓕⁻ (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')
⊢ 𝓕⁻ (E := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F)) =
    Lp.toTemperedDistribution (𝓕⁻ f')
have h : 𝓕⁻ (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f') = Lp.toTemperedDistribution (𝓕⁻ f')
Tactic: rw [hf', Lp.fourierInv_toTemperedDistribution_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)
f' : ↥(Lp F 2 volume)
hf' :
  𝓕⁻ (E := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F)) =
    𝓕⁻ (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f')
h : 𝓕⁻ (E := 𝓢'(E, F)) (Lp.toTemperedDistribution f') = Lp.toTemperedDistribution (𝓕⁻ f')
⊢ 𝓕⁻ (E := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F)) =
    Lp.toTemperedDistribution (𝓕⁻ f')
have h₁ : Eq (α := 𝓢'(E, F)) (Lp.toTemperedDistribution (𝓕⁻ f')) (Lp.toTemperedDistribution (𝓕⁻ f'))
Tactic: rw [hf', Lp.fourierInv_toTemperedDistribution_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 : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ ∃ (v : ↥(Lp F 1 volume)), 𝓕 f = Lp.toTemperedDistribution v
have obtain : ∀ (u : ↥(Lp F 2 volume))
  (hu :
    Eq (α := 𝓢'(E, F))
      ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
          (𝓕 f) :
        𝓢'(E, F))
      (Lp.toTemperedDistribution u : 𝓢'(E, F))),
  ∃ (v : ↥(Lp F 1 volume)), 𝓕 f = Lp.toTemperedDistribution v
Tactic: obtain ⟨u, hu⟩ := memSobolev_iff_exists_smulLeftCLM_fourier.mp 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 : ℝ
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
have left : AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
  (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) volume
Tactic: constructor
-- 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))
left :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) volume
⊢ MemLp (ε := ℝ) (m0 := MeasureSpace.toMeasurableSpace) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2
    volume
have right : @eLpNorm _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2 volume < ∞
Tactic: constructor
-- 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))
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) volume
have this : Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)
Tactic: have : (fun x : E ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)).HasTemperateGrowth := by
        fun_prop
-- 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))
⊢ @eLpNorm _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2 volume < ∞
have right : ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)‖ₑ ^ ENNReal.toReal 2 < ∞
Tactic: rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (by norm_num) (by norm_num)]
-- 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))
h : ∫⁻ (a : E), ENNReal.ofReal ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ < ∞
⊢ ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)‖ₑ ^ ENNReal.toReal 2 < ∞
have norm_cast : ∫⁻ (a : E), HPow.hPow (β := ℕ) ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)‖ₑ 2 < ∞
Tactic: norm_cast
-- 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))
h : ∫⁻ (a : E), ENNReal.ofReal ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ < ∞
⊢ ∫⁻ (a : E), HPow.hPow (β := ℕ) ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)‖ₑ 2 < ∞
have h₁ : ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ₑ < ∞
Tactic: simp_rw [ofReal_norm] at h
Cleared hypotheses: 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 : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
h : ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ₑ < ∞
⊢ ∫⁻ (a : E), HPow.hPow (β := ℕ) ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)‖ₑ 2 < ∞
have simp_rw : ∫⁻ (a : E), ‖HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)) 2‖ₑ < ∞
Tactic: simp_rw [← enorm_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 : ℝ
hs : (↑(Module.finrank ℝ E) : ℝ) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu :
  Eq (α := 𝓢'(E, F))
    ((smulLeftCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) :
      𝓢'(E, F))
    (Lp.toTemperedDistribution u : 𝓢'(E, F))
h : ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ₑ < ∞
⊢ ∫⁻ (a : E), ‖HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)) 2‖ₑ < ∞
have h₁ : ∀ (x : E), HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)
Tactic: convert! h using 4
-- 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))
h : ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ₑ < ∞
x : E
⊢ HPow.hPow (β := ℕ) ((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2)) 2 = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)
have h₁ : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s / 2 * (↑2 : ℝ)) = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)
Tactic: rw [← Real.rpow_mul_natCast (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))
⊢ ∫⁻ (a : E), ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s / 2)‖ₑ ^ ENNReal.toReal 2 < ∞
have right : ∫⁻ (a : E), ENNReal.ofReal ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ < ∞
Tactic: suffices h : ∫⁻ a : E, ENNReal.ofReal ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ < ⊤ from by
        norm_cast
        simp_rw [ofReal_norm] at h
        simp_rw [← enorm_pow]
        convert! h using 4
        rw [← Real.rpow_mul_natCast (by positivity)]
        simp
-- 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))
⊢ ∫⁻ (a : E), ENNReal.ofReal ‖(1 + HPow.hPow (β := ℕ) ‖a‖ 2) ^ (-s)‖ < ∞
have 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)‖
Tactic: apply ((integrable_rpow_neg_one_add_norm_sq hs).congr _).lintegral_lt_top
-- 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))
⊢ (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)‖
have h : ∀ (x : E), (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-(2 * s) / 2) = ‖(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)‖
Tactic: filter_upwards with 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))
x : E
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-(2 * s) / 2) = ‖(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-s)‖
have h : (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)]