LeanMachineLearning

Learning.IsAlgEnvSeq.identDistrib_trajectory๐Ÿ”—

Theorem

The law of the sequence of actions and observations generated by an algorithm-environment pair is unique: it does not depend on the probability space used.

๐Ÿ”—theorem
Learning.IsAlgEnvSeq.identDistrib_trajectory.{u_1, u_2, u_4, u_5}
  {๐“ : Type u_1} {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_4} {ฮฉ' : Type u_5}
  {mฮฉ : MeasurableSpace ฮฉ} {mฮฉ' : MeasurableSpace ฮฉ'}
  {alg : Algorithm ๐“ ๐“จ} {env : Environment ๐“ ๐“จ}
  {P : MeasureTheory.Measure ฮฉ} [MeasureTheory.IsProbabilityMeasure P]
  {P' : MeasureTheory.Measure ฮฉ'}
  [MeasureTheory.IsProbabilityMeasure P'] {Aโ‚ : โ„• โ†’ ฮฉ โ†’ ๐“}
  {Rโ‚ : โ„• โ†’ ฮฉ โ†’ ๐“จ} {Aโ‚‚ : โ„• โ†’ ฮฉ' โ†’ ๐“} {Rโ‚‚ : โ„• โ†’ ฮฉ' โ†’ ๐“จ}
  (h1 : IsAlgEnvSeq Aโ‚ Rโ‚ alg env P)
  (h2 : IsAlgEnvSeq Aโ‚‚ Rโ‚‚ alg env P') :
  ProbabilityTheory.IdentDistrib (trajectory Aโ‚ Rโ‚) (trajectory Aโ‚‚ Rโ‚‚) P
    P'
Learning.IsAlgEnvSeq.identDistrib_trajectory.{u_1,
    u_2, u_4, u_5}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_4}
  {ฮฉ' : Type u_5} {mฮฉ : MeasurableSpace ฮฉ}
  {mฮฉ' : MeasurableSpace ฮฉ'}
  {alg : Algorithm ๐“ ๐“จ}
  {env : Environment ๐“ ๐“จ}
  {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P]
  {P' : MeasureTheory.Measure ฮฉ'}
  [MeasureTheory.IsProbabilityMeasure P']
  {Aโ‚ : โ„• โ†’ ฮฉ โ†’ ๐“} {Rโ‚ : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  {Aโ‚‚ : โ„• โ†’ ฮฉ' โ†’ ๐“} {Rโ‚‚ : โ„• โ†’ ฮฉ' โ†’ ๐“จ}
  (h1 : IsAlgEnvSeq Aโ‚ Rโ‚ alg env P)
  (h2 : IsAlgEnvSeq Aโ‚‚ Rโ‚‚ alg env P') :
  ProbabilityTheory.IdentDistrib
    (trajectory Aโ‚ Rโ‚) (trajectory Aโ‚‚ Rโ‚‚)
    P P'

Code

theorem IsAlgEnvSeq.identDistrib_trajectory (h1 : IsAlgEnvSeq Aโ‚ Rโ‚ alg env P)
    (h2 : IsAlgEnvSeq Aโ‚‚ Rโ‚‚ alg env P') :
    IdentDistrib (trajectory Aโ‚ Rโ‚) (trajectory Aโ‚‚ Rโ‚‚) P P' where
  aemeasurable_fst
Proof
(measurable_pi_iff.2 fun n โ†ฆ (h1.measurable_action n).prodMk
    (h1.measurable_feedback n)).aemeasurable
  aemeasurable_snd := (measurable_pi_iff.2 fun n โ†ฆ (h2.measurable_action n).prodMk
    (h2.measurable_feedback n)).aemeasurable
  map_eq := isAlgEnvSeq_unique h1 h2

Actions: Source ยท Open Issue

Meaning last changed in v4.34.0-rc2-1-g439785b (2026-08-23), the 4th recorded change.

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file ยท open it in the Lean web editor.

Dependency graph

Audit surface: 5 project declarations, 42 external constants

โœ“ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.