CubeSetAtMeanValueStream

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

The exit mean-value property on a translated triadic cube for the stream field

CubeSetAtMeanValueConsumer.lean carries a global small-contrast datum, because the exit decomposition it invokes does. The stream field of the model supplies no such datum, and the coefficient-generic C₀ barrier comparison replaces it. This file is the small-contrast-free copy of that chain on cubeSetAt y n: the same statements, with the small-contrast datum removed from every hypothesis list and the analytic data fixed to the stream field of the model.

The analytic half — the Green potential of the cube, the harmonic part, and its H¹ packaging — carries no process hypothesis at all and is shared verbatim with the small-contrast route; only the four process statements and the two consumer lemmas are repeated here.

The assumptions are those of the coefficient-generic comparison: the resolvent carrying the process, its one-point regularity data, conservativity of the live kernel semigroup, the bounded-measurable identification of the kernel resolvent with the analytic minimal resolvent, and the operator identification against the C₀ barrier resolvent of the stream field.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.hasExitMeanValueOn_cubeSetAtHarmonicPart_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (hcons : R.kernelSemigroup.IsConservative) (hid : (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal R) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = (⋯.resolvent.operator mu) g) (y : HCPolySupport.Vec d) (n : ℤ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hg0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ g z) : StoppedDirichlet.HasExitMeanValueOn R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) (onePointRealExtension ((Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtHarmonicPart R y n mu g))

The harmonic part of a resolvent datum on a translated triadic cube is represented by the exit distribution, for the stream field.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.hasExitMeanValueOn_cubeSetAtHarmonicPart_sub_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (hcons : R.kernelSemigroup.IsConservative) (hid : (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal R) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = (⋯.resolvent.operator mu) g) (y : HCPolySupport.Vec d) (n : ℤ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g₁ g₂ : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hg₁ : ∀ (z : HCPolySupport.Vec d), 0 ≤ g₁ z) (hg₂ : ∀ (z : HCPolySupport.Vec d), 0 ≤ g₂ z) : StoppedDirichlet.HasExitMeanValueOn R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) (onePointRealExtension fun (z : HCPolySupport.Vec d) => (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtHarmonicPart R y n mu g₁ z - (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtHarmonicPart R y n mu g₂ z)

A difference of harmonic parts on a translated triadic cube is represented by the exit distribution, for the stream field.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.hasExitMeanValueOn_onePointRealExtension_of_forall_approx_harmonicPart_cubeSetAt_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (hcons : R.kernelSemigroup.IsConservative) (hid : (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal R) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = (⋯.resolvent.operator mu) g) (y : HCPolySupport.Vec d) (n : ℤ) {h : HCPolySupport.Vec d → ℝ} (hh : Measurable h) {N : ℝ} (hN : ∀ (z : HCPolySupport.Vec d), |h z| ≤ N) (happrox : ∀ eps > 0, ∃ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g₁ : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (g₂ : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (∀ (z : HCPolySupport.Vec d), 0 ≤ g₁ z) ∧ (∀ (z : HCPolySupport.Vec d), 0 ≤ g₂ z) ∧ ∀ (z : HCPolySupport.Vec d), |(Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtHarmonicPart R y n mu g₁ z - (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtHarmonicPart R y n mu g₂ z - h z| ≤ eps) : StoppedDirichlet.HasExitMeanValueOn R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) (onePointRealExtension h)

A uniform limit of differences of harmonic parts on a translated triadic cube is represented by the exit distribution, for the stream field.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtHarmonicPart_eq_partWholeSpaceHarmonicPart_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = (⋯.resolvent.operator mu) g) (y : HCPolySupport.Vec d) (n : ℤ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (z : HCPolySupport.Vec d) : (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtHarmonicPart R y n mu g z = (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).partWholeSpaceHarmonicPart ⋯ mu ⋯ ⋯ ⋯ z

The harmonic part of a stream resolvent datum on a translated triadic cube is the whole-space harmonic part of that datum there.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.exists_h1Function_cubeSetAtHarmonicPart_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = (⋯.resolvent.operator mu) g) (y : HCPolySupport.Vec d) (n : ℤ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : ∃ (z : HCPolySupport.H1Function (Algsuperdiff.Section5.Support.cubeSetAt y n)) (h : HCPolySupport.H1Function (Algsuperdiff.Section5.Support.cubeSetAt y n)), (∀ (w : HCPolySupport.Vec d), z.toFun w = ((R.operator mu) g) w) ∧ (∀ (w : HCPolySupport.Vec d), h.toFun w = (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtHarmonicPart R y n mu g w) ∧ IsScalarForcedWeakSolution (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).a (Algsuperdiff.Section5.Support.cubeSetAt y n) (fun (x : HCPolySupport.Vec d) => 0) h ∧ HCPolySupport.MemH10 (Algsuperdiff.Section5.Support.cubeSetAt y n) fun (w : HCPolySupport.Vec d) => z.toFun w - h.toFun w

The H¹ package of a harmonic part on a translated triadic cube, for the stream field.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.hasExitMeanValueOn_onePointRealExtension_of_isWeaklyHarmonicOn_cubeSetAt_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (hcons : R.kernelSemigroup.IsConservative) (hid : (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal R) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = (⋯.resolvent.operator mu) g) (y : HCPolySupport.Vec d) (n : ℤ) (F : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (Phi : HCPolySupport.H1Function (Algsuperdiff.Section5.Support.cubeSetAt y n)) (hPhi : ∀ (w : HCPolySupport.Vec d), Phi.toFun w = F w) {u : HCPolySupport.Vec d → ℝ} (hu : Measurable u) {N : ℝ} (hN : ∀ (w : HCPolySupport.Vec d), |u w| ≤ N) (hoff : ∀ w ∉ Algsuperdiff.Section5.Support.cubeSetAt y n, u w = F w) (hucont : ContinuousOn u (Algsuperdiff.Section5.Support.cubeSetAt y n)) (Y : HCPolySupport.H1Function (Algsuperdiff.Section5.Support.cubeSetAt y n)) (hY : ∀ (w : HCPolySupport.Vec d), Y.toFun w = u w) (hharm : IsScalarForcedWeakSolution (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).a (Algsuperdiff.Section5.Support.cubeSetAt y n) (fun (x : HCPolySupport.Vec d) => 0) Y) (htrace : HCPolySupport.MemH10 (Algsuperdiff.Section5.Support.cubeSetAt y n) fun (w : HCPolySupport.Vec d) => Y.toFun w - Phi.toFun w) : StoppedDirichlet.HasExitMeanValueOn R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) (onePointRealExtension u)

A weakly a-harmonic function on a translated triadic cube with a continuous boundary datum vanishing at infinity has the exit mean-value property, for the stream field.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.hasExitMeanValueOn_onePointRealExtension_of_contDiffBoundaryDatum_cubeSetAt_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (hcons : R.kernelSemigroup.IsConservative) (hid : (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal R) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = (⋯.resolvent.operator mu) g) (y : HCPolySupport.Vec d) (n : ℤ) {b : HCPolySupport.Vec d → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hbCompact : HasCompactSupport b) {u : HCPolySupport.Vec d → ℝ} (hu : Measurable u) {N : ℝ} (hN : ∀ (w : HCPolySupport.Vec d), |u w| ≤ N) (hoff : ∀ w ∉ Algsuperdiff.Section5.Support.cubeSetAt y n, u w = b w) (hucont : ContinuousOn u (Algsuperdiff.Section5.Support.cubeSetAt y n)) (Y : HCPolySupport.H1Function (Algsuperdiff.Section5.Support.cubeSetAt y n)) (hY : ∀ (w : HCPolySupport.Vec d), Y.toFun w = u w) (hharm : IsScalarForcedWeakSolution (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).a (Algsuperdiff.Section5.Support.cubeSetAt y n) (fun (x : HCPolySupport.Vec d) => 0) Y) (htrace : HCPolySupport.MemH10 (Algsuperdiff.Section5.Support.cubeSetAt y n) fun (w : HCPolySupport.Vec d) => u w - b w) : StoppedDirichlet.HasExitMeanValueOn R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) (onePointRealExtension u)

The instantiation shape on a translated triadic cube, for the stream field. When the boundary datum is a smooth compactly supported function b, the continuous datum vanishing at infinity and its H¹ realization on the cube are both supplied by b itself, and the only inputs left are the weak harmonicity of the observable inside the cube, its continuity there, its agreement with b outside, and its trace.