w_def — Mathlib

English

For every E with the stated structure and every D, the function w is exactly the expression given by the formula in the previous item.

Русский

Для каждого пространства E с заданной структурой функция w совпадает с выражением, указанным в предыдущем пункте.

LaTeX

$$$w(D)=\\lambda x.\\Bigl(\\int_E u(z)\\,d\\mu(z)\\Bigr)^{-1} |D|^{-\\operatorname{finrank}_{\\mathbb{R}} E}\\, u(D^{-1} x).$$$

Lean4

theorem w_def (D : ℝ) : (w D : E → ℝ) = fun x => ((∫ x : E, u x ∂μ) * |D| ^ finrank ℝ E)⁻¹ • u (D⁻¹ • x) := by ext1 x;
  rfl

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