ExitMeanValueIdentificationWhole

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

The whole-space resolvent is an H¹ function of every exhaustion cube

The Dirichlet resolvents of the exhaustion cubes converge to the whole-space resolvent pointwise, and their gradients are Cauchy in L² of every fixed cube by the Caccioppoli estimate. Both convergences are handed to the closed H¹ graph of the cube, which returns an H¹ function whose value function is the whole-space resolvent on the nose — the exact pointwise representative survives the limit, which matters because every later argument reads its values pointwise.

Passing to the limit in the level equations identifies the forcing: the whole-space resolvent psi = R_mu f solves -div (a grad psi) = f - mu psi weakly on every exhaustion cube.

Subtracting the Green potential of that residual leaves the whole-space harmonic part, which is weakly a-harmonic on the cube and differs from psi by a named zero-trace Sobolev function. This is the level-m statement of ExitMeanValueIdentificationLevel.lean with the level objects replaced by their limits, and no weak-compactness argument is used anywhere.

The elliptic pairing as a Hilbert inner product

theorem DivergenceFormProcess.Form.setIntegral_flux_eq_inner {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (u w : HCPolySupport.H1Function U) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (HCPolySupport.matVecMul (a x) (u.grad x)) (w.grad x) = inner ℝ ((HCPolySupport.hilbertCoeffOperator hEll) u.gradToHilbertVectorL2) w.gradToHilbertVectorL2

The flux pairing of two H¹ gradients is an inner product against the continuous coefficient operator.

The whole-space residual

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

The residual of the whole-space resolvent: the datum less the shift times the resolvent.

Equations

• A.wholeSpaceResidual mu hf hfD y = f y - ↑mu * A.analyticMinimalResolventReal mu f hf hfD y

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_wholeSpaceResidual_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (y : HCPolySupport.Vec d) : |A.wholeSpaceResidual mu hf hfD y| ≤ 2 * D

L² membership of the limit objects on a cube

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.memL2On_analyticMinimalResolventReal {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) : HCPolySupport.MemL2On (wholeSpaceCube d v) (A.analyticMinimalResolventReal mu f hf hfD)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.memL2On_wholeSpaceResidual {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) : HCPolySupport.MemL2On (wholeSpaceCube d v) (A.wholeSpaceResidual mu hf hfD)

The approximating sequence on a fixed cube

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

The Dirichlet resolvent of the exhaustion cube of index v + 1 + n, restricted to the cube of index v.

Equations

• A.cubeApproxSolution v n mu hf hfD = (A.cubeLevelSolution (v + 1 + n) mu hf hfD).restrict ⋯ ⋯

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeApproxSolution_grad {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : (A.cubeApproxSolution v n mu hf hfD).grad = (A.cubeLevelSolution (v + 1 + n) mu hf hfD).grad

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.isScalarForcedWeakSolution_cubeApproxSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (v n : ℕ) (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 v) (A.cubeLevelResidual (v + 1 + n) mu hf hfD) (A.cubeApproxSolution v n mu hf hfD)

Convergence of the approximating sequence

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tendsto_toScalarL2_cubeApproxSolution {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 : ℕ) => (A.cubeApproxSolution v n mu hf hfD).toScalarL2) Filter.atTop (nhds (HCPolySupport.toScalarL2 ⋯))

The values converge in L² of the cube.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cauchySeq_gradToHilbertVectorL2_cubeApproxSolution {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) : CauchySeq fun (n : ℕ) => (A.cubeApproxSolution v n mu hf hfD).gradToHilbertVectorL2

The gradients are Cauchy in L² of the cube. This is the Caccioppoli estimate against the L² convergence of the values on the next cube.

The whole-space resolvent on a cube

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.exists_h1Function_analyticMinimalResolventReal {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) : ∃ (z : HCPolySupport.H1Function (wholeSpaceCube d v)), z.toFun = A.analyticMinimalResolventReal mu f hf hfD ∧ IsScalarForcedWeakSolution A.a (wholeSpaceCube d v) (A.wholeSpaceResidual mu hf hfD) z

The whole-space resolvent is an H¹ function of every exhaustion cube and solves the shifted equation there. Its value function is the exact continuous representative of the resolvent, not merely a function almost everywhere equal to it.