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

Taylor bridges for test functions

This file packages Taylor-style little-oh remainders into the abstract second-order expansion predicate used by the viscosity solution definitions.

def ViscositySolns.IsSymmetricBilinear {n : ℕ} (D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ) : Prop

Symmetry of a bundled bilinear second-derivative map.

Equations

• ViscositySolns.IsSymmetricBilinear D2φ = ∀ (v w : ViscositySolns.Point n), (D2φ v) w = (D2φ w) v

theorem ViscositySolns.isSymmetricBilinear_fderivWithin_fderivWithin {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} {x0 : Point n} (h : IsSymmSndFDerivWithinAt ℝ φ C x0) : IsSymmetricBilinear (fderivWithin ℝ (fderivWithin ℝ φ C) C x0)

Mathlib's symmetry predicate for the second derivative gives the bundled bilinear symmetry used by the Taylor model derivative.

noncomputable def ViscositySolns.frechetSecondOrderModel {n : ℕ} (x0 : Point n) (r : ℝ) (Dφ : Point n →L[ℝ] ℝ) (D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ) (x : Point n) : ℝ

The second-order Taylor polynomial written using Fréchet derivative data rather than coordinate gradients and Hessian matrices.

Equations

• ViscositySolns.frechetSecondOrderModel x0 r Dφ D2φ x = r + Dφ (x - x0) + 1 / 2 * (D2φ (x - x0)) (x - x0)

@[simp]

theorem ViscositySolns.frechetSecondOrderModel_of_jet {n : ℕ} (x0 : Point n) (r : ℝ) (J : Jet n) (x : Point n) : frechetSecondOrderModel x0 r J.toFirstDerivative J.toSecondDerivative x = quadraticModel x0 r J.gradient J.hessian x

theorem ViscositySolns.contDiff_quadraticModel {n : ℕ} {k : WithTop ℕ∞} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : ContDiff ℝ k fun (x : Point n) => quadraticModel x0 r p X x

Fixed quadratic models are smooth.

In quantified mathematical form, for fixed x0, r, p, and X, the function x ↦ r + p · (x - x0) + (1 / 2) ⟪X(x - x0), x - x0⟫ is C^k for every differentiability order k.

theorem ViscositySolns.hasFDerivWithinAt_frechetSecondOrderModel {n : ℕ} {C : Set (Point n)} (x0 : Point n) (r : ℝ) (Dφ : Point n →L[ℝ] ℝ) (D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ) (hD2φ : IsSymmetricBilinear D2φ) (x : Point n) : HasFDerivWithinAt (fun (y : Point n) => frechetSecondOrderModel x0 r Dφ D2φ y) (Dφ + D2φ (x - x0)) C x

For a symmetric bilinear second derivative, the derivative of the Fréchet quadratic model at x is Dφ + D²φ (x - x₀).

theorem ViscositySolns.hasFDerivWithinAt_frechetSecondOrderResidual {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} {x0 x : Point n} {Dφ : Point n →L[ℝ] ℝ} {D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ} {Dφ_at : Point n → Point n →L[ℝ] ℝ} (hD2φ : IsSymmetricBilinear D2φ) (hφ : HasFDerivWithinAt φ (Dφ_at x) C x) : HasFDerivWithinAt (fun (y : Point n) => φ y - frechetSecondOrderModel x0 (φ x0) Dφ D2φ y) (Dφ_at x - (Dφ + D2φ (x - x0))) C x

Derivative of the residual after subtracting the Fréchet second-order model.

theorem ViscositySolns.frechetDerivativeResidual_isLittleO_of_hasFDerivWithinAt {n : ℕ} {C : Set (Point n)} {x0 : Point n} {Dφ : Point n →L[ℝ] ℝ} {D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ} {Dφ_at : Point n → Point n →L[ℝ] ℝ} (hDφ0 : Dφ_at x0 = Dφ) (hDφ_deriv : HasFDerivWithinAt Dφ_at D2φ C x0) : (fun (x : Point n) => Dφ_at x - (Dφ + D2φ (x - x0))) =o[nhdsWithin x0 C] fun (x : Point n) => ‖x - x0‖

