Nuclear Tensor Product via Köthe Sequence Spaces

Defines RapidDecaySeq, the Köthe sequence space s(ℕ) of rapidly decreasing sequences, and proves it is a nuclear Fréchet space. Then defines NuclearTensorProduct E₁ E₂ as RapidDecaySeq (via Cantor pairing), providing a DyninMityaginSpace instance for tensor products of nuclear spaces.

Main definitions

• RapidDecaySeq — rapidly decreasing sequences on ℕ
• rapidDecaySeminorm k — the k-th seminorm: ∑ₘ |aₘ| (1+m)^k
• NuclearTensorProduct E₁ E₂ — tensor product of nuclear spaces

Mathematical background

Every nuclear Fréchet space with a Schauder basis is isomorphic to a Köthe sequence space s(ℕ) with rapidly decreasing weights (Dynin-Mityagin). The tensor product s(ℕ) ⊗̂ s(ℕ) ≅ s(ℕ²) ≅ s(ℕ) via Cantor pairing.

References

• Dynin, Mityagin, "Criterion for nuclearity in terms of approximative dimension"
• Gel'fand-Vilenkin, "Generalized Functions" Vol. 4

Rapidly Decreasing Sequences

structure GaussianField.RapidDecaySeq : Type

A rapidly decreasing sequence: val : ℕ → ℝ such that ∑ₘ |val m| · (1 + m)^k converges for all k : ℕ.

• val : ℕ → ℝ

  The underlying sequence.

• rapid_decay (k : ℕ) : Summable fun (m : ℕ) => |self.val m| * (1 + ↑m) ^ k

theorem GaussianField.RapidDecaySeq.ext {a b : RapidDecaySeq} (h : ∀ (m : ℕ), a.val m = b.val m) : a = b

theorem GaussianField.RapidDecaySeq.ext_iff {a b : RapidDecaySeq} : a = b ↔ ∀ (m : ℕ), a.val m = b.val m

Weight function lemmas

theorem GaussianField.RapidDecaySeq.weight_pos (m k : ℕ) : 0 < (1 + ↑m) ^ k

theorem GaussianField.RapidDecaySeq.weight_nonneg (m k : ℕ) : 0 ≤ (1 + ↑m) ^ k

Algebraic structure

@[implicit_reducible]

instance GaussianField.RapidDecaySeq.instZero : Zero RapidDecaySeq

Equations

• GaussianField.RapidDecaySeq.instZero = { zero := { val := 0, rapid_decay := GaussianField.RapidDecaySeq.instZero._proof_1 } }

@[simp]

theorem GaussianField.RapidDecaySeq.zero_val (m : ℕ) : val 0 m = 0

@[implicit_reducible]

instance GaussianField.RapidDecaySeq.instAdd : Add RapidDecaySeq

Equations

• GaussianField.RapidDecaySeq.instAdd = { add := fun (a b : GaussianField.RapidDecaySeq) => { val := a.val + b.val, rapid_decay := ⋯ } }

@[simp]

theorem GaussianField.RapidDecaySeq.add_val (a b : RapidDecaySeq) (m : ℕ) : (a + b).val m = a.val m + b.val m

@[implicit_reducible]

instance GaussianField.RapidDecaySeq.instNeg : Neg RapidDecaySeq

Equations

• GaussianField.RapidDecaySeq.instNeg = { neg := fun (a : GaussianField.RapidDecaySeq) => { val := fun (m : ℕ) => -a.val m, rapid_decay := ⋯ } }

@[simp]

theorem GaussianField.RapidDecaySeq.neg_val (a : RapidDecaySeq) (m : ℕ) : (-a).val m = -a.val m

@[implicit_reducible]

instance GaussianField.RapidDecaySeq.instSMul : SMul ℝ RapidDecaySeq

Equations

• GaussianField.RapidDecaySeq.instSMul = { smul := fun (r : ℝ) (a : GaussianField.RapidDecaySeq) => { val := fun (m : ℕ) => r * a.val m, rapid_decay := ⋯ } }

@[simp]

