ExitTimePDEIdentification

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The torsion function of an exhaustion cube and its uniform bound

The unshifted Dirichlet problem with constant forcing on an exhaustion cube, -div (a grad w) = 1 in V, w = 0 on the boundary of V,

is solvable, and this file fixes one measurable solution and bounds it uniformly.

The constant forcing is written in divergence form once and for all (cubeTorsionField): the field with a single nonzero coordinate equal to the negative of the corresponding coordinate function. Its length at a point is the absolute value of that coordinate, hence at most the half-side of the cube. The divergence-form De Giorgi estimate therefore bounds the solution in the supremum norm by a dimensional constant times sqrt d, divided by the lower ellipticity constant, times the square of the half-side.

The solution is fixed as a measurable representative (cubeTorsionFunction), because the De Giorgi estimate and every later pointwise argument read the values of the function rather than its L² class.

The other statement proved here is the passage from the scalar weak equation to the shifted weak equation on the zero-trace graph carrier (isAlphaShiftedWeakSolution_of_isScalarForcedWeakSolution): a solution of -div (a grad u) = g also solves (lam - div (a grad)) u = g + lam u, and on an open bounded convex domain the graph carrier is exhausted by honest zero-trace Sobolev functions, so the test class is the same one.

The constant forcing in divergence form

noncomputable def DivergenceFormProcess.Form.cubeTorsionField (d : ℕ) [NeZero d] : HCPolySupport.Vec d → HCPolySupport.Vec d

The divergence form of the constant forcing one: the field whose only nonzero coordinate is the negative of the corresponding coordinate function.

Equations

• DivergenceFormProcess.Form.cubeTorsionField d = DivergenceFormProcess.scalarToDivergenceField (fun (x : HCPolySupport.Vec d) => 1) default 0

theorem DivergenceFormProcess.Form.coordinatePrimitive_one {d : ℕ} (i : Fin d) (x : HCPolySupport.Vec d) : coordinatePrimitive (fun (x : HCPolySupport.Vec d) => 1) i 0 x = x i

The coordinate primitive of the constant one based at the origin is the corresponding coordinate function.

theorem DivergenceFormProcess.Form.cubeTorsionField_apply {d : ℕ} [NeZero d] (x : HCPolySupport.Vec d) (j : Fin d) : cubeTorsionField d x j = if j = default then -x default else 0

theorem DivergenceFormProcess.Form.vecNormSq_cubeTorsionField {d : ℕ} [NeZero d] (x : HCPolySupport.Vec d) : HCPolySupport.vecNormSq (cubeTorsionField d x) = x default * x default

theorem DivergenceFormProcess.Form.memVectorL2_cubeTorsionField {d : ℕ} [NeZero d] {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) : HCPolySupport.MemVectorL2 U (cubeTorsionField d)

From the scalar equation to the shifted equation

theorem DivergenceFormProcess.Form.isAlphaShiftedWeakSolution_of_isScalarForcedWeakSolution {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {a : HCPolySupport.CoeffField d} {alpha : ℝ} (u : HCPolySupport.H10Function U) {g : HCPolySupport.Vec d → ℝ} (hg : IsScalarForcedWeakSolution a U g u.toH1Function) (G : ↥(HCPolySupport.ScalarL2 U)) (hG : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑G x = g x + alpha * u.toFun x) : IsAlphaShiftedWeakSolution a U alpha G (ZeroTraceSobolev.ofH10Function u)

The scalar weak equation is a shifted weak equation with shifted forcing. On an open bounded convex domain every element of the zero-trace graph carrier is an honest zero-trace Sobolev function, so the two test classes agree.

The torsion function

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.exists_measurable_cubeTorsionSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : ∃ (w : HCPolySupport.H10Function (wholeSpaceCube d v)), Measurable w.toFun ∧ HCPolySupport.IsZeroTraceDirichletRhsWeakSolution A.a (wholeSpaceCube d v) w (cubeTorsionField d)

A measurable torsion function exists on every exhaustion cube.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionFunction {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : HCPolySupport.H10Function (wholeSpaceCube d v)

The chosen measurable torsion function of an exhaustion cube.

Equations

• A.cubeTorsionFunction v = Classical.choose ⋯

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_cubeTorsionFunction {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : Measurable (A.cubeTorsionFunction v).toFun

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionFunction_isZeroTraceDirichletRhsWeakSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : HCPolySupport.IsZeroTraceDirichletRhsWeakSolution A.a (wholeSpaceCube d v) (A.cubeTorsionFunction v) (cubeTorsionField d)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionFunction_isScalarForcedWeakSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : IsScalarForcedWeakSolution A.a (wholeSpaceCube d v) (fun (x : HCPolySupport.Vec d) => 1) (A.cubeTorsionFunction v).toH1Function

The torsion function solves the unshifted problem with constant forcing.

The uniform bound

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionConstant {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) : ℝ

The dimensional constant of the torsion bound. It is twice the De Giorgi constant of the dimension. It reads the analytic data only through the proof of 2 ≤ d, so it does not depend on the cube, on the coefficient field or on the lower ellipticity constant.

Equations

• A.cubeTorsionConstant = 2 * Classical.choose ⋯

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionConstant_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) : 0 ≤ A.cubeTorsionConstant

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionBound {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : ℝ

The uniform bound for the torsion function of an exhaustion cube: the dimensional constant times the square root of the dimension, divided by the lower ellipticity constant, times the square of the half-side of the cube.

Equations

• A.cubeTorsionBound v = A.cubeTorsionConstant * (√↑d / A.nu) * (3 ^ v * 3 ^ v)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeTorsionBound_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : 0 ≤ A.cubeTorsionBound v

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_cubeTorsionFunction_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (wholeSpaceCube d v), |(A.cubeTorsionFunction v).toFun x| ≤ A.cubeTorsionBound v

The torsion function of an exhaustion cube is uniformly bounded, with a constant that does not depend on the cube. The divergence form of the constant forcing has length at most the half-side of the cube, so the divergence-form De Giorgi estimate applies at the dimensional constant, and the resulting bound is that constant times the square root of the dimension, divided by the lower ellipticity constant, times the square of the half-side.