From 4e2b92fea3fe1c470ba69e9d1a2c080143a3ceef Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 05:13:02 -0700
Subject: [PATCH 1/8] Develop Weyl criterion on finite additive tori

---
 .../Equidistribution/UnitAddTorusWeyl.lean    | 126 ++++++++++++++++++
 1 file changed, 126 insertions(+)
 create mode 100644 FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorusWeyl.lean

diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorusWeyl.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorusWeyl.lean
new file mode 100644
index 0000000000..0023c51e02
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorusWeyl.lean
@@ -0,0 +1,126 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib.Analysis.Fourier.AddCircleMulti
+
+@[expose] public section
+
+noncomputable section
+
+open MeasureTheory Filter Topology Set Algebra Submodule
+open scoped ENNReal ComplexConjugate Real
+
+/-- We normalize the measure on `ℝ / ℤ` to have total mass one. -/
+local instance : MeasureSpace UnitAddCircle := ⟨AddCircle.haarAddCircle⟩
+
+local instance : Measure.IsAddHaarMeasure (volume : Measure UnitAddCircle) :=
+  inferInstanceAs (Measure.IsAddHaarMeasure AddCircle.haarAddCircle)
+
+local instance : IsProbabilityMeasure (volume : Measure UnitAddCircle) :=
+  inferInstanceAs (IsProbabilityMeasure AddCircle.haarAddCircle)
+
+namespace UnitAddTorus
+
+variable {d : Type*} [Fintype d]
+
+/-- Weyl's criterion on a finite-dimensional additive unit torus: convergence of the
+averages of every Fourier character implies convergence of the averages of every
+continuous complex-valued function to its Haar integral. -/
+theorem tendsto_average_of_tendsto_mFourier (Y : ℕ → UnitAddTorus d)
+    (hfou : ∀ k : d → ℤ,
+      Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, mFourier k (Y n)) / N) atTop
+        (𝓝 (∫ b, mFourier k b))) :
+    ∀ F : C(UnitAddTorus d, ℂ),
+      Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, F (Y n)) / N) atTop
+        (𝓝 (∫ b, F b)) := by
+  have hint : ∀ g : C(UnitAddTorus d, ℂ), Integrable g volume := fun g =>
+    g.continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _)
+  have hspan : ∀ g ∈ Submodule.span ℂ (Set.range (mFourier (d := d))),
+      Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, g (Y n)) / N) atTop
+        (𝓝 (∫ b, g b)) := by
+    intro g hg
+    induction hg using Submodule.span_induction with
+    | mem g hgmem =>
+        obtain ⟨k, rfl⟩ := hgmem
+        exact hfou k
+    | zero =>
+        simp only [ContinuousMap.zero_apply, Finset.sum_const_zero, zero_div, integral_zero]
+        exact tendsto_const_nhds
+    | add g₁ g₂ _ _ ih₁ ih₂ =>
+        simp only [ContinuousMap.add_apply, Finset.sum_add_distrib, add_div,
+          integral_add (hint g₁) (hint g₂)]
+        exact ih₁.add ih₂
+    | smul c g _ ih =>
+        simp only [ContinuousMap.smul_apply, smul_eq_mul, ← Finset.mul_sum, mul_div_assoc,
+          integral_const_mul]
+        exact ih.const_mul c
+  intro F
+  rw [Metric.tendsto_atTop]
+  intro ε hε
+  have hF : F ∈ closure (Submodule.span ℂ (Set.range (mFourier (d := d))) : Set _) := by
+    rw [← Submodule.topologicalClosure_coe, span_mFourier_closure_eq_top, Submodule.top_coe]
+    exact Set.mem_univ F
+  obtain ⟨p, hp, hdist⟩ := Metric.mem_closure_iff.mp hF (ε / 3) (by positivity)
+  rw [dist_eq_norm] at hdist
+  obtain ⟨N₀, hN₀⟩ := (Metric.tendsto_atTop.mp (hspan p hp)) (ε / 3) (by positivity)
+  refine ⟨N₀, fun N hN => ?_⟩
+  have hbound : ∀ z : UnitAddTorus d, ‖F z - p z‖ ≤ ‖F - p‖ := fun z => by
+    simpa using (F - p).norm_coe_le_norm z
+  have h1 :
+      ‖(∑ n ∈ Finset.range N, F (Y n)) / N -
+          (∑ n ∈ Finset.range N, p (Y n)) / N‖ ≤ ‖F - p‖ := by
+    rw [div_sub_div_same, ← Finset.sum_sub_distrib, norm_div, Complex.norm_natCast]
+    rcases Nat.eq_zero_or_pos N with h | h
+    · simp [h]
+    · rw [div_le_iff₀ (by exact_mod_cast h)]
+      calc
+        ‖∑ n ∈ Finset.range N, (F (Y n) - p (Y n))‖
+            ≤ ∑ n ∈ Finset.range N, ‖F (Y n) - p (Y n)‖ := norm_sum_le _ _
+        _ ≤ ∑ _n ∈ Finset.range N, ‖F - p‖ :=
+          Finset.sum_le_sum (fun n _ => hbound _)
+        _ = ‖F - p‖ * N := by
+          rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_comm]
+  have h2 : ‖(∫ b, p b) - ∫ b, F b‖ ≤ ‖F - p‖ := by
+    rw [← integral_sub (hint p) (hint F)]
+    calc
+      ‖∫ b, (p b - F b)‖ ≤ ∫ b, ‖p b - F b‖ := norm_integral_le_integral_norm _
+      _ ≤ ∫ _b, ‖F - p‖ := by
+        refine integral_mono_of_nonneg (by filter_upwards with z using norm_nonneg _)
+          (integrable_const _) ?_
+        filter_upwards with z
+        rw [norm_sub_rev]
+        exact hbound z
+      _ = ‖F - p‖ := by simp
+  have hN0' := hN₀ N hN
+  rw [dist_eq_norm] at hN0' ⊢
+  have htri :
+      ‖(∑ n ∈ Finset.range N, F (Y n)) / N - ∫ b, F b‖ ≤
+        ‖(∑ n ∈ Finset.range N, F (Y n)) / N -
+            (∑ n ∈ Finset.range N, p (Y n)) / N‖ +
+          ‖(∑ n ∈ Finset.range N, p (Y n)) / N - ∫ b, p b‖ +
+          ‖(∫ b, p b) - ∫ b, F b‖ := by
+    have heq :
+        (∑ n ∈ Finset.range N, F (Y n)) / N - ∫ b, F b =
+          ((∑ n ∈ Finset.range N, F (Y n)) / N -
+              (∑ n ∈ Finset.range N, p (Y n)) / N) +
+            ((∑ n ∈ Finset.range N, p (Y n)) / N - ∫ b, p b) +
+            ((∫ b, p b) - ∫ b, F b) := by ring
+    rw [heq]
+    exact norm_add₃_le
+  linarith [htri, h1, h2, hN0', hdist]
+
+end UnitAddTorus

From aaeba8da3aa41ab9debe6d64af802ffddd82f38d Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 05:25:40 -0700
Subject: [PATCH 2/8] noop

---
 README_DO_NOT_CREATE | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 create mode 100644 README_DO_NOT_CREATE

diff --git a/README_DO_NOT_CREATE b/README_DO_NOT_CREATE
new file mode 100644
index 0000000000..e69de29bb2

From 6bcaeb2cf0f86a0035fd3cf197f5821c56d39f57 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 05:25:47 -0700
Subject: [PATCH 3/8] Remove accidental empty file

---
 README_DO_NOT_CREATE | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 delete mode 100644 README_DO_NOT_CREATE

diff --git a/README_DO_NOT_CREATE b/README_DO_NOT_CREATE
deleted file mode 100644
index e69de29bb2..0000000000

From 250f4a44d787b8bf3e32173b8ab5afc158e3f9ef Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 05:26:08 -0700
Subject: [PATCH 4/8] Mark branch superseded

---
 .../Equidistribution/UnitAddTorus.lean        | 126 ++++++++++++++++++
 1 file changed, 126 insertions(+)
 create mode 100644 FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorus.lean

diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorus.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorus.lean
new file mode 100644
index 0000000000..0023c51e02
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorus.lean
@@ -0,0 +1,126 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib.Analysis.Fourier.AddCircleMulti
+
+@[expose] public section
+
+noncomputable section
+
+open MeasureTheory Filter Topology Set Algebra Submodule
+open scoped ENNReal ComplexConjugate Real
+
+/-- We normalize the measure on `ℝ / ℤ` to have total mass one. -/
+local instance : MeasureSpace UnitAddCircle := ⟨AddCircle.haarAddCircle⟩
+
+local instance : Measure.IsAddHaarMeasure (volume : Measure UnitAddCircle) :=
+  inferInstanceAs (Measure.IsAddHaarMeasure AddCircle.haarAddCircle)
+
+local instance : IsProbabilityMeasure (volume : Measure UnitAddCircle) :=
+  inferInstanceAs (IsProbabilityMeasure AddCircle.haarAddCircle)
+
+namespace UnitAddTorus
+
+variable {d : Type*} [Fintype d]
+
+/-- Weyl's criterion on a finite-dimensional additive unit torus: convergence of the
+averages of every Fourier character implies convergence of the averages of every
+continuous complex-valued function to its Haar integral. -/
+theorem tendsto_average_of_tendsto_mFourier (Y : ℕ → UnitAddTorus d)
+    (hfou : ∀ k : d → ℤ,
+      Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, mFourier k (Y n)) / N) atTop
+        (𝓝 (∫ b, mFourier k b))) :
+    ∀ F : C(UnitAddTorus d, ℂ),
+      Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, F (Y n)) / N) atTop
+        (𝓝 (∫ b, F b)) := by
+  have hint : ∀ g : C(UnitAddTorus d, ℂ), Integrable g volume := fun g =>
+    g.continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _)
+  have hspan : ∀ g ∈ Submodule.span ℂ (Set.range (mFourier (d := d))),
+      Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, g (Y n)) / N) atTop
+        (𝓝 (∫ b, g b)) := by
+    intro g hg
+    induction hg using Submodule.span_induction with
+    | mem g hgmem =>
+        obtain ⟨k, rfl⟩ := hgmem
+        exact hfou k
+    | zero =>
+        simp only [ContinuousMap.zero_apply, Finset.sum_const_zero, zero_div, integral_zero]
+        exact tendsto_const_nhds
+    | add g₁ g₂ _ _ ih₁ ih₂ =>
+        simp only [ContinuousMap.add_apply, Finset.sum_add_distrib, add_div,
+          integral_add (hint g₁) (hint g₂)]
+        exact ih₁.add ih₂
+    | smul c g _ ih =>
+        simp only [ContinuousMap.smul_apply, smul_eq_mul, ← Finset.mul_sum, mul_div_assoc,
+          integral_const_mul]
+        exact ih.const_mul c
+  intro F
+  rw [Metric.tendsto_atTop]
+  intro ε hε
+  have hF : F ∈ closure (Submodule.span ℂ (Set.range (mFourier (d := d))) : Set _) := by
+    rw [← Submodule.topologicalClosure_coe, span_mFourier_closure_eq_top, Submodule.top_coe]
+    exact Set.mem_univ F
+  obtain ⟨p, hp, hdist⟩ := Metric.mem_closure_iff.mp hF (ε / 3) (by positivity)
+  rw [dist_eq_norm] at hdist
+  obtain ⟨N₀, hN₀⟩ := (Metric.tendsto_atTop.mp (hspan p hp)) (ε / 3) (by positivity)
+  refine ⟨N₀, fun N hN => ?_⟩
+  have hbound : ∀ z : UnitAddTorus d, ‖F z - p z‖ ≤ ‖F - p‖ := fun z => by
+    simpa using (F - p).norm_coe_le_norm z
+  have h1 :
+      ‖(∑ n ∈ Finset.range N, F (Y n)) / N -
+          (∑ n ∈ Finset.range N, p (Y n)) / N‖ ≤ ‖F - p‖ := by
+    rw [div_sub_div_same, ← Finset.sum_sub_distrib, norm_div, Complex.norm_natCast]
+    rcases Nat.eq_zero_or_pos N with h | h
+    · simp [h]
+    · rw [div_le_iff₀ (by exact_mod_cast h)]
+      calc
+        ‖∑ n ∈ Finset.range N, (F (Y n) - p (Y n))‖
+            ≤ ∑ n ∈ Finset.range N, ‖F (Y n) - p (Y n)‖ := norm_sum_le _ _
+        _ ≤ ∑ _n ∈ Finset.range N, ‖F - p‖ :=
+          Finset.sum_le_sum (fun n _ => hbound _)
+        _ = ‖F - p‖ * N := by
+          rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_comm]
+  have h2 : ‖(∫ b, p b) - ∫ b, F b‖ ≤ ‖F - p‖ := by
+    rw [← integral_sub (hint p) (hint F)]
+    calc
+      ‖∫ b, (p b - F b)‖ ≤ ∫ b, ‖p b - F b‖ := norm_integral_le_integral_norm _
+      _ ≤ ∫ _b, ‖F - p‖ := by
+        refine integral_mono_of_nonneg (by filter_upwards with z using norm_nonneg _)
+          (integrable_const _) ?_
+        filter_upwards with z
+        rw [norm_sub_rev]
+        exact hbound z
+      _ = ‖F - p‖ := by simp
+  have hN0' := hN₀ N hN
+  rw [dist_eq_norm] at hN0' ⊢
+  have htri :
+      ‖(∑ n ∈ Finset.range N, F (Y n)) / N - ∫ b, F b‖ ≤
+        ‖(∑ n ∈ Finset.range N, F (Y n)) / N -
+            (∑ n ∈ Finset.range N, p (Y n)) / N‖ +
+          ‖(∑ n ∈ Finset.range N, p (Y n)) / N - ∫ b, p b‖ +
+          ‖(∫ b, p b) - ∫ b, F b‖ := by
+    have heq :
+        (∑ n ∈ Finset.range N, F (Y n)) / N - ∫ b, F b =
+          ((∑ n ∈ Finset.range N, F (Y n)) / N -
+              (∑ n ∈ Finset.range N, p (Y n)) / N) +
+            ((∑ n ∈ Finset.range N, p (Y n)) / N - ∫ b, p b) +
+            ((∫ b, p b) - ∫ b, F b) := by ring
+    rw [heq]
+    exact norm_add₃_le
+  linarith [htri, h1, h2, hN0', hdist]
+
+end UnitAddTorus

From 77336dd4dc857db1af99033ff2db0885c570938a Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 05:26:49 -0700
Subject: [PATCH 5/8] noop

---
 README_DO_NOT_CREATE | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 README_DO_NOT_CREATE

diff --git a/README_DO_NOT_CREATE b/README_DO_NOT_CREATE
new file mode 100644
index 0000000000..c1b0730e01
--- /dev/null
+++ b/README_DO_NOT_CREATE
@@ -0,0 +1 @@
+x
\ No newline at end of file

From 26cc3ad0c47cdd8eaa7b183dbacdbe8e63cafc6c Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 05:26:55 -0700
Subject: [PATCH 6/8] Remove accidental marker

---
 README_DO_NOT_CREATE | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 README_DO_NOT_CREATE

diff --git a/README_DO_NOT_CREATE b/README_DO_NOT_CREATE
deleted file mode 100644
index c1b0730e01..0000000000
--- a/README_DO_NOT_CREATE
+++ /dev/null
@@ -1 +0,0 @@
-x
\ No newline at end of file

From aea78e26a89063672c3a5c4a5a77582331dabe2a Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 05:27:02 -0700
Subject: [PATCH 7/8] noop

---
 README_DO_NOT_CREATE | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 README_DO_NOT_CREATE

diff --git a/README_DO_NOT_CREATE b/README_DO_NOT_CREATE
new file mode 100644
index 0000000000..54299a48fb
--- /dev/null
+++ b/README_DO_NOT_CREATE
@@ -0,0 +1 @@
+no
\ No newline at end of file

From 5dfb7daf704daef4201305bf7eb512d46da9643d Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 05:27:10 -0700
Subject: [PATCH 8/8] Remove accidental marker

---
 README_DO_NOT_CREATE | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 README_DO_NOT_CREATE

diff --git a/README_DO_NOT_CREATE b/README_DO_NOT_CREATE
deleted file mode 100644
index 54299a48fb..0000000000
--- a/README_DO_NOT_CREATE
+++ /dev/null
@@ -1 +0,0 @@
-no
\ No newline at end of file