theorem GaussianField.RapidDecaySeq.smul_val (r : ℝ) (a : RapidDecaySeq) (m : ℕ) : (r • a).val m = r * a.val m

@[implicit_reducible]

instance GaussianField.RapidDecaySeq.instAddCommGroup : AddCommGroup RapidDecaySeq

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GaussianField.RapidDecaySeq.instModule : Module ℝ RapidDecaySeq

Equations

• One or more equations did not get rendered due to their size.

Seminorm family

noncomputable def GaussianField.RapidDecaySeq.rapidDecaySeminorm (k : ℕ) : Seminorm ℝ RapidDecaySeq

The k-th seminorm on rapid decay sequences: ∑ₘ |aₘ| · (1+m)^k.

Equations

• One or more equations did not get rendered due to their size.

Topology from seminorms

@[implicit_reducible]

noncomputable instance GaussianField.RapidDecaySeq.instTopologicalSpace : TopologicalSpace RapidDecaySeq

Equations

• GaussianField.RapidDecaySeq.instTopologicalSpace = (SeminormFamily.moduleFilterBasis GaussianField.RapidDecaySeq.rapidDecaySeminorm).topology

theorem GaussianField.RapidDecaySeq.rapidDecay_withSeminorms : WithSeminorms rapidDecaySeminorm

instance GaussianField.RapidDecaySeq.instIsTopologicalAddGroup : IsTopologicalAddGroup RapidDecaySeq

instance GaussianField.RapidDecaySeq.instContinuousSMul : ContinuousSMul ℝ RapidDecaySeq

instance GaussianField.RapidDecaySeq.instCompleteSpace : CompleteSpace RapidDecaySeq

Standard basis and coefficients

def GaussianField.RapidDecaySeq.basisVec (m : ℕ) : RapidDecaySeq

The m-th standard basis vector: 1 at position m, 0 elsewhere.

Equations

• GaussianField.RapidDecaySeq.basisVec m = { val := fun (n : ℕ) => if n = m then 1 else 0, rapid_decay := ⋯ }

@[simp]

theorem GaussianField.RapidDecaySeq.basisVec_val_self (m : ℕ) : (basisVec m).val m = 1

@[simp]

theorem GaussianField.RapidDecaySeq.basisVec_val_ne {m n : ℕ} (h : n ≠ m) : (basisVec m).val n = 0

theorem GaussianField.RapidDecaySeq.rapidDecaySeminorm_basisVec (k m : ℕ) : (rapidDecaySeminorm k) (basisVec m) = (1 + ↑m) ^ k

Seminorm of a basis vector is exactly (1 + m)^k.

def GaussianField.RapidDecaySeq.coeffLM (m : ℕ) : RapidDecaySeq →ₗ[ℝ] ℝ

The m-th coefficient linear map: extracts coordinate m.

Equations

• GaussianField.RapidDecaySeq.coeffLM m = { toFun := fun (a : GaussianField.RapidDecaySeq) => a.val m, map_add' := ⋯, map_smul' := ⋯ }

def GaussianField.RapidDecaySeq.coeffCLM (m : ℕ) : RapidDecaySeq →L[ℝ] ℝ

The m-th coefficient as a continuous linear map.

Continuity follows from |a.val m| ≤ rapidDecaySeminorm 0 a: the coordinate projection is bounded by the 0-th seminorm.

Equations

• GaussianField.RapidDecaySeq.coeffCLM m = { toLinearMap := GaussianField.RapidDecaySeq.coeffLM m, cont := ⋯ }

DyninMityaginSpace instance

theorem GaussianField.RapidDecaySeq.hasSum_basisVec (a : RapidDecaySeq) : HasSum (fun (m : ℕ) => a.val m • basisVec m) a

theorem GaussianField.RapidDecaySeq.rapidDecay_expansion (φ : RapidDecaySeq →L[ℝ] ℝ) (a : RapidDecaySeq) : φ a = ∑' (m : ℕ), a.val m * φ (basisVec m)

instance GaussianField.RapidDecaySeq.rapidDecayT1Space : T1Space RapidDecaySeq

