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μbyf, 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) ∂μ)
Instances For
@[simp]
theorem
MeasureTheory.tilted_of_not_integrable
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : ¬Integrable (fun (x : α) => Real.exp (f x)) μ)
:
@[simp]
theorem
MeasureTheory.tilted_of_not_aemeasurable
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : ¬AEMeasurable f μ)
:
@[simp]
theorem
MeasureTheory.tilted_const
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : Measure α)
[IsProbabilityMeasure μ]
(c : ℝ)
:
@[simp]
theorem
MeasureTheory.tilted_zero
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : Measure α)
[IsProbabilityMeasure μ]
:
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 : α → ℝ}
:
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)
:
theorem
MeasureTheory.setIntegral_tilted
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[SFinite μ]
(f : α → ℝ)
(g : α → E)
(s : Set α)
:
theorem
MeasureTheory.tilted_tilted
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : Integrable (fun (x : α) => Real.exp (f x)) μ)
(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)) μ)
:
@[simp]
theorem
MeasureTheory.tilted_neg_same'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : Integrable (fun (x : α) => Real.exp (f x)) μ)
:
theorem
MeasureTheory.tilted_neg_same
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
[IsProbabilityMeasure μ]
(hf : Integrable (fun (x : α) => Real.exp (f x)) μ)
:
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)
:
theorem
MeasureTheory.rnDeriv_tilted_right
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℝ}
(μ ν : Measure α)
[SigmaFinite μ]
[SigmaFinite ν]
(hf : Integrable (fun (x : α) => Real.exp (f x)) ν)
:
theorem
MeasureTheory.toReal_rnDeriv_tilted_right
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℝ}
(μ ν : Measure α)
[SigmaFinite μ]
[SigmaFinite ν]
(hf : Integrable (fun (x : α) => Real.exp (f x)) ν)
:
theorem
MeasureTheory.rnDeriv_tilted_left
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : Measure α)
{f : α → ℝ}
{ν : Measure α}
[SigmaFinite μ]
[SigmaFinite ν]
(hfν : AEMeasurable f ν)
:
theorem
MeasureTheory.toReal_rnDeriv_tilted_left
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : Measure α)
{f : α → ℝ}
{ν : Measure α}
[SigmaFinite μ]
[SigmaFinite ν]
(hfν : AEMeasurable f ν)
:
theorem
MeasureTheory.rnDeriv_tilted_left_self
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
[SigmaFinite μ]
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.log_rnDeriv_tilted_left_self
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
[SigmaFinite μ]
(hf : Integrable (fun (x : α) => Real.exp (f x)) μ)
: