Atlas.DifferentialAnalysis.code.CkBanach

theorem TestFunctions.ContDiffZeroAtInfty.differentiable {n : ℕ} (u : ContDiffZeroAtInfty n) :

Differentiable ℝ ⇑u.toZeroAtInftyContinuousMap

An element of ContDiffZeroAtInfty (a C¹ function on Euclidean space that vanishes at infinity) is differentiable as an underlying map.

source

theorem TestFunctions.ContDiffZeroAtInfty.toC0_injective {n : ℕ} :

Function.Injective toZeroAtInftyContinuousMap

The forgetful map from ContDiffZeroAtInfty to ZeroAtInftyContinuousMap is injective: an element of the former is determined by its underlying continuous map.

source

theorem TestFunctions.tendsto_partialDeriv_of_fderiv_eq {n : ℕ} (f : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (g : Fin n → EuclideanSpace ℝ (Fin n) → ℂ) (heq : ∀ (j : Fin n) (x : EuclideanSpace ℝ (Fin n)), (fderiv ℝ (⇑f) x) (EuclideanSpace.single j 1) = g j x) (htend : ∀ (j : Fin n), Filter.Tendsto (g j) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)) (j : Fin n) :

Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => (fderiv ℝ (⇑f) x) (EuclideanSpace.single j 1)) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

If for each direction j the partial derivative of f agrees with a function g j that vanishes at infinity, then the partial derivative of f itself vanishes at infinity.

source

@[implicit_reducible]

noncomputable instance TestFunctions.instZeroContDiffZeroAtInfty {n : ℕ} :

Zero (ContDiffZeroAtInfty n)

The zero element of ContDiffZeroAtInfty n: the constant 0.

source

@[implicit_reducible]

noncomputable instance TestFunctions.instAddContDiffZeroAtInfty {n : ℕ} :

Add (ContDiffZeroAtInfty n)

Pointwise addition on ContDiffZeroAtInfty n.

source

@[implicit_reducible]

noncomputable instance TestFunctions.instNegContDiffZeroAtInfty {n : ℕ} :

Neg (ContDiffZeroAtInfty n)

Pointwise negation on ContDiffZeroAtInfty n.

source

@[implicit_reducible]

noncomputable instance TestFunctions.instSubContDiffZeroAtInfty {n : ℕ} :

Sub (ContDiffZeroAtInfty n)

Pointwise subtraction on ContDiffZeroAtInfty n.

source

@[implicit_reducible]

noncomputable instance TestFunctions.instSMulComplexContDiffZeroAtInfty {n : ℕ} :

SMul ℂ (ContDiffZeroAtInfty n)

The complex scalar action on ContDiffZeroAtInfty n by pointwise multiplication.

source

@[implicit_reducible]

noncomputable instance TestFunctions.instSMulNatContDiffZeroAtInfty {n : ℕ} :

SMul ℕ (ContDiffZeroAtInfty n)

The natural-number scalar action on ContDiffZeroAtInfty n (repeated addition), required for the AddCommGroup structure.

source

@[implicit_reducible]

noncomputable instance TestFunctions.instSMulIntContDiffZeroAtInfty {n : ℕ} :

SMul ℤ (ContDiffZeroAtInfty n)

The integer scalar action on ContDiffZeroAtInfty n, required for the AddCommGroup structure.

source

@[implicit_reducible]

noncomputable instance TestFunctions.ContDiffZeroAtInfty.instAddCommGroup {n : ℕ} :

AddCommGroup (ContDiffZeroAtInfty n)

ContDiffZeroAtInfty n is an additive commutative group, inherited from the underlying continuous functions via the injective forgetful map.

source

@[implicit_reducible]

noncomputable instance TestFunctions.ContDiffZeroAtInfty.instModule {n : ℕ} :

Module ℂ (ContDiffZeroAtInfty n)

ContDiffZeroAtInfty n is a complex vector space, inherited from the underlying continuous functions via the injective forgetful map.

source

@[implicit_reducible]

noncomputable instance TestFunctions.ContDiffZeroAtInfty.instNorm {n : ℕ} :

Norm (ContDiffZeroAtInfty n)

The C¹ norm on ContDiffZeroAtInfty n, defined as the ckNorm (sum of the sup-norm of the function and the sup-norms of its partial derivatives) at order one.

source

theorem TestFunctions.ContDiffZeroAtInfty.norm_def {n : ℕ} (u : ContDiffZeroAtInfty n) :

‖u‖ = (⨆ (x : EuclideanSpace ℝ (Fin n)), ‖u.toZeroAtInftyContinuousMap x‖) + ∑ j : Fin n, ⨆ (x : EuclideanSpace ℝ (Fin n)), ‖(fderiv ℝ (⇑u.toZeroAtInftyContinuousMap) x) (EuclideanSpace.single j 1)‖

Unfolding the C¹ norm on ContDiffZeroAtInfty n as the supremum norm of the function plus the sum over coordinates of the supremum norms of the partial derivatives.

source

theorem TestFunctions.ContDiffZeroAtInfty.c1_norm_nonneg {n : ℕ} (u : ContDiffZeroAtInfty n) :

0 ≤ ‖u‖

The C¹ norm on ContDiffZeroAtInfty n is nonnegative.

source

theorem TestFunctions.ContDiffZeroAtInfty.c1_norm_zero {n : ℕ} :

‖0‖ = 0

The C¹ norm of the zero element of ContDiffZeroAtInfty n is zero.