Update to v4.36.0-rc1

LMLTutorial/Pages/MarkovKernels.lean

@@ -13,6 +13,7 @@ set_option linter.style.header false
 set_option linter.style.setOption false
 set_option linter.hashCommand false
 set_option linter.style.longLine false
+set_option linter.style.emptyLine false
 set_option pp.rawOnError true
 set_option verso.code.warnLineLength 100
 

LMLTutorial/Pages/Martingales.lean

@@ -13,6 +13,7 @@ set_option linter.style.header false
 set_option linter.style.setOption false
 set_option linter.hashCommand false
 set_option linter.style.longLine false
+set_option linter.style.emptyLine false
 set_option pp.rawOnError true
 set_option verso.code.warnLineLength 100
 

LMLTutorial/Tutorial.lean

@@ -12,12 +12,12 @@ set_option linter.style.setOption false
 
 @[expose] public section
 
-open Verso.Genre.Manual Verso.Output.Html
+open Verso.Genre.Manual
 
 def extraHead : Array Verso.Output.Html := #[
-  {{<link rel="icon" type="image/x-icon" href="static/favicon.svg"/>}},
-  {{<link rel="stylesheet" href="static/style.css"/>}},
-  {{<script src="static/scripts.js"></script>}},
+  html%{<link rel="icon" type="image/x-icon" href="static/favicon.svg"/>},
+  html%{<link rel="stylesheet" href="static/style.css"/>},
+  html%{<script src="static/scripts.js"></script>},
 ]
 
 def config : RenderConfig := {

LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/MapSequence.lean

@@ -89,8 +89,10 @@ lemma klDiv_eq_iSup_map {β : ℕ → Type*} [mβ : ∀ n, MeasurableSpace (β n
       (measurable_const.indicator hA).stronglyMeasurable.mono hℱ_sup.symm.le
     have hlim := hφ_int.tendsto_ae_condExp (ℱ := ℱ) hφ_meas
     set B : ℕ → Set α := fun n ↦ {x | (2⁻¹ : ℝ) < (ρ[φ | ℱ n]) x} with hB
-    have hB_meas : ∀ n, MeasurableSet[ℱ n] (B n) := fun n ↦
-      (stronglyMeasurable_condExp (m := ℱ n)).measurable measurableSet_Ioi
+    have hB_meas : ∀ n, MeasurableSet[ℱ n] (B n) := fun n ↦ by
+      have : B n = (ρ[φ | ℱ n]) ⁻¹' Set.Ioi 2⁻¹ := by ext; simp [hB]
+      rw [this]
+      exact (stronglyMeasurable_condExp (m := ℱ n)).measurable measurableSet_Ioi
     have hB_meas0 : ∀ n, MeasurableSet (B n) := fun n ↦ ℱ.le n _ (hB_meas n)
     have hB_lim : ∀ᵐ x ∂ρ, ∀ᶠ n in atTop, x ∈ B n ↔ x ∈ A := by
       filter_upwards [hlim] with x hx

LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Embedding.lean

@@ -160,8 +160,9 @@ lemma finSuccProd_apply {X : Type*} [MeasurableSpace X] (n : ℕ)
 lemma finSuccProd_symm_apply {X : Type*} [MeasurableSpace X] (n : ℕ)
     (p : (Fin n → X) × X) :
     (finSuccProd X n).symm p = Fin.snoc p.1 p.2 := by
-  simp [finSuccProd]
-  rfl
+  simp only [finSuccProd, trans_symm, trans_apply, piFinSuccAbove_symm_apply,
+    Fin.insertNthEquiv_last, Fin.snocEquiv_apply, Fin.snoc_inj]
+  exact ⟨rfl, rfl⟩
 
 end Fin
 

LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean

@@ -78,7 +78,8 @@ lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂
   constructor
   · intro hf x hx
     rw [← hf]
-    exact Classical.choose.congr_simp hx (exists_argmax x)
+    exact Classical.choose.congr_simp (funext fun j ↦ propext (Set.ext_iff.mp hx j))
+      (exists_argmax x)
   · intro h
     exact h f rfl
 

LeanMachineLearning/SequentialLearning/StoppedHistory.lean

@@ -80,8 +80,8 @@ lemma measurable_hittingAfter_sigmaHistory (hS : MeasurableSet S) :
       · infer_instance
     simp only [ENat.some_eq_natCast, this, Set.preimage_compl]
     exact (measurable_sigmaHistory hO hX hY n hS).inter
-      (MeasurableSet.biInter (Set.to_countable _) fun j _ ↦
-        measurable_sigmaHistory hO hX hY j hS.compl)
+      (MeasurableSet.iInter fun j ↦ MeasurableSet.iInter fun _ ↦
+        (measurable_sigmaHistory hO hX hY j hS).compl)
 
 @[fun_prop]
 lemma measurable_stoppedValue_sigmaHistory (hτ : Measurable τ) :

LeanMachineLearning/Tactic/KernelHom/Tactic/KernelDiagram.lean

@@ -59,7 +59,6 @@ def Node.toPenroseVar_kernel (n : Node) : MetaM PenroseVar := do
       pure n.e
   return ⟨"E", [n.vPos, n.hPosSrc, n.hPosTar], expr⟩
 
-open scoped Jsx in
 /-- Construct a kernelized string diagram from a Penrose `sub`stance program and
 expressions `embeds` to display as labels in the diagram. -/
 def mkKernelDiagram (nodes : List (List Node)) (strands : List (List Strand)) :
@@ -90,7 +89,6 @@ end Mathlib.Tactic.Widget.StringDiagram
 
 namespace KernelDiagram
 
-open scoped Jsx in
 /-- Given a kernel expression, return a string diagram. Otherwise `none`. -/
 def KernelM? (e : Expr) : MetaM (Option Html) := do
   let e ← instantiateMVars e
@@ -118,24 +116,23 @@ def KernelM? (e : Expr) : MetaM (Option Html) := do
         trace[string_diagram] "Penrose substance: \n{(← get).sub}"
         match ← DiagramBuilderM.buildDiagram StringDiagram.dsl StringDiagram.sty with
         | some html => return html
-        | none => return <span>No non-structural morphisms found.</span>
+        | none => return jsx%{<span>No non-structural morphisms found.</span>}
   catch _ => return none
 
-open scoped Jsx in
 /-- Help function for displaying two string diagrams in an equality. -/
 def mkEqHtml (lhs rhs : Html) : Html :=
-  <div className="flex">
+  jsx%{<div className="flex">
     <div className="w-50">
-      <details «open»={true}>
-        <summary className="mv2 pointer">Kernel diagram for LHS</summary> {lhs}
+      <details open={true}>
+        <summary className="mv2 pointer">Kernel diagram for LHS</summary>{lhs}
       </details>
     </div>
     <div className="w-50">
-      <details «open»={true}>
-        <summary className="mv2 pointer">Kernel diagram for RHS</summary> {rhs}
+      <details open={true}>
+        <summary className="mv2 pointer">Kernel diagram for RHS</summary>{rhs}
       </details>
     </div>
-  </div>
+  </div>}
 
 /-- Given an equality between kernels, return a string diagram of the LHS and RHS.
 Otherwise `none`. -/
@@ -155,7 +152,6 @@ def kernelEqMReduce? (e : Expr) : MetaM (Option Html) := do
   forallTelescopeReducing (← whnfR <| ← inferType e) fun _ expr => do
     kernelEqM? expr
 
-open scoped Jsx in
 /-- The RPC method for displaying kernel diagrams. -/
 @[server_rpc_method]
 def rpc (props : PanelWidgetProps) : RequestM (RequestTask Html) :=
@@ -169,7 +165,7 @@ def rpc (props : PanelWidgetProps) : RequestM (RequestTask Html) :=
           let type ← g.mvarId.getType
           kernelEqM? type)
     match html with
-    | none => return <span>No Kernel Diagram.</span>
+    | none => return jsx%{<span>No Kernel Diagram.</span>}
     | some inner => return inner
 
 end KernelDiagram

lake-manifest.json

@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "56a005855ea17e0b0958f73ec801ae140b0a1679",
+   "rev": "625d8914199bc567cca9b91f90e8e5afafa5ae51",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "56a005855ea17e0b0958f73ec801ae140b0a1679",
+   "inputRev": "625d8914199bc567cca9b91f90e8e5afafa5ae51",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "01a09f320122475119588526857a07d218aef600",
+   "rev": "f7a4dc6867f8df27778b2b320763ec9e3b7be070",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0-rc4",
+   "inputRev": "v4.36.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dfa4f38190d07c37e315953e08b90fe2d95b3c24",
+   "rev": "c2d7840c65673533e15b499f25beecdc6227f7d8",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d6b4c7be5be75ec4917c873ac50c756dc1436372",
+   "rev": "9d39f9bb0c30aa2f6200808805ff16e6ce950890",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93",
+   "rev": "b3cc36c295aa5e3e3c0197b09a6556298e710447",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "df72b022e558978a1c50264cfc4d7fec86fa8e04",
+   "rev": "17137fad38a2cc782ff00b323a13c3a991d085ab",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4a174c490d8707121c4a9290800489f105d85e07",
+   "rev": "cbdde3aa2665915fb286c48bcd4cdf885c629511",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dce0ad79c486cb1fb504af04f953c3466b0c6db8",
+   "rev": "6d26f8bb4b2bb78f929ad160feac508866821316",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "66e469188fe07963e5cf666c7d4433f45b8131c5",
+   "rev": "4453b52d2468f4c346a8711d728c0742e7483c9b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,17 +95,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8",
+   "rev": "34d2efffcb6dc8d5f3537cf6a7f88bfaa999ec49",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0",
+   "inputRev": "v4.36.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/illuminate",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "86aa7e62f42b2a82daf9692b191febde1f3d65f9",
+   "rev": "d22e76ef3d2a925132315af902ea432233b4a44a",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.toml

@@ -12,12 +12,12 @@ weak.linter.mathlibStandardSet = true
 [[require]]
 name = "verso"
 git = "https://github.com/leanprover/verso"
-rev = "v4.35.0-rc4"
+rev = "v4.36.0-rc1"
 
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "56a005855ea17e0b0958f73ec801ae140b0a1679"
+rev = "625d8914199bc567cca9b91f90e8e5afafa5ae51"
 
 [[lean_lib]]
 name = "LeanMachineLearning"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.35.0
+leanprover/lean4:v4.36.0-rc1