Documentation

Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm

Projective seminorm on the tensor of a finite family of normed spaces. #

Let 𝕜 be a nontrivially normed field and E be a family of normed 𝕜-vector spaces Eᵢ, indexed by a finite type ι. We define a seminorm on ⨂[𝕜] i, Eᵢ, which we call the "projective seminorm". For x an element of ⨂[𝕜] i, Eᵢ, its projective seminorm is the infimum over all expressions of x as ∑ j, ⨂ₜ[𝕜] mⱼ i (with the mⱼΠ i, Eᵢ) of ∑ j, Π i, ‖mⱼ i‖.

In particular, every norm ‖.‖ on ⨂[𝕜] i, Eᵢ satisfying ‖⨂ₜ[𝕜] i, m i‖ ≤ Π i, ‖m i‖ for every m in Π i, Eᵢ is bounded above by the projective seminorm.

Main definitions #

Main results #

TODO #

def PiTensorProduct.projectiveSeminormAux {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ιType uE} [(i : ι) → SeminormedAddCommGroup (E i)] :
FreeAddMonoid (𝕜 × ((i : ι) → E i))

A lift of the projective seminorm to FreeAddMonoid (𝕜 × Π i, Eᵢ), useful to prove the properties of projectiveSeminorm.

Equations
  • PiTensorProduct.projectiveSeminormAux = List.sum List.map fun (p : 𝕜 × ((i : ι) → E i)) => p.1 * i : ι, p.2 i
Instances For
    theorem PiTensorProduct.projectiveSeminormAux_nonneg {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ιType uE} [(i : ι) → SeminormedAddCommGroup (E i)] (p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) :
    theorem PiTensorProduct.projectiveSeminormAux_add_le {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ιType uE} [(i : ι) → SeminormedAddCommGroup (E i)] (p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) (q : FreeAddMonoid (𝕜 × ((i : ι) → E i))) :
    theorem PiTensorProduct.projectiveSeminormAux_smul {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ιType uE} [(i : ι) → SeminormedAddCommGroup (E i)] (p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) (a : 𝕜) :
    PiTensorProduct.projectiveSeminormAux (List.map (fun (y : 𝕜 × ((i : ι) → E i)) => (a * y.1, y.2)) p) = a * PiTensorProduct.projectiveSeminormAux p
    theorem PiTensorProduct.bddBelow_projectiveSemiNormAux {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ιType uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) :
    noncomputable def PiTensorProduct.projectiveSeminorm {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ιType uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] :
    Seminorm 𝕜 (PiTensorProduct 𝕜 fun (i : ι) => E i)

    The projective seminorm on ⨂[𝕜] i, Eᵢ. It sends an element x of ⨂[𝕜] i, Eᵢ to the infimum over all expressions of x as ∑ j, ⨂ₜ[𝕜] mⱼ i (with the mⱼΠ i, Eᵢ) of ∑ j, Π i, ‖mⱼ i‖.

    Equations
    Instances For
      theorem PiTensorProduct.projectiveSeminorm_apply {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ιType uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) :
      PiTensorProduct.projectiveSeminorm x = ⨅ (p : x.lifts), PiTensorProduct.projectiveSeminormAux p
      theorem PiTensorProduct.projectiveSeminorm_tprod_le {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ιType uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (m : (i : ι) → E i) :
      PiTensorProduct.projectiveSeminorm (⨂ₜ[𝕜] (i : ι), m i) i : ι, m i
      theorem PiTensorProduct.norm_eval_le_projectiveSeminorm {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ιType uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) (G : Type u_1) [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :
      (PiTensorProduct.lift f.toMultilinearMap) x PiTensorProduct.projectiveSeminorm x * f