/-
Copyright (c) 2026 Michael R. Douglas. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

# 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
-/

import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Adjoint
import Mathlib.Analysis.InnerProductSpace.Positive
import Mathlib.Analysis.InnerProductSpace.l2Space
import Mathlib.Analysis.LocallyConvex.WithSeminorms
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure

open MeasureTheory Complex Filter Topology Set InnerProductSpace
open scoped Real

noncomputable section

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]

/-! ## Positive Trace-Class Operators -/

/-- A positive operator S is trace-class if ∑ᵢ ⟪eᵢ, S eᵢ⟫ converges for some
    Hilbert basis {eᵢ}. For positive operators, this is basis-independent. -/
def IsPositiveTraceClass (S : H →L[ℝ] H) : Prop :=
  S.IsPositive ∧
  ∃ (ι : Type) (b : HilbertBasis ι ℝ H),
    Summable (fun i => @inner ℝ H _ (b i) (S (b i)))

/-! ## Quadratic Form and Seminorm -/

/-- The quadratic form associated to an operator: x ↦ ⟪x, Sx⟫. -/
def quadForm (S : H →L[ℝ] H) (x : H) : ℝ := @inner ℝ H _ x (S x)

section QuadFormLemmas

variable {S : H →L[ℝ] H}

private lemma star_real (a : ℝ) : (starRingEnd ℝ) a = a := rfl

omit [CompleteSpace H]

lemma quadForm_nonneg (hS : S.IsPositive) (x : H) : 0 ≤ quadForm S x := by
  have := hS.re_inner_nonneg_left x
  simp only [RCLike.re_to_real] at this
  rw [quadForm, real_inner_comm]
  exact this

lemma inner_S_smul_right (t : ℝ) (x y : H) :
    @inner ℝ H _ x (S (t • y)) = t * @inner ℝ H _ x (S y) := by
  rw [ContinuousLinearMap.map_smul, inner_smul_right]

lemma quadForm_smul (t : ℝ) (x : H) :
    quadForm S (t • x) = t ^ 2 * quadForm S x := by
  simp only [quadForm, ContinuousLinearMap.map_smul, inner_smul_left, inner_smul_right, star_real]
  ring

lemma quadForm_add (hS : S.IsPositive) (x y : H) :
    quadForm S (x + y) = quadForm S x + 2 * @inner ℝ H _ x (S y) + quadForm S y := by
  simp only [quadForm, map_add, inner_add_left, inner_add_right]
  have : @inner ℝ H _ y (S x) = @inner ℝ H _ x (S y) := by
    rw [← hS.inner_left_eq_inner_right x y, real_inner_comm]
  linarith

/-- 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. -/
lemma inner_sq_le_quadForm_mul (hS : S.IsPositive) (x y : H) :
    (@inner ℝ H _ x (S y)) ^ 2 ≤ quadForm S x * quadForm S y := by
  by_cases hy : quadForm S y = 0
  · suffices h : @inner ℝ H _ x (S y) = 0 by simp [h, hy]
    by_contra hne
    have h0 : ∀ t : ℝ, 0 ≤ quadForm S x + 2 * @inner ℝ H _ x (S y) * t := by
      intro t
      have := quadForm_nonneg hS (x + t • y)
      rw [quadForm_add hS, inner_S_smul_right, quadForm_smul, hy] at this
      linarith
    have hpos := h0 (-(quadForm S x + 1) / (2 * @inner ℝ H _ x (S y)))
    have hneg := h0 (-(quadForm S x - 1) / (2 * @inner ℝ H _ x (S y)))
    have hne2 : (2 : ℝ) * @inner ℝ H _ x (S y) ≠ 0 := by positivity
    have e1 : 2 * @inner ℝ H _ x (S y) *
        (-(quadForm S x + 1) / (2 * @inner ℝ H _ x (S y))) = -(quadForm S x + 1) := by
      field_simp
    have e2 : 2 * @inner ℝ H _ x (S y) *
        (-(quadForm S x - 1) / (2 * @inner ℝ H _ x (S y))) = -(quadForm S x - 1) := by
      field_simp
    linarith
  · have hcpos : 0 < quadForm S y := lt_of_le_of_ne (quadForm_nonneg hS y) (Ne.symm hy)
    have h0 : ∀ t : ℝ, 0 ≤ quadForm S x + 2 * @inner ℝ H _ x (S y) * t +
        quadForm S y * t ^ 2 := by
      intro t
      have := quadForm_nonneg hS (x + t • y)
      rw [quadForm_add hS, inner_S_smul_right, quadForm_smul] at this
      linarith
    have key := h0 (-@inner ℝ H _ x (S y) / quadForm S y)
    have hc : quadForm S y ≠ 0 := ne_of_gt hcpos
    have : quadForm S x + 2 * @inner ℝ H _ x (S y) *
        (-@inner ℝ H _ x (S y) / quadForm S y) +
        quadForm S y * (-@inner ℝ H _ x (S y) / quadForm S y) ^ 2 =
        quadForm S x - (@inner ℝ H _ x (S y)) ^ 2 / quadForm S y := by
      field_simp; ring
    rw [this] at key
    have h1 : (@inner ℝ H _ x (S y)) ^ 2 / quadForm S y ≤ quadForm S x := by linarith
    calc (@inner ℝ H _ x (S y)) ^ 2
        = (@inner ℝ H _ x (S y)) ^ 2 / quadForm S y * quadForm S y := by
          field_simp
      _ ≤ quadForm S x * quadForm S y :=
          mul_le_mul_of_nonneg_right h1 (le_of_lt hcpos)

