/-
Copyright (c) 2026 Scott Armstrong. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Armstrong
-/
import Mathlib.Probability.Process.Adapted

/-!
# Canonical discrete path space

This file records the elementary measurable and filtered structure on the
discrete path space `ℕ → α`.  It does not equip paths with a probability law or
assert any Markov property.

## Main definitions

* `DiscretePath`: the canonical space of `α`-valued discrete paths.
* `DiscretePath.coordinate`: evaluation of a path at one time.
* `DiscretePath.coordinateProcess`: the canonical coordinate process.
* `DiscretePath.canonicalFiltration`: the natural filtration of the coordinate process.
-/

open MeasureTheory
open TopologicalSpace

namespace MarkovProcess

/-- The canonical space of `α`-valued paths indexed by `ℕ`. -/
abbrev DiscretePath (α : Type*) := ℕ → α

namespace DiscretePath

variable {α : Type*}

/-- Evaluation of a discrete path at time `n`. -/
def coordinate (n : ℕ) (ω : DiscretePath α) : α :=
  ω n

/-- The canonical coordinate process on discrete path space. -/
def coordinateProcess : ℕ → DiscretePath α → α :=
  fun n => coordinate n

@[simp]
theorem coordinate_apply (n : ℕ) (ω : DiscretePath α) : coordinate n ω = ω n :=
  rfl

@[simp]
theorem coordinateProcess_apply (n : ℕ) (ω : DiscretePath α) :
    coordinateProcess n ω = ω n :=
  rfl

section Measurable

variable [MeasurableSpace α]

/-- Every coordinate evaluation is measurable for the product measurable
space on discrete paths. -/
@[fun_prop]
theorem measurable_coordinate (n : ℕ) : Measurable (coordinate (α := α) n) :=
  measurable_pi_apply n

/-- Every member of the coordinate process is measurable. -/
@[fun_prop]
theorem measurable_coordinateProcess (n : ℕ) :
    Measurable (coordinateProcess (α := α) n) :=
  measurable_coordinate n

end Measurable

section NaturalFiltration

variable [TopologicalSpace α]
variable [MetrizableSpace α]
variable [MeasurableSpace α]
variable [BorelSpace α]
variable [SecondCountableTopology α]

/-- Every coordinate evaluation is strongly measurable when the state space
is second-countable, metrizable, and carries its Borel measurable space. -/
theorem stronglyMeasurable_coordinate (n : ℕ) :
    StronglyMeasurable (coordinate (α := α) n) :=
  (measurable_coordinate n).stronglyMeasurable

/-- Every member of the coordinate process is strongly measurable. -/
theorem stronglyMeasurable_coordinateProcess (n : ℕ) :
    StronglyMeasurable (coordinateProcess (α := α) n) :=
  stronglyMeasurable_coordinate n

/-- The canonical filtration on discrete path space, defined as the natural
filtration generated by the coordinate process. -/
def canonicalFiltration : Filtration ℕ (inferInstance : MeasurableSpace (DiscretePath α)) :=
  Filtration.natural coordinateProcess stronglyMeasurable_coordinateProcess

/-- At time `n`, the canonical filtration is generated by coordinate maps at
times at most `n`. -/
theorem canonicalFiltration_apply (n : ℕ) :
    canonicalFiltration (α := α) n =
      ⨆ k ≤ n, MeasurableSpace.comap (coordinateProcess (α := α) k) inferInstance :=
  rfl

/-- The coordinate process is adapted to its canonical filtration. -/
theorem adapted_coordinateProcess :
    Adapted (canonicalFiltration (α := α)) (coordinateProcess (α := α)) := by
  exact (Filtration.stronglyAdapted_natural
    (u := coordinateProcess (α := α)) stronglyMeasurable_coordinateProcess).adapted

end NaturalFiltration

end DiscretePath

end MarkovProcess