tilted_zero' — Mathlib

English

Tilting μ by the zero density gives μ_tilted(0) = (μ(Ω))^{-1} μ, i.e., the zero-density tilt is a scaled version of μ.

Русский

Тильтование нулевой плотностью даёт μ_tilted(0) = (μ(Ω))^{-1} μ, то есть тильтованная нулем мера равна масштабуемой μ.

LaTeX

$$$$\\mu^{\\mathrm{tilted}}(0) = \\mu(\\mathcal{U})^{-1}\\cdot \\mu,$$$$

Lean4

@[simp]
theorem tilted_zero' (μ : Measure α) : μ.tilted 0 = (μ Set.univ)⁻¹ • μ :=
  by
  change μ.tilted (fun _ ↦ 0) = (μ Set.univ)⁻¹ • μ
  simp

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