PenalizedResolventIdentity

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

Resolvent identity for the penalized cubic supremum

For a fixed exterior penalty, the bounded-domain resolvent identity passes through both cubic exhaustions. The required pointwise passage for the inner datum uses local freezing, so the continuous skew part may have arbitrary size.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tendsto_analyticPenalizedCubeResolvent_comp {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu nu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (outer : ℕ) (x : HCPolySupport.Vec d) : let g := fun (y : HCPolySupport.Vec d) => (A.analyticPenalizedResolvent hV n mu f hf hfD y).toReal; Filter.Tendsto (fun (k : ℕ) => A.analyticPenalizedCubeResolvent hV n nu (A.analyticPenalizedCubeResolvent hV n mu f hf hfD k) ⋯ ⋯ outer x) Filter.atTop (nhds (A.analyticPenalizedCubeResolvent hV n nu g ⋯ ⋯ outer x))

Applying a fixed outer penalized cube resolvent commutes with the increasing exhaustion limit of the inner penalized resolvents.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedResolvent_comp_eq_iSup {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (nu mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : let g := fun (y : HCPolySupport.Vec d) => (A.analyticPenalizedResolvent hV n mu f hf hfD y).toReal; (A.analyticPenalizedResolvent hV n nu g ⋯ ⋯ x).toReal = ⨆ (m : ℕ), A.analyticPenalizedCubeResolvent hV n nu (A.analyticPenalizedCubeResolvent hV n mu f hf hfD m) ⋯ ⋯ m x

The diagonal of the two cubic exhaustions computes the composition of two minimal resolvents with the same exterior penalty.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedResolvent_toReal_resolventIdentity {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu nu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : (A.analyticPenalizedResolvent hV n mu f hf hfD x).toReal = (A.analyticPenalizedResolvent hV n nu f hf hfD x).toReal + (↑nu - ↑mu) * (A.analyticPenalizedResolvent hV n nu (fun (y : HCPolySupport.Vec d) => (A.analyticPenalizedResolvent hV n mu f hf hfD y).toReal) ⋯ ⋯ x).toReal

The real minimal resolvents with a fixed exterior penalty satisfy the resolvent identity on nonnegative bounded measurable data.