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

Perron bump global bridge interfaces

Global implications between Perron lower-envelope bump interfaces.

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

Source-shaped strict subsolution patch data at every failed subjet inequality.

Equations

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

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

Pointwise strict subsolution patch data at every failed subjet inequality.

Equations

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

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

Continuous strict subsolution patch data at every failed subjet inequality.

Equations

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

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

Continuous Dirichlet bump data at every failed subjet inequality.

Equations

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

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

Continuous max-patch bump data at every failed subjet inequality.

Equations

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

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

Continuous local max-patch data at every failed subjet inequality.

Equations

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

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

Branch-local continuous max-patch data at every failed subjet inequality.

Equations

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

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

Active-branch continuous max-patch data at every failed subjet inequality.

Equations

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

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

Strict active-branch continuous max-patch data at every failed subjet inequality.

Equations

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

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

Strict active-branch subsolution bump data at every failed subjet inequality.

Equations

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

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

Strict active-branch Dirichlet bump data at every failed subjet inequality.

Equations

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

theorem ViscositySolns.DirichletBarrierPair.continuousMaxPatch_of_continuousBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hbump : PerronLowerEnvelopeContinuousBump C boundary F g B) : PerronLowerEnvelopeContinuousMaxPatch C boundary F g B

A continuous Dirichlet bump at every failed contact gives continuous max-patch data at every failed contact.

theorem ViscositySolns.DirichletBarrierPair.continuousMaxPatch_of_continuousLocalMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hpatch : PerronLowerEnvelopeContinuousLocalMaxPatch C boundary F g B) : PerronLowerEnvelopeContinuousMaxPatch C boundary F g B

The local-germ max-patch formulation implies the continuous max-patch formulation.

theorem ViscositySolns.DirichletBarrierPair.localizedImprovement_of_continuousMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hne : ∀ x ∈ C, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hpatch : PerronLowerEnvelopeContinuousMaxPatch C boundary F g B) : PerronLowerEnvelopeLocalizedImprovement C boundary F g B

The continuous max-patch formulation implies localized improvement at every failed contact.

theorem ViscositySolns.DirichletBarrierPair.localizedImprovement_of_pointwiseStrictSubsolutionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hne : ∀ x ∈ C, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hpatch : PerronLowerEnvelopePointwiseStrictSubsolutionPatch C boundary F g B) : PerronLowerEnvelopeLocalizedImprovement C boundary F g B

The pointwise-lower-semicontinuous strict patch formulation implies localized improvement at every failed contact.

theorem ViscositySolns.DirichletBarrierPair.localizedImprovement_of_neighborhoodImprovement {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (himprove : PerronLowerEnvelopeNeighborhoodImprovement C boundary F g B) : PerronLowerEnvelopeLocalizedImprovement C boundary F g B

The neighborhood-form improvement implies the frequent localized-improvement form at every failed contact.

theorem ViscositySolns.DirichletBarrierPair.continuousLocalMaxPatch_of_branchMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hpatch : PerronLowerEnvelopeContinuousBranchMaxPatch C boundary F g B) : PerronLowerEnvelopeContinuousLocalMaxPatch C boundary F g B

The branch-local max-patch formulation implies the local-germ max-patch formulation.

theorem ViscositySolns.DirichletBarrierPair.branchMaxPatch_of_activeMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hpatch : PerronLowerEnvelopeContinuousActiveMaxPatch C boundary F g B) : PerronLowerEnvelopeContinuousBranchMaxPatch C boundary F g B

The active-branch max-patch formulation implies the branch-local max-patch formulation.

theorem ViscositySolns.DirichletBarrierPair.activeMaxPatch_of_strictActiveMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hpatch : PerronLowerEnvelopeContinuousStrictActiveMaxPatch C boundary F g B) : PerronLowerEnvelopeContinuousActiveMaxPatch C boundary F g B

The strict active-branch formulation implies the active-branch formulation.

