chore: sync Tau Ceti 4d91513, Mathlib 2ddf59c and LML, which brings Statlib

.github/workflows/ci.yml

@@ -220,7 +220,7 @@ jobs:
         # `--iofail`, as in the sandboxed PR build (TauCetiTools' sandbox-build.sh): the build
         # fails if any module, dependencies included, logs a warning or an info message. A plain
         # `lake build` here let main stay green while every PR build failed on deprecation
-        # warnings in LML.
+        # warnings in LML. Statlib, which LML requires, must also build without warnings.
         run: lake build --iofail
 
       # The same shared checks as trusted PR builds, compiled from merged main's sources.

.github/workflows/referee-site.yml

@@ -105,8 +105,8 @@ jobs:
         run: bash scripts/build.sh
 
       # The newest trust-extract release for lean-toolchain. The upstream closure brings in the LML,
-      # Tau Ceti and Mathlib declarations LMLExplore rests on: the site shows them, and the reviews
-      # of them in the imported stores. The kernel checks that each declaration's dependency
+      # Statlib, Tau Ceti and Mathlib declarations LMLExplore rests on: the site shows them, and the
+      # reviews of them in the imported stores. The kernel checks that each declaration's dependency
       # closure is all it needs, proofs included.
       - name: Extract the dataset
         id: extract
@@ -211,9 +211,9 @@ jobs:
         with:
           root: LMLExplore
           dataset: ${{ runner.temp }}/dataset
-          # An editorial claim: the publisher vouches for Mathlib and everything under it. LML and
-          # Tau Ceti are not under Mathlib, so the declarations of theirs that LMLExplore rests on
-          # count as unaudited, unless reviews in the imported stores say otherwise.
+          # An editorial claim: the publisher vouches for Mathlib and everything under it. LML,
+          # Statlib and Tau Ceti are not under Mathlib, so the declarations of theirs that LMLExplore
+          # rests on count as unaudited, unless reviews in the imported stores say otherwise.
           trust: mathlib
           evidence: LeanMachineLearning/LMLExplore-evidence
 

AGENTS.md

@@ -34,14 +34,14 @@ LMLRoadmaps, are what put new material in scope.
 
 ## The dependencies
 
-LMLExplore depends on Mathlib, Tau Ceti and LML, at the exact versions recorded in
-`lake-manifest.json` (their sources are under `.lake/packages/`).
+LMLExplore depends on Mathlib, Tau Ceti, LML and Statlib (which LML requires), at the exact
+versions recorded in `lake-manifest.json` (their sources are under `.lake/packages/`).
 
-- **Reuse what exists.** Before adding a declaration, search all three dependencies as well as
+- **Reuse what exists.** Before adding a declaration, search all four dependencies as well as
   `LMLExplore/` for it, up to renaming, generalisation and definitional unfolding. Material that
   already exists at the pinned version must be used, never restated.
 - **Other projects' plans do not block you.** Tau Ceti's own roadmaps, open pull requests to
-  Mathlib, Tau Ceti or LML, and anything else that is planned but not present at the pinned
+  Mathlib, Tau Ceti, LML or Statlib, and anything else that is planned but not present at the pinned
   versions, are not reasons to wait or to skip a target. Build what the LMLRoadmaps target needs
   here, now. Where such a plan, pull request or Mathlib convention already fixes a name or a
   statement shape, follow it, so that adopting the upstream version later is a deletion plus an
@@ -51,8 +51,8 @@ LMLExplore depends on Mathlib, Tau Ceti and LML, at the exact versions recorded
   declaration, keeping any additional mathematics. After each sync, a scan
   (`scripts/overlap/`) opens one issue labelled `upstream-overlap` per duplicate; resolve such an
   issue by following `scripts/overlap/fix.md`.
