Fibrewise essential self-adjointness glues

import Mathlib
import Definitions.Def_ChapterDirectSumEsa
import Definitions.Def_ChapterFarisLavine

namespace BookProof.DirectSumEsa

open BookProof.FarisLavine

noncomputable section

variable {ι : Type*} {G : ι → Type*} [∀ i, NormedAddCommGroup (G i)]
  [∀ i, InnerProductSpace ℂ (G i)] [∀ i, CompleteSpace (G i)]

variable {D : ∀ i, Submodule ℂ (G i)}

@[simp] theorem dsOp_coe (H : ∀ i, D i →ₗ[ℂ] G i) (x : dsCore D) (i : ι) :
    ((dsOp H x : lp G 2) : ∀ i, G i) i = H i ⟨(x : lp G 2) i, x.2.2 i⟩ := rfl

/-! ## The single-fibre states -/

theorem single_mem_dsCore [DecidableEq ι] (i : ι) (u : D i) :
    (lp.single 2 i ((u : G i)) : lp G 2) ∈ dsCore D := by
  classical
  constructor
  · refine Set.Finite.subset (Set.finite_singleton i) (fun j hj => ?_)
    simp only [Set.mem_setOf_eq, lp.single_apply] at hj
    by_contra hne
    exact hj (Pi.single_eq_of_ne (by simpa [eq_comm] using hne) _)
  · intro j
    rw [lp.single_apply]
    by_cases hj : j = i
    · subst hj
      simp only [Pi.single_eq_same]
      exact u.2
    · rw [Pi.single_eq_of_ne (by simpa [eq_comm] using hj)]
      exact Submodule.zero_mem _

/-- The direct sum operator on a single-fibre state is the fibre operator. -/
theorem dsOp_single [DecidableEq ι] (H : ∀ i, D i →ₗ[ℂ] G i) (i : ι) (u : D i) :
    (dsOp H ⟨lp.single 2 i ((u : G i)), single_mem_dsCore i u⟩ : lp G 2)
      = lp.single 2 i (H i u) := by
  classical
  refine lp.ext (funext fun j => ?_)
  rw [lp.single_apply]
  have hcoe : ((dsOp H ⟨lp.single 2 i ((u : G i)), single_mem_dsCore i u⟩ : lp G 2)
      : ∀ i, G i) j
      = H j ⟨(lp.single 2 i ((u : G i)) : lp G 2) j, (single_mem_dsCore i u).2 j⟩ := rfl
  rw [hcoe]
  by_cases hj : j = i
  · subst hj
    have hu : (⟨(lp.single 2 j ((u : G j)) : lp G 2) j, (single_mem_dsCore j u).2 j⟩ : D j)
        = u := Subtype.ext (by
          change (lp.single 2 j ((u : G j)) : lp G 2) j = (u : G j)
          rw [lp.single_apply, Pi.single_eq_same])
    rw [Pi.single_eq_same]
    exact congrArg (H j) hu
  · have hzero : (⟨(lp.single 2 i ((u : G i)) : lp G 2) j, (single_mem_dsCore i u).2 j⟩ : D j)
        = 0 := Subtype.ext (by
          change (lp.single 2 i ((u : G i)) : lp G 2) j = (0 : G j)
          rw [lp.single_apply, Pi.single_eq_of_ne hj])
    rw [Pi.single_eq_of_ne hj]
    exact (congrArg (H j) hzero).trans (map_zero (H j))

/-! ## Symmetry and the deficiency spaces -/

theorem dsOp_symmetricOn (H : ∀ i, D i →ₗ[ℂ] G i) (hsym : ∀ i, SymmetricOn (D i) (H i)) :
    SymmetricOn (dsCore D) (dsOp H) := by
  intro x y
  rw [lp.inner_eq_tsum, lp.inner_eq_tsum]
  refine tsum_congr fun i => ?_
  exact hsym i ⟨(x : lp G 2) i, x.2.2 i⟩ ⟨(y : lp G 2) i, y.2.2 i⟩

/-- **Fibrewise triviality of a deficiency space glues.** -/
theorem dsOp_deficiencyTrivialAt (H : ∀ i, D i →ₗ[ℂ] G i) {z : ℂ}
    (h : ∀ i, DeficiencyTrivialAt (D i) (H i) z) :
    DeficiencyTrivialAt (dsCore D) (dsOp H) z := by
  classical
  intro w hw
  have hcoord : ∀ i, ((w : lp G 2) : ∀ i, G i) i = 0 := by
    intro i
    refine h i _ (fun u => ?_)
    have hv := hw ⟨lp.single 2 i ((u : G i)), single_mem_dsCore i u⟩
    rw [dsOp_single H i u] at hv
    rw [lp.inner_single_left, lp.inner_single_left] at hv
    exact hv
  refine lp.ext (funext fun i => ?_)
  rw [hcoord i]
  simp

/-- **Fibrewise essential self-adjointness glues.** -/
theorem dsOp_essentiallySelfAdjointOn (H : ∀ i, D i →ₗ[ℂ] G i)
    (h : ∀ i, EssentiallySelfAdjointOn (D i) (H i)) :
    EssentiallySelfAdjointOn (dsCore D) (dsOp H) :=
  ⟨dsOp_deficiencyTrivialAt H (fun i => (h i).1),
    dsOp_deficiencyTrivialAt H (fun i => (h i).2)⟩

end

end BookProof.DirectSumEsa