If the first-derivative map has derivative D²φ at x₀, then the derivative residual for the second-order Taylor model is o(‖x - x₀‖).

theorem ViscositySolns.hasSecondOrderExpansionWithin_of_frechetLittleO {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} {x0 : Point n} {J : Jet n} (hφ : (fun (x : Point n) => φ x - frechetSecondOrderModel x0 (φ x0) J.toFirstDerivative J.toSecondDerivative x) =o[nhdsWithin x0 C] fun (x : Point n) => ‖x - x0‖ ^ 2) : HasSecondOrderExpansionWithin C φ x0 J

A Fréchet second-order Taylor expansion with coordinate derivative data gives the abstract second-order expansion predicate used for viscosity test functions.

theorem ViscositySolns.hasSecondOrderExpansionWithin_of_frechetTaylor {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} {x0 : Point n} {J : Jet n} {Dφ : Point n →L[ℝ] ℝ} {D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ} (hDφ : Dφ = J.toFirstDerivative) (hD2φ : D2φ = J.toSecondDerivative) (hφ : (fun (x : Point n) => φ x - frechetSecondOrderModel x0 (φ x0) Dφ D2φ x) =o[nhdsWithin x0 C] fun (x : Point n) => ‖x - x0‖ ^ 2) : HasSecondOrderExpansionWithin C φ x0 J

Version of hasSecondOrderExpansionWithin_of_frechetLittleO with explicit Fréchet derivative maps. The equalities identify those maps with the coordinate jet data.

theorem ViscositySolns.isLittleO_second_order_of_hasFDerivWithinAt_isLittleO_deriv {n : ℕ} {C : Set (Point n)} {x0 : Point n} {R : Point n → ℝ} {R' : Point n → Point n →L[ℝ] ℝ} (hC : Convex ℝ C) (hx0 : x0 ∈ C) (hRderiv : ∀ x ∈ C, HasFDerivWithinAt R (R' x) C x) (hR' : R' =o[nhdsWithin x0 C] fun (x : Point n) => ‖x - x0‖) (hR0 : R x0 = 0) : R =o[nhdsWithin x0 C] fun (x : Point n) => ‖x - x0‖ ^ 2

Mean-value upgrade from a little-oh first-derivative residual to a second-order little-oh residual on a convex domain.

theorem ViscositySolns.frechetLittleO_of_hasFDerivWithinAt_isLittleO_deriv {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} {x0 : Point n} {Dφ : Point n →L[ℝ] ℝ} {D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ} {R' : Point n → Point n →L[ℝ] ℝ} (hC : Convex ℝ C) (hx0 : x0 ∈ C) (hRderiv : ∀ x ∈ C, HasFDerivWithinAt (fun (y : Point n) => φ y - frechetSecondOrderModel x0 (φ x0) Dφ D2φ y) (R' x) C x) (hR' : R' =o[nhdsWithin x0 C] fun (x : Point n) => ‖x - x0‖) : (fun (x : Point n) => φ x - frechetSecondOrderModel x0 (φ x0) Dφ D2φ x) =o[nhdsWithin x0 C] fun (x : Point n) => ‖x - x0‖ ^ 2

If the residual after subtracting the Fréchet second-order Taylor polynomial has first derivative o(‖x - x₀‖), then it has the little-oh remainder needed for the viscosity expansion predicate.

theorem ViscositySolns.hasSecondOrderExpansionWithin_of_frechetDerivativeRemainder {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} {x0 : Point n} {J : Jet n} {Dφ : Point n →L[ℝ] ℝ} {D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ} {R' : Point n → Point n →L[ℝ] ℝ} (hC : Convex ℝ C) (hx0 : x0 ∈ C) (hDφ : Dφ = J.toFirstDerivative) (hD2φ : D2φ = J.toSecondDerivative) (hRderiv : ∀ x ∈ C, HasFDerivWithinAt (fun (y : Point n) => φ y - frechetSecondOrderModel x0 (φ x0) Dφ D2φ y) (R' x) C x) (hR' : R' =o[nhdsWithin x0 C] fun (x : Point n) => ‖x - x0‖) : HasSecondOrderExpansionWithin C φ x0 J

