CubeSetAtHarmonicDensity

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

The uniform bound of the harmonic parts on a translated triadic cube

The harmonic parts of CubeSetAtHarmonicPart.lean are attached to nonnegative continuous data vanishing at infinity, because the exit decomposition is an extended-real statement. A general datum is a difference of two nonnegative ones, so this file records the uniform bound the harmonic parts obey on a translated triadic cube, which is what a difference argument consumes.

cubeSetAtHarmonicPartBound is that bound; it is nonnegative and dominates the harmonic part of the cube everywhere.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtHarmonicPartBound {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (y : HCPolySupport.Vec d) (n : ℤ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : ℝ

The uniform bound of a harmonic part on a translated triadic cube.

Equations

• A.cubeSetAtHarmonicPartBound R y n mu g = ‖(R.operator mu) g‖ + DivergenceFormProcess.Form.cubeResolventResidualBound R mu g * A.partTorsionBound ⋯

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_cubeSetAtHarmonicPart_le' {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (y : HCPolySupport.Vec d) (n : ℤ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (z : HCPolySupport.Vec d) : |A.cubeSetAtHarmonicPart R y n mu g z| ≤ A.cubeSetAtHarmonicPartBound R y n mu g

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeSetAtHarmonicPartBound_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (y : HCPolySupport.Vec d) (n : ℤ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : 0 ≤ A.cubeSetAtHarmonicPartBound R y n mu g