move tests to Test

Author: RemyDegenne

RandomDo.lean

@@ -9,7 +9,7 @@ public import RandomDo.Monad.Notation
 public import RandomDo.Probability.AlgTrace
 public import RandomDo.Probability.Examples
 public import RandomDo.Probability.Extend
-public import RandomDo.Probability.ExtendExamples
+public import RandomDo.Probability.MeasurePreserving
 public import RandomDo.Probability.Record
 public import RandomDo.Probability.Tactic
 public import RandomDo.Probability.Thompson

RandomDo/Probability/AlgTrace.lean

@@ -512,151 +512,3 @@ elab_rules : tactic
 end RDo.Tactic
 
 end
-
-@[expose] public section
-
-open MeasureTheory ProbabilityTheory Finset Learning RDo
-
-noncomputable section
-
-/-! ## An example: an algorithm whose policy is an `rdo` program
-
-A toy sequential algorithm, to show the pipeline end to end: write the policy as an `rdo` program,
-get its trace from `rdo_trace`, package it as an `AlgTrace`, and then read the algorithm's internal
-draws off any algorithm-environment sequence.
-
-To do the same for `thompson` one needs the measurable equivalence between `Iic n → 𝓐 × 𝓨` and
-`Vector (𝓐 × 𝓨) (n + 1)` that turns it into a policy — `Vector.v_equiv` in
-`RandomDo.Tactic.Examples`, still a `sorry` there (and stated one element short). Everything after
-that point is what follows below.
--/
-
-namespace RDo.Example
-
-variable {K : ℕ} (hK : 0 < K)
-
-/-- The action, read off the history and the noise: depending on the sign of the noise, either
-switch to arm `0` or repeat the last action. -/
-def readout (n : ℕ) (p : (Iic n → Fin K × ℝ) × ℝ) : Fin K :=
-  if 0 < p.2 then ⟨0, hK⟩ else (p.1 ⟨n, by simp⟩).1
-
-@[fun_prop]
-lemma measurable_readout (n : ℕ) : Measurable (readout hK n) := by
-  unfold readout
-  exact Measurable.ite (measurableSet_lt measurable_const measurable_snd) measurable_const
-    (measurable_fst.comp ((measurable_pi_apply _).comp measurable_fst))
-
-/-- The policy: perturb the last reward by Gaussian noise, then read the action off it. -/
-def policy (n : ℕ) (h : Iic n → Fin K × ℝ) : Measure (Fin K) := rdo
-  let z ← gaussianReal (h ⟨n, by simp⟩).2 1
-  return readout hK n (h, z)
-
-instance (n : ℕ) : IsMarkov (policy hK n) := by unfold policy; is_markov
-
-/-- The noise the policy draws at step `n`, as a kernel: the one coordinate of its trace. -/
-def noise (n : ℕ) : Kernel (Iic n → Fin K × ℝ) ℝ :=
-  markovKernel (fun h ↦ gaussianReal (h ⟨n, by simp⟩).2 1)
-    (IsMarkov.gaussianReal (by fun_prop) measurable_const)
-
-instance (n : ℕ) : IsMarkovKernel (noise (K := K) n) := by unfold noise; infer_instance
-
-lemma hasTrace_policy (n : ℕ) : HasTrace (policy hK n) (noise n) (readout hK n) := by
-  rdo_trace (policy hK n) with h
-  exact h
-
-/-- The algorithm. -/
-def alg : Algorithm (Fin K) ℝ where
-  policy n := markovKernel (policy hK n) inferInstance
-  p0 := Measure.dirac ⟨0, hK⟩
-
-/-- Its trace: one Gaussian draw per step. -/
-def trace : AlgTrace (alg hK) ℝ where
-  K := noise
-  out := readout hK
-  hasTrace n := hasTrace_policy hK n
-  K0 := gaussianReal 0 1
-  out0 := fun _ ↦ ⟨0, hK⟩
-  measurable_out0 := measurable_const
-  map_out0 := by rw [Measure.map_const]; simp [alg]
-
-/-- **The payoff.** Given any algorithm-environment sequence for this algorithm, one may assume the
-space also carries the noise `Z` the policy draws at each step: it has the conditional law `noise n`
-given the history, and the action is `readout` of the history and it. The trajectory keeps the same
-law, so anything proved there about the actions and feedbacks holds of the original sequence. -/
-theorem exists_noise (env : Environment (Fin K) ℝ) {Ω₀ : Type*} [MeasurableSpace Ω₀]
-    {P : Measure Ω₀} [IsProbabilityMeasure P] {A : ℕ → Ω₀ → Fin K} {Y : ℕ → Ω₀ → ℝ}
-    (h : IsAlgEnvSeq A Y (alg hK) env P) :
-    ∃ (Ω' : Type) (_ : MeasurableSpace Ω') (P' : Measure Ω') (_ : IsProbabilityMeasure P')
-      (A' : ℕ → Ω' → Fin K) (Y' : ℕ → Ω' → ℝ) (Z : ℕ → Ω' → ℝ),
-      IsAlgEnvSeq A' Y' (alg hK) env P'
-        ∧ P'.map (trajectory A' Y') = P.map (trajectory A Y)
-        ∧ (∀ n, HasCondDistrib (Z (n + 1)) (history A' Y' n) (noise n) P')
-        ∧ (∀ n, A' (n + 1) =ᵐ[P'] fun ω ↦ readout hK n (history A' Y' n ω, Z (n + 1) ω)) := by
-  obtain ⟨Ω', mΩ', P', hP', A', Y', Z, hseq, hlaw, -, hZ, -, hA⟩ :=
-    (trace hK).exists_isAlgEnvSeq_trace h
-  exact ⟨Ω', mΩ', P', hP', A', Y', Z, hseq, hlaw, hZ, hA⟩
-
-/-- **The tactic at work.** `alg_env_trace` replaces the context and the goal by ones on a space
-that also carries the noise `Z` the policy draws. The obligation that the statement only depends
-on the law of the trajectory is discharged by `transfer` through the trajectory space, so only the
-traced goal is left. Any hypothesis mentioning the space travels with the goal, so nothing is
-silently lost. -/
-example (env : Environment (Fin K) ℝ) {Ω₀ : Type} [MeasurableSpace Ω₀] {P : Measure Ω₀}
-    [IsProbabilityMeasure P] {A : ℕ → Ω₀ → Fin K} {Y : ℕ → Ω₀ → ℝ}
-    (h : IsAlgEnvSeq A Y (alg hK) env P) :
-    P.map (A 0) = Measure.dirac ⟨0, hK⟩ := by
-  alg_env_trace (trace hK) with Ω P A Y Z hseq hZ₀ hZ hA₀ hA
-  -- `Z`, `hZ₀`, `hZ` and `hA` are the algorithm's draws and their laws, now available.
-  exact hseq.hasLaw_action_zero.map_eq
-
-/-- A statement `transfer` has no lemma for leaves the obligation, which is then proved by hand,
-here trivially. -/
-example (env : Environment (Fin K) ℝ) {Ω₀ : Type} [MeasurableSpace Ω₀] {P : Measure Ω₀}
-    [IsProbabilityMeasure P] {A : ℕ → Ω₀ → Fin K} {Y : ℕ → Ω₀ → ℝ}
-    (h : IsAlgEnvSeq A Y (alg hK) env P) :
-    IsProbabilityMeasure P := by
-  alg_env_trace (trace hK)
-  case traced => infer_instance
-  case transfer =>
-    intro Ω₁ _ P₁ _ A₁ Y₁ Ω₂ _ P₂ _ A₂ Y₂ h₁ h₂ hlaw h₀
-    infer_instance
-
-/-- **`extend_space` alongside an algorithm-environment sequence.** After the extension, `Ω`, `P`,
-`A` and `Y` live on a larger space that also carries a Gaussian `U` independent of the whole
-trajectory, and `h` has been transported by `IsAlgEnvSeq.comp_measurePreserving`. The statement
-does not mention the original space, so the `transfer` obligation is trivial and `extend_space`
-closes it. The measurability of the sequence is put in the context first, so that the
-independence statement `hind` covers `A` and `Y`. -/
-example (env : Environment (Fin K) ℝ) {Ω₀ : Type} [MeasurableSpace Ω₀] {P : Measure Ω₀}
-    [IsProbabilityMeasure P] {A : ℕ → Ω₀ → Fin K} {Y : ℕ → Ω₀ → ℝ}
-    (h : IsAlgEnvSeq A Y (alg hK) env P) :
-    ∃ (Ω' : Type) (_ : MeasurableSpace Ω') (P' : Measure Ω') (_ : IsProbabilityMeasure P')
-      (A' : ℕ → Ω' → Fin K) (Y' : ℕ → Ω' → ℝ) (U : Ω' → ℝ),
-      IsAlgEnvSeq A' Y' (alg hK) env P' ∧ HasLaw U (gaussianReal 0 1) P'
-        ∧ IndepFun (trajectory A' Y') U P' := by
-  have hA := h.measurable_action
-  have hY := h.measurable_feedback
-  extend_space! (gaussianReal 0 1) using P with U hU hind
-  have hAY : IndepFun (trajectory A Y) U P :=
-    hind.comp (φ := fun (p : (ℕ → Fin K) × (ℕ → ℝ)) (n : ℕ) ↦ (p.1 n, p.2 n)) (by fun_prop)
-      measurable_id
-  exact ⟨Ω₀, inferInstance, P, inferInstance, A, Y, U, h, hU, hAY⟩
-
-/-- **The explicit form, `extend_space_map`.** The goal mentions the space through `P` and `A 0`;
-`transfer` moves it to the new space, with the measurability of the sequence taken from `h`. In
-the extended goal, `transfer hf at h` pulls the sequence back. -/
-example (env : Environment (Fin K) ℝ) {Ω₀ : Type} [MeasurableSpace Ω₀] {P : Measure Ω₀}
-    [IsProbabilityMeasure P] {A : ℕ → Ω₀ → Fin K} {Y : ℕ → Ω₀ → ℝ}
-    (h : IsAlgEnvSeq A Y (alg hK) env P) :
-    P.map (A 0) = Measure.dirac ⟨0, hK⟩ := by
-  have hA := h.measurable_action
-  have hY := h.measurable_feedback
-  extend_space_map (gaussianReal 0 1) with Ω' P' f hf U hU hind
-  transfer hf at h
-  exact h.hasLaw_action_zero.map_eq
-
-end RDo.Example
-
-end
-
-end

RandomDo/Probability/Extend.lean

@@ -5,11 +5,7 @@ Authors: Rémy Degenne
 -/
 module
 
-public import RandomDo.Probability.Transfer
-public import Mathlib.MeasureTheory.Integral.Bochner.Basic
-public import Mathlib.MeasureTheory.Measure.Real
-public import Mathlib.Probability.HasCondDistrib
-public import Mathlib.Probability.Independence.Basic
+public import RandomDo.Probability.MeasurePreserving
 public import Mathlib.Probability.Kernel.Composition.MeasureCompProd
 public meta import Lean.Elab.Tactic.Basic
 
@@ -55,11 +51,9 @@ statement by statement. Here the projection `f` is measure preserving, which is
 ## Main results
 
 * `RDo.wlog_extend`, `RDo.wlog_extend_kernel`: the principles behind the tactic.
-* `MeasureTheory.MeasurePreserving.map_fun_comp`, `hasLaw_fun_comp_iff`, `indepFun_fun_comp_iff`,
-  `hasCondDistrib_fun_comp_iff`: pulling statements back along a measure-preserving map.
-* The `@[transfer]` lemmas `MeasurePreserving.transfer_*` and the `@[transfer_forward]` lemmas
-  `*.comp_measurePreserving`, `*.preimage_measurePreserving`: the same facts in the forms the
-  `transfer` tactic uses.
+* `RDo.indepFun_fst_snd_prod`, `RDo.hasCondDistrib_snd_fst_compProd`: the product extension.
+
+The lemmas the `transfer` tactic rewrites with are in `RandomDo.Probability.MeasurePreserving`.
 -/
 
 @[expose] public section
@@ -68,178 +62,6 @@ open MeasureTheory ProbabilityTheory
 
 noncomputable section
 
-/-! ### Pulling statements back along a measure-preserving map -/
-
-namespace MeasureTheory.MeasurePreserving
-
-variable {Ω Ω' 𝓧 𝓨 : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
-  {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {P : Measure Ω} {P' : Measure Ω'}
-  {f : Ω' → Ω} {X : Ω → 𝓧} {Y : Ω → 𝓨}
-
-/-- The law of `X ∘ f` under `P'` is the law of `X` under `P`. -/
-lemma map_fun_comp (hf : MeasurePreserving f P' P) (hX : AEMeasurable X P) :
-    P'.map (fun ω ↦ X (f ω)) = P.map X := by
-  rw [← hf.map_eq] at hX ⊢
-  exact (AEMeasurable.map_map_of_aemeasurable hX hf.measurable.aemeasurable).symm
-
-lemma hasLaw_fun_comp_iff (hf : MeasurePreserving f P' P) (hX : Measurable X) {ν : Measure 𝓧} :
-    HasLaw (fun ω ↦ X (f ω)) ν P' ↔ HasLaw X ν P where
-  mp h := ⟨hX.aemeasurable, by rw [← hf.map_fun_comp hX.aemeasurable]; exact h.map_eq⟩
-  mpr h := h.comp hf.hasLaw
-
-lemma indepFun_fun_comp_iff (hf : MeasurePreserving f P' P) (hX : Measurable X)
-    (hY : Measurable Y) :
-    IndepFun (fun ω ↦ X (f ω)) (fun ω ↦ Y (f ω)) P' ↔ IndepFun X Y P := by
-  simp only [indepFun_iff_measure_inter_preimage_eq_mul]
-  refine forall₄_congr fun s t hs ht ↦ ?_
-  change P' (f ⁻¹' (X ⁻¹' s) ∩ f ⁻¹' (Y ⁻¹' t))
-    = P' (f ⁻¹' (X ⁻¹' s)) * P' (f ⁻¹' (Y ⁻¹' t)) ↔ _
-  rw [← Set.preimage_inter, hf.measure_preimage ((hX hs).inter (hY ht)).nullMeasurableSet,
-    hf.measure_preimage (hX hs).nullMeasurableSet, hf.measure_preimage (hY ht).nullMeasurableSet]
-
-lemma hasCondDistrib_fun_comp_iff (hf : MeasurePreserving f P' P) (hX : Measurable X)
-    (hY : Measurable Y) {κ : Kernel 𝓧 𝓨} :
-    HasCondDistrib (fun ω ↦ Y (f ω)) (fun ω ↦ X (f ω)) κ P' ↔ HasCondDistrib Y X κ P := by
-  unfold HasCondDistrib
-  rw [hf.map_fun_comp hX.aemeasurable]
-  exact hf.hasLaw_fun_comp_iff (hX.prodMk hY)
-
-/-! ### The `@[transfer]` lemmas: from the old space to the new one
-
-The same facts, stated with the old space on the left and `hf` as the first explicit argument,
-which is what the `transfer` tactic rewrites with. -/
-
-@[transfer]
-lemma transfer_map (hf : MeasurePreserving f P' P) (hX : AEMeasurable X P) :
-    P.map X = P'.map (fun ω ↦ X (f ω)) :=
-  (hf.map_fun_comp hX).symm
-
-@[transfer]
-lemma transfer_measure (hf : MeasurePreserving f P' P) {s : Set Ω} (hs : NullMeasurableSet s P) :
-    P s = P' (f ⁻¹' s) :=
-  (hf.measure_preimage hs).symm
-
-@[transfer]
-lemma transfer_real (hf : MeasurePreserving f P' P) {s : Set Ω} (hs : NullMeasurableSet s P) :
-    P.real s = P'.real (f ⁻¹' s) := by
-  simp only [measureReal_def, hf.measure_preimage hs]
-
-@[transfer]
-lemma transfer_hasLaw (hf : MeasurePreserving f P' P) (hX : Measurable X) {ν : Measure 𝓧} :
-    HasLaw X ν P ↔ HasLaw (fun ω ↦ X (f ω)) ν P' :=
-  (hf.hasLaw_fun_comp_iff hX).symm
-
-@[transfer]
-lemma transfer_indepFun (hf : MeasurePreserving f P' P) (hX : Measurable X) (hY : Measurable Y) :
-    IndepFun X Y P ↔ IndepFun (fun ω ↦ X (f ω)) (fun ω ↦ Y (f ω)) P' :=
-  (hf.indepFun_fun_comp_iff hX hY).symm
-
-@[transfer]
-lemma transfer_hasCondDistrib (hf : MeasurePreserving f P' P) (hX : Measurable X)
-    (hY : Measurable Y) {κ : Kernel 𝓧 𝓨} :
-    HasCondDistrib Y X κ P ↔ HasCondDistrib (fun ω ↦ Y (f ω)) (fun ω ↦ X (f ω)) κ P' :=
-  (hf.hasCondDistrib_fun_comp_iff hX hY).symm
-
-@[transfer]
-lemma transfer_integral {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
-    (hf : MeasurePreserving f P' P) {g : Ω → G} (hg : AEStronglyMeasurable g P) :
-    ∫ ω, g ω ∂P = ∫ ω, g (f ω) ∂P' := by
-  rw [← hf.map_eq] at hg ⊢
-  exact integral_map hf.measurable.aemeasurable hg
-
-@[transfer]
-lemma transfer_lintegral (hf : MeasurePreserving f P' P) {g : Ω → ENNReal}
-    (hg : AEMeasurable g P) :
-    ∫⁻ ω, g ω ∂P = ∫⁻ ω, g (f ω) ∂P' := by
-  rw [← hf.map_eq] at hg ⊢
-  exact lintegral_map' hg hf.measurable.aemeasurable
-
-@[transfer]
-lemma transfer_ae (hf : MeasurePreserving f P' P) {p : Ω → Prop}
-    (hp : NullMeasurableSet {ω | p ω} P) :
-    (∀ᵐ ω ∂P, p ω) ↔ ∀ᵐ ω ∂P', p (f ω) := by
-  rw [ae_iff, ae_iff, ← hf.measure_preimage (s := {ω | ¬ p ω}) hp.compl, Set.preimage_ofPred_eq]
-
-@[transfer]
-lemma transfer_ae_eq (hf : MeasurePreserving f P' P) {X Y : Ω → 𝓧}
-    (h : NullMeasurableSet {ω | X ω = Y ω} P) :
-    X =ᵐ[P] Y ↔ (fun ω ↦ X (f ω)) =ᵐ[P'] fun ω ↦ Y (f ω) :=
-  hf.transfer_ae h
-
-@[transfer]
-lemma transfer_integrable {G : Type*} [NormedAddCommGroup G] (hf : MeasurePreserving f P' P)
-    {g : Ω → G} (hg : AEStronglyMeasurable g P) :
-    Integrable g P ↔ Integrable (fun ω ↦ g (f ω)) P' :=
-  (hf.integrable_comp hg).symm
-
-end MeasureTheory.MeasurePreserving
-
-/-! ### Forward transport of hypotheses
-
-A hypothesis about the old space gives one about the new space. These are the
-`@[transfer_forward]` lemmas: the hypothesis first, then `hf`, then side conditions. -/
-
-section Forward
-
-variable {Ω Ω' 𝓧 𝓨 : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
-  {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {P : Measure Ω} {P' : Measure Ω'}
-  {f : Ω' → Ω} {X : Ω → 𝓧} {Y : Ω → 𝓨}
-
-@[transfer_forward]
-lemma Measurable.comp_measurePreserving (hX : Measurable X) (hf : MeasurePreserving f P' P) :
-    Measurable fun ω ↦ X (f ω) :=
-  hX.comp hf.measurable
-
-@[transfer_forward]
-lemma AEMeasurable.comp_measurePreserving (hX : AEMeasurable X P)
-    (hf : MeasurePreserving f P' P) :
-    AEMeasurable (fun ω ↦ X (f ω)) P' :=
-  hX.comp_quasiMeasurePreserving hf.quasiMeasurePreserving
-
-attribute [transfer_forward] MeasureTheory.AEStronglyMeasurable.comp_measurePreserving
-
-@[transfer_forward]
-lemma MeasurableSet.preimage_measurePreserving {s : Set Ω} (hs : MeasurableSet s)
-    (hf : MeasurePreserving f P' P) :
-    MeasurableSet (f ⁻¹' s) :=
-  hf.measurable hs
-
-@[transfer_forward]
-lemma MeasureTheory.NullMeasurableSet.preimage_measurePreserving {s : Set Ω}
-    (hs : NullMeasurableSet s P) (hf : MeasurePreserving f P' P) :
-    NullMeasurableSet (f ⁻¹' s) P' :=
-  hs.preimage hf.quasiMeasurePreserving
-
-@[transfer_forward]
-lemma ProbabilityTheory.HasLaw.comp_measurePreserving {ν : Measure 𝓧} (hX : HasLaw X ν P)
-    (hf : MeasurePreserving f P' P) :
-    HasLaw (fun ω ↦ X (f ω)) ν P' :=
-  hX.comp hf.hasLaw
-
-/-- A conditional law pulls back along a measure-preserving map. -/
-@[transfer_forward]
-lemma ProbabilityTheory.HasCondDistrib.comp_measurePreserving {κ : Kernel 𝓧 𝓨}
-    (h : HasCondDistrib Y X κ P) (hf : MeasurePreserving f P' P) :
-    HasCondDistrib (fun ω ↦ Y (f ω)) (fun ω ↦ X (f ω)) κ P' := by
-  have hX := h.aemeasurable_fst
-  unfold HasCondDistrib at h ⊢
-  rw [hf.map_fun_comp hX]
-  exact h.comp hf.hasLaw
-
-@[transfer_forward]
-lemma ProbabilityTheory.IndepFun.comp_measurePreserving (h : IndepFun X Y P)
-    (hf : MeasurePreserving f P' P) (hX : Measurable X) (hY : Measurable Y) :
-    IndepFun (fun ω ↦ X (f ω)) (fun ω ↦ Y (f ω)) P' :=
-  (hf.indepFun_fun_comp_iff hX hY).2 h
-
-@[transfer_forward]
-lemma MeasureTheory.Integrable.comp_measurePreserving {G : Type*} [NormedAddCommGroup G]
-    {g : Ω → G} (hg : Integrable g P) (hf : MeasurePreserving f P' P) :
-    Integrable (fun ω ↦ g (f ω)) P' :=
-  (hf.integrable_comp hg.aestronglyMeasurable).2 hg
-
-end Forward
-
 namespace RDo
 
 /-! ### The product extension -/