extend — Mathlib

English

The Pi-orthonormalBasis, constructed from component bases, yields the product basis via the specified map.

Русский

Pi-ортонормBasis преобразуется в базис через компонентные базисы и отображение.

LaTeX

$$$ (\Pi.orthonormalBasis B).toBasis = ((\Pi.basis) (\{i \mapsto (B i).toBasis\}).map(WithLp.linearEquiv 2 _ _).symm)$$$

Lean4

/-- Let `S` be a subspace of a finite-dimensional complex inner product space `V`.  A linear
isometry mapping `S` into `V` can be extended to a full isometry of `V`.

TODO:  The case when `S` is a finite-dimensional subspace of an infinite-dimensional `V`. -/
noncomputable def extend (L : S →ₗᵢ[𝕜] V) : V →ₗᵢ[𝕜] V := by
  -- Build an isometry from Sᗮ to L(S)ᗮ through `EuclideanSpace`

  let d := finrank 𝕜 Sᗮ
  let LS := LinearMap.range L.toLinearMap
  have E : Sᗮ ≃ₗᵢ[𝕜] LSᗮ :=
    by
    have dim_LS_perp : finrank 𝕜 LSᗮ = d :=
      calc
        finrank 𝕜 LSᗮ = finrank 𝕜 V - finrank 𝕜 LS := by
          simp only [← LS.finrank_add_finrank_orthogonal, add_tsub_cancel_left]
        _ = finrank 𝕜 V - finrank 𝕜 S := by simp only [LS, LinearMap.finrank_range_of_inj L.injective]
        _ = finrank 𝕜 Sᗮ := by simp only [← S.finrank_add_finrank_orthogonal, add_tsub_cancel_left]
    exact (stdOrthonormalBasis 𝕜 Sᗮ).repr.trans ((stdOrthonormalBasis 𝕜 LSᗮ).reindex <| finCongr dim_LS_perp).repr.symm
  let L3 := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
  haveI : CompleteSpace S := FiniteDimensional.complete 𝕜 S
  haveI : CompleteSpace V := FiniteDimensional.complete 𝕜 V
  let p1 := S.orthogonalProjection.toLinearMap
  let p2 := Sᗮ.orthogonalProjection.toLinearMap
  let M := L.toLinearMap.comp p1 + L3.toLinearMap.comp p2
  have M_norm_map : ∀ x : V, ‖M x‖ = ‖x‖ := by
    intro x
    have Mx_decomp : M x = L (p1 x) + L3 (p2 x) := by
      simp only [M, LinearMap.add_apply, LinearMap.comp_apply, LinearMap.comp_apply, LinearIsometry.coe_toLinearMap]
        -- Mx_decomp is the orthogonal decomposition of M x

    have Mx_orth : ⟪L (p1 x), L3 (p2 x)⟫ = 0 :=
      by
      have Lp1x : L (p1 x) ∈ LinearMap.range L.toLinearMap := LinearMap.mem_range_self L.toLinearMap (p1 x)
      have Lp2x : L3 (p2 x) ∈ (LinearMap.range L.toLinearMap)ᗮ :=
        by
        simp only [LS, ← Submodule.range_subtype LSᗮ]
        apply LinearMap.mem_range_self
      apply Submodule.inner_right_of_mem_orthogonal Lp1x Lp2x
    rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), norm_sq_eq_add_norm_sq_projection x S]
    simp only [sq, Mx_decomp]
    rw [norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (L (p1 x)) (L3 (p2 x)) Mx_orth]
    simp only [p1, p2, LinearIsometry.norm_map, ContinuousLinearMap.coe_coe, Submodule.coe_norm]
  exact
    { toLinearMap := M
      norm_map' := M_norm_map }

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