MeasureTheory.tilted_of_not_integrable
theorem MeasureTheory.tilted_of_not_integrable :
∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
¬MeasureTheory.Integrable (fun x => (f x).exp) μ → μ.tilted f = 0
The theorem `MeasureTheory.tilted_of_not_integrable` states that for any type `α` with an associated measurable space `mα` and a measure `μ` of that space, and for any function `f` that maps from `α` to the real numbers, if the function that applies the real exponential function to the result of `f` (i.e., `fun x => Real.exp (f x)`) is not integrable with respect to the measure `μ`, then the tilted measure of `μ` with respect to `f` is `0`. In mathematical terms, this theorem asserts that if $\int \exp(f(x)) d\mu$ is not finite, then the tilted measure of `μ` with `f` is zero.
More concisely: If the exponential function of the integrable function `f` is not integrable with respect to measure `μ` on type `α`, then the tilted measure of `μ` by `f` is zero.
|
MeasureTheory.tilted_zero_measure
theorem MeasureTheory.tilted_zero_measure : ∀ {α : Type u_1} {mα : MeasurableSpace α} (f : α → ℝ), 0.tilted f = 0 := by
sorry
This theorem states that for any type `α` and any measurable space `mα` over this type `α`, the measure zero 'tilted' by any real-valued function `f` from `α` remains zero. In other words, it asserts that applying the 'tilting' operation (a certain transformation in measure theory) to the zero measure, irrespective of the function used, results in the zero measure.
More concisely: For any measurable space `(α, mα)` and measurable function `f: α → ℝ`, the tilted measure `mα' = mα ⊤ f` is zero.
|