CruxGeneralDomainTail

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

The Agmon tail comparison for a killed set inside an exhaustion cube

The exterior-penalization interchange compares the whole-space penalized resolvents of a killed set V with the penalized resolvents of the next exhaustion cube. The error is the scale-free Agmon tail at mass mu + n, and the only geometric input is that the data vanish off V and that V lies inside a fixed exhaustion cube: a point beyond the collar of that cube has a unit Euclidean ball disjoint from V, which is what the tail theorem reads.

The killed set is an arbitrary open subset of the cube. No interchange statement is asserted for data which remain nonzero outside the killed set.

theorem DivergenceFormProcess.Form.disjoint_unitBall_of_subset_wholeSpaceCube {d : ℕ} {V : Set (HCPolySupport.Vec d)} {v : ℕ} (hVcube : V ⊆ wholeSpaceCube d v) {x : HCPolySupport.Vec d} (hx : x ∉ interchangeCollar d v) : Disjoint (HCPolySupport.euclideanBall x 1) V

A point beyond the collar of an exhaustion cube has a unit Euclidean ball disjoint from every subset of that cube.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.penalizedCubeResolventH10_ae_eq {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : (A.penalizedCubeResolventH10 hV n mu hf hfD m).toFun =ᵐ[HCPolySupport.volumeMeasureOn (wholeSpaceCube d m)] A.analyticPenalizedCubeResolvent hV n mu f hf hfD m

The zero-trace penalized cube solution and its analytic representative agree almost everywhere on the cube.

theorem DivergenceFormProcess.Form.boundedMeasurableToScalarL2_wholeSpaceCube_ae_eq {d : ℕ} {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : ↑↑(boundedMeasurableToScalarL2 ⋯ ⋯ ⋯) =ᵐ[HCPolySupport.volumeMeasureOn (wholeSpaceCube d m)] f

The L² class of a globally defined bounded measurable observable on an exhaustion cube is that observable almost everywhere there.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpacePenalizationPotential_ae_eq_penalizationPotential {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (n : ℕ) : wholeSpacePenalizationPotential V n =ᵐ[HCPolySupport.volumeMeasureOn U] penalizationPotential U V n

On a measurable set the whole-space exterior penalization potential of a killed set agrees almost everywhere with the local penalization potential.