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

Quadratic gluing data for the Perron bump step (OpenBumpMaxPatches)

Part of the quadratic-gluing development connecting the lifted quadratic supplied by operator continuity to the strict local max-patch formulation. Split from QuadraticGluing.lean; see the umbrella module docstring.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticOpenBumpAt.bentQuadraticMaxPatchAt_of_openBarrierExteriorAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hquad : PerronLowerEnvelopeBentQuadraticOpenBumpAt C boundary F g B x J) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hpatch : PerronLowerEnvelopeBentQuadraticOpenBarrierExteriorPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticMaxPatchAt C boundary F g B x J

Bent open lifted-quadratic data plus bent open-active lower-barrier exterior data gives the bent max-patch datum.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticOpenBump.bentQuadraticMaxPatch_of_openBarrierExterior {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hquad : PerronLowerEnvelopeBentQuadraticOpenBump C boundary F g B) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hpatch : PerronLowerEnvelopeBentQuadraticOpenBarrierExteriorPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticMaxPatch C boundary F g B

Global bent open lifted-quadratic data plus bent open-active lower-barrier exterior data gives the global bent max-patch datum.

theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_strictLocalPatch_of_bentOpenBarrierExterior {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hF : OperatorContinuous F) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hpatch : PerronLowerEnvelopeBentQuadraticOpenBarrierExteriorPatch C boundary F g B) : PerronLowerEnvelopeStrictLocalPatch C boundary F g B

Operator continuity reduces the bent strict-local patch step to the source-shaped bent exterior annulus data.

theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticOpenBumpAt.maxPatchAt_of_openBarrierExteriorAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hquad : PerronLowerEnvelopeLocalQuadraticOpenBumpAt C boundary F g B x J) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hpatch : PerronLowerEnvelopeLocalQuadraticOpenBarrierExteriorPatchAt C boundary F g B x J) : PerronLowerEnvelopeLocalQuadraticMaxPatchAt C boundary F g B x J

Open lifted-quadratic data plus open-active lower-barrier exterior data gives the local quadratic max-patch datum.

The active domain required by the patch proof is generated from the open sets C and V, while the inactive compact is handled by finite Perron selection using the lower barrier as the local old branch.

theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticOpenBump.localQuadraticMaxPatch_of_openBarrierExterior {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hquad : PerronLowerEnvelopeLocalQuadraticOpenBump C boundary F g B) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hpatch : PerronLowerEnvelopeLocalQuadraticOpenBarrierExteriorPatch C boundary F g B) : PerronLowerEnvelopeLocalQuadraticMaxPatch C boundary F g B

Global open lifted-quadratic data plus open-active lower-barrier exterior data gives the global local quadratic max-patch datum.

theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_localQuadraticMaxPatch_of_openBarrierExterior {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hF : OperatorContinuous F) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hpatch : PerronLowerEnvelopeLocalQuadraticOpenBarrierExteriorPatch C boundary F g B) : PerronLowerEnvelopeLocalQuadraticMaxPatch C boundary F g B

Operator continuity reduces the local quadratic max-patch step to open-active lower-barrier exterior data.

theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticGluingAt.localQuadraticMaxPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hglue : PerronLowerEnvelopeLocalQuadraticGluingAt C boundary F g B x J) : PerronLowerEnvelopeLocalQuadraticMaxPatchAt C boundary F g B x J

The local-germ quadratic gluing datum supplies the max-patch datum.

theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticGluing.localQuadraticMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hglue : PerronLowerEnvelopeLocalQuadraticGluing C boundary F g B) : PerronLowerEnvelopeLocalQuadraticMaxPatch C boundary F g B

The global local-germ quadratic gluing datum supplies the global max-patch datum.

theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticMaxPatchAt.strictLocalPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hpatch : PerronLowerEnvelopeLocalQuadraticMaxPatchAt C boundary F g B x J) : PerronLowerEnvelopeStrictLocalPatchAt C boundary F g B x

The quadratic max-patch datum gives the existing strict local-patch interface.

The only proof work here is turning pointwise strict improvement at x into a relative neighborhood where the lifted quadratic is above an intermediate level; this is exactly where continuity of the lifted quadratic is used.

theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticMaxPatch.strictLocalPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeLocalQuadraticMaxPatch C boundary F g B) : PerronLowerEnvelopeStrictLocalPatch C boundary F g B

The global quadratic max-patch datum gives the existing global strict local-patch interface.