Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Smooth test-function adapters

This file connects the coordinate gradient/Hessian data used by semijets with mathlib's continuous-linear derivative definitions and theorems. The Taylor theorems for smooth test functions are phrased using continuous linear and multilinear maps, while the viscosity solution definitions use concrete finite coordinate gradients and Hessian matrices.

def ViscositySolns.coordinateVector {n : ℕ} (i : Fin n) : Point n

The coordinate basis vector with value 1 at i and 0 elsewhere.

Equations

• ViscositySolns.coordinateVector i j = if i = j then 1 else 0

@[simp]

theorem ViscositySolns.coordinateVector_apply {n : ℕ} (i j : Fin n) : coordinateVector i j = if i = j then 1 else 0

theorem ViscositySolns.coordinateVector_apply_self {n : ℕ} (i : Fin n) : coordinateVector i i = 1

theorem ViscositySolns.point_eq_sum_coordinateVector {n : ℕ} (v : Point n) : ∑ i : Fin n, v i • coordinateVector i = v

def ViscositySolns.gradientLinearMap {n : ℕ} (p : Point n) : Point n →L[ℝ] ℝ

The continuous linear functional represented by a coordinate gradient.

Equations

• ViscositySolns.gradientLinearMap p = ∑ i : Fin n, (ContinuousLinearMap.proj i).smulRight (p i)

@[simp]

theorem ViscositySolns.gradientLinearMap_apply {n : ℕ} (p v : Point n) : (gradientLinearMap p) v = p ⬝ᵥ v

def ViscositySolns.linearMapGradient {n : ℕ} (D : Point n →L[ℝ] ℝ) : Point n

The coordinate gradient represented by a continuous linear functional.

Equations

• ViscositySolns.linearMapGradient D i = D (ViscositySolns.coordinateVector i)

@[simp]

theorem ViscositySolns.linearMapGradient_apply {n : ℕ} (D : Point n →L[ℝ] ℝ) (i : Fin n) : linearMapGradient D i = D (coordinateVector i)

noncomputable def ViscositySolns.linearMapGradientCLM {n : ℕ} : (Point n →L[ℝ] ℝ) →L[ℝ] Point n

The coordinate-gradient extraction map as a continuous linear map.

In quantified mathematical form, this sends a continuous linear functional D : R^n ->L R to the vector whose i-th coordinate is D e_i.

Equations

• ViscositySolns.linearMapGradientCLM = ContinuousLinearMap.pi fun (i : Fin n) => (ContinuousLinearMap.apply ℝ ℝ) (ViscositySolns.coordinateVector i)

@[simp]

theorem ViscositySolns.linearMapGradientCLM_apply {n : ℕ} (D : Point n →L[ℝ] ℝ) : linearMapGradientCLM D = linearMapGradient D

@[simp]

theorem ViscositySolns.gradientLinearMap_linearMapGradient {n : ℕ} (D : Point n →L[ℝ] ℝ) : gradientLinearMap (linearMapGradient D) = D

@[simp]

theorem ViscositySolns.linearMapGradient_gradientLinearMap {n : ℕ} (p : Point n) : linearMapGradient (gradientLinearMap p) = p

noncomputable def ViscositySolns.hessianBilinearMap {n : ℕ} (X : Hessian n) : Point n →L[ℝ] Point n →L[ℝ] ℝ

The continuous bilinear form represented by a coordinate Hessian matrix.

Equations

• ViscositySolns.hessianBilinearMap X = ∑ i : Fin n, (ContinuousLinearMap.proj i).smulRight (ViscositySolns.gradientLinearMap (X i))

@[simp]

theorem ViscositySolns.hessianBilinearMap_apply {n : ℕ} (X : Hessian n) (v w : Point n) : ((hessianBilinearMap X) v) w = Matrix.mulVec X w ⬝ᵥ v

def ViscositySolns.bilinearMapHessian {n : ℕ} (D2 : Point n →L[ℝ] Point n →L[ℝ] ℝ) : Hessian n

The coordinate Hessian represented by a continuous bilinear map.

Equations

• ViscositySolns.bilinearMapHessian D2 i j = (D2 (ViscositySolns.coordinateVector i)) (ViscositySolns.coordinateVector j)

@[simp]

