English
Let μ be a measure on α. For any real constant c, tilting μ by the constant density c yields the same measure as μ scaled by the total mass of μ on the universe; i.e. μ.tilted (fun _ ↦ c) = (μ(Ω))^{-1} μ, where Ω is the ambient space.
Русский
Пусть μ — мера на множествах α. Для любого вещественного постоянного значения c тильтинг меры μ константной плотностью даёт ту же самую меру, что и нормирование μ на суммарную величину μ(Ω); то есть μ.tilted (предел по константе) = (μ(Ω))^{-1} μ.
LaTeX
$$$$\\mu(\\mathcal{U})^{-1}\\cdot \\mu = \\mu^{\\text{tilted}}(c)$$$$
Lean4
@[simp]
theorem tilted_const' (μ : Measure α) (c : ℝ) : μ.tilted (fun _ ↦ c) = (μ Set.univ)⁻¹ • μ := by
cases eq_zero_or_neZero μ with
| inl h => rw [h]; simp
| inr h0 =>
simp only [Measure.tilted, withDensity_const, integral_const, smul_eq_mul]
by_cases h_univ : μ Set.univ = ∞
·
simp only [measureReal_def, h_univ, ENNReal.toReal_top, zero_mul, div_zero, ENNReal.ofReal_zero, zero_smul,
ENNReal.inv_top]
congr
rw [div_eq_mul_inv, mul_inv, mul_comm, mul_assoc, inv_mul_cancel₀ (exp_pos _).ne', mul_one, measureReal_def, ←
ENNReal.toReal_inv, ENNReal.ofReal_toReal]
simp [h0.out]
