PrimeNumberTheoremAnd.Sobolev

structure CS (n : ℕ) (E : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] :

toFun : ℝ → E
h1 : ContDiff ℝ (↑n) self.toFun
h2 : HasCompactSupport self.toFun

Instances For

theorem CS.ext {n : ℕ} {E : Type u_2} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {x y : CS n E} (toFun : x.toFun = y.toFun) :

x = y

Inspect dependencies

CS.ext · compiled type and proof/definition references.

source

theorem CS.ext_iff {n : ℕ} {E : Type u_2} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {x y : CS n E} :

x = y ↔ x.toFun = y.toFun

Inspect dependencies

CS.ext_iff · compiled type and proof/definition references.

source

structure truncextends CS 2 ℝ :

Type

toFun : ℝ → ℝ
h1 : ContDiff ℝ (↑2) self.toFun
h2 : HasCompactSupport self.toFun
h3 : (Set.Icc (-1) 1).indicator 1 ≤ self.toFun
h4 : self.toFun ≤ (Set.Ioo (-2) 2).indicator 1

Instances For

source

structure W1 (n : ℕ) (E : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] :

Type u_2

toFun : ℝ → E
smooth : ContDiff ℝ (↑n) self.toFun
integrable ⦃k : ℕ⦄ : k ≤ n → MeasureTheory.Integrable (iteratedDeriv k self.toFun) MeasureTheory.volume

Instances For

source

@[reducible, inline]

abbrev W21 :

Type

Equations

W21 = W1 2 ℂ

Instances For

Inspect dependencies

W21 · compiled type and proof/definition references.

source

noncomputable def funscale {E : Type u_2} (g : ℝ → E) (R x : ℝ) :

Equations

funscale g R x = g (R⁻¹ • x)

Instances For

Inspect dependencies

funscale · compiled type and proof/definition references.

source

theorem contDiff_ofReal :

ContDiff ℝ (↑⊤) Complex.ofReal

Inspect dependencies

contDiff_ofReal · compiled type and proof/definition references.

source

theorem tendsto_funscale {E : Type u_1} [NormedAddCommGroup E] {f : ℝ → E} (hf : ContinuousAt f 0) (x : ℝ) :

Filter.Tendsto (fun (R : ℝ) => funscale f R x) Filter.atTop (nhds (f 0))

Inspect dependencies

tendsto_funscale · compiled type and proof/definition references.

source

@[instance_reducible]

instance CS.instCoeFunForallReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} :

CoeFun (CS n E) fun (x : CS n E) => ℝ → E

Equations

CS.instCoeFunForallReal = { coe := CS.toFun }

Inspect dependencies

CS.instCoeFunForallReal · compiled type and proof/definition references.

source

@[instance_reducible]

instance CS.instCoeRealComplex {n : ℕ} :

Coe (CS n ℝ) (CS n ℂ)

Equations

CS.instCoeRealComplex = { coe := fun (f : CS n ℝ) => { toFun := fun (x : ℝ) => ↑(f.toFun x), h1 := ⋯, h2 := ⋯ } }

Inspect dependencies

CS.instCoeRealComplex · compiled type and proof/definition references.

source

def CS.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : CS n E) :

CS n E

Equations

f.neg = { toFun := -f.toFun, h1 := ⋯, h2 := ⋯ }

Instances For

Inspect dependencies

CS.neg · compiled type and proof/definition references.

source

@[instance_reducible]

instance CS.instNeg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} :

Neg (CS n E)

Equations

CS.instNeg = { neg := CS.neg }

Inspect dependencies

CS.instNeg · compiled type and proof/definition references.

source

@[simp]

theorem CS.neg_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {f : CS n E} {x : ℝ} :

(-f).toFun x = -f.toFun x

Inspect dependencies

CS.neg_apply · compiled type and proof/definition references.

source

def CS.smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (R : ℝ) (f : CS n E) :

CS n E

Equations

CS.smul R f = { toFun := R • f.toFun, h1 := ⋯, h2 := ⋯ }

Instances For

Inspect dependencies

CS.smul · compiled type and proof/definition references.

source

@[instance_reducible]

instance CS.instHSMulReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} :

HSMul ℝ (CS n E) (CS n E)

Equations

CS.instHSMulReal = { hSMul := CS.smul }

Inspect dependencies

CS.instHSMulReal · compiled type and proof/definition references.

source

@[simp]

theorem CS.smul_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {f : CS n E} {R x : ℝ} :

(R • f).toFun x = R • f.toFun x

Inspect dependencies

CS.smul_apply · compiled type and proof/definition references.

source

theorem CS.continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : CS n E) :

Continuous f.toFun

Inspect dependencies

CS.continuous · compiled type and proof/definition references.

source

noncomputable def CS.deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : CS (n + 1) E) :

CS n E

Equations

f.deriv = { toFun := deriv f.toFun, h1 := ⋯, h2 := ⋯ }

Instances For

Inspect dependencies

CS.deriv · compiled type and proof/definition references.

source

