Sazonov Topology

The Sazonov topology on a real Hilbert space H is the locally convex topology generated by seminorms x ↦ √⟪x, Sx⟫ where S ranges over positive trace-class operators on H.

A function φ : H → ℂ is continuous in the Sazonov topology iff for every ε > 0 there exists a positive trace-class operator S such that |φ(x) - φ(y)| < ε whenever √⟪x-y, S(x-y)⟫ < 1.

Main definitions

• IsPositiveTraceClass — positive operator with finite trace
• quadForm S x — the quadratic form ⟪x, Sx⟫
• sazonovSeminorm S hS — the seminorm x ↦ √⟪x, Sx⟫
• sazonovTopology H — the Sazonov topology on H

Main results

• inner_sq_le_quadForm_mul — Cauchy-Schwarz for ⟪·, S·⟫
• sqrt_quadForm_add_le — triangle inequality for √⟪·, S·⟫

References

• Sazonov, "A remark on characteristic functionals" (1958)
• Da Prato-Zabczyk, "Stochastic Equations in Infinite Dimensions", §1.2

Positive Trace-Class Operators

def IsPositiveTraceClass {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S : H →L[ℝ] H) : Prop

A positive operator S is trace-class if ∑ᵢ ⟪eᵢ, S eᵢ⟫ converges for some Hilbert basis {eᵢ}. For positive operators, this is basis-independent.

Equations

• IsPositiveTraceClass S = (S.IsPositive ∧ ∃ (ι : Type) (b : HilbertBasis ι ℝ H), Summable fun (i : ι) => inner ℝ (b i) (S (b i)))

Quadratic Form and Seminorm

def quadForm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S : H →L[ℝ] H) (x : H) : ℝ

The quadratic form associated to an operator: x ↦ ⟪x, Sx⟫.

Equations

• quadForm S x = inner ℝ x (S x)

theorem quadForm_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {S : H →L[ℝ] H} (hS : S.IsPositive) (x : H) : 0 ≤ quadForm S x

theorem inner_S_smul_right {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {S : H →L[ℝ] H} (t : ℝ) (x y : H) : inner ℝ x (S (t • y)) = t * inner ℝ x (S y)

theorem quadForm_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {S : H →L[ℝ] H} (t : ℝ) (x : H) : quadForm S (t • x) = t ^ 2 * quadForm S x

theorem quadForm_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {S : H →L[ℝ] H} (hS : S.IsPositive) (x y : H) : quadForm S (x + y) = quadForm S x + 2 * inner ℝ x (S y) + quadForm S y

theorem inner_sq_le_quadForm_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {S : H →L[ℝ] H} (hS : S.IsPositive) (x y : H) : inner ℝ x (S y) ^ 2 ≤ quadForm S x * quadForm S y

Cauchy-Schwarz inequality for the semi-inner product ⟪·, S·⟫: ⟪x, Sy⟫² ≤ ⟪x, Sx⟫ · ⟪y, Sy⟫ when S is positive.

Proof: the quadratic t ↦ ⟪x + ty, S(x + ty)⟫ is nonneg for all t, so its discriminant is nonpositive.

theorem sqrt_quadForm_add_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {S : H →L[ℝ] H} (hS : S.IsPositive) (x y : H) : √(quadForm S (x + y)) ≤ √(quadForm S x) + √(quadForm S y)

Triangle inequality for the Sazonov seminorm: √⟪x+y, S(x+y)⟫ ≤ √⟪x, Sx⟫ + √⟪y, Sy⟫.

noncomputable def sazonovSeminorm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S : H →L[ℝ] H) (hS : S.IsPositive) : Seminorm ℝ H

The Sazonov seminorm for a positive operator S: x ↦ √⟪x, Sx⟫.

Equations

• sazonovSeminorm S hS = { toFun := fun (x : H) => √(quadForm S x), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, smul' := ⋯ }

Sazonov Topology

structure SazonovIndex (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] : Type u

The index type for the Sazonov seminorm family: positive trace-class operators.

• op : H →L[ℝ] H

  The positive trace-class operator defining this seminorm.

• pos : self.op.IsPositive
• traceClass : IsPositiveTraceClass self.op

noncomputable def sazonovFamily (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] : SeminormFamily ℝ H (SazonovIndex H)

The Sazonov seminorm family, indexed by positive trace-class operators.

Equations

• sazonovFamily H S = sazonovSeminorm S.op ⋯

@[reducible]

noncomputable def sazonovTopology (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] : TopologicalSpace H

The Sazonov topology on a real Hilbert space, generated by the seminorms x ↦ √⟪x, Sx⟫ as S ranges over positive trace-class operators.

Equations

• sazonovTopology H = (sazonovFamily H).moduleFilterBasis.topology