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

Quadratic gluing data for the Perron bump step (OuterSemijetPatches)

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.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetPatchAt.of_isOpen {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hx : x ∈ C) (hCopen : IsOpen C) (hboundaryOutside : ∀ z ∈ boundary, z ∉ C) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetPatchAt C boundary F g B x J

Open-domain geometry supplies the no-branch-LSC geometric package.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetPatch.of_isOpen {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hCopen : IsOpen C) (hboundaryOutside : ∀ z ∈ boundary, z ∉ C) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetPatch C boundary F g B

Open-domain geometry supplies the global no-branch-LSC geometric semijet package.

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetPatchAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) (J : Jet n) : Prop

Small-radius semijet-driven outer-annulus source data without branch lower-semicontinuity.

Equations

• One or more equations did not get rendered due to their size.

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetPatch {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) : Prop

Small-radius semijet-driven outer-annulus source data without branch lower-semicontinuity at every failed lower-envelope subjet inequality.

Equations

• One or more equations did not get rendered due to their size.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetPatchAt.smallRadiusSemijetPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hgeom : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetPatchAt C boundary F g B x J) (hF : OperatorContinuous F) (hneg : F x (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x) J.gradient J.hessian < 0) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetPatchAt C boundary F g B x J

Operator continuity supplies the strict-negativity part of the no-branch-LSC small-radius semijet package; the geometric package supplies closed-ball domain control.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetPatch.smallRadiusSemijetPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hgeom : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetPatch C boundary F g B) (hF : OperatorContinuous F) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetPatch C boundary F g B

Global no-branch-LSC geometric semijet data supplies the no-branch-LSC small-radius package once operator continuity provides the source strict-negativity scale.

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetPatchAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) (J : Jet n) : Prop

Semijet-driven outer-annulus source data without branch lower-semicontinuity.

Equations

• One or more equations did not get rendered due to their size.

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetPatch {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) : Prop

Semijet-driven outer-annulus source data without branch lower-semicontinuity at every failed lower-envelope subjet inequality.

Equations

• One or more equations did not get rendered due to their size.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetPatchAt.semijetPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hx : x ∈ C) (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetPatchAt C boundary F g B x J

Small-radius no-branch-LSC data supplies the relative-neighborhood semijet package by shrinking the radius so the explicit outer annulus lies in the prescribed relative neighborhood.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetPatch.semijetPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetPatch C boundary F g B

Global small-radius no-branch-LSC data supplies the semijet-driven relative-neighborhood package.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetPatchAt.outerClosedBallLowerEnvelopePatchAt {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 : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetPatchAt C boundary F g B x J) (hJ : J ∈ Subjet C (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper)) x) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatchAt C boundary F g B x J

The no-branch-LSC semijet support estimate supplies strict lower-envelope domination on the outer annulus once the annulus is chosen inside its relative neighborhood.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetPatch.outerClosedBallLowerEnvelopePatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatch C boundary F g B

Global no-branch-LSC semijet-driven outer-annulus source data supplies the no-branch-LSC outer-annulus lower-envelope package.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetPatch.outerClosedBallLowerEnvelopePatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hgeom : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetPatch C boundary F g B) (hF : OperatorContinuous F) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatch C boundary F g B

Global no-branch-LSC geometric semijet data supplies the no-branch-LSC outer-annulus lower-envelope package once operator continuity provides the source strict-negativity scale.

theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_sourceOuterClosedBallLowerEnvelopePatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hF : OperatorContinuous F) (hCopen : IsOpen C) (hboundaryOutside : ∀ z ∈ boundary, z ∉ C) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatch C boundary F g B

