Definitions bundle OAIW2HM002 of the split of OpenAI, Spontaneous magnetization in the quantum Heisenberg ferromagnet

import Mathlib
import Definitions.Def_Heisenberg
import Definitions.Def_OAIW2HM000
import Definitions.Def_OAIW2HM001

section
-- module Solutions.OAIW2_Heis.Heisenberg_LocalAlgebra
attribute [-instance] _root_.OAI.Heisenberg.quasiLocalClosed
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

noncomputable section
open scoped ComplexConjugate ENNReal Classical

open scoped ComplexConjugate BigOperators
namespace Heisenberg

instance quasiLocalStarMul (d ℓ : ℕ) : StarMul (QuasiLocal d ℓ) :=
  (quasiLocalAlgebra d ℓ).starRing.toStarMul

instance quasiLocalComplete (d ℓ : ℕ) : CompleteSpace (QuasiLocal d ℓ) :=
  (StarSubalgebra.isClosed_topologicalClosure _).completeSpace_coe

instance quasiLocalRationalAlgebra (d ℓ : ℕ) : NormedAlgebra ℚ (QuasiLocal d ℓ) :=
  NormedAlgebra.restrictScalars ℚ ℂ _

end Heisenberg
end

end OAI
end

section
-- module Solutions.OAIW2_Heis.Heisenberg_ExponentialEvolution
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

noncomputable section
open scoped ComplexConjugate ENNReal Classical
open scoped ComplexConjugate BigOperators

namespace Heisenberg

def incidentEdges {d : ℕ} (F : Finset (Site d)) : Finset (Site d × Site d) :=
  F.biUnion fun x => ((neighbors x).image (fun y => (x,y))) ∪
    ((neighbors x).image (fun y => (y,x)))

def neighborhood {d : ℕ} (F : Finset (Site d)) : Finset (Site d) :=
  F ∪ F.biUnion neighbors

end Heisenberg
end

end OAI
end

section
-- module Solutions.OAIW2_Heis.Heisenberg_LocalDynamics
attribute [-instance] _root_.OAI.Heisenberg.quasiLocalClosed
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

noncomputable section
open scoped ComplexConjugate ENNReal Classical
open scoped ComplexConjugate BigOperators

namespace Heisenberg

def localCore (d ℓ : ℕ) : StarSubalgebra ℂ (QuasiLocal d ℓ) :=
  StarAlgebra.adjoin ℂ {A | ∃ x a b, A = localUnit d ℓ x a b}

end Heisenberg

end

end OAI
end

section
-- module Solutions.OAIW2_Heis.Heisenberg_ThermodynamicDynamics
attribute [-instance] _root_.OAI.Heisenberg.quasiLocalClosed
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

noncomputable section
open scoped ComplexConjugate ENNReal Classical
open scoped ComplexConjugate BigOperators

namespace Heisenberg

local instance instIsTopologicalRingContinuousLinearMapComplexIdSubtypeSpinOperatorMemStarSubalgebraQuasiLocal (d ℓ : ℕ) : IsTopologicalRing (QuasiLocal d ℓ →L[ℂ] QuasiLocal d ℓ) :=
  clm_topologicalRing

end Heisenberg

open Filter Topology Metric
open scoped NNReal

open scoped NNReal
end

end OAI
end

section
-- module Solutions.OAIW2_Heis.Heisenberg_StateCompactness
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

noncomputable section
open scoped ComplexConjugate ENNReal Classical
open scoped ComplexConjugate BigOperators
open Filter Topology Metric
open scoped NNReal
open scoped NNReal

namespace Heisenberg

open scoped ComplexOrder

open scoped InnerProductSpace

def sandwichState {d ℓ : ℕ} (ω : State d ℓ) (B : QuasiLocal d ℓ) (hB : IsUnit B) :
    State d ℓ := by
  let : PartialOrder (QuasiLocal d ℓ) := CStarAlgebra.spectralOrder _
  let : StarOrderedRing (QuasiLocal d ℓ) := CStarAlgebra.spectralOrderedRing _
  have hp : ∀ C, 0 ≤ ω.functional (star C * C) :=
    fun C => ⟨(ω.positive C).2, by simpa using (ω.positive C).1.symm⟩
  have hZ := sandwich_one_pos ω.functional ω.normalized hp hB
  let Z := (sandwichFunctional ω.functional B 1).re
  refine ⟨((Z : ℂ)⁻¹) • sandwichFunctional ω.functional B, ?_, ?_⟩
  · change (Z : ℂ)⁻¹ * sandwichFunctional ω.functional B 1 = 1
    have hz : sandwichFunctional ω.functional B 1 = (Z : ℂ) := by
      apply Complex.ext
      · rfl
      · simpa only [sandwichFunctional_apply, mul_one, Complex.ofReal_im] using (ω.positive B).1
    rw [hz]
    exact inv_mul_cancel₀ (Complex.ofReal_ne_zero.mpr (ne_of_gt hZ))
  · intro A
    change (((Z : ℂ)⁻¹) * sandwichFunctional ω.functional B (star A*A)).im = 0 ∧ _
    have hA := sandwichFunctional_positive ω.functional hp B A
    have hi : 0 ≤ ((Z : ℂ)⁻¹) := by
      rw [← Complex.ofReal_inv]
      exact ⟨le_of_lt (inv_pos.mpr hZ), by simp⟩
    have hh := mul_nonneg hi hA
    exact ⟨hh.2.symm, hh.1⟩

def gibbsDensity {d ℓ : ℕ} (K : QuasiLocal d ℓ) (β : ℝ) : QuasiLocal d ℓ :=
  NormedSpace.exp (((-β : ℝ) : ℂ) • K)

def gibbsHalf {d ℓ : ℕ} (K : QuasiLocal d ℓ) (β : ℝ) : QuasiLocal d ℓ :=
  NormedSpace.exp (((-β/2 : ℝ) : ℂ) • K)

def gibbsState {d ℓ : ℕ} (τ : State d ℓ) (K : QuasiLocal d ℓ) (β : ℝ) : State d ℓ :=
  sandwichState τ (gibbsHalf K β) (NormedSpace.isUnit_exp _)

end Heisenberg
end

end OAI
end

section
-- module Solutions.OAIW2_Heis.Heisenberg_SpinMatrixTrace
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
noncomputable section
open scoped Classical BigOperators Matrix Matrix.Norms.Operator
namespace Heisenberg
open TensorUnits
variable {d ℓ : ℕ} {X : Type} [Fintype X] [DecidableEq X]

def realFunctional (τ : State d ℓ) : QuasiLocal d ℓ →ₗ[ℝ] ℝ :=
  (Complex.reCLM.comp (τ.functional.restrictScalars ℝ)).toLinearMap

end Heisenberg
end
end

end OAI
end