Repository navigation

feat: the policy-mixture lemma for occupancy measures [AJKS, Lemma 14.1] - #154

Merged

lmlexplore-automation[bot] merged 4 commits into

mainfrom

roadmap/policy-mixture-lemma-worker1

Nov 5, 2026

Merged

feat: the policy-mixture lemma for occupancy measures [AJKS, Lemma 14.1]#154
lmlexplore-automation[bot] merged 4 commits into
mainfrom
roadmap/policy-mixture-lemma-worker1

Commits on Nov 5, 2026
- feat: the policy-mixture lemma for occupancy measures [AJKS, Lemma 14.1]
  
  RemyDegenne
  and
  web-flow
  committed
  01a1320
- refactor: drop equal-mass hypotheses from the tvDist sum and kernel bounds
  
  RemyDegenne
  and
  web-flow
  committed
  f7802f6
- refactor: shorten two tvDist proofs per proof-quality review
  
  RemyDegenne
  and
  web-flow
  committed
  a55c723
- refactor: use Mathlib's IsMarkovKernel.integrable in tvDist_comp_right_le
  
  RemyDegenne
  and
  web-flow
  committed
  f37bdd1