Documentation

LeanPool.ViscositySolutionTheory.ViscositySolns.Existence.Perron.Bump.QuadraticGluing.CertifiedPatches

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

Quadratic gluing data for the Perron bump step (CertifiedPatches) #

This module connects lifted quadratics to strict local max patches.

source
theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceAnnulusSelectionPatchAt.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 : PerronLowerEnvelopeBentQuadraticSourceAnnulusSelectionPatchAt 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 transition-annulus selection data gives the strict patch by selecting one old Perron branch on the compact transition set and patching piecewise across the ball.

source
theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceAnnulusSelectionPatch.strictPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceAnnulusSelectionPatch 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 transition-annulus selection data gives the global strict patch interface.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBarrierExteriorPatchAt.exteriorPatchAt {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 : PerronLowerEnvelopeLocalQuadraticBarrierExteriorPatchAt C boundary F g B x J) :
PerronLowerEnvelopeLocalQuadraticCompactInactiveExteriorPatchAt C boundary F g B x J

Lower-barrier exterior data supplies exterior compact-inactive data.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBarrierExteriorPatch.exteriorPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeLocalQuadraticBarrierExteriorPatch C boundary F g B) :
PerronLowerEnvelopeLocalQuadraticCompactInactiveExteriorPatch C boundary F g B

Global lower-barrier exterior data supplies global exterior compact-inactive data.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticCompactInactiveBoundaryPatchAt.symCertifiedPatchAt {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 : PerronLowerEnvelopeLocalQuadraticCompactInactiveBoundaryPatchAt C boundary F g B x J) :
PerronLowerEnvelopeLocalQuadraticCompactInactiveSymCertifiedPatchAt C boundary F g B x J

Boundary-safe compact-inactive data supplies the symmetrized certified datum.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticCompactInactiveBoundaryPatch.symCertifiedPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveBoundaryPatch C boundary F g B) :
PerronLowerEnvelopeLocalQuadraticCompactInactiveSymCertifiedPatch C boundary F g B

Global boundary-safe compact-inactive data supplies the global symmetrized certified datum.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticCompactInactiveCertifiedPatchAt.quadraticPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hcert : PerronLowerEnvelopeLocalQuadraticCompactInactiveCertifiedPatchAt C boundary F g B x J) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) :
PerronLowerEnvelopeLocalQuadraticCompactInactiveQuadraticPatchAt C boundary F g B x J

Certified active-domain compact-inactive data supplies the quadratic-active patch datum.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticCompactInactiveCertifiedPatch.quadraticPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hcert : PerronLowerEnvelopeLocalQuadraticCompactInactiveCertifiedPatch C boundary F g B) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) :
PerronLowerEnvelopeLocalQuadraticCompactInactiveQuadraticPatch C boundary F g B

Global certified active-domain data supplies the global quadratic-active patch datum.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticCompactInactiveSymCertifiedPatchAt.quadraticPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hcert : PerronLowerEnvelopeLocalQuadraticCompactInactiveSymCertifiedPatchAt C boundary F g B x J) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) :
PerronLowerEnvelopeLocalQuadraticCompactInactiveQuadraticPatchAt C boundary F g B x J

Symmetrized certified active-domain compact-inactive data supplies the quadratic-active patch datum.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticCompactInactiveSymCertifiedPatch.quadraticPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hcert : PerronLowerEnvelopeLocalQuadraticCompactInactiveSymCertifiedPatch C boundary F g B) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) :
PerronLowerEnvelopeLocalQuadraticCompactInactiveQuadraticPatch C boundary F g B

Global symmetrized certified active-domain data supplies the global quadratic-active patch datum.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticCompactInactiveQuadraticPatchAt.subsolutionPatchAt {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 : PerronLowerEnvelopeLocalQuadraticCompactInactiveQuadraticPatchAt C boundary F g B x J) :
PerronLowerEnvelopeLocalQuadraticCompactInactiveSubsolutionPatchAt C boundary F g B x J

The quadratic-active compact-inactive datum supplies the local subsolution-patch datum.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticCompactInactiveQuadraticPatch.subsolutionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveQuadraticPatch C boundary F g B) :
PerronLowerEnvelopeLocalQuadraticCompactInactiveSubsolutionPatch C boundary F g B

