Conservativity

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

Conservativity of the whole-space analytic resolvent

The defect 1 - mu R^{U_m}_mu 1 is represented as an H¹ solution of the homogeneous shifted equation. Interior decay along the cubic exhaustion then removes the defect in the limit.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeOneResolventH10 {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (m : ℕ) : HCPolySupport.H10Function (wholeSpaceCube d m)

A fixed H¹₀ representative of the local resolvent of one.

Equations

• A.cubeOneResolventH10 mu m = Classical.choose ⋯

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeOneResolventH10_value {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (m : ℕ) : (A.cubeOneResolventH10 mu m).toScalarL2 = (alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (boundedMeasurableToScalarL2 ⋯ ⋯ ⋯)

The chosen representative has the prescribed zero-trace Sobolev class.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.volume_wholeSpaceCube_toReal {d : ℕ} (m : ℕ) : (MeasureTheory.volume (wholeSpaceCube d m)).toReal = (2 * 3 ^ m) ^ d

The volume of the mth exhaustion cube.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.norm_cubeConstantOne_le {d : ℕ} (m : ℕ) : ‖boundedMeasurableToScalarL2 ⋯ ⋯ ⋯‖ ≤ √(MeasureTheory.volume (wholeSpaceCube d m)).toReal

The constant-one datum on a cube has the expected volume-order L² bound.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeConstantOneH1 {d : ℕ} (m : ℕ) : HCPolySupport.H1Function (wholeSpaceCube d m)

The constant-one function as an H¹ function on a cube.

Equations

• DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeConstantOneH1 m = HCPolySupport.H1Function.ofContDiffOnIsOpenBoundedConvexDomain ⋯ ⋯

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryRemainderH1 {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (m : ℕ) : HCPolySupport.H1Function (wholeSpaceCube d m)

The H¹ boundary defect 1 - mu R^{U_m}_mu 1.

Equations

• A.cubeBoundaryRemainderH1 mu m = DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeConstantOneH1 m - ↑mu • (A.cubeOneResolventH10 mu m).toH1Function

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryRemainder_ae {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (m : ℕ) : (A.cubeBoundaryRemainderH1 mu m).toFun =ᵐ[HCPolySupport.volumeMeasureOn (wholeSpaceCube d m)] fun (x : HCPolySupport.Vec d) => 1 - ↑mu * A.analyticCubeResolvent mu (fun (x : HCPolySupport.Vec d) => 1) ⋯ ⋯ m x

The H¹ boundary defect agrees almost everywhere with the analytic pointwise defect.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryRemainder_abs_le_one_ae {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (m : ℕ) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (wholeSpaceCube d m), |(A.cubeBoundaryRemainderH1 mu m).toFun x| ≤ 1

The boundary defect lies between zero and one almost everywhere.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryRemainder_isScalarForcedWeakSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (m : ℕ) : IsScalarForcedWeakSolution A.a (wholeSpaceCube d m) (fun (y : HCPolySupport.Vec d) => -(↑mu * (A.cubeBoundaryRemainderH1 mu m).toFun y)) (A.cubeBoundaryRemainderH1 mu m)

The cube boundary defect solves the homogeneous shifted equation. This form is independent of any global small-contrast assumption and is the PDE input for both the original and localized interior-decay routes.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryCutoffInnerRadius (m : ℕ) : ℝ

Inner radius of the cutoff used to measure distance from the boundary of the mth cube.

Equations

• DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryCutoffInnerRadius m = 3 ^ m / 2

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryCutoffOuterRadius (m : ℕ) : ℝ

Outer transition radius of the boundary cutoff.

Equations

• DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryCutoffOuterRadius m = 3 * 3 ^ m / 4

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryCutoff {d : ℕ} (m : ℕ) : HCPolySupport.Vec d → ℝ

A smooth localization supported strictly inside the mth cube and equal to one on its central half ball.

Equations

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.contDiff_cubeBoundaryCutoff {d : ℕ} (m : ℕ) : ContDiff ℝ (↑⊤) (cubeBoundaryCutoff m)

The boundary localization is smooth.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.hasCompactSupport_cubeBoundaryCutoff {d : ℕ} (m : ℕ) : HasCompactSupport (cubeBoundaryCutoff m)

The boundary localization has compact support.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tsupport_cubeBoundaryCutoff_subset {d : ℕ} (m : ℕ) : tsupport (cubeBoundaryCutoff m) ⊆ wholeSpaceCube d m

The support of the boundary localization lies inside its cube.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tsupport_cubeBoundaryCutoff_subset_euclideanBall {d : ℕ} (m : ℕ) : tsupport (cubeBoundaryCutoff m) ⊆ HCPolySupport.euclideanBall 0 (3 ^ m)

The full active support of the boundary cutoff lies in the origin-centred ball of radius 3^m. This is the carrier used by the localized split-skew coefficient bounds.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryCutoff_eq_one {d m : ℕ} {y : HCPolySupport.Vec d} (hy : y ∈ HCPolySupport.euclideanBall 0 (cubeBoundaryCutoffInnerRadius m)) : cubeBoundaryCutoff m y = 1

The boundary localization is one throughout its inner ball.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryCutoffInnerRadius_le_euclideanNorm {d m : ℕ} {y : HCPolySupport.Vec d} (hy : fderiv ℝ (cubeBoundaryCutoff m) y ≠ 0) : cubeBoundaryCutoffInnerRadius m ≤ HCPolySupport.euclideanNorm (y - 0)

A nonzero derivative of the boundary localization lies outside its inner radius.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryRemainder_gradient_budget {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (m : ℕ) {W : Set (HCPolySupport.Vec d)} (hW : W ⊆ wholeSpaceCube d m) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorLpSizeOn W 2 (A.cubeBoundaryRemainderH1 mu m).grad ≤ ↑mu * (min (↑mu) A.nu)⁻¹ * (MeasureTheory.volume (wholeSpaceCube d m)).toReal

A volume-order budget for the gradient of the boundary defect on every subset of the cube.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryCutoffGradientBudget {d : ℕ} (m : ℕ) : ℝ

The explicit coordinate-gradient budget of the boundary localization.

Equations

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

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryCutoffUniformGradientBudget {d : ℕ} : ℝ

A scale-independent upper bound for the coordinate-gradient budget of the boundary localization.

Equations

• DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryCutoffUniformGradientBudget = ↑d * (HCPolySupport.smoothTransitionProfile.derivBound * (8 * ↑d)) ^ 2

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryCutoff_gradSq_le_uniform {d : ℕ} (m : ℕ) (y : HCPolySupport.Vec d) : (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ (cubeBoundaryCutoff m) y) (HCPolySupport.basisVec i)) ≤ cubeBoundaryCutoffUniformGradientBudget

The coordinate-gradient square of the boundary cutoff is bounded by the scale-independent cutoff budget.