Documentation

LeanPool.ViscositySolutionTheory.ViscositySolns.TestFunctions.Solutions

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

Smooth test functions for viscosity solutions #

This file packages the Taylor bridge for C^2 test functions into the subsolution and supersolution inequalities.

source
noncomputable def ViscositySolns.smoothTestJetWithin {n : ℕ} (C : Set (Point n)) (φ : Point n → ℝ) (x : Point n) :
Jet n

The coordinate jet obtained from mathlib's canonical first and second fderivWithin maps for a test function on a set.

Equations
Instances For
    source
    theorem ViscositySolns.smoothTestJetWithin_congr_nhdsWithin {n : ℕ} {C D : Set (Point n)} {φ : Point n → ℝ} {x : Point n} (h : nhdsWithin x C = nhdsWithin x D) :
    smoothTestJetWithin C φ x = smoothTestJetWithin D φ x

    The canonical smooth test jet only depends on the germ of the domain at the base point.

    source
    theorem ViscositySolns.continuousOn_smoothTestJetWithin {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} (huniq : UniqueDiffOn ℝ C) (hφ : ContDiffOn ℝ 2 φ C) :
    ContinuousOn (smoothTestJetWithin C φ) C

    The canonical smooth test jet varies continuously on the domain whenever the test function is C^2 there.

    source
    theorem ViscositySolns.ViscositySubsolution.of_touchesAbove_contDiffOn_two {n : ℕ} {C : Set (Point n)} {F : Operator n} {u φ : Point n → ℝ} {x : Point n} {J : Jet n} (hu : ViscositySubsolution C F u) (hC : Convex ℝ C) (huniq : UniqueDiffOn ℝ C) (hx : x ∈ C) (hx_closure : x ∈ closure (interior C)) (htouch : TouchesAboveOn C u φ x) (hφ : ContDiffOn ℝ 2 φ C) (hDφ : fderivWithin ℝ φ C x = J.toFirstDerivative) (hD2φ : fderivWithin ℝ (fderivWithin ℝ φ C) C x = J.toSecondDerivative) :
    F x (u x) J.gradient J.hessian ≤ 0

    A viscosity subsolution satisfies the expected inequality for every C^2 test function touching from above, provided its canonical fderivWithin data matches the coordinate jet.

    source
    theorem ViscositySolns.ViscositySubsolution.of_touchesAbove_contDiffOn_two_smoothTestJetWithin {n : ℕ} {C : Set (Point n)} {F : Operator n} {u φ : Point n → ℝ} {x : Point n} (hu : ViscositySubsolution C F u) (hC : Convex ℝ C) (huniq : UniqueDiffOn ℝ C) (hx : x ∈ C) (hx_closure : x ∈ closure (interior C)) (htouch : TouchesAboveOn C u φ x) (hφ : ContDiffOn ℝ 2 φ C) :
    F x (u x) (smoothTestJetWithin C φ x).gradient (smoothTestJetWithin C φ x).hessian ≤ 0

    A viscosity subsolution satisfies the expected inequality for every C^2 test function touching from above, using the coordinate jet extracted from mathlib's canonical fderivWithin derivatives.

    source
    theorem ViscositySolns.ViscositySupersolution.of_touchesBelow_contDiffOn_two {n : ℕ} {C : Set (Point n)} {F : Operator n} {u φ : Point n → ℝ} {x : Point n} {J : Jet n} (hu : ViscositySupersolution C F u) (hC : Convex ℝ C) (huniq : UniqueDiffOn ℝ C) (hx : x ∈ C) (hx_closure : x ∈ closure (interior C)) (htouch : TouchesBelowOn C u φ x) (hφ : ContDiffOn ℝ 2 φ C) (hDφ : fderivWithin ℝ φ C x = J.toFirstDerivative) (hD2φ : fderivWithin ℝ (fderivWithin ℝ φ C) C x = J.toSecondDerivative) :
    0 ≤ F x (u x) J.gradient J.hessian

    A viscosity supersolution satisfies the expected inequality for every C^2 test function touching from below, provided its canonical fderivWithin data matches the coordinate jet.

    source
    theorem ViscositySolns.ViscositySupersolution.of_touchesBelow_contDiffOn_two_smoothTestJetWithin {n : ℕ} {C : Set (Point n)} {F : Operator n} {u φ : Point n → ℝ} {x : Point n} (hu : ViscositySupersolution C F u) (hC : Convex ℝ C) (huniq : UniqueDiffOn ℝ C) (hx : x ∈ C) (hx_closure : x ∈ closure (interior C)) (htouch : TouchesBelowOn C u φ x) (hφ : ContDiffOn ℝ 2 φ C) :
    0 ≤ F x (u x) (smoothTestJetWithin C φ x).gradient (smoothTestJetWithin C φ x).hessian

    A viscosity supersolution satisfies the expected inequality for every C^2 test function touching from below, using the coordinate jet extracted from mathlib's canonical fderivWithin derivatives.