Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Perron method core assembly #
Core Perron existence assembly from upper and lower envelope hypotheses.
Assembly form of Perron's method.
The analytic Perron work splits into two inputs:
- the upper envelope of the Perron candidate is a Dirichlet subsolution;
- the lower envelope of the Perron candidate is a Dirichlet supersolution.
Once those are available, comparison gives the reverse inequality between the two envelopes. If the standard envelope order supplies the forward inequality on the Dirichlet domain and boundary, the upper envelope is a Dirichlet solution. Later files should discharge the two analytic inputs via supremum stability and the bump lemma.
Perron's method after the envelope boundary traces have been inherited from the barriers.
Compared with PerronMethodExistenceTheorem, this statement asks only for the
interior viscosity properties of W^* and W_*. The Dirichlet boundary
inequalities are derived from the lower/upper barrier traces and the pointwise
Perron bounds.
Variant of Perron's method where the elementary order W_* <= W^* is supplied
by local boundedness of the Perron envelope on every relevant nhdsWithin
filter.
Perron's method with local boundedness supplied by the barrier pair.
For every x ∈ C ∪ boundary, if the upper barrier is locally bounded above
and the lower barrier is locally bounded below relative to C, then the
pointwise Perron envelope inherits the local boundedness needed for the
elementary envelope order W_* <= W^*. On boundary points the same hypotheses
also provide the coboundedness assumptions needed to pass the barrier trace
inequalities through limsup and liminf.
After the upper Perron envelope has been certified as a Dirichlet subsolution, comparison with the upper barrier places it back in the Perron class.
This is the formal version of the first maximality step in the source proof:
W^* is admissible, hence it cannot lie above the Perron supremum.
The admissibility of W^* forces equality between the pointwise Perron
envelope W and its upper envelope on the PDE domain.
Perron's method with the upper-envelope Dirichlet subsolution supplied by half-relaxed-limit stability.
This discharges the W^* subsolution input from
PerronMethodExistenceTheorem.of_viscosityEnvelopes_of_barrierLocalBounded.
The remaining analytic input is the viscosity supersolution property of
W_*, which is the role of the Perron bump argument.
Perron's method with both analytic envelope inputs exposed in the form produced by the Perron construction.
The upper envelope is supplied by half-relaxed-limit stability. The lower envelope is supplied by the subjet inequality that the localized bump argument is meant to prove.
Perron's method with the lower-envelope supersolution supplied by the formal bump contradiction.
This is the final assembly interface before the analytic localized bump construction itself: the only lower-side hypothesis is that a failed subjet inequality produces an impossible Perron-class function above the envelope.
Perron's method from the source-shaped strict patch form of Lemma 4.4.
The lower-side analytic input says that each failed lower-envelope subjet
inequality produces an admissible Perron-class member that is strictly above a
level greater than W_* x on a relative neighborhood of the failed contact.
Perron's method from the source-shaped bumped-subsolution form of Lemma 4.4.
Here the bump lemma only has to construct a Dirichlet subsolution patch above
the lower barrier. The upper-barrier bound needed for Perron-class membership
is obtained from the same explicit DirichletComparisonPrinciple hypothesis
used by the final Perron argument.