diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 8bf9da4e..9bc9ac39 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,6 +1,5 @@ module -- shake: keep-all --deprecated_module: ignore -public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.Polish.StandardBorel public import LeanMachineLearning.ForMathlib.MeasureTheory.Measurable public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.Lattice diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Constructions/Polish/StandardBorel.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Constructions/Polish/StandardBorel.lean deleted file mode 100644 index ba3cf26f..00000000 --- a/LeanMachineLearning/ForMathlib/MeasureTheory/Constructions/Polish/StandardBorel.lean +++ /dev/null @@ -1,22 +0,0 @@ -/- -Copyright (c) 2025 Rémy Degenne. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne --/ -module - -public import Mathlib.MeasureTheory.Constructions.Polish.Basic - -/-! -# Properties of standard Borel spaces --/ - -@[expose] public section - -open MeasureTheory - -variable {Ω : Type*} {mΩ : MeasurableSpace Ω} - -instance [StandardBorelSpace Ω] : MeasurableEq Ω := by - letI := upgradeStandardBorel Ω - infer_instance diff --git a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean index 138f013a..c76aa2df 100644 --- a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean +++ b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean @@ -5,7 +5,6 @@ Authors: Rémy Degenne, Paulo Rauber -/ module -public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.Polish.StandardBorel public import LeanMachineLearning.ForMathlib.Probability.Independence.CondIndepFun public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepFun public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepInfinitePi diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean index 512f8a41..c23e291e 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean @@ -109,7 +109,7 @@ theorem action_tendsto_any (h : IsAlgEnvSeq A Y (randomSampling μ) (evalEnv f h exact (Metric.measure_ball_pos μ a hε).ne' · intro n refine measure_mono ?_ - simp only [mem_Iic, Set.subset_iInter_iff, Set.setOf_subset_setOf] + simp only [mem_Iic, Set.subset_iInter_iff, Set.ofPred_subset_ofPred] intro i hi ω (hω : ε ≤ (fun (j : Iic n) ↦ dist (A j.1 ω) a).min) simp_all only [univ_eq_attach, le_inf'_iff, mem_attach, forall_const, Subtype.forall, mem_Iic] @@ -127,7 +127,7 @@ lemma image_action_tendsto_any refine action_tendsto_any h a hδ |> tendsto_zero_of_le <| ?_ intro n refine measure_mono ?_ - simp only [Set.setOf_subset_setOf] + simp only [Set.ofPred_subset_ofPred] intro ω hω rw [← argmin_spec] set j := argmin (fun (i : Iic n) ↦ dist (A i.1 ω) a) @@ -162,7 +162,7 @@ lemma tendsto_min₀ (h : IsAlgEnvSeq A R (randomSampling μ) (evalEnv f hfc.mea refine image_action_tendsto_any hfc h a hε |> tendsto_zero_of_le <| ?_ intro n refine measure_mono ?_ - simp only [Set.setOf_subset_setOf] + simp only [Set.ofPred_subset_ofPred] intro ω hω rw [← argmin_spec] set j := argmin (fun (i : Iic n) ↦ dist (f (A i ω)) (f a)) @@ -191,7 +191,7 @@ lemma tendsto_max₀ (h : IsAlgEnvSeq A R (randomSampling μ) (evalEnv f hfc.mea refine image_action_tendsto_any hfc h a hε |> tendsto_zero_of_le <| ?_ intro n refine measure_mono ?_ - simp only [Set.setOf_subset_setOf] + simp only [Set.ofPred_subset_ofPred] intro ω hω rw [← argmin_spec] set j := argmin (fun (i : Iic n) ↦ dist (f (A i ω)) (f a)) diff --git a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean index 39539bd7..d707a586 100644 --- a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean +++ b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean @@ -191,11 +191,18 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω} namespace IsAlgEnvSeq +/-- The conditional distribution of the feedback at time `n` given the action at time `n` +is `ν n`. -/ +lemma hasCondDistrib_feedback_obliviousEnv {ν : ℕ → Kernel 𝓐 𝓨} [∀ n, IsMarkovKernel (ν n)] + (h : IsAlgEnvSeq A Y alg (obliviousEnv ν) P) (n : ℕ) : + HasCondDistrib (Y n) (A n) (ν n) P := by + simpa using IsObliviousEnv.hasCondDistrib_feedback h n + /-- The conditional distribution of the feedback at time `n` given the action at time `n` is `ν`. -/ lemma hasCondDistrib_feedback_stationaryEnv (h : IsAlgEnvSeq A Y alg (stationaryEnv ν) P) (n : ℕ) : - HasCondDistrib (Y n) (A n) ν P := by - simpa using IsObliviousEnv.hasCondDistrib_feedback h n + HasCondDistrib (Y n) (A n) ν P := + hasCondDistrib_feedback_obliviousEnv h n /-- The conditional distribution of the feedback at time `n` given the action at time `n` is `ν`. -/ lemma condDistrib_feedback_stationaryEnv [StandardBorelSpace 𝓨] [Nonempty 𝓨] diff --git a/lake-manifest.json b/lake-manifest.json index 6050ab24..c0d22f33 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,27 +5,27 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "18f56bef5344cefb0563662c495e3eb3824a2589", + "rev": "51e6992efd06126df61a496bebf8f49482a4e129", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "18f56bef5344cefb0563662c495e3eb3824a2589", + "inputRev": "v4.33.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/verso", "type": "git", "subDir": null, "scope": "", - "rev": "6af30619664960f9c816b27157dff3ceb1500dcf", + "rev": "755ccbe968ad1b0255bee8b46d9cb2306486d6d8", "name": "verso", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.33.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", + "rev": "123d15766ba49356c02ebad2a4462dfe12d79899", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715", + "rev": "f5c090429dff3cf66cb65562526c9ea6e8edfbcb", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c", + "rev": "bb3469a87774349fe01898d8bf2fc6a1ce6411ca", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69", + "rev": "222c58dad7706a6e7cae46c0edd65ea881d3ee27", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "57d3325be72a842920813bcb40f96a6f7393c185", + "rev": "7db8190085343afde2f5d2cdcc9bac719b6ec02c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d", + "rev": "ef42f8944eaf5b6cbfbe75d1917d824c7dd6cf33", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0ecf8993df88c044962426c2cbca0de5717d6150", + "rev": "76e1c118b0700b4ceafe99532e887d6431625e1a", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "56958b3901ca108830de34fbce6cecd4b5757c1f", + "rev": "006dc1d1db18c5dc73d637c926cf132e88df05b5", "name": "illuminate", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -115,7 +115,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d", + "rev": "4343da18d95390b09fde98efb18125677c4b500c", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -125,10 +125,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf", + "rev": "1319485273bf87833fa472afbcefdedecb16b45f", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0-rc1", + "inputRev": "v4.33.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "LeanMachineLearning", diff --git a/lakefile.toml b/lakefile.toml index 713262e4..27156236 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -12,12 +12,12 @@ weak.linter.mathlibStandardSet = true [[require]] name = "verso" git = "https://github.com/leanprover/verso" -rev = "main" +rev = "v4.33.0-rc2" [[require]] name = "mathlib" scope = "leanprover-community" -rev = "18f56bef5344cefb0563662c495e3eb3824a2589" +rev = "v4.33.0-rc2" [[lean_lib]] name = "LeanMachineLearning" diff --git a/lean-toolchain b/lean-toolchain index 1770ccdb..c084c7fb 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0-rc1 \ No newline at end of file +leanprover/lean4:v4.33.0-rc2