English
Extending linearity to general scalars: for any scalar c from a field 𝕜 and any x ∈ F, condExpIndL1 hm μ s (c · x) = c · condExpIndL1 hm μ s x, provided the scalar action commutes suitably with the real scalars.
Русский
Расширяем линейность до произвольного скаляра c из поля 𝕜 и элемента x ∈ F: condExpIndL1 hm μ s (c · x) = c · condExpIndL1 hm μ s x при надлежащем коммутировании действия скаляров.
LaTeX
$$$ condExpIndL1\; hm\; \mu\; s\; (c \cdot x) = c \cdot condExpIndL1\; hm\; \mu\; s\; x, \quad c \in 𝕜,\ x \in F,$$
Lean4
theorem condExpIndL1_smul' [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (x : F) :
condExpIndL1 hm μ s (c • x) = c • condExpIndL1 hm μ s x :=
by
by_cases hs : MeasurableSet s
swap; · simp_rw [condExpIndL1_of_not_measurableSet hs]; rw [smul_zero]
by_cases hμs : μ s = ∞
· simp_rw [condExpIndL1_of_measure_eq_top hμs]; rw [smul_zero]
· simp_rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs]
exact condExpIndL1Fin_smul' hs hμs c x