-- **Never contribute upstream.** Do not open pull requests or issues in Mathlib, Tau Ceti or LML.
-  Their maintainers decide, by hand, whether to adopt anything from here.
+- **Never contribute upstream.** Do not open pull requests or issues in Mathlib, Tau Ceti, LML or
+  Statlib. Their maintainers decide, by hand, whether to adopt anything from here.
 
 ## The rules of the repo
 

LMLExplore/Analysis/InnerProductSpace/OptimalDesign.lean

@@ -644,7 +644,7 @@ theorem exists_design_inner_moorePenroseInverse_le_finrank_and_card_support_le {
   have : Nontrivial K := Submodule.nontrivial_iff_ne_bot.2 h0
   -- the Kiefer–Wolfowitz theorem in `K` for the preimage of `𝒜`, which is compact and spans `K`
   have h𝒜K : IsCompact (((↑) : K → E) ⁻¹' 𝒜) :=
-    K.closed_of_finiteDimensional.isClosedEmbedding_subtypeVal.isCompact_preimage h𝒜
+    K.isClosed_of_finiteDimensional.isClosedEmbedding_subtypeVal.isCompact_preimage h𝒜
   obtain ⟨w, hw, hu, hle, hcard⟩ :=
     exists_design_inner_ringInverse_le_finrank_and_card_support_le h𝒜K
       Submodule.span_span_coe_preimage

LMLExplore/Bandits/UnitBallFTRL.lean

@@ -282,7 +282,7 @@ theorem isUnbiasedRound_unitBall (b : OrthonormalBasis ι ℝ E) (hm : m ≤ mΩ
       Integrable (fun ω ↦ unitBallEstimate b (a ω) (y ω) o) P :=
     (hyi.norm.const_mul _).mono' ((hY o).mono hm) (hY_le o)
   have := b.toBasis.finiteDimensional_of_finite
-  have : CompleteSpace E := FiniteDimensional.complete ℝ E
+  have : CompleteSpace E := FiniteDimensional.completeSpace ℝ E
   refine
     { le := hm
       integrable_action := integrable_apply_of_measurableSet_preimage (X := X)
@@ -435,7 +435,7 @@ theorem ftrl_integral_regret_le_of_unitBallEstimate (b : OrthonormalBasis ι ℝ
     ∫ ω, ∑ t ∈ range n, y t ω (unitBallAction b (a t ω) (X t ω) - u) ∂P ≤
       (1 - r) * n - log (1 - r) / η + η * Fintype.card ι * n / 2 := by
   have := b.toBasis.finiteDimensional_of_finite
-  have : CompleteSpace E := FiniteDimensional.complete ℝ E
+  have : CompleteSpace E := FiniteDimensional.completeSpace ℝ E
   set A : ℕ → Ω → E := fun t ω ↦ unitBallAction b (a t ω) (X t ω) with hA_def
   set Y : ℕ → Ω → E →L[ℝ] ℝ := fun t ω ↦ unitBallEstimate b (a t ω) (y t ω) (X t ω) with hY_def
   have har (t : ℕ) (ht : t ≤ n) : ∀ᵐ ω ∂P, ‖a t ω‖ ≤ r := by

LMLExplore/Identification/DifficultyRatio.lean

@@ -7,7 +7,7 @@ module
 
 public import LMLExplore.Identification.ErrorLowerBound
 public import LMLExplore.InformationTheory.KullbackLeibler.Bernoulli
-import LMLExplore.Data.EReal.Inv
+import Statlib.ForMathlib.EReal
 
 /-!
 # Difficulty ratios and complexity of fixed-budget identification, and their lower bounds

LMLExplore/InformationTheory/KullbackLeibler/Bernoulli.lean

@@ -11,11 +11,11 @@ public import Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
 public import LMLExplore.Probability.Distributions.Bernoulli
 public import TauCeti.InformationTheory.KullbackLeibler.Basic
 public import TauCeti.InformationTheory.KullbackLeibler.Pinsker
-public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
+public import Statlib.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing
 public import TauCeti.InformationTheory.KullbackLeibler.Variational
 import Mathlib.Analysis.Complex.ExponentialBounds
-import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Convex
+import Statlib.Divergence.KullbackLeibler.Basic
 
 /-!
 # The binary relative entropy
@@ -747,7 +747,7 @@ theorem klBer_add_klBer_le {r : ℝ} (hpq : p ≤ q) (hqr : q ≤ r) :
 `a, b ≥ 0` with `a + b = 1`, `d(a p + b p', a q + b q') ≤ a d(p, q) + b d(p', q')`, the values
 `∞` included. The Bernoulli law of a mixture of two parameters is the mixture of the two
 Bernoulli laws (`ProbabilityTheory.bernoulliMeasure_eq_smul_add_smul`), and the relative entropy
-is jointly convex (`InformationTheory.klDiv_smul_add_smul_le`). In particular `d` is convex in
+is jointly convex (`ProbabilityTheory.klDiv_smul_add_smul_le`). In particular `d` is convex in
 each argument [LS, Lemma 10.2]. -/
 theorem klBer_mul_add_mul_le {p' q' : ℝ} (hp : p ∈ Set.Icc 0 1) (hq : q ∈ Set.Icc 0 1)
     (hp' : p' ∈ Set.Icc 0 1) (hq' : q' ∈ Set.Icc 0 1) {a b : ℝ≥0} (hab : a + b = 1) :

LMLExplore/InformationTheory/KullbackLeibler/ChainRule.lean

@@ -5,7 +5,7 @@ Authors: LMLExplore contributors
 -/
 module
 
-public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
+public import Statlib.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Restrict
 public import TauCeti.Probability.Kernel.Composition.MeasureCompProd

LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean

@@ -12,7 +12,7 @@ import Mathlib.MeasureTheory.Integral.Bochner.Set
 import Mathlib.MeasureTheory.Integral.IntegrableOn
 import Mathlib.MeasureTheory.VectorMeasure.Integral
 import LMLExplore.Order.ConditionallyCompleteLattice.Group
-import TauCeti.MeasureTheory.Measure.TotalVariation
+import TauCeti.MeasureTheory.Measure.TotalVariation.Basic
 
 /-!
 # Integrals against measures close in total variation

LMLExplore/Probability/Distributions/Bernoulli.lean

@@ -180,7 +180,7 @@ parameter is clamped to `[0, 1]` by `Set.projIcc`, so that the kernel is defined
 noncomputable def bernoulliKernel : Kernel ℝ ℝ where
   toFun x := Ber((1 : ℝ), 0, Set.projIcc 0 1 zero_le_one x)
   measurable' :=
-    (TauCeti.Probability.measurable_bernoulliMeasure _ _).comp continuous_projIcc.measurable
+    measurable_const.bernoulliMeasure measurable_const continuous_projIcc.measurable
 
 @[simp]
 lemma bernoulliKernel_apply (x : ℝ) :

LMLExplore/Probability/Distributions/ExponentialFamily/Bernoulli.lean

@@ -339,7 +339,6 @@ private lemma map_deriv_cgf_withDensity_jeffreysPrior_bernoulliMeasure_sigmoid
   -- the density `g` on `(0, 1)`
   have hmap := TauCeti.MeasureTheory.map_withDensity_abs_deriv_mul
     (φ := fun η ↦ Real.sigmoid (η₀ + η)) (f := g) MeasurableSet.univ
-    (continuous_sigmoid.comp (continuous_const_add η₀)).measurable
     (fun η _ ↦ ((Real.hasDerivAt_sigmoid (η₀ + η)).comp_const_add η₀ η).hasDerivWithinAt)
     (Real.sigmoid_strictMono.comp (strictMono_id.const_add η₀)).injective.injOn
   have hrange : range (fun η ↦ Real.sigmoid (η₀ + η)) = Ioo 0 1 := by

LMLExplore/Probability/HasCondDistrib.lean

@@ -99,6 +99,7 @@ lemma HasCondDistrib.lintegral_comp_prodMk_eq_lintegral_lintegral (h : HasCondDi
     _ = ∫⁻ ω, ∫⁻ y, g (X ω, y) ∂(κ (X ω)) ∂P :=
         lintegral_map' hg.lintegral_kernel_prod_right'.aemeasurable h.aemeasurable_fst
 
+omit [IsSFiniteKernel κ] in
 /-- If `κ` is the conditional distribution of `Y` given `X` under `P`, it is also the conditional
 distribution of `Y` given `X` under the restriction of `P` to an event `X ⁻¹' s` determined by
 `X`. -/

LMLExplore/Probability/Kernel/Composition/Comp.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Probability.Kernel.Composition.Comp
 public import Mathlib.Probability.Kernel.Invariance
+public import TauCeti.Probability.Kernel.Composition.Power
 
 /-!
 # The monoid of kernels from a space to itself
@@ -16,8 +17,8 @@ Mathlib's monoid structure on `Kernel α α` has unit `Kernel.id` and product th
 facts as lemmas, in the form of Mathlib's `Module.End.one_eq_id` and `Module.End.mul_eq_comp`, so
 that statements about powers of kernels can be rewritten into compositions. It also provides the
 instances stating that the powers of a Markov kernel are Markov kernels, and the powers of an
-s-finite kernel are s-finite kernels, and that a measure invariant for a kernel is invariant for
-all its powers (`ProbabilityTheory.Kernel.Invariant.pow`).
+s-finite kernel are s-finite kernels. That a measure invariant for a kernel is invariant for all its
+powers is Tau Ceti's `ProbabilityTheory.Kernel.Invariant.pow`.
 -/
 
 public section
@@ -48,11 +49,4 @@ instance (κ : Kernel α α) [IsSFiniteKernel κ] (n : ℕ) : IsSFiniteKernel (
   | zero => rw [pow_zero, one_eq_id]; infer_instance
   | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance
 
-/-- An invariant measure of `κ` is invariant for all its powers. -/
-lemma Invariant.pow {κ : Kernel α α} {π : Measure α} (hπ : κ.Invariant π) (n : ℕ) :
-    (κ ^ n).Invariant π := by
-  induction n with
-  | zero => simp [Invariant, one_eq_id]
-  | succ n ih => rw [pow_succ, mul_eq_comp]; exact ih.comp hπ
-
 end ProbabilityTheory.Kernel

LMLExplore/Probability/Kernel/Primitive.lean

@@ -7,7 +7,7 @@ module
 
 public import LMLExplore.Probability.Kernel.Dobrushin
 public import Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
-public import TauCeti.Probability.Kernel.Matrix
+public import TauCeti.Probability.Kernel.Matrix.Basic
 
 /-!
 # Primitive Markov chains on finite spaces

LMLExplore/Probability/Moments/SubGaussian/Simplex.lean

@@ -54,7 +54,7 @@ theorem log_sum_mul_exp_le {w : α → ℝ} (hw : w ∈ simplex α) {ℓ : α 
   rw [hsplit, ← le_div_iff₀' (exp_pos _), ← exp_sub] at h
   rw [log_le_iff_le_exp hpos]
   refine h.trans_eq (congrArg exp ?_)
-  simp only [NNReal.coe_pow, NNReal.coe_div, coe_nnnorm, Real.norm_eq_abs, NNReal.coe_ofNat,
+  simp only [NNReal.coe_pow, NNReal.coe_div, coe_nnNorm, Real.norm_eq_abs, NNReal.coe_ofNat,
     div_pow, sq_abs]
   ring
 

LMLExplore/Probability/Moments/SubGaussian/Sum.lean

@@ -232,7 +232,7 @@ private lemma sum_tailBound_le (hσ2 : σ2 ≠ 0) (hε : 0 < ε) (hc : 0 ≤ c)
     rw [intervalIntegral.integral_of_le (Nat.cast_nonneg m)] at h_sum
     have h_mono : ∫ t in Ioc 0 (m : ℝ), tailBound σ2 ε c t ≤ ∫ t in Ioi 0, tailBound σ2 ε c t :=
       setIntegral_mono_set hint (ae_of_all _ fun t ↦ (exp_pos _).le)
-        Ioc_subset_Ioi_self.eventuallyLE
+        Ioc_subset_Ioi_self.eventuallySubset
     have h_zero := tailBound_le_one σ2 ε c 0
     push_cast at h_sum ⊢
     linarith

LMLExplore/Probability/Moments/Tilted.lean

@@ -154,7 +154,7 @@ lemma tilted_mul_apply_mem_Icc (ht : Integrable (fun ω ↦ exp (t * X ω)) μ)
   have h_mono {f g : Ω → ℝ} (h : ∀ ω ∈ A, f ω ≤ g ω) :
       ∫⁻ ω in A, ENNReal.ofReal (exp (f ω)) ∂μ ≤ ∫⁻ ω in A, ENNReal.ofReal (exp (g ω)) ∂μ :=
     lintegral_mono_ae ((ae_restrict_iff'₀ hA).2 (ae_of_all _ fun ω hω ↦ by gcongr; exact h ω hω))
-  rw [← measure_congr ((tilted_absolutelyContinuous _ _).ae_eq hA.toMeasurable_ae_eq),
+  rw [← measure_congr ((tilted_absolutelyContinuous _ _).ae_le hA.toMeasurable_ae_eq),
     tilted_mul_apply_cgf' (measurableSet_toMeasurable _ _) ht,
     setLIntegral_congr hA.toMeasurable_ae_eq, ← setLIntegral_const, ← setLIntegral_const]
   exact ⟨h_mono fun ω hω ↦ by linarith [(hX ω hω).1], h_mono fun ω hω ↦ by linarith [(hX ω hω).2]⟩

LMLExplore/Probability/Moments/Variance.lean

@@ -58,7 +58,7 @@ theorem Measurable.variance_kernel {η : Kernel β δ} [IsSFiniteKernel η] {X :
     hX.stronglyMeasurable.integral_kernel.measurable
   refine ENNReal.measurable_toReal.comp (Measurable.lintegral_kernel_prod_right'
     (f := fun p : β × δ ↦ ‖X p.2 - ∫ z, X z ∂(η p.1)‖ₑ ^ 2) ?_)
-  exact ((hX.comp measurable_snd).sub (h_mean.comp measurable_fst)).enorm.pow_const 2
+  exact ((hX.comp measurable_snd).sub (h_mean.comp measurable_fst)).eNorm.pow_const 2
 
 namespace ProbabilityTheory
 

LMLExplore/SequentialLearning/Algorithm.lean

@@ -184,9 +184,9 @@ lemma IsAlgEnvSeq.integrable_feedback [SFinite P] [OpensMeasurableSpace 𝓨]
     (hY : ∫⁻ ω, ∫⁻ y, ‖y‖ₑ ∂(env.feedbackKernel O A Y n ω (A n ω)) ∂P ≠ ∞) :
     Integrable (Y n) P := by
   refine ⟨(h.measurable_feedback n).aestronglyMeasurable, ?_⟩
-  have h_eq := h.setLIntegral_comp_feedback (n := n) MeasurableSet.univ measurable_enorm
+  have h_eq := h.setLIntegral_comp_feedback (n := n) MeasurableSet.univ measurable_eNorm
   simp only [Measure.restrict_univ] at h_eq
-  rw [hasFiniteIntegral_iff_enorm, h_eq]
+  rw [hasFiniteIntegral_iff_eNorm, h_eq]
   exact hY.lt_top
 
 variable [NormedSpace ℝ 𝓨]

LMLExplore/SequentialLearning/DivergenceDecomposition.lean

@@ -271,12 +271,12 @@ private lemma tsum_klDiv_restrict_compProd_stepKernel_eq_lintegral
   have hf (t : ℕ) : Measurable fun ω ↦
       klDiv (stepKernel alg env t (history IT.obs IT.action IT.feedback t ω))
         (stepKernel alg' env' t (history IT.obs IT.action IT.feedback t ω)) :=
-    (measurable_klDiv_kernel _ _).comp (hH t)
+    (measurable_klDiv _ _).comp (hH t)
   refine (tsum_congr fun t ↦ ?_).trans
     (tsum_setLIntegral_notStoppedSet IT.measurable_obs IT.measurable_action IT.measurable_feedback
       hS hτ hf)
-  rw [klDiv_compProd_right_eq_lintegral,
-    setLIntegral_map (measurableSet_notStoppedSet hS t) (measurable_klDiv_kernel _ _) (hH t)]
+  rw [← condKL, condKL_eq_lintegral,
+    setLIntegral_map (measurableSet_notStoppedSet hS t) (measurable_klDiv _ _) (hH t)]
 
 /-- **Chain rule at a stopping time**, integral form. For two algorithms `alg`, `alg'` run against
 two environments `env`, `env'` with countably generated spaces of observations, actions and
@@ -342,7 +342,7 @@ lemma IsAlgEnvSeq.klDiv_map_history_eq_sum_pullCount
   have hsum : ∑ t ∈ range M, ∫⁻ ω, klDiv (κ (A t ω)) (κ' (A t ω)) ∂P =
       ∫⁻ ω, ∑ t ∈ range M, klDiv (κ (A t ω)) (κ' (A t ω)) ∂P :=
     (lintegral_finsetSum _ fun t _ ↦
-      (measurable_klDiv_kernel κ κ').comp (h.measurable_action t)).symm
+      (measurable_klDiv κ κ').comp (h.measurable_action t)).symm
   rw [h.klDiv_map_history_bandit h' M, hsum]
   exact (LMLExplore.sum_lintegral_pullCount_mul (g := fun _ ↦ M) h.measurable_action
     measurable_const fun a ↦ klDiv (κ a) (κ' a)).symm
@@ -411,8 +411,8 @@ lemma IsAlgEnvSeq.klDiv_restrict_compProd_stepKernel_bandit
         ((P.map fun ω ↦ ((history O A Y t ω, O t ω), A t ω)).restrict
           ((s ×ˢ .univ) ×ˢ .univ) ⊗ₘ κ'.prodMkLeft _) := by
     rw [stepKernel_bandit, stepKernel_bandit, klDiv_compProd_assoc, klDiv_compProd_assoc, h_joint]
-  rw [h_assoc, klDiv_compProd_right_eq_lintegral,
-    setLIntegral_map ((hs.prod .univ).prod .univ) (measurable_klDiv_kernel _ _) hX]
+  rw [h_assoc, ← condKL, condKL_eq_lintegral,
+    setLIntegral_map ((hs.prod .univ).prod .univ) (measurable_klDiv _ _) hX]
   have h_pre : (fun ω ↦ ((history O A Y t ω, O t ω), A t ω)) ⁻¹' ((s ×ˢ .univ) ×ˢ .univ) =
       history O A Y t ⁻¹' s := by
     ext; simp
@@ -441,7 +441,7 @@ private lemma tsum_klDiv_restrict_compProd_stepKernel_bandit_eq_sum (hS : Measur
     IT.measurable_obs IT.measurable_action IT.measurable_feedback hS
   have hf (t : ℕ) : Measurable fun ω : ℕ → Round Unit 𝓐 𝓨 ↦
       klDiv (κ (IT.action t ω)) (κ' (IT.action t ω)) :=
-    (measurable_klDiv_kernel κ κ').comp (IT.measurable_action t)
+    (measurable_klDiv κ κ').comp (IT.measurable_action t)
   refine ((tsum_congr fun t ↦ h.klDiv_restrict_compProd_stepKernel_bandit (κ' := κ')
       (measurableSet_notStoppedSet hS t)).trans
         (tsum_setLIntegral_notStoppedSet IT.measurable_obs IT.measurable_action