theorem TestFunctions.ContDiffZeroAtInfty.bddAbove_range_norm_val {n : ℕ} (u : ContDiffZeroAtInfty n) : BddAbove (Set.range fun (x : EuclideanSpace ℝ (Fin n)) => ‖u.toZeroAtInftyContinuousMap x‖)

The range of the pointwise norm of a ContDiffZeroAtInfty element is bounded above.

theorem TestFunctions.ContDiffZeroAtInfty.continuous_partialDeriv {n : ℕ} (u : ContDiffZeroAtInfty n) (j : Fin n) : Continuous fun (x : EuclideanSpace ℝ (Fin n)) => (fderiv ℝ (⇑u.toZeroAtInftyContinuousMap) x) (EuclideanSpace.single j 1)

The j-th partial derivative of a ContDiffZeroAtInfty element is continuous.

noncomputable def TestFunctions.ContDiffZeroAtInfty.partialDerivC0 {n : ℕ} (u : ContDiffZeroAtInfty n) (j : Fin n) : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ

The j-th partial derivative of u as a C₀ continuous function (vanishing at infinity).

theorem TestFunctions.ContDiffZeroAtInfty.bddAbove_range_norm_deriv {n : ℕ} (u : ContDiffZeroAtInfty n) (j : Fin n) : BddAbove (Set.range fun (x : EuclideanSpace ℝ (Fin n)) => ‖(fderiv ℝ (⇑u.toZeroAtInftyContinuousMap) x) (EuclideanSpace.single j 1)‖)

The range of the norm of the j-th partial derivative is bounded above.

theorem TestFunctions.ContDiffZeroAtInfty.norm_apply_le_iSup {n : ℕ} (u : ContDiffZeroAtInfty n) (x : EuclideanSpace ℝ (Fin n)) : ‖u.toZeroAtInftyContinuousMap x‖ ≤ ⨆ (y : EuclideanSpace ℝ (Fin n)), ‖u.toZeroAtInftyContinuousMap y‖

Pointwise norm of u at x is bounded by the supremum of ‖u y‖.

theorem TestFunctions.ContDiffZeroAtInfty.norm_deriv_apply_le_iSup {n : ℕ} (u : ContDiffZeroAtInfty n) (j : Fin n) (x : EuclideanSpace ℝ (Fin n)) : ‖(fderiv ℝ (⇑u.toZeroAtInftyContinuousMap) x) (EuclideanSpace.single j 1)‖ ≤ ⨆ (y : EuclideanSpace ℝ (Fin n)), ‖(fderiv ℝ (⇑u.toZeroAtInftyContinuousMap) y) (EuclideanSpace.single j 1)‖

Pointwise norm of the j-th partial derivative at x is bounded by the supremum.

theorem TestFunctions.ContDiffZeroAtInfty.c1_norm_add_le {n : ℕ} (u v : ContDiffZeroAtInfty n) : ‖u + v‖ ≤ ‖u‖ + ‖v‖

Triangle inequality for the C^1₀ norm on ContDiffZeroAtInfty n.

theorem TestFunctions.ContDiffZeroAtInfty.c1_norm_smul {n : ℕ} (c : ℂ) (u : ContDiffZeroAtInfty n) : ‖c • u‖ = ‖c‖ * ‖u‖

Scalar homogeneity of the C^1₀ norm: ‖c • u‖ = ‖c‖ * ‖u‖.

theorem TestFunctions.ContDiffZeroAtInfty.c1_norm_eq_zero_iff {n : ℕ} (u : ContDiffZeroAtInfty n) : ‖u‖ = 0 ↔ u = 0

Separation: the C^1₀ norm vanishes iff the element is zero.

theorem TestFunctions.ContDiffZeroAtInfty.normedSpaceCore {n : ℕ} : NormedSpace.Core ℂ (ContDiffZeroAtInfty n)

