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

/-!
# Dense-time generation of the continuous-path filtration

At a nonnegative rational terminal time, the canonical filtration on continuous-path space is
already generated by the rational-time coordinates up to that terminal time. This deterministic
fact is the filtration bridge needed to extend finite-cylinder restart identities to all past
events. No probability law or Markov property is asserted here.
-/

open Filter MeasureTheory

namespace MarkovProcess
namespace ContinuousPath

noncomputable section

variable {alpha : Type*} [PseudoMetricSpace alpha]
  [MeasurableSpace alpha] [BorelSpace alpha]

set_option warn.classDefReducibility false in
/-- The measurable space generated by rational-time path coordinates up to `S`. -/
def denseCanonicalFiltration (S : DenseTime) : MeasurableSpace (ContinuousPath alpha) :=
  ⨆ r : Set.Iic S,
    MeasurableSpace.comap
      (coordinateProcess (alpha := alpha) (DenseTime.castOrderEmbedding r))
      inferInstance

/-- Restrict a continuous path to the rational times at most `S`. -/
def densePastRestriction (S : DenseTime) (omega : ContinuousPath alpha) : Set.Iic S → alpha :=
  fun r ↦ coordinateProcess (alpha := alpha) (DenseTime.castOrderEmbedding r) omega

omit [MeasurableSpace alpha] [BorelSpace alpha] in
@[simp]
theorem densePastRestriction_apply (S : DenseTime) (omega : ContinuousPath alpha)
    (r : Set.Iic S) :
    densePastRestriction S omega r = omega (DenseTime.castOrderEmbedding r) :=
  rfl

omit [BorelSpace alpha] in
/-- The measurable space generated by the combined rational-past restriction is exactly the
supremum of the individual rational-coordinate measurable spaces. -/
theorem comap_densePastRestriction_eq_denseCanonicalFiltration (S : DenseTime) :
    MeasurableSpace.comap (densePastRestriction (alpha := alpha) S) inferInstance =
      denseCanonicalFiltration (alpha := alpha) S := by
  rw [denseCanonicalFiltration]
  change
    MeasurableSpace.comap (densePastRestriction (alpha := alpha) S)
        (⨆ r, MeasurableSpace.comap (fun path : Set.Iic S → alpha ↦ path r) inferInstance) =
      _
  simp only [MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp]
  rfl

/-- At a rational terminal time, dense-time coordinates generate the full canonical
continuous-path filtration. -/
theorem denseCanonicalFiltration_eq_canonicalFiltration (S : DenseTime) :
    denseCanonicalFiltration (alpha := alpha) S =
      canonicalFiltration (alpha := alpha) (DenseTime.castOrderEmbedding S) := by
  apply le_antisymm
  · rw [denseCanonicalFiltration]
    refine iSup_le fun r ↦ ?_
    exact le_iSup_of_le
      (⟨DenseTime.castOrderEmbedding r,
        DenseTime.castOrderEmbedding.le_iff_le.mpr r.property⟩ :
          Set.Iic (DenseTime.castOrderEmbedding S))
      le_rfl
  · rw [canonicalFiltration]
    refine iSup_le fun s ↦ ?_
    by_cases hs : (s : NNReal) = DenseTime.castOrderEmbedding S
    · rw [hs]
      exact le_iSup_of_le (⟨S, show S ≤ S from le_rfl⟩ : Set.Iic S) le_rfl
    · have hst : (s : NNReal) < DenseTime.castOrderEmbedding S :=
        lt_of_le_of_ne s.property hs
      obtain ⟨q, _hqAnti, hqMem, hq⟩ :=
        ContinuousPath.denseRange_castOrderEmbedding
          |>.exists_seq_strictAnti_tendsto_of_lt
            DenseTime.castOrderEmbedding.monotone hst
      let qIic : ℕ → Set.Iic S := fun n ↦
        ⟨q n, DenseTime.castOrderEmbedding.le_iff_le.mp (hqMem n).2.le⟩
      let : MeasurableSpace (ContinuousPath alpha) :=
        denseCanonicalFiltration (alpha := alpha) S
      have hmeas : Measurable (coordinateProcess (alpha := alpha) s) := by
        apply measurable_of_tendsto_metrizable
          (f := fun n ↦ coordinateProcess (alpha := alpha)
            (DenseTime.castOrderEmbedding (qIic n)))
        · intro n
          apply Measurable.of_comap_le
          exact le_iSup_of_le (qIic n) le_rfl
        · apply tendsto_pi_nhds.2
          intro omega
          exact Filter.Tendsto.comp omega.continuous.continuousAt hq
      exact hmeas.comap_le

/-- At a rational terminal time, the complete rational-past restriction generates the canonical
continuous-path filtration. -/
theorem comap_densePastRestriction_eq_canonicalFiltration (S : DenseTime) :
    MeasurableSpace.comap (densePastRestriction (alpha := alpha) S) inferInstance =
      canonicalFiltration (alpha := alpha) (DenseTime.castOrderEmbedding S) := by
  rw [comap_densePastRestriction_eq_denseCanonicalFiltration,
    denseCanonicalFiltration_eq_canonicalFiltration]

end
end ContinuousPath
end MarkovProcess