integrable_mulExpNegMulSq_comp_restrict_of_isCompact

English

If P and P' produce the same integrals for all g in a subalgebra A of bounded continuous functions, then they give the same integral after applying mulExpNegMulSq with any g ∈ A.

Русский

Если для всех g из подпольной алгебры A интегралы по P и P' совпадают, то интегралы после применения mulExpNegMulSq также совпадают.

LaTeX

$$$\\forall g \\in A,\\; \\int_E mulExpNegMulSq(\\varepsilon, g)\\, dP = \\int_E mulExpNegMulSq(\\varepsilon, g)\\, dP'$$$

Lean4

theorem integrable_mulExpNegMulSq_comp_restrict_of_isCompact {K : Set E} (hK : IsCompact K) (hKmeas : MeasurableSet K)
    (g : C(E, ℝ)) : Integrable (fun x => mulExpNegMulSq ε (g x)) (P.restrict K) :=
  g.continuous.mulExpNegMulSq.continuousOn.integrableOn_compact' hK hKmeas

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