`BookProof.CarlemanUnboundedHop.geoHop_herm` (b : ℕ → ℝ) (rho : ℝ) : IsHermitianKernel (geoHop b rho)

-- Generated from ChapterCarlemanUnboundedHop.lean — theorem BookProof.CarlemanUnboundedHop.geoHop_herm
import Mathlib
import Definitions.Def_ChapterCarlemanUnboundedHop
open BookProof.CarlemanUnboundedHop



open Finset

noncomputable section

variable {a : ℕ → ℕ → ℂ} {u : ℕ → ℂ} {A θ Θ : ℕ → ℝ}

theorem BookProof.CarlemanUnboundedHop.geoHop_herm (b : ℕ → ℝ) (rho : ℝ) : IsHermitianKernel (geoHop b rho) := by sorry