theorem ViscositySolns.bilinearMapHessian_apply {n : ℕ} (D2 : Point n →L[ℝ] Point n →L[ℝ] ℝ) (i j : Fin n) : bilinearMapHessian D2 i j = (D2 (coordinateVector i)) (coordinateVector j)

@[simp]

theorem ViscositySolns.hessianBilinearMap_bilinearMapHessian {n : ℕ} (D2 : Point n →L[ℝ] Point n →L[ℝ] ℝ) : hessianBilinearMap (bilinearMapHessian D2) = D2

@[simp]

theorem ViscositySolns.bilinearMapHessian_hessianBilinearMap {n : ℕ} (X : Hessian n) : bilinearMapHessian (hessianBilinearMap X) = X

def ViscositySolns.Jet.toFirstDerivative {n : ℕ} (J : Jet n) : Point n →L[ℝ] ℝ

The first Fréchet derivative represented by a jet's coordinate gradient.

Equations

• J.toFirstDerivative = ViscositySolns.gradientLinearMap J.gradient

noncomputable def ViscositySolns.Jet.toSecondDerivative {n : ℕ} (J : Jet n) : Point n →L[ℝ] Point n →L[ℝ] ℝ

The second Fréchet derivative represented by a jet's coordinate Hessian.

Equations

• J.toSecondDerivative = ViscositySolns.hessianBilinearMap J.hessian

def ViscositySolns.Jet.ofDerivatives {n : ℕ} (Dφ : Point n →L[ℝ] ℝ) (D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ) : Jet n

The coordinate jet represented by continuous first- and second-derivative maps.

Equations

• ViscositySolns.Jet.ofDerivatives Dφ D2φ = { gradient := ViscositySolns.linearMapGradient Dφ, hessian := ViscositySolns.bilinearMapHessian D2φ }

@[simp]

theorem ViscositySolns.Jet.toFirstDerivative_apply {n : ℕ} (J : Jet n) (v : Point n) : J.toFirstDerivative v = J.gradient ⬝ᵥ v

@[simp]

theorem ViscositySolns.Jet.toSecondDerivative_apply {n : ℕ} (J : Jet n) (v w : Point n) : (J.toSecondDerivative v) w = Matrix.mulVec J.hessian w ⬝ᵥ v

@[simp]

theorem ViscositySolns.Jet.toFirstDerivative_ofDerivatives {n : ℕ} (Dφ : Point n →L[ℝ] ℝ) (D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ) : (ofDerivatives Dφ D2φ).toFirstDerivative = Dφ

@[simp]

theorem ViscositySolns.Jet.toSecondDerivative_ofDerivatives {n : ℕ} (Dφ : Point n →L[ℝ] ℝ) (D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ) : (ofDerivatives Dφ D2φ).toSecondDerivative = D2φ

@[simp]

theorem ViscositySolns.Jet.ofDerivatives_toFirst_toSecond {n : ℕ} (J : Jet n) : ofDerivatives J.toFirstDerivative J.toSecondDerivative = J

theorem ViscositySolns.quadraticModel_eq_linearMap {n : ℕ} (x0 : Point n) (r : ℝ) (J : Jet n) (x : Point n) : quadraticModel x0 r J.gradient J.hessian x = r + J.toFirstDerivative (x - x0) + 1 / 2 * (J.toSecondDerivative (x - x0)) (x - x0)

The concrete quadratic model is the Taylor polynomial built from the continuous linear maps associated to a coordinate jet.

theorem ViscositySolns.quadraticModelJetAt_mem_superjet {n : ℕ} {C : Set (Point n)} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) (x : Point n) : quadraticModelJetAt x0 p X x ∈ Superjet C (fun (y : Point n) => quadraticModel x0 r p X y) x

The recentered jet of a quadratic model is a superjet of that quadratic model.

This is the exact-touching test-function fact used by Perron bump certification and by smooth-selection arguments.

theorem ViscositySolns.quadraticModelJetAt_mem_subjet {n : ℕ} {C : Set (Point n)} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) (x : Point n) : quadraticModelJetAt x0 p X x ∈ Subjet C (fun (y : Point n) => quadraticModel x0 r p X y) x

The recentered jet of a quadratic model is also a subjet of that quadratic model.