import GinibrePoincare.Concrete.Configuration
import Mathlib.Topology.ContinuousMap.StoneWeierstrass

/-! # Polynomial approximation on compact configuration sets -/

open scoped ComplexConjugate

namespace GinibrePoincare

noncomputable section

/-- Restriction of a complex coordinate to a compact configuration set. -/
def compactCoordinate (n : ℕ) (K : Set (Configuration n)) (i : Fin n) :
    C(K, ℂ) :=
  ⟨fun z ↦ z.1 i, (continuous_apply i).comp continuous_subtype_val⟩

/-- The star algebra generated by the coordinate functions.  Its elements
are precisely finite algebraic expressions in coordinates and their complex
conjugates, hence restrictions of complex coordinate/conjugate-coordinate
polynomials. -/
def configurationPolynomialStarAlgebra (n : ℕ)
    (K : Set (Configuration n)) : StarSubalgebra ℂ C(K, ℂ) :=
  StarAlgebra.adjoin ℂ
    (Set.range fun i : Fin n ↦ compactCoordinate n K i)

theorem compactCoordinate_mem_configurationPolynomialStarAlgebra
    (n : ℕ) (K : Set (Configuration n)) (i : Fin n) :
    compactCoordinate n K i ∈ configurationPolynomialStarAlgebra n K := by
  exact (StarAlgebra.subset_adjoin ℂ _) ⟨i, rfl⟩

theorem configurationPolynomialStarAlgebra_one_mem
    (n : ℕ) (K : Set (Configuration n)) :
    (1 : C(K, ℂ)) ∈ configurationPolynomialStarAlgebra n K :=
  (configurationPolynomialStarAlgebra n K).one_mem

/-- Coordinate polynomials separate configurations on every subset. -/
theorem configurationPolynomialStarAlgebra_separatesPoints
    (n : ℕ) (K : Set (Configuration n)) :
    (configurationPolynomialStarAlgebra n K).SeparatesPoints := by
  intro x y hxy
  have hi : ∃ i : Fin n, x.1 i ≠ y.1 i := by
    by_contra h
    push_neg at h
    apply hxy
    apply Subtype.ext
    exact funext h
  obtain ⟨i, hi⟩ := hi
  exact ⟨compactCoordinate n K i,
    ⟨compactCoordinate n K i,
      compactCoordinate_mem_configurationPolynomialStarAlgebra n K i, rfl⟩, hi⟩

/-- Complex coordinate/conjugate-coordinate polynomials are uniformly dense
in continuous functions on any compact configuration set. -/
theorem configurationPolynomialStarAlgebra_topologicalClosure
    (n : ℕ) (K : Set (Configuration n)) [CompactSpace K] :
    (configurationPolynomialStarAlgebra n K).topologicalClosure = ⊤ := by
  exact ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
    _ (configurationPolynomialStarAlgebra_separatesPoints n K)

/-- Epsilon form of uniform polynomial approximation on a compact
configuration set. -/
theorem exists_configurationPolynomial_uniform_approximation
    (n : ℕ) (K : Set (Configuration n)) [CompactSpace K]
    (f : C(K, ℂ)) {ε : ℝ} (hε : 0 < ε) :
    ∃ g : configurationPolynomialStarAlgebra n K,
      ‖(g : C(K, ℂ)) - f‖ < ε := by
  have hf : f ∈ (configurationPolynomialStarAlgebra n K).topologicalClosure := by
    rw [configurationPolynomialStarAlgebra_topologicalClosure n K]
    simp
  have hf' : f ∈ closure
      (configurationPolynomialStarAlgebra n K : Set C(K, ℂ)) := hf
  obtain ⟨g, hg, hgf⟩ := (Metric.mem_closure_iff.mp hf') ε hε
  exact ⟨⟨g, hg⟩, by simpa [dist_eq_norm, norm_sub_rev] using hgf⟩

/-- Stone--Weierstrass on a closed configuration ball. -/
theorem configurationPolynomial_closedBall_topologicalClosure
    (n : ℕ) (R : ℝ) :
    let K : Set (Configuration n) := Metric.closedBall 0 R
    (configurationPolynomialStarAlgebra n K).topologicalClosure = ⊤ := by
  let K : Set (Configuration n) := Metric.closedBall 0 R
  have hK : IsCompact K := ProperSpace.isCompact_closedBall 0 R
  letI : CompactSpace K := isCompact_iff_compactSpace.mp hK
  exact configurationPolynomialStarAlgebra_topologicalClosure n K

end

end GinibrePoincare