English
Let φ be an integrable family of finite-dimensional continuous multilinear maps. Integration commutes with applying a fixed coordinate vector to the map inside the integral.
Русский
Пусть φ — интегрируемая совокупность многолинейных отображений. Интегрирование можно обменять с применением фиксированного аргумента к отображению внутри интеграла.
LaTeX
$$$\\int_x φ(x) \\, dμ = φ\\left(\\int_x x \\, dμ\\right)$ в смысле соответствующих координат$$
Lean4
theorem _root_.ContinuousMultilinearMap.integral_apply {ι : Type*} [Fintype ι] {M : ι → Type*}
[∀ i, NormedAddCommGroup (M i)] [∀ i, NormedSpace 𝕜 (M i)] {φ : X → ContinuousMultilinearMap 𝕜 M E}
(φ_int : Integrable φ μ) (m : ∀ i, M i) : (∫ x, φ x ∂μ) m = ∫ x, φ x m ∂μ :=
by
by_cases hE : CompleteSpace E
· exact ((ContinuousMultilinearMap.apply 𝕜 M E m).integral_comp_comm φ_int).symm
· by_cases hm : ∀ i, m i ≠ 0
· have : ¬CompleteSpace (ContinuousMultilinearMap 𝕜 M E) := by
rwa [SeparatingDual.completeSpace_continuousMultilinearMap_iff _ _ hm]
simp [integral, hE, this]
· push_neg at hm
rcases hm with ⟨i, hi⟩
simp [ContinuousMultilinearMap.map_coord_zero _ i hi]
