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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

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

theorem MeasureTheory.tilted_apply' {α : Type u_1} {mα : MeasurableSpace α} (μ : 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 α} (μ : Measure α) [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 α} {μ : 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 α} {μ : Measure α} [SFinite μ] (f : α → ℝ) (s : Set α) : (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, Real.exp (f a) / ∫ (x : α), Real.exp (f x) ∂μ ∂μ)

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

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

theorem MeasureTheory.setLIntegral_tilted' {α : Type u_1} {mα : MeasurableSpace α} {μ : 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.setLIntegral_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [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 α} {μ : 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.setIntegral_tilted' {α : Type u_1} {mα : MeasurableSpace α} {μ : 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.setIntegral_tilted {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [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 α} {μ : 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 α} {μ : 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 α} {μ : Measure α} {f : α → ℝ} (hf : Integrable (fun (x : α) => Real.exp (f x)) μ) (g : α → ℝ) : (μ.tilted f).tilted g = μ.tilted (f + g)

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

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

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

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

theorem MeasureTheory.integrable_tilted_iff {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → ℝ} (hf : Integrable (fun (x : α) => Real.exp (f x)) μ) (g : α → E) : Integrable g (μ.tilted f) ↔ Integrable (fun (x : α) => Real.exp (f x) • g x) μ

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

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

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

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

theorem MeasureTheory.rnDeriv_tilted_left_self {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} [SigmaFinite μ] (hf : AEMeasurable f μ) : (μ.tilted f).rnDeriv μ =ᵐ[μ] 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 α} {μ : Measure α} {f : α → ℝ} [SigmaFinite μ] (hf : Integrable (fun (x : α) => Real.exp (f x)) μ) : (fun (x : α) => Real.log ((μ.tilted f).rnDeriv μ x).toReal) =ᵐ[μ] fun (x : α) => f x - Real.log (∫ (x : α), Real.exp (f x) ∂μ)