theorem CS.hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : CS (n + 1) E) (x : ℝ) :

HasDerivAt f.toFun (f.deriv.toFun x) x

Inspect dependencies

CS.hasDerivAt · compiled type and proof/definition references.

source

theorem CS.deriv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {f : CS (n + 1) E} {x : ℝ} :

f.deriv.toFun x = _root_.deriv f.toFun x

Inspect dependencies

CS.deriv_apply · compiled type and proof/definition references.

source

theorem CS.deriv_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {R : ℝ} {f : CS (n + 1) E} :

(R • f).deriv = R • f.deriv

Inspect dependencies

CS.deriv_smul · compiled type and proof/definition references.

source

noncomputable def CS.scale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (g : CS n E) (R : ℝ) :

CS n E

Equations

g.scale R = if h : R = 0 then { toFun := 0, h1 := ⋯, h2 := ⋯ } else { toFun := fun (x : ℝ) => funscale g.toFun R x, h1 := ⋯, h2 := ⋯ }

Instances For

Inspect dependencies

CS.scale · compiled type and proof/definition references.

source

theorem CS.deriv_scale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {R : ℝ} {f : CS (n + 1) E} :

(f.scale R).deriv = R⁻¹ • f.deriv.scale R

Inspect dependencies

CS.deriv_scale · compiled type and proof/definition references.

source

theorem CS.deriv_scale' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {R v : ℝ} {f : CS (n + 1) E} :

(f.scale R).deriv.toFun v = R⁻¹ • f.deriv.toFun (R⁻¹ • v)

Inspect dependencies

CS.deriv_scale' · compiled type and proof/definition references.

source

theorem CS.hasDerivAt_scale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : CS (n + 1) E) (R x : ℝ) :

HasDerivAt (f.scale R).toFun (R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x)) x

Inspect dependencies

CS.hasDerivAt_scale · compiled type and proof/definition references.

source

theorem CS.tendsto_scale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : CS n E) (x : ℝ) :

Filter.Tendsto (fun (R : ℝ) => (f.scale R).toFun x) Filter.atTop (nhds (f.toFun 0))

Inspect dependencies

CS.tendsto_scale · compiled type and proof/definition references.

source

theorem CS.bounded {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {f : CS n E} :

∃ (C : ℝ), ∀ (v : ℝ), ‖f.toFun v‖ ≤ C

Inspect dependencies

CS.bounded · compiled type and proof/definition references.

source

@[instance_reducible]

instance trunc.instCoeFunForallReal :

CoeFun trunc fun (x : trunc) => ℝ → ℝ

Equations

trunc.instCoeFunForallReal = { coe := fun (f : trunc) => f.toFun }

Inspect dependencies

trunc.instCoeFunForallReal · compiled type and proof/definition references.

source

@[instance_reducible]

instance trunc.instCoeCSOfNatNatReal :

Coe trunc (CS 2 ℝ)

Equations

trunc.instCoeCSOfNatNatReal = { coe := trunc.toCS }

Inspect dependencies

trunc.instCoeCSOfNatNatReal · compiled type and proof/definition references.

source

theorem trunc.nonneg (g : trunc) (x : ℝ) :

0 ≤ g.toFun x

Inspect dependencies

trunc.nonneg · compiled type and proof/definition references.

source

theorem trunc.le_one (g : trunc) (x : ℝ) :

g.toFun x ≤ 1

Inspect dependencies

trunc.le_one · compiled type and proof/definition references.

source

theorem trunc.zero (g : trunc) :

g.toFun =ᶠ[nhds 0] 1

Inspect dependencies

trunc.zero · compiled type and proof/definition references.

source

@[simp]

theorem trunc.zero_at {g : trunc} :

g.toFun 0 = 1

Inspect dependencies

trunc.zero_at · compiled type and proof/definition references.

source

@[instance_reducible]

instance W1.instCoeFunForallReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} :

CoeFun (W1 n E) fun (x : W1 n E) => ℝ → E

Equations

W1.instCoeFunForallReal = { coe := W1.toFun }

Inspect dependencies

W1.instCoeFunForallReal · compiled type and proof/definition references.

source

theorem W1.continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : W1 n E) :

Continuous f.toFun

Inspect dependencies

W1.continuous · compiled type and proof/definition references.

source

theorem W1.differentiable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : W1 (n + 1) E) :

Differentiable ℝ f.toFun

Inspect dependencies

W1.differentiable · compiled type and proof/definition references.

source

theorem W1.iteratedDeriv_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {f g : ℝ → E} (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) :

iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g

Inspect dependencies

W1.iteratedDeriv_sub · compiled type and proof/definition references.

source

noncomputable def W1.deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : W1 (n + 1) E) :

W1 n E

Equations

f.deriv = { toFun := deriv f.toFun, smooth := ⋯, integrable := ⋯ }

Instances For

Inspect dependencies

W1.deriv · compiled type and proof/definition references.

source

theorem W1.hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : W1 (n + 1) E) (x : ℝ) :