Operator continuity and open-domain geometry supply the final no-branch-LSC source outer-closed-ball lower-envelope patch package.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusSelectionPatchAt.annulusSelectionPatchAt {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 : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusSelectionPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticSourceAnnulusSelectionPatchAt C boundary F g B x J

The explicit closed annulus supplies the abstract transition-annulus selection interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusSelectionPatch.annulusSelectionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusSelectionPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticSourceAnnulusSelectionPatch C boundary F g B

Global closed-annulus source-radius transition data supplies the abstract transition-annulus selection interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticLocalizedLowerPatchAt.of_piecewiseSet {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hsets : ∀ (δ γ : ℝ) (V : Set (Point n)) (Xb : Hessian n) (q : Point n → ℝ), Xb = J.hessian - γ • 1 → (q = fun (z : Point n) => quadraticModel x (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x + δ) J.gradient Xb z) → 0 < δ → 0 < γ → IsOpen V → V ∈ nhdsWithin x C → lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x < q x → ContinuousWithinAt q C x → (∀ z ∈ V, z ∈ C → F z (q z) (quadraticModelJetAt x J.gradient Xb z).gradient (quadraticModelJetAt x J.gradient Xb z).hessian < 0) → ∃ (P : Set (Point n)), (∀ z ∈ C, z ∈ V → P ∈ nhdsWithin z C) ∧ (∀ z ∈ C, z ∉ V → ∀ᶠ (y : Point n) in nhdsWithin z C, y ∉ P ∨ q y ≤ B.lower y) ∧ ∀ z ∈ boundary, z ∉ closure P ∨ q z ≤ B.lower z) : PerronLowerEnvelopeBentQuadraticLocalizedLowerPatchAt C boundary F g B x J

A concrete piecewise-set constructor for the localized bent lower-barrier patch interface.

The set P is the region where the patch uses max(lower, q). It must be a relative neighborhood of every active point, locally inactive off the active neighborhood, and inactive or dominated on the Dirichlet boundary.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticOpenPiecewisePatchAt.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} (hpatch : PerronLowerEnvelopeBentQuadraticOpenPiecewisePatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticLocalizedLowerPatchAt C boundary F g B x J

Open patch-set data supplies the localized lower-barrier patch interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticOpenPiecewisePatch.localizedLowerPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticOpenPiecewisePatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticLocalizedLowerPatch C boundary F g B

Global open patch-set data supplies the global localized lower-barrier patch interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticBoundaryAwayOpenPatchAt.openPiecewisePatchAt {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 : PerronLowerEnvelopeBentQuadraticBoundaryAwayOpenPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticOpenPiecewisePatchAt C boundary F g B x J

Boundary-away open patch-set data supplies the open piecewise patch interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticBoundaryAwayOpenPatch.openPiecewisePatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticBoundaryAwayOpenPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticOpenPiecewisePatch C boundary F g B

Global boundary-away open patch-set data supplies the global open piecewise patch interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticBallPatchAt.boundaryAwayOpenPatchAt {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 : PerronLowerEnvelopeBentQuadraticBallPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticBoundaryAwayOpenPatchAt C boundary F g B x J

Ball patch data supplies the boundary-away open patch-set interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticBallPatch.boundaryAwayOpenPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticBallPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticBoundaryAwayOpenPatch C boundary F g B

Global ball patch data supplies the global boundary-away open patch-set interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticClosedBallAnnulusPatchAt.ballPatchAt {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 : PerronLowerEnvelopeBentQuadraticClosedBallAnnulusPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticBallPatchAt C boundary F g B x J

Closed-ball annulus data supplies the ball patch interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticClosedBallAnnulusPatch.ballPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticClosedBallAnnulusPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticBallPatch C boundary F g B

Global closed-ball annulus data supplies the global ball patch interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticShrinkingClosedBallAnnulusPatchAt.shrinkingPatchAt {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 : PerronLowerEnvelopeBentQuadraticShrinkingClosedBallAnnulusPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticShrinkingLocalizedLowerPatchAt C boundary F g B x J

Shrinking closed-ball annulus data supplies the shrinkable localized patch interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticShrinkingClosedBallAnnulusPatch.shrinkingPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticShrinkingClosedBallAnnulusPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticShrinkingLocalizedLowerPatch C boundary F g B

Global shrinking closed-ball annulus data supplies the global shrinkable localized patch interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSmallRadiusClosedBallAnnulusPatchAt.shrinkingAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hx : x ∈ C) (hpatch : PerronLowerEnvelopeBentQuadraticSmallRadiusClosedBallAnnulusPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticShrinkingClosedBallAnnulusPatchAt C boundary F g B x J

Small-radius annulus data supplies shrinking annulus data by choosing a radius inside both the active operator-continuity neighborhood and the analytic small-radius range.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSmallRadiusClosedBallAnnulusPatch.shrinking {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSmallRadiusClosedBallAnnulusPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticShrinkingClosedBallAnnulusPatch C boundary F g B

Global small-radius annulus data supplies global shrinking annulus data.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedBallAnnulusPatchAt.chosenPatchAt {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 : PerronLowerEnvelopeBentQuadraticSourceClosedBallAnnulusPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticChosenLocalizedLowerPatchAt C boundary F g B x J

Source-radius annulus data supplies one chosen localized lower-barrier patch.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedBallAnnulusPatch.chosenPatch {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) : PerronLowerEnvelopeBentQuadraticChosenLocalizedLowerPatch C boundary F g B

Global source-radius annulus data supplies global chosen localized patches.

theorem ViscositySolns.exists_activeDomain_inter_of_isOpen {n : ℕ} {C V : Set (Point n)} (hCopen : IsOpen C) (hVopen : IsOpen V) {z : Point n} (hzC : z ∈ C) (hzV : z ∈ V) : ∃ D ⊆ C, D ∈ nhdsWithin z C ∧ (∀ y ∈ D, D ∈ nhdsWithin y C) ∧ (∀ y ∈ D, y ∈ interior D) ∧ ∀ y ∈ D, y ∈ V

If both the ambient domain and the active neighborhood are open, their intersection is the active local domain required by the compact-inactive patch interfaces.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticMaxPatchAt.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 : PerronLowerEnvelopeBentQuadraticMaxPatchAt C boundary F g B x J) : PerronLowerEnvelopeStrictLocalPatchAt C boundary F g B x

Bent quadratic max-patch data feeds the generic strict-local max-patch interface.

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

Global bent quadratic max-patch data feeds the global strict-local patch interface.