RapidDecaySeq is T1: if a ≠ 0, the 0-th seminorm ∑ |a_m| > 0.

@[implicit_reducible]

noncomputable instance GaussianField.RapidDecaySeq.rapidDecayDyninMityaginSpace : DyninMityaginSpace RapidDecaySeq

Equations

• One or more equations did not get rendered due to their size.

instance GaussianField.RapidDecaySeq.rapidDecayHasBiorthogonalBasis : DyninMityaginSpace.HasBiorthogonalBasis RapidDecaySeq

Helper lemmas for seminorm transfer

theorem GaussianField.RapidDecaySeq.rapidDecaySeminorm_mono {j j' : ℕ} (hjj : j ≤ j') : rapidDecaySeminorm j ≤ rapidDecaySeminorm j'

Monotonicity of rapid-decay seminorms: for j ≤ j', seminorm j ≤ seminorm j'.

theorem GaussianField.RapidDecaySeq.finset_sup_rapidDecaySeminorm_le (s : Finset ℕ) : s.sup rapidDecaySeminorm ≤ rapidDecaySeminorm (s.sup id)

The sup of rapid-decay seminorms over a finset is bounded by the seminorm at the max index.

theorem GaussianField.RapidDecaySeq.finset_sup_rapidDecaySeminorm_basisVec_le (s : Finset ℕ) (m : ℕ) : (s.sup rapidDecaySeminorm) (basisVec m) ≤ (1 + ↑m) ^ s.sup id

The sup of rapid-decay seminorms evaluated at a basis vector gives polynomial growth.

Transfer constructor for DyninMityaginSpace

@[reducible]

