CruxGeneralDomainCube

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

The killed resolvent on a translated triadic cube

The localized Dirichlet problems of the field are indexed by the translated triadic cube cubeSetAt y n, the open cube of side 3 ^ n centred at y. It is an axis cube, so the caller obligation of the whole-space barrier data — a continuous zero extension of the part solution — is discharged there, and the barrier data may be built with the triadic cube itself as its part domain.

The resulting identification is the one the localized exit-time estimates consume: at every positive shift and every point of the cube, the resolvent of the process killed on leaving the compactified image of the cube, applied to the constant one, is the continuous representative of the Dirichlet resolvent of the constant datum on the cube.

theorem DivergenceFormProcess.Form.exists_continuous_partSolution_zeroExtension_of_eq_axisCube {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) (hVeq : V = HCPolySupport.axisCube z L) (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 ∉ V, w x = 0) ∧ w =ᵐ[HCPolySupport.volumeMeasureOn V] ↑↑(ZeroTraceSobolev.toL2 ((alphaShiftedSolution A.a ⋯ ⋯ ⋯) (partDatumL2 hV hf hfD)))

The continuous zero extension of the part solution on a domain which is an axis cube. The obligation is discharged on the axis cube and read back through the set equation.

noncomputable def DivergenceFormProcess.Form.eqAxisCubeBarrierData {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) (hVeq : V = HCPolySupport.axisCube z 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] V.indicator f) : WholeSpaceBarrierData A

The barrier data on a domain which is an axis cube. Every field is discharged, and the part domain of the data is the given set, not the axis cube it is equal to.

Equations

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

@[simp]

theorem DivergenceFormProcess.Form.eqAxisCubeBarrierData_V {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) (hVeq : V = HCPolySupport.axisCube z 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] V.indicator f) : (eqAxisCubeBarrierData A hV z hL hVeq lam hf hf0 hfD hfV).V = V

@[simp]

theorem DivergenceFormProcess.Form.eqAxisCubeBarrierData_f {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) (hVeq : V = HCPolySupport.axisCube z 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] V.indicator f) : (eqAxisCubeBarrierData A hV z hL hVeq lam hf hf0 hfD hfV).f = f

@[simp]

theorem DivergenceFormProcess.Form.eqAxisCubeBarrierData_lam {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) (hVeq : V = HCPolySupport.axisCube z 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] V.indicator f) : (eqAxisCubeBarrierData A hV z hL hVeq lam hf hf0 hfD hfV).lam = lam

The constant datum on a translated triadic cube

noncomputable def DivergenceFormProcess.Form.cubeSetAtOneDatum {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : HCPolySupport.Vec d → ℝ

The datum of the exit-time problem on a translated triadic cube: the constant one on the cube, extended by zero.

Equations

• DivergenceFormProcess.Form.cubeSetAtOneDatum y n = (Algsuperdiff.Section5.Support.cubeSetAt y n).indicator fun (x : HCPolySupport.Vec d) => 1

theorem DivergenceFormProcess.Form.measurable_cubeSetAtOneDatum {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : Measurable (cubeSetAtOneDatum y n)

theorem DivergenceFormProcess.Form.cubeSetAtOneDatum_nonneg {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (x : HCPolySupport.Vec d) : 0 ≤ cubeSetAtOneDatum y n x

theorem DivergenceFormProcess.Form.abs_cubeSetAtOneDatum_le {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (x : HCPolySupport.Vec d) : |cubeSetAtOneDatum y n x| ≤ 1

theorem DivergenceFormProcess.Form.cubeSetAtOneDatum_of_mem {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ Algsuperdiff.Section5.Support.cubeSetAt y n) : cubeSetAtOneDatum y n x = 1

theorem DivergenceFormProcess.Form.cubeSetAtOneDatum_ae_indicator {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : cubeSetAtOneDatum y n =ᵐ[MeasureTheory.volume] (Algsuperdiff.Section5.Support.cubeSetAt y n).indicator (cubeSetAtOneDatum y n)

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtOneBarrierData {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : WholeSpaceBarrierData A

The barrier data of the exit-time problem on a translated triadic cube. The part domain is cubeSetAt y n itself and the observable is the constant datum on it.

Equations

• A.cubeSetAtOneBarrierData y n lam = DivergenceFormProcess.Form.eqAxisCubeBarrierData A ⋯ (fun (i : Fin d) => y i - 3 ^ n / 2) ⋯ ⋯ lam ⋯ ⋯ ⋯ ⋯

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtOneBarrierData_V {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : (A.cubeSetAtOneBarrierData y n lam).V = Algsuperdiff.Section5.Support.cubeSetAt y n

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtOneBarrierData_f {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : (A.cubeSetAtOneBarrierData y n lam).f = cubeSetAtOneDatum y n

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtOneBarrierData_lam {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : (A.cubeSetAtOneBarrierData y n lam).lam = lam

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtOneResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : HCPolySupport.Vec d → ℝ

The Dirichlet resolvent of the constant datum on a translated triadic cube, in its continuous zero extension to the whole space.

Equations

• A.cubeSetAtOneResolvent y n lam = (A.cubeSetAtOneBarrierData y n lam).utilde

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.continuous_cubeSetAtOneResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : Continuous (A.cubeSetAtOneResolvent y n lam)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtOneResolvent_ae {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ↑MarkovProcess.Semigroup.PositiveShift) : A.cubeSetAtOneResolvent y n lam =ᵐ[HCPolySupport.volumeMeasureOn (Algsuperdiff.Section5.Support.cubeSetAt y n)] ↑↑(ZeroTraceSobolev.toL2 ((alphaShiftedSolution A.a ⋯ ⋯ ⋯) (partDatumL2 ⋯ ⋯ ⋯)))

The Dirichlet resolvent of the constant datum on a translated triadic cube represents the shifted part solution. This is the characterization the continuous zero extension is named by.

The expected exit time from a translated triadic cube

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtExitResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) (lam : ℝ) : OnePoint (HCPolySupport.Vec d) → ENNReal

The Dirichlet resolvent of the constant datum on a translated triadic cube, transported to the one-point compactification by zero extension. Outside the positive shifts the value is zero; the identifications below are stated at positive shifts only.

Equations

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtExitResolvent_coe {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) {lam : ℝ} (hlam : 0 < lam) (w : HCPolySupport.Vec d) : A.cubeSetAtExitResolvent y n lam ↑w = ENNReal.ofReal (A.cubeSetAtOneResolvent y n ⟨lam, hlam⟩ w)

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtExitFunction {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (y : HCPolySupport.Vec d) (n : ℤ) : OnePoint (HCPolySupport.Vec d) → ENNReal

The limit of the Dirichlet resolvents of the constant datum on a translated triadic cube as the shift decreases to zero, taken as the supremum along the shifts 1 / (m + 1). This is the shape in which the expected exit time consumes the limit.

Equations

• A.cubeSetAtExitFunction y n z = ⨆ (m : ℕ), A.cubeSetAtExitResolvent y n (↑m + 1)⁻¹ z