update mathlib, fix FourierD

Polya.lean

@@ -2,3 +2,5 @@
 -- Import modules here that should be built as part of the library.
 import «Polya».MiscLemmas
 import «Polya».RegularizedOccupation
+import «Polya».GreenFourier
+import «Polya».FourierD

Polya/FourierD.lean

@@ -120,7 +120,7 @@ instance : IsProbabilityMeasure (haarAddTorus (Ts := Ts)) :=
 
 /-- The canonical map fun from `ℝᵈ / ℤᵈ ⬝ Ts` to the standard multiplicative
 torus (product of unit circles in ℂ). -/
-def toTorus (x : AddTorus Ts) : ∀ (_ : ι), circle  := fun i ↦ AddCircle.toCircle (x i)
+def toTorus (x : AddTorus Ts) : ∀ (_ : ι), Circle  := fun i ↦ AddCircle.toCircle (x i)
 
 end AddTorus
 
@@ -129,7 +129,7 @@ open AddTorus
 section Monomials
 
 variable {ι : Type u} {Ts : ι → ℝ}
-variable [hTs : ∀ i, Fact (0 < Ts i)]
+-- variable [hTs : ∀ i, Fact (0 < Ts i)]
 
 /-- The family of exponential monomials `fun x => exp (2 π i n ⬝ x / Ts)`, parametrized by `n : ℤ` and
 considered as bundled continuous maps from `ℝ / ℤ • T` to `ℂ`. -/
@@ -143,11 +143,15 @@ def fourierD [Fintype ι] (ns : ι → ℤ) : C(AddTorus Ts, ℂ) where
 lemma fourierD_apply [Fintype ι] {ns : ι → ℤ} {x : AddTorus Ts} :
     fourierD ns x = ∏ (i : ι), AddCircle.toCircle ((ns i) • (AddTorus.proj (Ts := Ts) i x)) := by
   simp [fourierD]
+  rw [← @SubmonoidClass.coe_finset_prod]
 
 @[simp] lemma fourierD_coe_apply [Fintype ι] {ns : ι → ℤ} {xs : ι → ℝ} :
     fourierD ns (AddTorus.mk Ts xs)
       = Complex.exp (∑ i, 2 * π * Complex.I * (ns i) * (xs i) / (Ts i)) := by
-  simp [fourierD_apply, AddTorus.mk, Complex.exp_sum]
+  simp [fourierD_apply, Complex.exp_sum]
+  rw [@SubmonoidClass.coe_finset_prod]
+  simp only [fourier_coe_apply']
+
 
 -- -- Q: Do we want `SMul (ι → ℤ) (AddTorus Ts)` for this to typecheck?
 --@[simp]

Polya/MiscLemmas.lean

@@ -7,10 +7,6 @@ open ENNReal NNReal
 
 section Auxiliary
 
--- This `@[simp]`lemma should be soon added to Mathlib (there is a PR including this already).
-@[simp] lemma ENNReal.toNNReal_toReal_eq (z : ℝ≥0∞) : z.toReal.toNNReal = z.toNNReal := by
-  ext; simp only [Real.coe_toNNReal', ge_iff_le, toReal_nonneg, max_eq_left]; rfl
-
 /-- The (topological) sum of `ℝ≥0∞` valued functions evaluated at a point is the (topological)
 sum of the evaluations of those functions.  -/
 lemma tsum_pi_ennreal_apply {ι α : Type*} (fs : ι → α → ℝ≥0∞) (a : α) :

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f27beb10b53350d6c1257ba3a8899df369135cc3",
+   "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "rev": "2b2f6d7fbe9d917fc010e9054c1ce11774c9088b",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
+   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,37 +35,47 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.39",
+   "inputRev": "v0.0.42",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "scope": "leanprover",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "7376ac07aa2b0492372c056b7a2c3163b3026d1e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "4b61d4abc1659f15ffda5ec24fdebc229d51d066",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "863c4af0d6a201265dd01536ebc81d129a972f63",
+   "rev": "90cf978d2237de99eb5a639301b5b0b3f913d744",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -75,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "21a36f3c07a9229e1287483c16a0dd04e479ecc5",
+   "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce",
    "name": "checkdecls",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
+   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f93115d0209de6db335725dee900d379f40c0317",
+   "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f",
+   "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -115,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04",
+   "rev": "ccb4e97ffb7ad0f9b1852e9669d5e2922f984175",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -19,4 +19,4 @@ require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 
 meta if get_config? env = some "dev" then
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "main"
+  "https://github.com/leanprover/doc-gen4" @ "main"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc2
+leanprover/lean4:v4.13.0-rc3