ExitMeanValueIdentificationCauchy

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

The Caccioppoli Cauchy estimate for the exhaustion resolvents

The Dirichlet resolvents of a fixed bounded measurable datum on the cubes of the exhaustion converge pointwise to the whole-space resolvent, and are uniformly bounded. Their gradients are controlled by the Caccioppoli inequality at level zero: on two consecutive cubes V ⊆ V' the difference of two exhaustion levels solves the homogeneous shifted equation, whose forcing is a negative multiple of the difference, so the forcing pairing in the Caccioppoli estimate is nonpositive and ∫_V |grad (psi_k - psi_m)|² ≤ C ∫_{V'} (psi_k - psi_m)².

The right-hand side goes to zero by dominated convergence, so the gradients are Cauchy in L²(V) and no weak-compactness argument is needed.

This file supplies the two halves: the L² convergence of the values on any cube, and the Caccioppoli Cauchy estimate with a constant depending only on the cube index.

Two Hilbert-space identities

theorem DivergenceFormProcess.Form.gradToHilbertVectorL2_sub {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u w : HCPolySupport.H1Function U) : (u - w).gradToHilbertVectorL2 = u.gradToHilbertVectorL2 - w.gradToHilbertVectorL2

The Hilbert gradient class of a difference is the difference of the classes.

theorem DivergenceFormProcess.Form.norm_gradToHilbertVectorL2_sub_sq {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u w : HCPolySupport.H1Function U) : ‖u.gradToHilbertVectorL2 - w.gradToHilbertVectorL2‖ ^ 2 = ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecNormSq (u.grad x - w.grad x)

The squared L² norm of a gradient difference is the integral of the squared pointwise difference.

theorem DivergenceFormProcess.Form.norm_toScalarL2_sub_sq {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : HCPolySupport.H1Function U) {g : HCPolySupport.Vec d → ℝ} (hg : HCPolySupport.MemL2On U g) : ‖u.toScalarL2 - HCPolySupport.toScalarL2 hg‖ ^ 2 = ∫ (x : HCPolySupport.Vec d) in U, (u.toFun x - g x) ^ 2

The squared L² norm of a value difference is the integral of the squared pointwise difference.

Integrability of the cutoff energy density

The exhaustion-level solutions

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeLevelSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (m : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : HCPolySupport.H1Function (wholeSpaceCube d m)

The exact H¹ representative of the Dirichlet resolvent of the m-th exhaustion cube.

Equations

• A.cubeLevelSolution m mu hf hfD = Classical.choose ⋯

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeLevelSolution_toFun {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (m : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : (A.cubeLevelSolution m mu hf hfD).toFun = A.analyticCubeResolvent mu f hf hfD m

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.isScalarForcedWeakSolution_cubeLevelSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (m : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : IsScalarForcedWeakSolution A.a (wholeSpaceCube d m) (A.cubeLevelResidual m mu hf hfD) (A.cubeLevelSolution m mu hf hfD)

L² convergence of the values

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tendsto_setIntegral_analyticCubeResolvent_sub_sq {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : HCPolySupport.Vec d) in wholeSpaceCube d v, (A.analyticCubeResolvent mu f hf hfD n x - A.analyticMinimalResolventReal mu f hf hfD x) ^ 2) Filter.atTop (nhds 0)

The exhaustion resolvents converge to the whole-space resolvent in L² of every cube. The pointwise convergence is the exhaustion limit and the domination is the shift bound.

The Caccioppoli Cauchy estimate

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.exists_cubeCauchyConstant {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (k m : ℕ), v + 1 ≤ k → v + 1 ≤ m → ∫ (x : HCPolySupport.Vec d) in wholeSpaceCube d v, HCPolySupport.vecNormSq ((A.cubeLevelSolution k mu hf hfD).grad x - (A.cubeLevelSolution m mu hf hfD).grad x) ≤ C * ∫ (x : HCPolySupport.Vec d) in wholeSpaceCube d (v + 1), (A.analyticCubeResolvent mu f hf hfD k x - A.analyticCubeResolvent mu f hf hfD m x) ^ 2

The Caccioppoli Cauchy estimate. On the v-th exhaustion cube the gradients of the exhaustion resolvents at two levels beyond v differ in L² by at most a fixed multiple of their L² value difference on the next cube. The constant depends only on the ellipticity constants of the larger cube and on the cutoff between the two cubes.