isZeroOrProbabilityMeasure_tilted

English

For any μ and f, the tilted measure μ.tilted f is either the zero measure or a probability measure.

Русский

Для любой μ и f тильтованная мера либо нулевая, либо мера вероятности.

LaTeX

$$$$\\mu^{\\mathrm{tilted}} f \\;\\text{is either } 0 \\text{ or a probability measure.}$$$$

Lean4

instance isZeroOrProbabilityMeasure_tilted : IsZeroOrProbabilityMeasure (μ.tilted f) :=
  by
  rcases eq_zero_or_neZero μ with hμ | hμ
  · simp only [hμ, tilted_zero_measure]
    infer_instance
  by_cases hf : Integrable (fun x ↦ exp (f x)) μ
  · have := isProbabilityMeasure_tilted hf
    infer_instance
  · simp only [hf, not_false_eq_true, tilted_of_not_integrable]
    infer_instance

Похожие утверждения