Global quadratic-active compact-inactive data supplies the global subsolution-patch datum.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBumpAt.localQuadraticGluingAt_of_compactInactiveSelectionAt {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 : PerronLowerEnvelopeLocalQuadraticBumpAt C boundary F g B x J) (hselect : PerronLowerEnvelopeLocalQuadraticCompactInactiveSelectionAt C boundary F g B x J) :
PerronLowerEnvelopeLocalQuadraticGluingAt C boundary F g B x J

Local lifted-quadratic data plus compact-inactive selection gives the local-germ quadratic gluing datum.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBump.localQuadraticGluing_of_compactInactiveSelection {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hquad : PerronLowerEnvelopeLocalQuadraticBump C boundary F g B) (hselect : PerronLowerEnvelopeLocalQuadraticCompactInactiveSelection C boundary F g B) :
PerronLowerEnvelopeLocalQuadraticGluing C boundary F g B

Global local lifted-quadratic data plus compact-inactive selection gives the global local-germ quadratic gluing datum.

source
theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_localQuadraticGluing_of_compactInactiveSelection {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hF : OperatorContinuous F) (hselect : PerronLowerEnvelopeLocalQuadraticCompactInactiveSelection C boundary F g B) :
PerronLowerEnvelopeLocalQuadraticGluing C boundary F g B

Operator continuity reduces local-germ Perron bump gluing to the compact-inactive selection problem.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBumpAt.branchGluingAt_of_patchSelectionAt {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 : PerronLowerEnvelopeLocalQuadraticBumpAt C boundary F g B x J) (hselect : PerronLowerEnvelopeLocalQuadraticPatchSelectionAt C boundary F g B x J) :
PerronLowerEnvelopeLocalQuadraticBranchGluingAt C boundary F g B x J

The explicit lifted-quadratic data plus patch selection gives branch-local quadratic gluing at a failed contact.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBump.branchGluing_of_patchSelection {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hquad : PerronLowerEnvelopeLocalQuadraticBump C boundary F g B) (hselect : PerronLowerEnvelopeLocalQuadraticPatchSelection C boundary F g B) :
PerronLowerEnvelopeLocalQuadraticBranchGluing C boundary F g B

Local lifted-quadratic data plus patch selection gives global branch-local quadratic gluing.

source
theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_branchGluing_of_patchSelection {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hF : OperatorContinuous F) (hselect : PerronLowerEnvelopeLocalQuadraticPatchSelection C boundary F g B) :
PerronLowerEnvelopeLocalQuadraticBranchGluing C boundary F g B

Operator continuity reduces the branch-local Perron bump step to the explicit patch-selection problem.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBranchGluingAt.localQuadraticGluingAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hbranch : PerronLowerEnvelopeLocalQuadraticBranchGluingAt C boundary F g B x J) :
PerronLowerEnvelopeLocalQuadraticGluingAt C boundary F g B x J

Branch-local quadratic gluing supplies the local-germ quadratic gluing datum.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBranchGluing.localQuadraticGluing {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hbranch : PerronLowerEnvelopeLocalQuadraticBranchGluing C boundary F g B) :
PerronLowerEnvelopeLocalQuadraticGluing C boundary F g B

The global branch-local quadratic gluing datum supplies the global local-germ quadratic gluing datum.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticActiveGluingAt.localQuadraticGluingAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hactive : PerronLowerEnvelopeLocalQuadraticActiveGluingAt C boundary F g B x J) :
PerronLowerEnvelopeLocalQuadraticGluingAt C boundary F g B x J

Active-branch quadratic gluing supplies the local-germ quadratic gluing datum.

source
theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticActiveGluing.localQuadraticGluing {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hactive : PerronLowerEnvelopeLocalQuadraticActiveGluing C boundary F g B) :
PerronLowerEnvelopeLocalQuadraticGluing C boundary F g B

The global active-branch quadratic gluing datum supplies the global local-germ quadratic gluing datum.

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

Source-shaped local quadratic max-patch data at a failed lower-envelope contact.