HasDerivAt f.toFun (f.deriv.toFun x) x

Inspect dependencies

W1.hasDerivAt · compiled type and proof/definition references.

source

def W1.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f g : W1 n E) :

W1 n E

Equations

f.sub g = { toFun := f.toFun - g.toFun, smooth := ⋯, integrable := ⋯ }

Instances For

Inspect dependencies

W1.sub · compiled type and proof/definition references.

source

@[instance_reducible]

instance W1.instSub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} :

Sub (W1 n E)

Equations

W1.instSub = { sub := W1.sub }

Inspect dependencies

W1.instSub · compiled type and proof/definition references.

source

theorem W1.integrable_iteratedDeriv_Schwarz {n : ℕ} {f : SchwartzMap ℝ ℂ} :

MeasureTheory.Integrable (iteratedDeriv n ⇑f) MeasureTheory.volume

Inspect dependencies

W1.integrable_iteratedDeriv_Schwarz · compiled type and proof/definition references.

source

noncomputable def W1.of_Schwartz {n : ℕ} (f : SchwartzMap ℝ ℂ) :

W1 n ℂ

Equations

W1.of_Schwartz f = { toFun := ⇑f, smooth := ⋯, integrable := ⋯ }

Instances For

Inspect dependencies

W1.of_Schwartz · compiled type and proof/definition references.

source

noncomputable def W21.norm (f : ℝ → ℂ) :

ℝ

Equations

W21.norm f = (∫ (v : ℝ), ‖f v‖) + (4 * Real.pi ^ 2)⁻¹ * ∫ (v : ℝ), ‖deriv (deriv f) v‖

Instances For

Inspect dependencies

W21.norm · compiled type and proof/definition references.

source

theorem W21.norm_nonneg {f : ℝ → ℂ} :

0 ≤ norm f

Inspect dependencies

W21.norm_nonneg · compiled type and proof/definition references.

source

@[instance_reducible]

noncomputable instance W21.instNorm :

Norm W21

Equations

W21.instNorm = { norm := W21.norm ∘ W1.toFun }

Inspect dependencies

W21.instNorm · compiled type and proof/definition references.

source

@[instance_reducible]

noncomputable instance W21.instCoeSchwartzMapRealComplex :

Coe (SchwartzMap ℝ ℂ) W21

Equations

W21.instCoeSchwartzMapRealComplex = { coe := W1.of_Schwartz }

Inspect dependencies

W21.instCoeSchwartzMapRealComplex · compiled type and proof/definition references.

source

def W21.ofCS2 (f : CS 2 ℂ) :

W21

Equations

W21.ofCS2 f = { toFun := f.toFun, smooth := ⋯, integrable := ⋯ }

Instances For

Inspect dependencies

W21.ofCS2 · compiled type and proof/definition references.

source

@[instance_reducible]

instance W21.instCoeCSOfNatNatComplex :

Coe (CS 2 ℂ) W21

Equations

W21.instCoeCSOfNatNatComplex = { coe := W21.ofCS2 }

Inspect dependencies

W21.instCoeCSOfNatNatComplex · compiled type and proof/definition references.

source

@[instance_reducible]

instance W21.instHMulCSOfNatNatComplex :

HMul (CS 2 ℂ) W21 (CS 2 ℂ)

Equations

W21.instHMulCSOfNatNatComplex = { hMul := fun (g : CS 2 ℂ) (f : W21) => { toFun := g.toFun * f.toFun, h1 := ⋯, h2 := ⋯ } }

Inspect dependencies

W21.instHMulCSOfNatNatComplex · compiled type and proof/definition references.

source

@[instance_reducible]

instance W21.instHMulCSOfNatNatRealComplex :

HMul (CS 2 ℝ) W21 (CS 2 ℂ)

Equations

W21.instHMulCSOfNatNatRealComplex = { hMul := fun (g : CS 2 ℝ) (f : W21) => { toFun := fun (x : ℝ) => ↑(g.toFun x), h1 := ⋯, h2 := ⋯ } * f }

Inspect dependencies

W21.instHMulCSOfNatNatRealComplex · compiled type and proof/definition references.

source

theorem W21.hf (f : W21) :

MeasureTheory.Integrable f.toFun MeasureTheory.volume

Inspect dependencies

W21.hf · compiled type and proof/definition references.

source

theorem W21.hf' (f : W21) :

MeasureTheory.Integrable (deriv f.toFun) MeasureTheory.volume

Inspect dependencies

W21.hf' · compiled type and proof/definition references.

source

theorem W21.hf'' (f : W21) :

MeasureTheory.Integrable (deriv (deriv f.toFun)) MeasureTheory.volume

Inspect dependencies

W21.hf'' · compiled type and proof/definition references.

source

theorem W21_approximation (f : W21) (g : trunc) :

Filter.Tendsto (fun (R : ℝ) => ‖f - W21.ofCS2 (g.scale R * f)‖) Filter.atTop (nhds 0)

Inspect dependencies

W21_approximation · compiled type and proof/definition references.