ExcessiveBarrier #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The barrier of the whole-space part-domain comparison #
Let V be an open bounded convex domain, f a nonnegative bounded measurable
observable vanishing off V, and u the shifted Dirichlet solution on V.
The barrier of the whole-space comparison is the difference
v = R^min f - u~,
where R^min is the analytic minimal resolvent of the cubic exhaustion and
u~ is the extension of u by zero to the whole space.
This file fixes the data of that barrier and proves the first analytic step:
on every exhaustion cube containing V, the zero extension of the part
solution is a weak subsolution of the shifted equation with the same forcing.
The continuous representative of the part solution vanishing on the geometric
boundary of V is a caller-supplied field of WholeSpaceBarrierData, not a
claim proved here. On an axis cube it is discharged by the closed-cube
boundary representative of the regularity layer.
The canonical shifted solution does not depend on the ellipticity certificate used to build it.
Restricting the L² class of a globally defined bounded measurable
observable to a smaller domain returns its L² class there.
A pointwise nonnegative bounded measurable observable has an almost
everywhere nonnegative L² class.
The L² class on the part domain of a globally defined bounded
measurable observable.
Equations
Instances For
Every bounded set lies inside an exhaustion cube.
The index of an exhaustion cube containing a bounded part domain.
Equations
Instances For
The ellipticity certificate of a bounded part domain, obtained by restricting the certificate of an exhaustion cube containing it. The shifted solution does not depend on the certificate, so nothing is lost by fixing this one.
The data of the whole-space barrier. A part domain V, a
nonnegative bounded measurable observable supported in V, and a continuous
zero extension utilde of the shifted Dirichlet solution on V. The last
three fields are the caller's obligation: they record that utilde is a
continuous representative of the part solution which vanishes off V.
- V : Set (HCPolySupport.Vec d)
The part domain.
- hV : HCPolySupport.IsOpenBoundedConvexDomain self.V
The part domain is an open bounded convex domain.
The shift.
- f : HCPolySupport.Vec d → ℝ
The observable.
- hf : Measurable self.f
Measurability of the observable.
Nonnegativity of the observable.
- D : ℝ
A uniform bound for the observable.
The uniform bound.
- hfV : self.f =ᵐ[MeasureTheory.volume] self.V.indicator self.f
The observable vanishes almost everywhere off the part domain.
- utilde : HCPolySupport.Vec d → ℝ
The continuous zero extension of the part solution.
- hutildeCont : Continuous self.utilde
Continuity of the zero extension.
- hutildeOff (x : HCPolySupport.Vec d) : x ∉ self.V → self.utilde x = 0
The zero extension vanishes off the part domain.
- hutildeRep : self.utilde =ᵐ[HCPolySupport.volumeMeasureOn self.V] ↑↑(ZeroTraceSobolev.toL2 ((alphaShiftedSolution A.a ⋯ ⋯ ⋯) (partDatumL2 ⋯ ⋯ ⋯)))
The zero extension represents the part solution.
Instances For
The shifted Dirichlet solution on the part domain.
Equations
Instances For
On an exhaustion cube containing the part domain, the restriction of the ambient datum solves the same part problem.
The zero extension of the part solution to an exhaustion cube.