Exponentially tilted measures

The exponential tilting of a measure μ on α by a function f : α → ℝ is the measure with density x ↦ exp (f x) / ∫ y, exp (f y) ∂μ with respect to μ. This is sometimes also called the Esscher transform.

The definition is mostly used for f linear, in which case the exponentially tilted measure belongs to the natural exponential family of the base measure. Exponentially tilted measures for general f can be used for example to establish variational expressions for the Kullback-Leibler divergence.

Main definitions

• Measure.tilted μ f: exponential tilting of μ by f, equal to μ.withDensity (fun x ↦ ENNReal.ofReal (exp (f x) / ∫ x, exp (f x) ∂μ)).

noncomputable def MeasureTheory.Measure.tilted {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ) : MeasureTheory.Measure α

Exponentially tilted measure. When x ↦ exp (f x) is integrable, μ.tilted f is the probability measure with density with respect to μ proportional to exp (f x). Otherwise it is 0.

Equations

• μ.tilted f = μ.withDensity fun (x : α) => ENNReal.ofReal ((f x).exp / ∫ (x : α), (f x).exp ∂μ)

@[simp]

theorem MeasureTheory.tilted_of_not_integrable {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : ¬MeasureTheory.Integrable (fun (x : α) => (f x).exp) μ) : μ.tilted f = 0

@[simp]

theorem MeasureTheory.tilted_of_not_aemeasurable {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : ¬AEMeasurable f μ) : μ.tilted f = 0

@[simp]

theorem MeasureTheory.tilted_zero_measure {α : Type u_1} {mα : MeasurableSpace α} (f : α → ℝ) : 0.tilted f = 0

@[simp]

theorem MeasureTheory.tilted_const' {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (c : ℝ) : (μ.tilted fun (x : α) => c) = (↑↑μ Set.univ)⁻¹ • μ

theorem MeasureTheory.tilted_const {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (c : ℝ) : (μ.tilted fun (x : α) => c) = μ

@[simp]

theorem MeasureTheory.tilted_zero' {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) : μ.tilted 0 = (↑↑μ Set.univ)⁻¹ • μ

theorem MeasureTheory.tilted_zero {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : μ.tilted 0 = μ

theorem MeasureTheory.tilted_congr {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} {g : α → ℝ} (hfg : μ.ae.EventuallyEq f g) : μ.tilted f = μ.tilted g

theorem MeasureTheory.tilted_eq_withDensity_nnreal {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ) : μ.tilted f = μ.withDensity fun (x : α) => ↑⟨(f x).exp / ∫ (x : α), (f x).exp ∂μ, ⋯⟩

theorem MeasureTheory.tilted_apply' {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ) {s : Set α} (hs : MeasurableSet s) : ↑↑(μ.tilted f) s = ∫⁻ (a : α) in s, ENNReal.ofReal ((f a).exp / ∫ (x : α), (f x).exp ∂μ) ∂μ

theorem MeasureTheory.tilted_apply {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (f : α → ℝ) (s : Set α) : ↑↑(μ.tilted f) s = ∫⁻ (a : α) in s, ENNReal.ofReal ((f a).exp / ∫ (x : α), (f x).exp ∂μ) ∂μ

theorem MeasureTheory.tilted_apply_eq_ofReal_integral' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (f : α → ℝ) (hs : MeasurableSet s) : ↑↑(μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, (f a).exp / ∫ (x : α), (f x).exp ∂μ ∂μ)

theorem MeasureTheory.tilted_apply_eq_ofReal_integral {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (f : α → ℝ) (s : Set α) : ↑↑(μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, (f a).exp / ∫ (x : α), (f x).exp ∂μ ∂μ)

instance MeasureTheory.isFiniteMeasure_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} : MeasureTheory.IsFiniteMeasure (μ.tilted f)

Equations

• ⋯ = ⋯

theorem MeasureTheory.isProbabilityMeasure_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [NeZero μ] (hf : MeasureTheory.Integrable (fun (x : α) => (f x).exp) μ) : MeasureTheory.IsProbabilityMeasure (μ.tilted f)

theorem MeasureTheory.set_lintegral_tilted' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ℝ) (g : α → ENNReal) {s : Set α} (hs : MeasurableSet s) : ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal ((f x).exp / ∫ (x : α), (f x).exp ∂μ) * g x ∂μ

theorem MeasureTheory.set_lintegral_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (f : α → ℝ) (g : α → ENNReal) (s : Set α) : ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal ((f x).exp / ∫ (x : α), (f x).exp ∂μ) * g x ∂μ

theorem MeasureTheory.lintegral_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ℝ) (g : α → ENNReal) : ∫⁻ (x : α), g x ∂μ.tilted f = ∫⁻ (x : α), ENNReal.ofReal ((f x).exp / ∫ (x : α), (f x).exp ∂μ) * g x ∂μ

theorem MeasureTheory.setIntegral_tilted' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : α → ℝ) (g : α → E) {s : Set α} (hs : MeasurableSet s) : ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, ((f x).exp / ∫ (x : α), (f x).exp ∂μ) • g x ∂μ

@[deprecated MeasureTheory.setIntegral_tilted']

theorem MeasureTheory.set_integral_tilted' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : α → ℝ) (g : α → E) {s : Set α} (hs : MeasurableSet s) : ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, ((f x).exp / ∫ (x : α), (f x).exp ∂μ) • g x ∂μ

Alias of MeasureTheory.setIntegral_tilted'.

theorem MeasureTheory.setIntegral_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.SFinite μ] (f : α → ℝ) (g : α → E) (s : Set α) : ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, ((f x).exp / ∫ (x : α), (f x).exp ∂μ) • g x ∂μ

@[deprecated MeasureTheory.setIntegral_tilted]

theorem MeasureTheory.set_integral_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.SFinite μ] (f : α → ℝ) (g : α → E) (s : Set α) : ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, ((f x).exp / ∫ (x : α), (f x).exp ∂μ) • g x ∂μ

Alias of MeasureTheory.setIntegral_tilted.

theorem MeasureTheory.integral_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : α → ℝ) (g : α → E) : ∫ (x : α), g x ∂μ.tilted f = ∫ (x : α), ((f x).exp / ∫ (x : α), (f x).exp ∂μ) • g x ∂μ