Core data for the NormedSpace structure on ContDiffZeroAtInfty n.

@[implicit_reducible]

noncomputable instance TestFunctions.ContDiffZeroAtInfty.instNormedAddCommGroup {n : ℕ} : NormedAddCommGroup (ContDiffZeroAtInfty n)

The NormedAddCommGroup instance on ContDiffZeroAtInfty n via the C^1₀ norm.

@[implicit_reducible]

noncomputable instance TestFunctions.ContDiffZeroAtInfty.instNormedSpace {n : ℕ} : NormedSpace ℂ (ContDiffZeroAtInfty n)

The ℂ-NormedSpace instance on ContDiffZeroAtInfty n.

theorem TestFunctions.ContDiffZeroAtInfty.sub_partialDerivC0 {n : ℕ} (u v : ContDiffZeroAtInfty n) (j : Fin n) : (u - v).partialDerivC0 j = u.partialDerivC0 j - v.partialDerivC0 j

The j-th partial derivative is additive on differences.

theorem TestFunctions.ContDiffZeroAtInfty.c0_norm_le {n : ℕ} (f : ContDiffZeroAtInfty n) : ‖f.toZeroAtInftyContinuousMap‖ ≤ ‖f‖

The C₀ norm of the underlying continuous map is bounded by the C^1₀ norm.

theorem TestFunctions.ContDiffZeroAtInfty.pd_norm_le {n : ℕ} (f : ContDiffZeroAtInfty n) (j : Fin n) : ‖f.partialDerivC0 j‖ ≤ ‖f‖

The C₀ norm of the j-th partial derivative is bounded by the C^1₀ norm of f.

noncomputable def TestFunctions.ContDiffZeroAtInfty.ofLimitData {n : ℕ} (v : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (w : Fin n → ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (u : ℕ → ContDiffZeroAtInfty n) (hv : Filter.Tendsto (fun (k : ℕ) => (u k).toZeroAtInftyContinuousMap) Filter.atTop (nhds v)) (hw : ∀ (j : Fin n), Filter.Tendsto (fun (k : ℕ) => (u k).partialDerivC0 j) Filter.atTop (nhds (w j))) : ContDiffZeroAtInfty n

Reconstruct a ContDiffZeroAtInfty element from a sequence converging uniformly with its partial derivatives.

theorem TestFunctions.ContDiffZeroAtInfty.ofLimitData_toC0 {n : ℕ} (v : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (w : Fin n → ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (u : ℕ → ContDiffZeroAtInfty n) (hv : Filter.Tendsto (fun (k : ℕ) => (u k).toZeroAtInftyContinuousMap) Filter.atTop (nhds v)) (hw : ∀ (j : Fin n), Filter.Tendsto (fun (k : ℕ) => (u k).partialDerivC0 j) Filter.atTop (nhds (w j))) : (ofLimitData v w u hv hw).toZeroAtInftyContinuousMap = v

The underlying C₀ map of the reconstructed limit equals v.

theorem TestFunctions.ContDiffZeroAtInfty.ofLimitData_pd {n : ℕ} (v : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (w : Fin n → ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (u : ℕ → ContDiffZeroAtInfty n) (hv : Filter.Tendsto (fun (k : ℕ) => (u k).toZeroAtInftyContinuousMap) Filter.atTop (nhds v)) (hw : ∀ (j : Fin n), Filter.Tendsto (fun (k : ℕ) => (u k).partialDerivC0 j) Filter.atTop (nhds (w j))) (j : Fin n) : (ofLimitData v w u hv hw).partialDerivC0 j = w j

The j-th partial derivative of the reconstructed limit equals w j.

theorem TestFunctions.ContDiffZeroAtInfty.c1_banach (n : ℕ) : CompleteSpace (ContDiffZeroAtInfty n)

Melrose Proposition 6.3: C^1₀(ℝⁿ) is a Banach space (complete in the C^1₀ norm).