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

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

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

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

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

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

@[reducible, inline]

abbrev W21 : Type

Equations

• W21 = W1 2 ℂ

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

Equations

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

theorem contDiff_ofReal : ContDiff ℝ (↑⊤) Complex.ofReal

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))

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 }

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 := ⋯ } }

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 := ⋯ }

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

Equations

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

@[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

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 := ⋯ }

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 }

@[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

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

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 := ⋯ }

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

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

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

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 := ⋯ }

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

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)

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

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))

theorem CS.bounded {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {f : CS n E} : ∃ (C : ℝ), ∀ (v : ℝ), ‖f.toFun v‖ ≤ C

instance trunc.instCoeFunForallReal : CoeFun trunc fun (x : trunc) => ℝ → ℝ

Equations

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

instance trunc.instCoeCSOfNatNatReal : Coe trunc (CS 2 ℝ)

Equations

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

theorem trunc.nonneg (g : trunc) (x : ℝ) : 0 ≤ g.toFun x

theorem trunc.le_one (g : trunc) (x : ℝ) : g.toFun x ≤ 1

theorem trunc.zero (g : trunc) : g.toFun =ᶠ[nhds 0] 1

@[simp]

theorem trunc.zero_at {g : trunc} : g.toFun 0 = 1

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 }

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

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

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

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 := ⋯ }

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

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 := ⋯ }

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

Equations

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

theorem W1.integrable_iteratedDeriv_Schwarz {n : ℕ} {f : SchwartzMap ℝ ℂ} : MeasureTheory.Integrable (iteratedDeriv n ⇑f) MeasureTheory.volume

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

Equations

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

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

Equations

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

theorem W21.norm_nonneg {f : ℝ → ℂ} : 0 ≤ norm f

noncomputable instance W21.instNorm : Norm W21

Equations

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

noncomputable instance W21.instCoeSchwartzMapRealComplex : Coe (SchwartzMap ℝ ℂ) W21

Equations

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

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

Equations

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

instance W21.instCoeCSOfNatNatComplex : Coe (CS 2 ℂ) W21

Equations

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

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 := ⋯ } }

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 }

theorem W21.hf (f : W21) : MeasureTheory.Integrable f.toFun MeasureTheory.volume

theorem W21.hf' (f : W21) : MeasureTheory.Integrable (deriv f.toFun) MeasureTheory.volume

theorem W21.hf'' (f : W21) : MeasureTheory.Integrable (deriv (deriv f.toFun)) MeasureTheory.volume

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