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 = MeasureTheory.Measure.withDensity μ fun (x : α) => ENNReal.ofReal (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ)

@[simp]

theorem MeasureTheory.tilted_of_not_integrable {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : ¬MeasureTheory.Integrable fun (x : α) => Real.exp (f x)) : μ.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 : f =ᶠ[MeasureTheory.Measure.ae μ] g) : μ.tilted f = μ.tilted g

theorem MeasureTheory.tilted_eq_withDensity_nnreal {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ) : μ.tilted f = MeasureTheory.Measure.withDensity μ fun (x : α) => ↑{ val := Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ, property := (_ : 0 ≤ Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) }

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 (Real.exp (f a) / ∫ (x : α), Real.exp (f x) ∂μ) ∂μ

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

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, Real.exp (f a) / ∫ (x : α), Real.exp (f x) ∂μ ∂μ)

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, Real.exp (f a) / ∫ (x : α), Real.exp (f x) ∂μ ∂μ)

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

Equations

• (_ : MeasureTheory.IsFiniteMeasure (μ.tilted f)) = (_ : MeasureTheory.IsFiniteMeasure (μ.tilted f))

theorem MeasureTheory.isProbabilityMeasure_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [NeZero μ] (hf : MeasureTheory.Integrable fun (x : α) => Real.exp (f x)) : 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 (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) * 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 (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) * g x ∂μ

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

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, (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) • g x ∂μ

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, (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) • g x ∂μ

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 : α), (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) • g x ∂μ

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

theorem MeasureTheory.tilted_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable fun (x : α) => Real.exp (f x)) (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 : α) => Real.exp (f x)) {g : α → ℝ} (hg : MeasureTheory.Integrable fun (x : α) => Real.exp (g x)) : (μ.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 : α) => Real.exp (f x)) : (μ.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 : α) => Real.exp (f x)) : (μ.tilted f).tilted (-f) = μ

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

theorem MeasureTheory.absolutelyContinuous_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable fun (x : α) => Real.exp (f x)) : MeasureTheory.Measure.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 : α) => Real.exp (f x)) : MeasureTheory.Measure.rnDeriv μ (ν.tilted f) =ᶠ[MeasureTheory.Measure.ae ν] fun (x : α) => ENNReal.ofReal (Real.exp (-f x) * ∫ (x : α), Real.exp (f x) ∂ν) * MeasureTheory.Measure.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 : α) => Real.exp (f x)) : (fun (x : α) => ENNReal.toReal (MeasureTheory.Measure.rnDeriv μ (ν.tilted f) x)) =ᶠ[MeasureTheory.Measure.ae ν] fun (x : α) => (Real.exp (-f x) * ∫ (x : α), Real.exp (f x) ∂ν) * ENNReal.toReal (MeasureTheory.Measure.rnDeriv μ ν x)

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) : MeasureTheory.Measure.rnDeriv (μ.tilted f) ν =ᶠ[MeasureTheory.Measure.ae ν] fun (x : α) => ENNReal.ofReal (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) * MeasureTheory.Measure.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) : (fun (x : α) => ENNReal.toReal (MeasureTheory.Measure.rnDeriv (μ.tilted f) ν x)) =ᶠ[MeasureTheory.Measure.ae ν] fun (x : α) => (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) * ENNReal.toReal (MeasureTheory.Measure.rnDeriv μ ν x)

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

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