_aux_Mathlib_Probability_Moments_Variance___macroRules_ProbabilityTheory_termVar[_]_1

English

evariance X μ equals the lintegral of ENNReal.ofReal((X−Eμ[X])^2) with respect to μ.

Русский

evariance X μ равна линтегралу ENNReal.ofReal((X−Eμ[X])^2) по μ.

LaTeX

$$evariance X μ = ∫⁻ ω, ENNReal.ofReal ((X(ω) - μ[X])^2) ∂μ$$

Lean4

@[scoped macro ProbabilityTheory.«termVar[_]»]
public meta def «_aux_Mathlib_Probability_Moments_Variance___macroRules_ProbabilityTheory_termVar[_]_1» : Macro✝ := fun
  | `(Var[$X]) => ``(Var[$X; MeasureTheory.MeasureSpace.volume])
  | _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝

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