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

Lifted quadratic data for the Perron bump step

Continuity packages for the lifted quadratic produced at a failed lower Perron-envelope subjet inequality.

theorem ViscositySolns.OperatorContinuous.exists_pos_eventually_lowerEnvelope_quadratic_lift_lt_of_neg {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) : ∃ (κ : ℝ), 0 < κ ∧ lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x < quadraticModel x (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x + κ) J.gradient J.hessian x ∧ ∀ᶠ (z : Point n) in nhdsWithin x C, F z (quadraticModel x (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x + κ) J.gradient J.hessian z) (quadraticModelJetAt x J.gradient J.hessian z).gradient (quadraticModelJetAt x J.gradient J.hessian z).hessian < 0

At a failed lower-envelope subjet inequality, operator continuity supplies a positive vertical lift of the touching quadratic whose operator value remains strictly negative near the contact.

This is the Perron-shaped version of the local quadratic continuity step in Lemma 4.4. The remaining bump work is to localize/glue this lifted quadratic against the Perron family.

theorem ViscositySolns.OperatorContinuous.exists_pos_pos_eventually_lowerEnvelope_bentQuadratic_lift_lt_of_neg {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hF : OperatorContinuous F) {x : Point n} (hx : x ∈ C) {J : Jet n} (hneg : F x (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x) J.gradient J.hessian < 0) : ∃ (δ : ℝ) (γ : ℝ), 0 < δ ∧ 0 < γ ∧ lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x < quadraticModel x (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x + δ) J.gradient (J.hessian - γ • 1) x ∧ ∀ᶠ (z : Point n) in nhdsWithin x C, F z (quadraticModel x (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x + δ) J.gradient (J.hessian - γ • 1) z) (quadraticModelJetAt x J.gradient (J.hessian - γ • 1) z).gradient (quadraticModelJetAt x J.gradient (J.hessian - γ • 1) z).hessian < 0

At a failed lower-envelope subjet inequality, operator continuity also allows a small downward identity-Hessian bend of the lifted quadratic.

This is the analytic continuity choice behind the source bump Q + δ - γ |· - x|²: after choosing a positive vertical lift, one can choose a positive bend parameter and still keep the operator value strictly negative in a relative neighborhood of the contact.

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

Local lifted-quadratic data at a failed lower-envelope subjet inequality.

The data records the first analytic move in the source proof of Lemma 4.4: after the lower-envelope viscosity inequality fails, one can lift the touching quadratic by a positive height so that it is strictly above W_* at the contact and still has strictly negative operator value in a relative neighborhood of the contact.

Equations

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

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

Lifted-quadratic negativity at every failed lower-envelope subjet inequality.

This is the continuity-only input to the later gluing/localization step of Lemma 4.4.

Equations

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

theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_liftedQuadraticNegative {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hF : OperatorContinuous F) : PerronLowerEnvelopeLiftedQuadraticNegative C boundary F g B

Operator continuity supplies the local lifted-quadratic negativity datum at every failed lower-envelope subjet inequality.

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

Neighborhood-form local quadratic bump data at a failed lower-envelope contact.

This is the same continuity output as PerronLowerEnvelopeLiftedQuadraticNegativeAt, but with the relative neighborhood made explicit. Later gluing arguments can use V as the region where the lifted quadratic branch is certified to satisfy the strict differential inequality.

Equations

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

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

Neighborhood-form local quadratic bump data at every failed lower-envelope subjet inequality.

Equations

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

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

Open-neighborhood local quadratic bump data at a failed lower-envelope contact.

This strengthens PerronLowerEnvelopeLocalQuadraticBumpAt by recording that the strict-negativity neighborhood can be taken open in the ambient topology. That openness lets later patching arguments use C ∩ V as the active local domain.

Equations

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

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

Open-neighborhood local quadratic bump data at every failed lower-envelope subjet inequality.

Equations

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

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

Open-neighborhood bent quadratic bump data at a failed lower-envelope contact.

This is closer to the source bump than the pure lifted quadratic: the quadratic is lifted by a positive height δ and bent downward by a positive identity-Hessian amount γ.

Equations

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

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

Open-neighborhood bent quadratic bump data at every failed lower-envelope subjet inequality.

Equations

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

theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticOpenBumpAt.localQuadraticBumpAt {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) : PerronLowerEnvelopeLocalQuadraticBumpAt C boundary F g B x J

Open-neighborhood bump data forgets to ordinary neighborhood-form data.

theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticOpenBump.localQuadraticBump {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) : PerronLowerEnvelopeLocalQuadraticBump C boundary F g B

Global open-neighborhood bump data forgets to ordinary neighborhood-form local quadratic bump data.

theorem ViscositySolns.PerronLowerEnvelopeLiftedQuadraticNegativeAt.localQuadraticBumpAt {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 : PerronLowerEnvelopeLiftedQuadraticNegativeAt C boundary F g B x J) : PerronLowerEnvelopeLocalQuadraticBumpAt C boundary F g B x J

The filter-form lifted quadratic datum supplies the explicit neighborhood-form local quadratic bump datum.

theorem ViscositySolns.PerronLowerEnvelopeLiftedQuadraticNegative.localQuadraticBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hquad : PerronLowerEnvelopeLiftedQuadraticNegative C boundary F g B) : PerronLowerEnvelopeLocalQuadraticBump C boundary F g B

The global lifted-quadratic datum supplies the global neighborhood-form local quadratic bump datum.

theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_localQuadraticBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hF : OperatorContinuous F) : PerronLowerEnvelopeLocalQuadraticBump C boundary F g B

Operator continuity supplies the explicit neighborhood-form local quadratic bump datum at every failed lower-envelope subjet inequality.

theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_localQuadraticOpenBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hF : OperatorContinuous F) : PerronLowerEnvelopeLocalQuadraticOpenBump C boundary F g B

Operator continuity supplies the open-neighborhood local quadratic bump datum at every failed lower-envelope subjet inequality.

theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_bentQuadraticOpenBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hF : OperatorContinuous F) : PerronLowerEnvelopeBentQuadraticOpenBump C boundary F g B

Operator continuity supplies the open-neighborhood bent quadratic bump datum at every failed lower-envelope subjet inequality.