theorem MeasureTheory.integral_exp_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ℝ) (g : α → ℝ) : ∫ (x : α), (g x).exp ∂μ.tilted f = (∫ (x : α), ((f + g) x).exp ∂μ) / ∫ (x : α), (f x).exp ∂μ

theorem MeasureTheory.tilted_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable (fun (x : α) => (f x).exp) μ) (g : α → ℝ) : (μ.tilted f).tilted g = μ.tilted (f + g)

theorem MeasureTheory.tilted_comm {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable (fun (x : α) => (f x).exp) μ) {g : α → ℝ} (hg : MeasureTheory.Integrable (fun (x : α) => (g x).exp) μ) : (μ.tilted f).tilted g = (μ.tilted g).tilted f

@[simp]

theorem MeasureTheory.tilted_neg_same' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable (fun (x : α) => (f x).exp) μ) : (μ.tilted f).tilted (-f) = (↑↑μ Set.univ)⁻¹ • μ

@[simp]

theorem MeasureTheory.tilted_neg_same {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hf : MeasureTheory.Integrable (fun (x : α) => (f x).exp) μ) : (μ.tilted f).tilted (-f) = μ

theorem MeasureTheory.tilted_absolutelyContinuous {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ) : (μ.tilted f).AbsolutelyContinuous μ

theorem MeasureTheory.absolutelyContinuous_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable (fun (x : α) => (f x).exp) μ) : μ.AbsolutelyContinuous (μ.tilted f)

theorem MeasureTheory.rnDeriv_tilted_right {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hf : MeasureTheory.Integrable (fun (x : α) => (f x).exp) ν) : ν.ae.EventuallyEq (μ.rnDeriv (ν.tilted f)) fun (x : α) => ENNReal.ofReal ((-f x).exp * ∫ (x : α), (f x).exp ∂ν) * μ.rnDeriv ν x

theorem MeasureTheory.toReal_rnDeriv_tilted_right {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hf : MeasureTheory.Integrable (fun (x : α) => (f x).exp) ν) : ν.ae.EventuallyEq (fun (x : α) => (μ.rnDeriv (ν.tilted f) x).toReal) fun (x : α) => ((-f x).exp * ∫ (x : α), (f x).exp ∂ν) * (μ.rnDeriv ν x).toReal

theorem MeasureTheory.rnDeriv_tilted_left {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hfμ : AEMeasurable f μ) (hfν : AEMeasurable f ν) : ν.ae.EventuallyEq ((μ.tilted f).rnDeriv ν) fun (x : α) => ENNReal.ofReal ((f x).exp / ∫ (x : α), (f x).exp ∂μ) * μ.rnDeriv ν x

theorem MeasureTheory.toReal_rnDeriv_tilted_left {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hfμ : AEMeasurable f μ) (hfν : AEMeasurable f ν) : ν.ae.EventuallyEq (fun (x : α) => ((μ.tilted f).rnDeriv ν x).toReal) fun (x : α) => ((f x).exp / ∫ (x : α), (f x).exp ∂μ) * (μ.rnDeriv ν x).toReal

theorem MeasureTheory.rnDeriv_tilted_left_self {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.SigmaFinite μ] (hf : AEMeasurable f μ) : μ.ae.EventuallyEq ((μ.tilted f).rnDeriv μ) fun (x : α) => ENNReal.ofReal ((f x).exp / ∫ (x : α), (f x).exp ∂μ)

theorem MeasureTheory.log_rnDeriv_tilted_left_self {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.SigmaFinite μ] (hf : MeasureTheory.Integrable (fun (x : α) => (f x).exp) μ) : μ.ae.EventuallyEq (fun (x : α) => ((μ.tilted f).rnDeriv μ x).toReal.log) fun (x : α) => f x - (∫ (x : α), (f x).exp ∂μ).log