/-- Triangle inequality for the Sazonov seminorm:
    √⟪x+y, S(x+y)⟫ ≤ √⟪x, Sx⟫ + √⟪y, Sy⟫. -/
lemma sqrt_quadForm_add_le (hS : S.IsPositive) (x y : H) :
    Real.sqrt (quadForm S (x + y)) ≤
    Real.sqrt (quadForm S x) + Real.sqrt (quadForm S y) := by
  have ha := quadForm_nonneg hS x
  have hc := quadForm_nonneg hS y
  have h_cs := inner_sq_le_quadForm_mul hS x y
  rw [← Real.sqrt_sq (add_nonneg (Real.sqrt_nonneg _) (Real.sqrt_nonneg _))]
  apply Real.sqrt_le_sqrt
  rw [quadForm_add hS]
  have h_bound : @inner ℝ H _ x (S y) ≤
      Real.sqrt (quadForm S x) * Real.sqrt (quadForm S y) := by
    by_cases hb : @inner ℝ H _ x (S y) ≤ 0
    · exact le_trans hb (mul_nonneg (Real.sqrt_nonneg _) (Real.sqrt_nonneg _))
    · push_neg at hb
      rw [← Real.sqrt_mul ha]
      exact Real.le_sqrt_of_sq_le h_cs
  nlinarith [Real.sq_sqrt ha, Real.sq_sqrt hc]

end QuadFormLemmas

/-- The Sazonov seminorm for a positive operator S: x ↦ √⟪x, Sx⟫. -/
def sazonovSeminorm (S : H →L[ℝ] H) (hS : S.IsPositive) : Seminorm ℝ H where
  toFun x := Real.sqrt (quadForm S x)
  map_zero' := by simp [quadForm, map_zero, Real.sqrt_zero]
  add_le' x y := sqrt_quadForm_add_le hS x y
  neg' x := by simp [quadForm, map_neg, inner_neg_left, neg_neg]
  smul' a x := by
    simp only [quadForm, ContinuousLinearMap.map_smul, inner_smul_left, inner_smul_right,
      star_real]
    rw [show a * (a * @inner ℝ H _ x (S x)) = a ^ 2 * @inner ℝ H _ x (S x) by ring]
    rw [Real.sqrt_mul (sq_nonneg a), Real.sqrt_sq_eq_abs]
    simp [Real.norm_eq_abs]

/-! ## Sazonov Topology -/

/-- The index type for the Sazonov seminorm family: positive trace-class operators. -/
structure SazonovIndex (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    [CompleteSpace H] where
  op : H →L[ℝ] H
  pos : op.IsPositive
  traceClass : IsPositiveTraceClass op

/-- The Sazonov seminorm family, indexed by positive trace-class operators. -/
def sazonovFamily (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    [CompleteSpace H] : SeminormFamily ℝ H (SazonovIndex H) :=
  fun S => sazonovSeminorm S.op S.pos

/-- The Sazonov topology on a real Hilbert space, generated by the seminorms
    x ↦ √⟪x, Sx⟫ as S ranges over positive trace-class operators. -/
@[reducible] def sazonovTopology (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    [CompleteSpace H] : TopologicalSpace H :=
  (sazonovFamily H).moduleFilterBasis.topology

end