This records the remaining gluing output after the lifted quadratic has been chosen: an old Perron-class member can be maxed with the lifted quadratic, and the result is still Perron-admissible. The local negativity and continuity fields keep the datum tied to the quadratic produced by the failed subjet inequality.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def ViscositySolns.PerronLowerEnvelopeLocalQuadraticMaxPatch {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) :
    Prop

    Local quadratic max-patch data at every failed lower-envelope subjet inequality.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBumpAt.localQuadraticMaxPatchAt_of_compactInactivePatchAt {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 : PerronLowerEnvelopeLocalQuadraticBumpAt C boundary F g B x J) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactivePatchAt C boundary F g B x J) :
      PerronLowerEnvelopeLocalQuadraticMaxPatchAt C boundary F g B x J

      Local lifted-quadratic data plus compact-inactive local patch data gives the source-shaped local quadratic max-patch datum.

      source
      theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBump.localQuadraticMaxPatch_of_compactInactivePatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hquad : PerronLowerEnvelopeLocalQuadraticBump C boundary F g B) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactivePatch C boundary F g B) :
      PerronLowerEnvelopeLocalQuadraticMaxPatch C boundary F g B

      Global local lifted-quadratic data plus compact-inactive local patch data gives the global source-shaped local quadratic max-patch datum.

      source
      theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_localQuadraticMaxPatch_of_compactInactivePatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hF : OperatorContinuous F) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactivePatch C boundary F g B) :
      PerronLowerEnvelopeLocalQuadraticMaxPatch C boundary F g B

      Operator continuity reduces the local quadratic max-patch step to compact-inactive local patch data.

      source
      theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBumpAt.maxPatchAt_of_compactInactiveSubsolutionAt {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 : PerronLowerEnvelopeLocalQuadraticBumpAt C boundary F g B x J) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveSubsolutionPatchAt C boundary F g B x J) :
      PerronLowerEnvelopeLocalQuadraticMaxPatchAt C boundary F g B x J

      Local lifted-quadratic data plus compact-inactive local subsolution-patch data and comparison gives the source-shaped local quadratic max-patch datum.

      source
      theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBump.localQuadraticMaxPatch_of_compactInactiveSubsolution {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hquad : PerronLowerEnvelopeLocalQuadraticBump C boundary F g B) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveSubsolutionPatch C boundary F g B) :
      PerronLowerEnvelopeLocalQuadraticMaxPatch C boundary F g B

      Global local lifted-quadratic data plus compact-inactive local subsolution-patch data and comparison gives the global source-shaped local quadratic max-patch datum.

      source
      theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_localQuadraticMaxPatch_of_compactInactiveSubsolution {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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveSubsolutionPatch C boundary F g B) :
      PerronLowerEnvelopeLocalQuadraticMaxPatch C boundary F g B

      Operator continuity reduces the local quadratic max-patch step to compact-inactive local subsolution-patch data plus comparison.

      source
      theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBumpAt.maxPatchAt_of_compactInactiveCoveredAt {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 : PerronLowerEnvelopeLocalQuadraticBumpAt C boundary F g B x J) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveCoveredPatchAt C boundary F g B x J) :
      PerronLowerEnvelopeLocalQuadraticMaxPatchAt C boundary F g B x J

      Local lifted-quadratic data plus boundary-covered compact-inactive data gives the source-shaped local quadratic max-patch datum.

      The inactive compact covers both the inactive portion of C and the Dirichlet boundary. After finite Perron selection, the selected old branch dominates the lifted quadratic on the boundary, so the patched function agrees with the old branch there.

      source
      theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticBump.localQuadraticMaxPatch_of_compactInactiveCovered {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hquad : PerronLowerEnvelopeLocalQuadraticBump C boundary F g B) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveCoveredPatch C boundary F g B) :
      PerronLowerEnvelopeLocalQuadraticMaxPatch C boundary F g B

      Global local lifted-quadratic data plus boundary-covered compact-inactive data gives the global source-shaped local quadratic max-patch datum.

      source
      theorem ViscositySolns.OperatorContinuous.perronLowerEnvelope_localQuadraticMaxPatch_of_compactInactiveCovered {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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveCoveredPatch C boundary F g B) :
      PerronLowerEnvelopeLocalQuadraticMaxPatch C boundary F g B

      Operator continuity reduces the local quadratic max-patch step to boundary-covered compact-inactive data.