Resolvent Transform of a Measure

Given a normed algebra A over a normed field 𝕜, and μ : Measure 𝕜, we define the resolvent transform of μ by the formula

resolventTransform μ a = ∫ x, resolvent a x ∂μ = ∫ x, (↑ₐ x - a)⁻¹ʳ ∂μ

This is not a standard notion in the literature, but specializes to a few standard notions, namely the case 𝕜 = ℝ and A = ℂ is the Stieltjes transform, and the case 𝕜 = A = ℂ is the Cauchy transform, given by the formulas:

∫ (x : ℝ), (↑x - a)⁻¹ ∂μ and ∫ (x : ℂ), (↑x - a)⁻¹ ∂μ respectively.

Main definitions

• resolventTransform μ a: The resolvent transform of a measure μ at a

Main statements

• hasDerivAt_resolventTransform: For any a not in the support of μ, the resolventTransform has derivative ∫ x, resolvent a x ^ 2 ∂u at a.
• analyticOn_resolventTransform: In the case A = ℂ, the resolventTransform is holomorphic on the complement of μ.support.

Tags

resolvent transform, Stieljes transform, Cauchy transform

theorem MeasureTheory.measurable_resolvent {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [MeasurableSpace 𝕜] {a : A} [OpensMeasurableSpace 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [MeasurableSpace A] [BorelSpace A] : Measurable (resolvent a)

theorem MeasureTheory.norm_resolvent_le_inv_infDist_support {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [MeasurableSpace 𝕜] [CompleteSpace 𝕜] [NormedDivisionRing A] [NormedAlgebra 𝕜 A] {μ : Measure 𝕜} {a : A} (hz : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support) {x : 𝕜} (hx : x ∈ μ.support) : ‖resolvent a x‖ ≤ (Metric.infDist a (⇑(algebraMap 𝕜 A) '' μ.support))⁻¹

theorem MeasureTheory.integrable_resolvent {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [MeasurableSpace 𝕜] [CompleteSpace 𝕜] [NormedDivisionRing A] [NormedAlgebra 𝕜 A] [HereditarilyLindelofSpace 𝕜] [OpensMeasurableSpace 𝕜] [CompleteSpace A] [SecondCountableTopology A] [MeasurableSpace A] [BorelSpace A] {μ : Measure 𝕜} [IsFiniteMeasure μ] {a : A} (hz : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support) : Integrable (resolvent a) μ

noncomputable def MeasureTheory.resolventTransform {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra ℝ A] [NormedAlgebra 𝕜 A] {m𝕜 : MeasurableSpace 𝕜} (μ : Measure 𝕜) (a : A) : A

The resolvent transform of a measure.

Equations

• MeasureTheory.resolventTransform μ a = ∫ (x : 𝕜), resolvent a x ∂μ

theorem MeasureTheory.resolventTransform_def {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra ℝ A] [NormedAlgebra 𝕜 A] {m𝕜 : MeasurableSpace 𝕜} (μ : Measure 𝕜) : resolventTransform μ = fun (a : A) => ∫ (x : 𝕜), resolvent a x ∂μ

theorem MeasureTheory.resolventTransform_apply {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra ℝ A] [NormedAlgebra 𝕜 A] {m𝕜 : MeasurableSpace 𝕜} (μ : Measure 𝕜) (a : A) : resolventTransform μ a = ∫ (x : 𝕜), resolvent a x ∂μ

@[simp]

theorem MeasureTheory.resolventTransform_zero_measure {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra ℝ A] [NormedAlgebra 𝕜 A] {m𝕜 : MeasurableSpace 𝕜} : resolventTransform 0 = 0

@[simp]

theorem MeasureTheory.resolventTransform_dirac {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra ℝ A] [NormedAlgebra 𝕜 A] {m𝕜 : MeasurableSpace 𝕜} [MeasurableSingletonClass 𝕜] [CompleteSpace A] (x : 𝕜) (a : A) : resolventTransform (Measure.dirac x) a = resolvent a x

theorem MeasureTheory.hasDerivAt_resolventTransform {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [HereditarilyLindelofSpace 𝕜] [CompleteSpace 𝕜] [MeasurableSpace 𝕜] [BorelSpace 𝕜] [RCLike A] [NormedAlgebra 𝕜 A] {μ : Measure 𝕜} [IsFiniteMeasure μ] (a : A) (ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support) : HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), resolvent a x ^ 2 ∂μ) a

theorem MeasureTheory.analyticOn_resolventTransform {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [HereditarilyLindelofSpace 𝕜] [CompleteSpace 𝕜] [MeasurableSpace 𝕜] [BorelSpace 𝕜] [NormedAlgebra 𝕜 ℂ] {μ : Measure 𝕜} [IsFiniteMeasure μ] : AnalyticOn ℂ (resolventTransform μ) (⇑(algebraMap 𝕜 ℂ) '' μ.support)ᶜ