theorem ViscositySolns.DirichletBarrierPair.strictActiveMaxPatch_of_strictActiveSubsolutionBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hbump : PerronLowerEnvelopeContinuousStrictActiveSubsolutionBump C boundary F g B) : PerronLowerEnvelopeContinuousStrictActiveMaxPatch C boundary F g B

The strict active subsolution-bump formulation implies the strict active max-patch formulation.

theorem ViscositySolns.DirichletBarrierPair.strictActiveSubsolutionBump_of_strictActiveDirichletBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hbump : PerronLowerEnvelopeContinuousStrictActiveDirichletBump C boundary F g B) : PerronLowerEnvelopeContinuousStrictActiveSubsolutionBump C boundary F g B

The strict active Dirichlet-bump formulation implies the strict active subsolution-bump formulation.

theorem ViscositySolns.DirichletBarrierPair.strictActiveDirichletBump_of_interiorQuadraticBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hFell : DegenerateElliptic F) (hinterior : ∀ z ∈ C, z ∈ interior C) (hbump : PerronLowerEnvelopeInteriorQuadraticBump C boundary F g B) : PerronLowerEnvelopeContinuousStrictActiveDirichletBump C boundary F g B

Interior quadratic bump data supplies the strict active Dirichlet-bump interface used by the Perron lower-envelope argument.

theorem ViscositySolns.DirichletBarrierPair.branchMaxPatch_of_strictActiveMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hpatch : PerronLowerEnvelopeContinuousStrictActiveMaxPatch C boundary F g B) : PerronLowerEnvelopeContinuousBranchMaxPatch C boundary F g B

The strict active-branch formulation implies the branch-local max-patch formulation.

theorem ViscositySolns.DirichletBarrierPair.continuousLocalMaxPatch_of_activeMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hpatch : PerronLowerEnvelopeContinuousActiveMaxPatch C boundary F g B) : PerronLowerEnvelopeContinuousLocalMaxPatch C boundary F g B

The active-branch max-patch formulation implies the local-germ max-patch formulation.

theorem ViscositySolns.DirichletBarrierPair.continuousMaxPatch_of_branchMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hpatch : PerronLowerEnvelopeContinuousBranchMaxPatch C boundary F g B) : PerronLowerEnvelopeContinuousMaxPatch C boundary F g B

The branch-local max-patch formulation implies the continuous max-patch formulation.

theorem ViscositySolns.DirichletBarrierPair.strictSubsolutionPatch_of_continuousMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hpatch : PerronLowerEnvelopeContinuousMaxPatch C boundary F g B) : PerronLowerEnvelopeStrictSubsolutionPatch C boundary F g B

The continuous max-patch formulation implies the strict subsolution patch formulation.

theorem ViscositySolns.DirichletBarrierPair.strictSubsolutionPatch_of_continuousBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hbump : PerronLowerEnvelopeContinuousBump C boundary F g B) : PerronLowerEnvelopeStrictSubsolutionPatch C boundary F g B

The continuous Dirichlet bump formulation implies the strict subsolution patch formulation by maxing each bump with the lower barrier.

theorem ViscositySolns.PerronLowerEnvelopeContinuousStrictSubsolutionPatch.pointwiseStrict {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeContinuousStrictSubsolutionPatch C boundary F g B) : PerronLowerEnvelopePointwiseStrictSubsolutionPatch C boundary F g B

The continuous pointwise patch formulation implies the lower-semicontinuous pointwise patch formulation.

theorem ViscositySolns.DirichletBarrierPair.strictSubsolutionPatch_of_pointwiseStrictSubsolutionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hpatch : PerronLowerEnvelopePointwiseStrictSubsolutionPatch C boundary F g B) : PerronLowerEnvelopeStrictSubsolutionPatch C boundary F g B

The pointwise-lower-semicontinuous patch formulation implies the neighborhood-strict subsolution patch formulation.