IndisputableMonolith.YM.Kernel

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace YM
   5
   6noncomputable section
   7open Classical Complex
   8
   9structure TransferKernel (ι : Type) where
  10  T : (ι → ℂ) →L[ℂ] (ι → ℂ)
  11
  12structure MatrixView (ι : Type) [Fintype ι] [DecidableEq ι] where
  13  A : Matrix ι ι ℂ
  14
  15noncomputable def CLM.ofLM {ι : Type}
  16  (L : (ι → ℂ) →ₗ[ℂ] (ι → ℂ)) : (ι → ℂ) →L[ℂ] (ι → ℂ) :=
  17{ toLinearMap := L, cont := by exact ContinuousLinearMap.continuous _ }
  18
  19structure MatrixBridge (ι : Type) [Fintype ι] [DecidableEq ι]
  20  (K : TransferKernel ι) (V : MatrixView ι) where
  21  intertwine : K.T = CLM.ofLM (Matrix.toLin' V.A)
  22
  23def KernelHasMatrixView (ι : Type) [Fintype ι] [DecidableEq ι]
  24  (K : TransferKernel ι) (V : MatrixView ι) : Prop :=
  25  Nonempty (MatrixBridge ι K V)
  26
  27noncomputable def buildKernelFromMatrix (ι : Type) [Fintype ι] [DecidableEq ι]
  28  (V : MatrixView ι) : Σ K : TransferKernel ι, MatrixBridge ι K V :=
  29by
  30  let K : TransferKernel ι := { T := CLM.ofLM (Matrix.toLin' V.A) }
  31  exact ⟨K, { intertwine := rfl }⟩
  32
  33noncomputable def constantStochastic3x3 : MatrixView (Fin 3) :=
  34{ A := fun _ _ => ((1/3 : ℝ) : ℂ) }
  35
  36noncomputable def kernel3x3_with_bridge :
  37  Σ K : TransferKernel (Fin 3), MatrixBridge (Fin 3) K constantStochastic3x3 :=
  38  buildKernelFromMatrix (ι := Fin 3) constantStochastic3x3
  39
  40end
  41end YM
  42end IndisputableMonolith
  43