Repository navigation
Rework the algorithm/environment classes and constructors - #254
RemyDegenne wants to merge 9 commits into
Conversation
paulorauber
left a comment
paulorauber
left a comment
There was a problem hiding this comment.
I have left some very minor comments. Many have nothing to do with this PR, and are just about things that we did not get to discuss/minor nitpicks.
| /-- The conditional distribution of the feedback at time `n` given the action at time `n` is `ν`. -/ | ||
| lemma condDistrib_feedback_stationaryEnv [StandardBorelSpace 𝓨] [Nonempty 𝓨] | ||
| (h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P) (n : ℕ) : | ||
| lemma condDistrib_feedback_bandit [StandardBorelSpace 𝓨] [Nonempty 𝓨] |
There was a problem hiding this comment.
This is not strictly about this PR, but there are leftover condDistrib (rather than hasCondDistrib ) lemmas that we may want to remove.
| (env.feedback n).sectR (history O A Y n ω, O n ω) | ||
|
|
||
| /-- The means of the feedback distribution as a function of the action chosen at time `n`. -/ | ||
| noncomputable def Environment.means (env : Environment 𝓞 𝓐 𝓨) (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) |
There was a problem hiding this comment.
Also not about this PR, but I think the name Environment.means works in the plural if n comes before k in the list of arguments. Otherwise Environment.mean may be a better name.
| simp_rw [h_eq] | ||
| fun_prop | ||
|
|
||
| @[fun_prop] |
There was a problem hiding this comment.
I think this probably runs into the old fun_prop issue with the hypothesis h .
There was a problem hiding this comment.
I think we can safely remove this file and consult it whenever we consider adding new kinds of environments/algorithms. I found it a bit difficult to parse before looking at the code.
| {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} | ||
|
|
||
| /-- One round of interaction: an observation, then an action, then a feedback. -/ | ||
| abbrev Round (𝓞 𝓐 𝓨 : Type*) := 𝓞 × 𝓐 × 𝓨 |
There was a problem hiding this comment.
Out of curiosity, what made you decide for Round and History as abbreviations?
| structure Environment (𝓞 𝓐 𝓨 : Type*) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] | ||
| where | ||
| /-- Law of the observation of round `n` given the past rounds. -/ | ||
| obs : (n : ℕ) → Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞 |
There was a problem hiding this comment.
obs as an abbreviation is a bit inconsistent with the rest of the names in these basic structures.
|
|
||
| /-- Conditionally on the event `(O 0, A 0) = p`, the first feedback has law `env.ν0 p`. -/ | ||
| /-- Conditionally on the event `(O 0, A 0) = p`, the first feedback has law `env.feedbackZero p`. -/ | ||
| lemma IsAlgEnvSeq.hasLaw_feedback_zero_cond [MeasurableSingletonClass 𝓞] |
There was a problem hiding this comment.
I think this is no longer needed.
| and the observation process of an algorithm-environment sequence is `noObs`. -/ | ||
|
|
||
| /-- Every probability measure on `Unit` is `Measure.dirac ()`. -/ | ||
| lemma Measure.eq_dirac_unit (μ : Measure Unit) [IsProbabilityMeasure μ] : |
There was a problem hiding this comment.
This and below seem to be candidates for Mathlib?
| {P : Measure Ω} [IsFiniteMeasure P] {N : ℕ} | ||
|
|
||
| /-- Step of the algorithm-environment sequence: the round at time `n`. -/ | ||
| def step (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : Round 𝓞 𝓐 𝓨 := |
There was a problem hiding this comment.
On the subject of renaming, I would suggest renaming step to round, except that round is taken by Mathlib. So I would instead suggest renaming Round to Step. This is so that we have a more consistent way of naming random variables based on the type of their values.
|
|
||
| /-- `hist n` is the history before time `n`: the rounds at times `0, ..., n - 1`. | ||
| This is a random variable on the measurable space `ℕ → Round 𝓞 𝓐 𝓨`. -/ | ||
| def hist (n : ℕ) (h : ℕ → Round 𝓞 𝓐 𝓨) : Hist 𝓞 𝓐 𝓨 n := fun i ↦ h i |
There was a problem hiding this comment.
This could also be called history to match the random variable in Algorithm.lean.
AI disclorure: the new list of names and plan for the organisation of algorithms and environments were done manually. The changes in the code to follow the plan (mostly renames) are done with AI.
See the new naming-convention README at LeanMachineLearning/SequentialLearning/README.md . It gives the current names for algorithms or environments that don't depend on some parts of the problem, as well as proposed names for not yet implemented classes and constructors (marked MISSING).
Environment.banditandEnvironment.banditSeq.Renames:
IsDeterministicAlgAlgorithm.IsDeterministicIsDeterministicEnvEnvironment.HasDeterministicFeedbackIsObliviousEnvEnvironment.IsOblivious(meaning changed, see above)nextAction,actionZeroAlgorithm.nextAction,Algorithm.actionZerofeedbackFun,feedbackFunZeroEnvironment.feedbackFun,Environment.feedbackFunZeroAlgorithm.p0Algorithm.policyZeroEnvironment.obs0Environment.obsZeroEnvironment.ν0Environment.feedbackZerodetAlgorithmAlgorithm.deterministicrandomSamplingAlgorithm.constdetEnvironmentEnvironment.detFeedbackobliviousEnv ν(no observations)Environment.banditSeq νstationaryEnv ν(no observations)Environment.bandit νonlineEvalEnvEnvironment.evalSeq(now built onbanditSeq)evalEnvEnvironment.evalNotable breaking changes: the names
Environment.stationaryandEnvironment.obliviousstill exist, but now mean the versions with observations. Code that used the old observation-free environments should switch toEnvironment.banditandEnvironment.banditSeq.