linearIsometry — Mathlib

English

There is a HasSum statement tying the coordinatewise images under V to the linear isometry image of f.

Русский

Существует утверждение имеет сумму, связывающее координатные изображения под V с образом линейной изометрии от f.

LaTeX

$$$ \\text{HasSum}(i \\mapsto V_i(f(i)),\\; hV.linearIsometry f)$$$

Lean4

/-- A mutually orthogonal family of subspaces of `E` induce a linear isometry from `lp 2` of the
subspaces into `E`. -/
protected def linearIsometry (hV : OrthogonalFamily 𝕜 G V) : lp G 2 →ₗᵢ[𝕜] E
    where
  toFun f := ∑' i, V i (f i)
  map_add' f
    g := by
    simp only [(hV.summable_of_lp f).tsum_add (hV.summable_of_lp g), lp.coeFn_add, Pi.add_apply, LinearIsometry.map_add]
  map_smul' c
    f := by
    simpa only [LinearIsometry.map_smul, Pi.smul_apply, lp.coeFn_smul] using (hV.summable_of_lp f).tsum_const_smul c
  norm_map'
    f := by
    classical
      -- needed for lattice instance on `Finset ι`, for `Filter.atTop_neBot`

    have H : 0 < (2 : ℝ≥0∞).toReal := by simp
    suffices ‖∑' i : ι, V i (f i)‖ ^ (2 : ℝ≥0∞).toReal = ‖f‖ ^ (2 : ℝ≥0∞).toReal by
      exact Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this
    refine tendsto_nhds_unique ?_ (lp.hasSum_norm H f)
    convert (hV.summable_of_lp f).hasSum.norm.rpow_const (Or.inr H.le) using 1
    ext s
    exact mod_cast (hV.norm_sum f s).symm

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