instIsZeroOrProbabilityMeasureCond

English

The conditional measure μ[|s] is either zero or a probability measure, in all generality.

Русский

Условная мера μ[|s] либо нулевая, либо вероятностная в общем случае.

LaTeX

$$IsZeroOrProbabilityMeasure(μ[|s])$$

Lean4

instance : IsZeroOrProbabilityMeasure μ[|s] := by
  constructor
  simp only [cond, Measure.coe_smul, Pi.smul_apply, MeasurableSet.univ, Measure.restrict_apply, univ_inter, smul_eq_mul,
    ← ENNReal.div_eq_inv_mul]
  rcases eq_or_ne (μ s) 0 with h | h
  · simp [h]
  rcases eq_or_ne (μ s) ∞ with h' | h'
  · simp [h']
  simp [ENNReal.div_self h h']

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