Submodules of E × F

In this module we define submoduleToLp which reinterprets a submodule of E × F, where E and F are inner product spaces, as a submodule of WithLp 2 (E × F). This allows us to take advantage of the inner product structure, since otherwise by default E × F is given the sup norm.

def InnerProductSpaceSubmodule.submoduleToLp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (M : Submodule ℂ (E × F)) : Submodule ℂ (WithLp 2 (E × F))

The submodule of WithLp 2 (E × F) defined by M.

Equations

• InnerProductSpaceSubmodule.submoduleToLp M = { carrier := {x : WithLp 2 (E × F) | x.ofLp ∈ M}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem InnerProductSpaceSubmodule.mem_submodule_iff_mem_submoduleToLp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (M : Submodule ℂ (E × F)) (f : E × F) : f ∈ M ↔ WithLp.toLp 2 f ∈ submoduleToLp M

theorem InnerProductSpaceSubmodule.submoduleToLp_closure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (M : Submodule ℂ (E × F)) : submoduleToLp M.topologicalClosure = (submoduleToLp M).topologicalClosure

theorem InnerProductSpaceSubmodule.mem_submodule_closure_iff_mem_submoduleToLp_closure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (M : Submodule ℂ (E × F)) (f : E × F) : f ∈ M.topologicalClosure ↔ WithLp.toLp 2 f ∈ (submoduleToLp M).topologicalClosure

theorem InnerProductSpaceSubmodule.mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (M : Submodule ℂ (E × F)) (g : F × E) : g ∈ M.adjoint ↔ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮ

theorem InnerProductSpaceSubmodule.mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (M : Submodule ℂ (E × F)) (f : E × F) : f ∈ M.adjoint.adjoint ↔ WithLp.toLp 2 f ∈ (submoduleToLp M)ᗮᗮ

theorem InnerProductSpaceSubmodule.mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (M : Submodule ℂ (E × F)) (g : F × E) : g ∈ M.topologicalClosure.adjoint ↔ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M).topologicalClosureᗮ