noncomputable def GaussianField.DyninMityaginSpace.ofRapidDecayEquiv {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {ι : Type} [Countable ι] (p : ι → Seminorm ℝ E) (hp : WithSeminorms p) (equiv : E ≃L[ℝ] RapidDecaySeq) : DyninMityaginSpace E

Transfer a DyninMityaginSpace structure from RapidDecaySeq to any space that is continuously linearly equivalent to it. Given seminorms p with WithSeminorms p and a CLE equiv : E ≃L[ℝ] RapidDecaySeq, constructs the DyninMityaginSpace instance using basis m := equiv.symm (basisVec m) and coeff m := coeffCLM m ∘ equiv. Countability of ι and completeness of E (transferred from RapidDecaySeq via the CLE) are propagated automatically.

Equations

• One or more equations did not get rendered due to their size.

theorem GaussianField.DyninMityaginSpace.ofRapidDecayEquiv_hasBiorthogonalBasis {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {ι : Type} [Countable ι] (p : ι → Seminorm ℝ E) (hp : WithSeminorms p) (equiv : E ≃L[ℝ] RapidDecaySeq) : HasBiorthogonalBasis E

ofRapidDecayEquiv always produces a biorthogonal DM space.

Cantor Pairing Bound

theorem GaussianField.nat_pair_bound (n m : ℕ) : Nat.pair n m ≤ (n + m + 1) ^ 2

The Cantor pairing function is bounded by a quadratic.

theorem GaussianField.nat_unpair_le (p : ℕ) : (Nat.unpair p).1 ≤ p ∧ (Nat.unpair p).2 ≤ p

Converse bound: each component of Nat.unpair is bounded by the pair index.

Nuclear Tensor Product

def GaussianField.NuclearTensorProduct (_E₁ : Type u_1) (_E₂ : Type u_2) : Type

The nuclear tensor product of two nuclear spaces, realized as the Köthe sequence space of rapidly decreasing sequences. The product basis indices ℕ × ℕ are encoded into ℕ via Nat.pair.

Mathematically, if E₁ ≅ s(ℕ) and E₂ ≅ s(ℕ) as nuclear Fréchet spaces, then E₁ ⊗̂ E₂ ≅ s(ℕ × ℕ) ≅ s(ℕ) via the Cantor pairing.

Equations

• GaussianField.NuclearTensorProduct _E₁ _E₂ = GaussianField.RapidDecaySeq

theorem GaussianField.NuclearTensorProduct.ext {E₁ : Type u_1} {E₂ : Type u_2} {a b : NuclearTensorProduct E₁ E₂} (h : ∀ (m : ℕ), a.val m = b.val m) : a = b

theorem GaussianField.NuclearTensorProduct.ext_iff {E₁ : Type u_1} {E₂ : Type u_2} {a b : NuclearTensorProduct E₁ E₂} : a = b ↔ ∀ (m : ℕ), a.val m = b.val m

@[implicit_reducible]

instance GaussianField.NuclearTensorProduct.instAddCommGroup {E₁ : Type u_1} {E₂ : Type u_2} : AddCommGroup (NuclearTensorProduct E₁ E₂)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GaussianField.NuclearTensorProduct.instModuleReal {E₁ : Type u_1} {E₂ : Type u_2} : Module ℝ (NuclearTensorProduct E₁ E₂)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GaussianField.NuclearTensorProduct.add_val {E₁ : Type u_1} {E₂ : Type u_2} (a b : NuclearTensorProduct E₁ E₂) (m : ℕ) : (a + b).val m = a.val m + b.val m

@[simp]

theorem GaussianField.NuclearTensorProduct.smul_val {E₁ : Type u_1} {E₂ : Type u_2} (r : ℝ) (a : NuclearTensorProduct E₁ E₂) (m : ℕ) : (r • a).val m = r * a.val m

@[implicit_reducible]

instance GaussianField.NuclearTensorProduct.instTopologicalSpace {E₁ : Type u_1} {E₂ : Type u_2} : TopologicalSpace (NuclearTensorProduct E₁ E₂)

Equations

• GaussianField.NuclearTensorProduct.instTopologicalSpace = { IsOpen := GaussianField.NuclearTensorProduct.instTopologicalSpace._aux_1, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

instance GaussianField.NuclearTensorProduct.instIsTopologicalAddGroup {E₁ : Type u_1} {E₂ : Type u_2} : IsTopologicalAddGroup (NuclearTensorProduct E₁ E₂)

instance GaussianField.NuclearTensorProduct.instContinuousSMulReal {E₁ : Type u_1} {E₂ : Type u_2} : ContinuousSMul ℝ (NuclearTensorProduct E₁ E₂)

@[implicit_reducible]

noncomputable instance GaussianField.NuclearTensorProduct.dyninMityaginSpace {E₁ : Type u_1} {E₂ : Type u_2} : DyninMityaginSpace (NuclearTensorProduct E₁ E₂)

The nuclear tensor product is a nuclear space.

Equations

• GaussianField.NuclearTensorProduct.dyninMityaginSpace = GaussianField.RapidDecaySeq.rapidDecayDyninMityaginSpace

def GaussianField.NuclearTensorProduct.fromPairIndex (n m : ℕ) : ℕ

Map from product basis indices to the Cantor-paired linear index.

Equations

• GaussianField.NuclearTensorProduct.fromPairIndex n m = Nat.pair n m

def GaussianField.NuclearTensorProduct.toPairIndex (p : ℕ) : ℕ × ℕ

Recover product basis indices from a linear index.

Equations

• GaussianField.NuclearTensorProduct.toPairIndex p = Nat.unpair p

theorem GaussianField.NuclearTensorProduct.toPairIndex_fromPairIndex (n m : ℕ) : toPairIndex (fromPairIndex n m) = (n, m)

theorem GaussianField.NuclearTensorProduct.fromPairIndex_toPairIndex (p : ℕ) : fromPairIndex (toPairIndex p).1 (toPairIndex p).2 = p

Pure tensor embedding

theorem GaussianField.NuclearTensorProduct.summable_inv_one_add_sq : Summable fun (n : ℕ) => ((1 + ↑n) ^ 2)⁻¹

∑_n 1/(1+n)^2 converges, as a shifted version of ∑ 1/n^2.

noncomputable def GaussianField.NuclearTensorProduct.pure {E₁ : Type u_1} {E₂ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] (e₁ : E₁) (e₂ : E₂) : NuclearTensorProduct E₁ E₂

The pure tensor map: given e₁ : E₁ and e₂ : E₂ with DM structure, produces the sequence m ↦ coeff(unpair(m).1, e₁) * coeff(unpair(m).2, e₂).

This is the bilinear embedding E₁ × E₂ → E₁ ⊗̂ E₂ realized at the level of Köthe sequence spaces.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GaussianField.NuclearTensorProduct.pure_val {E₁ : Type u_1} {E₂ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] (e₁ : E₁) (e₂ : E₂) (m : ℕ) : (pure e₁ e₂).val m = (DyninMityaginSpace.coeff (Nat.unpair m).1) e₁ * (DyninMityaginSpace.coeff (Nat.unpair m).2) e₂

theorem GaussianField.NuclearTensorProduct.pure_seminorm_bound {E₁ : Type u_1} {E₂ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] (k : ℕ) : ∃ (C : NNReal) (s₁ : Finset (DyninMityaginSpace.ι E₁)) (s₂ : Finset (DyninMityaginSpace.ι E₂)), ∀ (e₁ : E₁) (e₂ : E₂), (RapidDecaySeq.rapidDecaySeminorm k) (pure e₁ e₂) ≤ ↑C * (s₁.sup DyninMityaginSpace.p) e₁ * (s₂.sup DyninMityaginSpace.p) e₂

Seminorm bound for the pure tensor: for each target seminorm index k, there exist constants C, source seminorm index sets s₁, s₂ such that rapidDecaySeminorm k (pure e₁ e₂) ≤ C * (s₁.sup p) e₁ * (s₂.sup p) e₂.

noncomputable def GaussianField.NuclearTensorProduct.pureLin {E₁ : Type u_1} {E₂ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] : E₁ →ₗ[ℝ] E₂ →ₗ[ℝ] NuclearTensorProduct E₁ E₂

The pure tensor map as a bilinear map.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GaussianField.NuclearTensorProduct.pureCLMRight {E₁ : Type u_1} {E₂ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] (e₁ : E₁) : E₂ →L[ℝ] NuclearTensorProduct E₁ E₂

For fixed e₁, the map e₂ ↦ pure e₁ e₂ is a continuous linear map. Continuity follows from the seminorm bound via continuous_of_isBounded.

Equations

• GaussianField.NuclearTensorProduct.pureCLMRight e₁ = { toLinearMap := GaussianField.NuclearTensorProduct.pureLin e₁, cont := ⋯ }

theorem GaussianField.NuclearTensorProduct.pure_continuous_left {E₁ : Type u_1} {E₂ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] (e₂ : E₂) : Continuous fun (e₁ : E₁) => pure e₁ e₂

For fixed e₂, the map e₁ ↦ pure e₁ e₂ is continuous.

theorem GaussianField.NuclearTensorProduct.pure_continuous {E₁ : Type u_1} {E₂ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] : Continuous fun (p : E₁ × E₂) => pure p.1 p.2

The pure tensor map is jointly continuous on E₁ × E₂.

Universal Property: Lift

noncomputable def GaussianField.NuclearTensorProduct.lift {E₁ : Type u_1} {E₂ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] (B : E₁ →ₗ[ℝ] E₂ →ₗ[ℝ] G) {C : ℝ} {s₁ : Finset (DyninMityaginSpace.ι E₁)} {s₂ : Finset (DyninMityaginSpace.ι E₂)} (hC : 0 < C) (hB : ∀ (e₁ : E₁) (e₂ : E₂), ‖(B e₁) e₂‖ ≤ C * (s₁.sup DyninMityaginSpace.p) e₁ * (s₂.sup DyninMityaginSpace.p) e₂) : NuclearTensorProduct E₁ E₂ →L[ℝ] G

Universal property of the nuclear tensor product.

Every continuous bilinear map B : E₁ × E₂ → G (into a complete normed space) factors through pure via a CLM lift B : NuclearTensorProduct E₁ E₂ →L[ℝ] G.

The definition is lift B a = ∑' m, aₘ • B(ψ₁ᵢ, ψ₂ⱼ) where (i,j) = unpair(m). Linearity follows from tsum linearity; continuity from a seminorm bound.

Equations

• GaussianField.NuclearTensorProduct.lift B hC hB = { toLinearMap := GaussianField.NuclearTensorProduct.liftLM✝ B hC hB, cont := ⋯ }

theorem GaussianField.NuclearTensorProduct.lift_pure {E₁ : Type u_1} {E₂ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] (B : E₁ →ₗ[ℝ] E₂ →ₗ[ℝ] G) {C : ℝ} {s₁ : Finset (DyninMityaginSpace.ι E₁)} {s₂ : Finset (DyninMityaginSpace.ι E₂)} (hC : 0 < C) (hB : ∀ (e₁ : E₁) (e₂ : E₂), ‖(B e₁) e₂‖ ≤ C * (s₁.sup DyninMityaginSpace.p) e₁ * (s₂.sup DyninMityaginSpace.p) e₂) (e₁ : E₁) (e₂ : E₂) : (lift B hC hB) (pure e₁ e₂) = (B e₁) e₂

The lift factors through pure: lift B (pure e₁ e₂) = B e₁ e₂.

The proof uses the double Schauder expansion: hasSum_basis gives convergent expansions e₁ = ∑ c₁_n • ψ₁_n and e₂ = ∑ c₂_j • ψ₂_j, then applies B (continuous from the bound) and rearranges via Cantor pairing.

Bilinear evaluation: tensor product of functionals

noncomputable def GaussianField.NuclearTensorProduct.evalCLM {E₁ : Type u_1} {E₂ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₁] [DyninMityaginSpace E₂] (φ₁ : E₁ →L[ℝ] ℝ) (φ₂ : E₂ →L[ℝ] ℝ) : NuclearTensorProduct E₁ E₂ →L[ℝ] ℝ

Tensor product of continuous linear functionals.

Given φ₁ ∈ E₁' and φ₂ ∈ E₂', the tensor product functional φ₁ ⊗ φ₂ : E₁ ⊗̂ E₂ → ℝ is defined via the universal property lift applied to the bilinear form (e₁, e₂) ↦ φ₁(e₁) · φ₂(e₂).

On pure tensors: evalCLM φ₁ φ₂ (pure e₁ e₂) = φ₁ e₁ * φ₂ e₂.

The bilinear bound ‖φ₁(e₁) · φ₂(e₂)‖ ≤ C · p₁(e₁) · p₂(e₂) follows from Seminorm.bound_of_continuous applied to each functional.

Equations

• One or more equations did not get rendered due to their size.

theorem GaussianField.NuclearTensorProduct.evalCLM_pure {E₁ : Type u_3} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [DyninMityaginSpace E₁] {E₂ : Type u_4} [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₂] (φ₁ : E₁ →L[ℝ] ℝ) (φ₂ : E₂ →L[ℝ] ℝ) (e₁ : E₁) (e₂ : E₂) : (evalCLM φ₁ φ₂) (pure e₁ e₂) = φ₁ e₁ * φ₂ e₂

evalCLM on pure tensors gives the product of evaluations.

theorem GaussianField.NuclearTensorProduct.basisVec_eq_pure {E₁ : Type u_3} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [DyninMityaginSpace E₁] {E₂ : Type u_4} [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [DyninMityaginSpace E₂] (hbasis₁ : ∀ (n m : ℕ), (DyninMityaginSpace.coeff n) (DyninMityaginSpace.basis m) = if n = m then 1 else 0) (hbasis₂ : ∀ (n m : ℕ), (DyninMityaginSpace.coeff n) (DyninMityaginSpace.basis m) = if n = m then 1 else 0) (m : ℕ) : RapidDecaySeq.basisVec m = pure (DyninMityaginSpace.basis (Nat.unpair m).1) (DyninMityaginSpace.basis (Nat.unpair m).2)

Under biorthogonality, basis vectors equal pure tensors of basis elements. basisVec m = pure (basis a) (basis b) where (a,b) = unpair(m).