A derivative-residual form of the Fréchet Taylor bridge. This is often easier to feed from continuity of the second derivative than the final little-oh remainder itself.

theorem ViscositySolns.hasSecondOrderExpansionWithin_of_frechetC2Data {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} {x0 : Point n} {J : Jet n} {Dφ : Point n →L[ℝ] ℝ} {D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ} {Dφ_at : Point n → Point n →L[ℝ] ℝ} (hC : Convex ℝ C) (hx0 : x0 ∈ C) (hD2sym : IsSymmetricBilinear D2φ) (hDφ : Dφ = J.toFirstDerivative) (hD2φ : D2φ = J.toSecondDerivative) (hDφ0 : Dφ_at x0 = Dφ) (hφ_deriv : ∀ x ∈ C, HasFDerivWithinAt φ (Dφ_at x) C x) (hDφ_deriv : HasFDerivWithinAt Dφ_at D2φ C x0) : HasSecondOrderExpansionWithin C φ x0 J

Smooth-test-function bridge from first- and second-derivative data. The hypotheses say that Dφ_at is the Fréchet derivative of φ on C, that Dφ_at has derivative D²φ at x₀, and that this derivative data matches the coordinate jet.

theorem ViscositySolns.hasSecondOrderExpansionWithin_of_fderivWithinC2Data {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} {x0 : Point n} {J : Jet n} (hC : Convex ℝ C) (hx0 : x0 ∈ C) (hD2sym : IsSymmSndFDerivWithinAt ℝ φ C x0) (hDφ : fderivWithin ℝ φ C x0 = J.toFirstDerivative) (hD2φ : fderivWithin ℝ (fderivWithin ℝ φ C) C x0 = J.toSecondDerivative) (hφ_deriv : ∀ x ∈ C, HasFDerivWithinAt φ (fderivWithin ℝ φ C x) C x) (hDφ_deriv : HasFDerivWithinAt (fderivWithin ℝ φ C) (fderivWithin ℝ (fderivWithin ℝ φ C) C x0) C x0) : HasSecondOrderExpansionWithin C φ x0 J

Canonical fderivWithin version of the smooth-test-function bridge. This specializes hasSecondOrderExpansionWithin_of_frechetC2Data to mathlib's chosen first and second derivative maps.

theorem ViscositySolns.hasSecondOrderExpansionWithin_of_fderivWithinDifferentiable {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} {x0 : Point n} {J : Jet n} (hC : Convex ℝ C) (hx0 : x0 ∈ C) (hD2sym : IsSymmSndFDerivWithinAt ℝ φ C x0) (hDφ : fderivWithin ℝ φ C x0 = J.toFirstDerivative) (hD2φ : fderivWithin ℝ (fderivWithin ℝ φ C) C x0 = J.toSecondDerivative) (hφ_diff : ∀ x ∈ C, DifferentiableWithinAt ℝ φ C x) (hDφ_diff : DifferentiableWithinAt ℝ (fderivWithin ℝ φ C) C x0) : HasSecondOrderExpansionWithin C φ x0 J

Canonical fderivWithin theorem with differentiability hypotheses. The derivative maps are mathlib's fderivWithin choices.

theorem ViscositySolns.hasSecondOrderExpansionWithin_of_contDiffOn_two {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} {x0 : Point n} {J : Jet n} (hC : Convex ℝ C) (huniq : UniqueDiffOn ℝ C) (hx0 : x0 ∈ C) (hx0_closure : x0 ∈ closure (interior C)) (hφ : ContDiffOn ℝ 2 φ C) (hDφ : fderivWithin ℝ φ C x0 = J.toFirstDerivative) (hD2φ : fderivWithin ℝ (fderivWithin ℝ φ C) C x0 = J.toSecondDerivative) : HasSecondOrderExpansionWithin C φ x0 J

C^2 functions on a uniquely differentiable convex domain have the abstract second-order expansion associated to their canonical fderivWithin data.