constOfIsEmptyLIE — Mathlib

English

For a subsingleton index, the difference f(m1) - f(m2) is bounded by a quantity linear in ||f|| and a sum of products of the norms of m.

Русский

Для подмножества индексов норма разности f(m1) - f(m2) ограничена величиной, пропорциональной ||f||, и суммой произведений норм элементов m.

LaTeX

$$$\|f(m_1) - f(m_2)\| \le \|f\| \cdot \sum_i \prod_j \big(\|m_{1,i} - m_{2,i}\|^{\delta_{j,i}} \cdot \max(\|m_{1,j}\|,\|m_{2,j}\|)^{1-\delta_{j,i}}\big)$$$

Lean4

/-- `constOfIsEmpty` as a linear isometry equivalence. -/
@[simps]
def constOfIsEmptyLIE [IsEmpty ι] : F ≃ₗᵢ[𝕜] (E [⋀^ι]→L[𝕜] F)
    where
  toFun := constOfIsEmpty _ _ _
  invFun f := f 0
  left_inv x := by simp
  right_inv f := by ext x; simp [Subsingleton.allEq x 0]
  map_add' f g := rfl
  map_smul' c f := rfl
  norm_map' := norm_constOfIsEmpty _ _

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