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

Quadratic gluing data for the Perron bump step (OpenBumpPatches)

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.strictPatchAt_of_localizedLowerPatchAt {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) (hx : x ∈ C) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hpatch : PerronLowerEnvelopeBentQuadraticLocalizedLowerPatchAt C boundary F g B x J) : PerronLowerEnvelopeStrictPatchAt C boundary F g B x

Bent open lifted-quadratic data plus a localized lower-barrier piecewise patch gives the strict patch needed for Perron's contradiction.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticOpenBump.strictPatch_of_localizedLowerPatch {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 : PerronLowerEnvelopeBentQuadraticLocalizedLowerPatch C boundary F g B) : PerronLowerEnvelopeStrictPatch C boundary F g B

Global bent open lifted-quadratic data plus localized lower-barrier piecewise patches gives the global strict patch interface.

theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_strictPatch_of_bentLocalizedLowerPatch {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 : PerronLowerEnvelopeBentQuadraticLocalizedLowerPatch C boundary F g B) : PerronLowerEnvelopeStrictPatch C boundary F g B

Operator continuity reduces the strict patch step to localized bent lower-barrier piecewise patch data.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticOpenBumpAt.strictPatchAt_of_shrinkingLocalizedLowerPatchAt {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) (hx : x ∈ C) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hpatch : PerronLowerEnvelopeBentQuadraticShrinkingLocalizedLowerPatchAt C boundary F g B x J) : PerronLowerEnvelopeStrictPatchAt C boundary F g B x

Bent open lifted-quadratic data plus a shrinkable localized lower-barrier piecewise patch gives the strict patch needed for Perron's contradiction.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticOpenBump.strictPatch_of_shrinkingLocalizedLowerPatch {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 : PerronLowerEnvelopeBentQuadraticShrinkingLocalizedLowerPatch C boundary F g B) : PerronLowerEnvelopeStrictPatch C boundary F g B

Global bent open lifted-quadratic data plus shrinkable localized lower-barrier patches gives the global strict patch interface.

theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_strictPatch_of_bentShrinkingLocalizedLowerPatch {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 : PerronLowerEnvelopeBentQuadraticShrinkingLocalizedLowerPatch C boundary F g B) : PerronLowerEnvelopeStrictPatch C boundary F g B

Operator continuity reduces the strict patch step to shrinkable localized bent lower-barrier piecewise patch data.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticChosenLocalizedLowerPatchAt.strictPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hchosen : PerronLowerEnvelopeBentQuadraticChosenLocalizedLowerPatchAt C boundary F g B x J) (hx : x ∈ C) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) : PerronLowerEnvelopeStrictPatchAt C boundary F g B x

A chosen bent localized lower-barrier patch gives the strict patch needed for Perron's contradiction.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticChosenLocalizedLowerPatch.strictPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hchosen : PerronLowerEnvelopeBentQuadraticChosenLocalizedLowerPatch C boundary F g B) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) : PerronLowerEnvelopeStrictPatch C boundary F g B

Global chosen bent localized lower-barrier patches give the global strict patch interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedBallAnnulusPatch.strictPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedBallAnnulusPatch C boundary F g B) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) : PerronLowerEnvelopeStrictPatch C boundary F g B

Source-radius closed-ball annulus data gives the global strict patch interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceCompactInactivePatchAt.strictPatchAt {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 : PerronLowerEnvelopeBentQuadraticSourceCompactInactivePatchAt C boundary F g B x J) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) : PerronLowerEnvelopeStrictPatchAt C boundary F g B x

Source-radius compact-inactive data gives the strict patch by finite Perron selection on the inactive compact set.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceCompactInactivePatch.strictPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceCompactInactivePatch C boundary F g B) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) : PerronLowerEnvelopeStrictPatch C boundary F g B

Global source-radius compact-inactive data gives the global strict patch interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatchAt.strictPatchAt_of_old_eq_perronEnvelope {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 : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatchAt C boundary F g B x J) (old : Point n → ℝ) (hold : PerronClass C boundary F g B.lower B.upper old) (hOldEq : Set.EqOn old (perronEnvelope C boundary F g B.lower B.upper) C) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerBddBelow : ∀ z ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin z C) B.lower) : PerronLowerEnvelopeStrictPatchAt C boundary F g B x

Source outer-annulus lower-envelope data gives a strict patch by patching directly over an already admissible old function that agrees with the Perron envelope on the domain.

This is the direct source-proof variant of the annulus construction: on the transition annulus the source estimate gives q < W_*, local boundedness gives W_* <= W, and the supplied identity gives W = old. No Perron-family branch selection or branch lower-semicontinuity is used.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatch.strictPatch_of_old_eq_perronEnvelope {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatch C boundary F g B) (old : Point n → ℝ) (hold : PerronClass C boundary F g B.lower B.upper old) (hOldEq : Set.EqOn old (perronEnvelope C boundary F g B.lower B.upper) C) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerBddBelow : ∀ z ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin z C) B.lower) : PerronLowerEnvelopeStrictPatch C boundary F g B

Global source outer-annulus lower-envelope data gives strict patches by patching directly over an already admissible old function that agrees with the Perron envelope on the domain.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatch.strictPatch_of_old_eq_perronEnvelope {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatch C boundary F g B) (old : Point n → ℝ) (hold : PerronClass C boundary F g B.lower B.upper old) (hOldEq : Set.EqOn old (perronEnvelope C boundary F g B.lower B.upper) C) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerBddBelow : ∀ z ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin z C) B.lower) : PerronLowerEnvelopeStrictPatch C boundary F g B

Legacy outer-annulus data gives the direct strict patch after forgetting its unused branch lower-semicontinuity field.