Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Adapter from the external Aleksandrov formalization #
This module connects the completed convex Aleksandrov theorem in the sibling
AleksandrovDifferentiability project to the jet-based statement used by the
comparison proof in this project.
theorem
ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem.proof_external
(n : ℕ)
:
The completed sibling Aleksandrov formalization implies the closed-ball second-order jet differentiability theorem used by the viscosity comparison proofs in this repository.