PenalizedNormalizedTail

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

Shift-normalized tails for exterior penalization

An exterior-penalized equation can be read as a constant-shift equation at mass mu + n. After multiplication by mu / (mu + n), its zero-trace solution has the sharp maximum-principle normalization required by the scale-free resolvent-tail theorem. The resulting bound is uniform in the outer cube and decays with sqrt (mu + n) away from the data cube.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.mul_abs_analyticPenalizedCubeResolvent_le_localizedTail {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (L : WholeSpaceLocalizedSplitData A) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf1 : ∀ (x : HCPolySupport.Vec d), |f x| ≤ 1) (hfsupp : ∀ᵐ (x : HCPolySupport.Vec d), x ∉ V → f x = 0) (m : ℕ) {x : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) (hball : HCPolySupport.euclideanBall x r ⊆ wholeSpaceCube d m) (hdisjoint : Disjoint (HCPolySupport.euclideanBall x r) V) : ↑mu * |A.analyticPenalizedCubeResolvent hV n mu f hf hf1 m x| ≤ L.tail ⟨↑mu + ↑n, ⋯⟩ x r

Away from the data cube, the local exterior-penalized resolvent satisfies the localized split-skew tail at the enlarged mass mu + n. The rough and smooth-divergence constants are read only on the displayed source-free ball.