Densities, masses, and parameter measurability of exponentially tilted measures

Mathlib's MeasureTheory.Measure.tilted sends a measure μ and a potential f to the normalized measure (∫ exp f ∂μ)⁻¹ • exp f • μ. This file adds the facts used to identify tilted members of concrete families of distributions.

• MeasureTheory.Measure.map_tilted transports a tilt by a statistic on the target through a measurable pushforward.
• TauCeti.tilted_withDensity: tilting a measure with density g multiplies g by the normalized weight, so a tilted law with a density again has an explicit density.
• TauCeti.tilted_singleton: the mass of a singleton under a tilted measure, which identifies tilted laws on countable spaces; TauCeti.tilted_dirac records that point masses are fixed.
• TauCeti.measurable_tilted and TauCeti.measurable_tilted_mul: a jointly measurable family of potentials tilts an s-finite kernel into a measurable family of measures. For any measure μ (s-finite or not), t ↦ μ.tilted (t * X ·) is measurable for the Giry measurable structure.

theorem TauCeti.tilted_withDensity {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → ENNReal} (hg : AEMeasurable g μ) {f : α → ℝ} (hf : AEMeasurable f μ) : (μ.withDensity g).tilted f = μ.withDensity fun (x : α) => g x * ENNReal.ofReal (Real.exp (f x) / ∫ (y : α), Real.exp (f y) ∂μ.withDensity g)

Tilting a measure with density g multiplies the density by the normalized exponential weight.

theorem TauCeti.tilted_singleton {α : Type u_1} {mα : MeasurableSpace α} [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) (f : α → ℝ) (a : α) : (μ.tilted f) {a} = ENNReal.ofReal (Real.exp (f a) / ∫ (x : α), Real.exp (f x) ∂μ) * μ {a}

The mass of a singleton under an exponentially tilted measure.

@[simp]

theorem TauCeti.tilted_dirac {α : Type u_1} {mα : MeasurableSpace α} [MeasurableSingletonClass α] (a : α) (f : α → ℝ) : (MeasureTheory.Measure.dirac a).tilted f = MeasureTheory.Measure.dirac a

A point mass is unchanged by every tilt.

theorem TauCeti.measurable_tilted {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel β α) [ProbabilityTheory.IsSFiniteKernel κ] {f : β → α → ℝ} (hf : Measurable (Function.uncurry f)) : Measurable fun (b : β) => (κ b).tilted (f b)

Parameter measurability of tilting. Tilting the members of an s-finite kernel by a jointly measurable family of potentials gives a measurable family of measures.

theorem TauCeti.measurable_tilted_mul {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) {X : α → ℝ} (hX : Measurable X) : Measurable fun (t : ℝ) => μ.tilted fun (x : α) => t * X x

The exponential tilts μ.tilted (t * X ·) of a measure along a measurable statistic form a measurable family in the tilting parameter t. If μ is not s-finite, then no exp (t * X ·) is integrable (a positive integrable density would make μ s-finite), so every tilt vanishes.

theorem MeasureTheory.Measure.map_tilted {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure α) {f : α → β} {g : β → ℝ} (hf : Measurable f) (hg : Measurable g) : map f (μ.tilted (g ∘ f)) = (map f μ).tilted g

Pushing an exponential tilt forward commutes with tilting by a statistic on the target.