Theorems · Theorem · measure theory

MeasureTheory.analyticOn_resolventTransform

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

Defined in

Mathlib.MeasureTheory.Measure.ResolventTransform

Cited by

0 results in Mathlib

Foundations

Depth 288 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldHereditarilyLindelofSpaceCompleteSpaceMeasurableSpaceBorelSpaceNormedAlgebraMeasureTheory.IsFiniteMeasure