LatticeMeasure

formal source

   8open Complex
   9
  10/-- Abstract lattice measure (interface-level). -/
  11structure LatticeMeasure where
  12  deriving Inhabited
  13
  14/-- Transfer kernel acting on complex observables. -/
  15structure Kernel where
  16  T : (LatticeMeasure → ℂ) →L[ℂ] (LatticeMeasure → ℂ)
  17
  18noncomputable instance : Inhabited ((LatticeMeasure → ℂ) →L[ℂ] (LatticeMeasure → ℂ)) :=
  19  ⟨ContinuousLinearMap.id ℂ (LatticeMeasure → ℂ)⟩
  20
  21noncomputable instance : Inhabited Kernel :=
  22  ⟨{ T := ContinuousLinearMap.id ℂ (LatticeMeasure → ℂ) }⟩
  23
  24/-- The transfer operator associated with a kernel. -/
  25noncomputable def TransferOperator (K : Kernel) : (LatticeMeasure → ℂ) →L[ℂ] (LatticeMeasure → ℂ) :=
  26  K.T
  27
  28/-- OS reflection positivity surrogate: existence of a transfer kernel with a
  29    uniform overlap lower bound β ∈ (0,1]. This encodes a spectral positivity
  30    guard compatible with Dobrushin-type contraction. -/
  31def OSPositivity (_μ : LatticeMeasure) : Prop := ∃ K : Kernel, ∃ β : ℝ, OverlapLowerBoundOS K β
  32
  33lemma OSPositivity_default (_μ : LatticeMeasure) : OSPositivity _μ := by
  34  refine ⟨default, 1, ?_⟩
  35  dsimp [OverlapLowerBoundOS]
  36  constructor <;> norm_num
  37
  38/-- Overlap lower bound for a kernel (β ∈ (0,1]). -/
  39def OverlapLowerBoundOS (_K : Kernel) (β : ℝ) : Prop := 0 < β ∧ β ≤ 1
  40
  41/-- Perron–Frobenius transfer spectral gap property. -/