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

Quadratic gluing data for the Perron bump step (BentStrictNegativity)

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.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatchAt.sourceAnnulusSelectionPatchAt {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 : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatchAt C boundary F g B x J) (hlowerBddBelow : ∀ z ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin z C) B.lower) : PerronLowerEnvelopeBentQuadraticSourceAnnulusSelectionPatchAt C boundary F g B x J

The outer closed annulus supplies the abstract transition-annulus selection interface. Local lower boundedness compares the lower relaxed Perron envelope with the Perron envelope on the annulus, and lower semicontinuity turns pointwise Perron-branch approximation into local domination.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatch.sourceAnnulusSelectionPatch {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) (hlowerBddBelow : ∀ z ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin z C) B.lower) : PerronLowerEnvelopeBentQuadraticSourceAnnulusSelectionPatch C boundary F g B

Global outer-transition closed-ball lower-envelope data supplies the abstract source annulus selection interface.

theorem ViscositySolns.sourceOuterAnnulus_lift_lt_bendMargin {n : ℕ} {γ r : ℝ} {x z : Point n} (hγpos : 0 < γ) (hrpos : 0 < r) (hzK : 3 * r / 4 ≤ dist z x ∧ dist z x ≤ r) : γ * r ^ 2 / 8 < 1 / 4 * γ * ‖z - x‖ ^ 2

On the outer transition annulus, the source lift γ * r^2 / 8 is strictly smaller than the bend margin coming from the subjet support estimate.

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetLscSelectionPatchAt {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

Geometric small-radius semijet data.

For the bend and active neighborhood supplied by operator continuity, this package supplies the domain geometry and branch lower semicontinuity on all sufficiently small source outer annuli.

Equations

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

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

Geometric small-radius semijet data at every failed lower-envelope subjet inequality.

Equations

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

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterAnnulusLscSelectionPatchAt {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

Pure outer-annulus lower-semicontinuity radius data.

For any bend and active neighborhood later chosen by operator continuity, this package only supplies a small-radius scale on which Perron-family branches are lower semicontinuous on the source outer annulus. Domain closed-ball containment is derived separately from openness of C.

Equations

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

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

Pure outer-annulus lower-semicontinuity radius data at every failed lower-envelope subjet inequality.

Equations

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

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

Domain lower-semicontinuity for every Perron-family branch.

This is the branch regularity actually needed to supply the source outer annulus LSC package: once the contact point is interior to the open PDE domain, the annulus radius can be chosen small enough that the annulus lies in C.

Equations

• ViscositySolns.PerronFamilyLowerSemicontinuousOnDomain C boundary F g B = ∀ (w : ViscositySolns.PerronFamily C boundary F g B.lower B.upper), LowerSemicontinuousOn w.fun C

theorem ViscositySolns.OperatorContinuous.exists_sourceOuterClosedBall_smallRadius_bentStrictNegativity {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hF : OperatorContinuous F) {x : Point n} {J : Jet n} (hneg : F x (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x) J.gradient J.hessian < 0) : ∃ (γ : ℝ) (V : Set (Point n)) (ρ : ℝ), have Xb := J.hessian - γ • 1; 0 < γ ∧ IsOpen V ∧ V ∈ nhdsWithin x C ∧ 0 < ρ ∧ ∀ (r : ℝ), 0 < r → r ≤ ρ → have δ := γ * r ^ 2 / 8; have q := fun (z : Point n) => quadraticModel x (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x + δ) J.gradient Xb z; ∀ z ∈ V, z ∈ C → F z (q z) (quadraticModelJetAt x J.gradient Xb z).gradient (quadraticModelJetAt x J.gradient Xb z).hessian < 0

Operator continuity supplies a bend, an active open neighborhood, and a small-radius scale on which the source-radius lifted bent quadratic has strictly negative operator value.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterAnnulusLscSelectionPatchAt.geometricSemijetLscSelectionPatchAt {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 : PerronLowerEnvelopeBentQuadraticSourceOuterAnnulusLscSelectionPatchAt C boundary F g B x J) (hx : x ∈ C) (hCopen : IsOpen C) (hboundaryOutside : ∀ z ∈ boundary, z ∉ C) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetLscSelectionPatchAt C boundary F g B x J

Open-domain geometry turns pure annulus-LSC radius data into the geometric closed-ball semijet package.

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

Global pure annulus-LSC data supplies the geometric semijet package when the domain is open and the Dirichlet boundary is outside the domain.

theorem ViscositySolns.PerronFamilyLowerSemicontinuousOnDomain.bentSourceOuterAnnulusLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hreg : PerronFamilyLowerSemicontinuousOnDomain C boundary F g B) (hCopen : IsOpen C) : PerronLowerEnvelopeBentQuadraticSourceOuterAnnulusLscSelectionPatch C boundary F g B

Domain lower-semicontinuity for Perron-family branches supplies the pure outer-annulus LSC package on an open domain.

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetLscSelectionPatchAt {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.

This is the geometric small-radius form of the current semijet package: once the bend, active neighborhood, and radius scale are chosen, all sufficiently small radii have the closed ball in the domain, the patch ball in the active neighborhood, the strict operator inequality, and Perron-family lower semicontinuity on the outer transition annulus. The bridge below shrinks the radius further to place that annulus inside any prescribed relative neighborhood.

Equations

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

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetLscSelectionPatch {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 at every failed lower-envelope subjet inequality.

Equations

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

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetLscSelectionPatchAt.smallRadiusSemijetLscSelectionPatchAt {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 : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetLscSelectionPatchAt 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) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetLscSelectionPatchAt C boundary F g B x J

Operator continuity supplies the strict-negativity part of the small-radius semijet package; the geometric package supplies the closed-ball domain, boundary, and branch-lower-semicontinuity fields.

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

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

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetLscSelectionPatchAt {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.

The caller chooses the bend and active neighborhood first. For every relative neighborhood supplied later, it can choose a sufficiently small patch radius so the outer transition annulus lies inside that neighborhood. The bridge below uses the neighborhood supplied by the subjet support estimate.

Equations

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

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetLscSelectionPatch {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 at every failed lower-envelope subjet inequality.

Equations

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

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

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

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetLscSelectionPatchAt.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 : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetLscSelectionPatchAt 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 semijet support estimate also supplies the no-branch-LSC lower-envelope package by forgetting the legacy branch lower-semicontinuity field.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetLscSelectionPatch.outerClosedBallLowerEnvelopeLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetLscSelectionPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatch C boundary F g B

Global semijet-driven outer-annulus source data supplies the current outer-annulus lower-envelope package.

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

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

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetLscSelectionPatchAt.semijetLscSelectionPatchAt {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 : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetLscSelectionPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetLscSelectionPatchAt C boundary F g B x J

Small-radius data supplies the relative-neighborhood selection package by shrinking the radius so the explicit outer annulus lies in the prescribed relative neighborhood.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetLscSelectionPatch.semijetLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetLscSelectionPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetLscSelectionPatch C boundary F g B

Global small-radius data supplies the semijet-driven relative-neighborhood selection package.

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

Global small-radius semijet data supplies the no-branch-LSC outer-annulus lower-envelope package.

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

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

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetPatchAt {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

Geometric small-radius semijet data without Perron-family branch lower-semicontinuity.

For any bend and active neighborhood later chosen by operator continuity, this package supplies a small-radius scale on which the closed patch ball lies in the PDE domain.

Equations

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

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

Geometric small-radius semijet 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.