ExcessiveCubeData

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

The barrier data on an axis cube

The caller obligation of WholeSpaceBarrierData is the continuous representative of the part solution which vanishes on the geometric boundary of the part domain. On an axis cube it is discharged: the shifted residual of a bounded measurable datum is a bounded scalar source, so the closed-cube boundary representative of the regularity layer applies, and a continuous function on the closed cube vanishing on its geometric boundary extends by zero to a continuous function on the whole space.

The resulting barrier data needs no input beyond the coefficient field and the observable.

theorem DivergenceFormProcess.Form.exists_continuous_zeroExtension_of_cube_boundary_zero {d : ℕ} (z : HCPolySupport.Vec d) (L : ℝ) (v : HCPolySupport.Vec d → ℝ) (hv : ContinuousOn v {x : HCPolySupport.Vec d | Algsuperdiff.StochasticProcess.Common.Regularity.MemAxisCubeClosure z L x}) (hvzero : ∀ (x : HCPolySupport.Vec d), Algsuperdiff.StochasticProcess.Common.Regularity.MemAxisCubeClosure z L x → x ∉ HCPolySupport.axisCube z L → v x = 0) : ∃ (w : HCPolySupport.Vec d → ℝ), Continuous w ∧ (∀ x ∈ HCPolySupport.axisCube z L, w x = v x) ∧ ∀ x ∉ HCPolySupport.axisCube z L, w x = 0

A continuous closed-cube function vanishing on the geometric boundary extends by zero to a continuous function on the whole space.

theorem DivergenceFormProcess.Form.exists_continuous_partSolution_zeroExtension {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) {LamV : ℝ} (hEllV : HCPolySupport.IsEllipticFieldOn A.nu LamV (HCPolySupport.axisCube z L) A.a) (lam : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : ∃ (w : HCPolySupport.Vec d → ℝ), Continuous w ∧ (∀ x ∉ HCPolySupport.axisCube z L, w x = 0) ∧ w =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.axisCube z L)] ↑↑(ZeroTraceSobolev.toL2 ((alphaShiftedSolution A.a ⋯ ⋯ hEllV) (partDatumL2 ⋯ hf hfD)))

The continuous zero extension of the part solution on an axis cube. The closed-cube boundary representative of the regularity layer applies to the shifted residual of a bounded measurable datum, and its zero extension is continuous on the whole space.

noncomputable def DivergenceFormProcess.Form.axisCubeBarrierData {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) (lam : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hfV : f =ᵐ[MeasureTheory.volume] (HCPolySupport.axisCube z L).indicator f) : WholeSpaceBarrierData A

The barrier data of the whole-space comparison on an axis cube. Every field is discharged: the continuous zero extension of the part solution comes from the closed-cube boundary representative.

Equations

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

@[simp]

theorem DivergenceFormProcess.Form.axisCubeBarrierData_V {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) (lam : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hfV : f =ᵐ[MeasureTheory.volume] (HCPolySupport.axisCube z L).indicator f) : (axisCubeBarrierData A z hL lam hf hf0 hfD hfV).V = HCPolySupport.axisCube z L

@[simp]

theorem DivergenceFormProcess.Form.axisCubeBarrierData_lam {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) (lam : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hfV : f =ᵐ[MeasureTheory.volume] (HCPolySupport.axisCube z L).indicator f) : (axisCubeBarrierData A z hL lam hf hf0 hfD hfV).lam = lam

@[simp]

theorem DivergenceFormProcess.Form.axisCubeBarrierData_f {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) (lam : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hfV : f =ᵐ[MeasureTheory.volume] (HCPolySupport.axisCube z L).indicator f) : (axisCubeBarrierData A z hL lam hf hf0 hfD hfV).f = f