condExp_finset_sum — Mathlib

English

Scaling: μ[c f|m] equals c μ[f|m] a.e. for any scalar c in the field.

Русский

Умножение на скаляр: μ[c f|m] = c μ[f|m] a.e. для любого скаляра c.

LaTeX

$$$$\\mu[c\\cdot f|m] =_{\\text{ae}} c\\cdot\\mu[f|m].$$$$

Lean4

theorem condExp_finset_sum {ι : Type*} {s : Finset ι} {f : ι → α → E} (hf : ∀ i ∈ s, Integrable (f i) μ)
    (m : MeasurableSpace α) : μ[∑ i ∈ s, f i|m] =ᵐ[μ] ∑ i ∈ s, μ[f i|m] := by
  classical
    induction s using Finset.induction_on with
  | empty => rw [Finset.sum_empty, Finset.sum_empty, condExp_zero]
  | insert i s his heq =>
    rw [Finset.sum_insert his, Finset.sum_insert his]
    exact
      (condExp_add (hf i <| Finset.mem_insert_self i s) (integrable_finset_sum' _ <| Finset.forall_of_forall_insert hf)
            _).trans
        ((EventuallyEq.refl _ _).add <| heq <| Finset.forall_of_forall_insert hf)

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