Blueprint work

PhD.lean

@@ -1 +1 @@
-import PhD.Example
+import PhD.RPS.def

PhD/RPS/def.lean

@@ -0,0 +1,181 @@
+/-
+Copyright (c) 2025 William Coram. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: William Coram
+-/
+
+import Mathlib.Algebra.Group.NatPowAssoc
+import Mathlib.Analysis.Normed.Group.Ultra
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.RingTheory.PowerSeries.Basic
+
+/-!
+# Restricted power series
+
+We say a powerseries over a normed ring `R` is restricted for a parameter `c` if
+`‖coeff R i f‖ * c^i → 0`.
+
+## Main results
+
+- `IsGroup`: for a normed ring `R` the set of restricted power series forms an additive group.
+- `IsRing`: if `R` is a normed ring with the ultrametric property then the set of restricted
+  power series forms a ring.
+
+-/
+
+namespace PowerSeries
+
+open PowerSeries Filter
+open scoped Topology
+
+/-- A power series over `R` is restricted of paramerter `c` if we have the following limit. -/
+def IsRestricted (R : Type*) [NormedRing R] (f : PowerSeries R) (c : ℝ) :=
+  Tendsto (fun (i : ℕ) => (norm (coeff R i f)) * c^i) atTop (𝓝 0)
+
+namespace Restricted
+
+variable (R : Type*) [NormedRing R] (c : ℝ)
+
+lemma Equiv_cToAbs (f : PowerSeries R) : IsRestricted R f c ↔ IsRestricted R f |c| := by
+  simp_rw [IsRestricted, NormedAddCommGroup.tendsto_atTop, sub_zero, norm_mul, norm_norm, norm_pow,
+    Real.norm_eq_abs, abs_abs]
+
+/-- The set of restricted power series over `R` for a parameter `c`. -/
+def SetOf : Set (PowerSeries R) :=
+  {f : PowerSeries R | IsRestricted R f c}
+
+lemma zero : IsRestricted R 0 c := by
+  simp_rw [IsRestricted, map_zero, norm_zero, zero_mul, tendsto_const_nhds_iff]
+
+lemma one : IsRestricted R 1 c := by
+  simp_rw [IsRestricted, coeff_one, NormedAddCommGroup.tendsto_atTop, sub_zero, norm_mul, norm_norm,
+    norm_pow, Real.norm_eq_abs]
+  intro ε hε
+  refine ⟨1, fun n hn => ?_ ⟩
+  simpa only [Nat.ne_zero_of_lt hn, ↓reduceIte, norm_zero, zero_mul] using hε
+
+lemma add {f g : PowerSeries R} (hf : IsRestricted R f c) (hg : IsRestricted R g c) :
+    IsRestricted R (f + g) c := by
+  simp only [IsRestricted, map_add, NormedAddCommGroup.tendsto_atTop] at hf hg ⊢
+  intro ε hε
+  obtain ⟨fN, hfN⟩ := hf (ε/2) (half_pos hε)
+  obtain ⟨gN, hgN⟩ := hg (ε/2) (half_pos hε)
+  simp only [sub_zero, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at hfN hgN
+  refine ⟨max fN gN, fun n hn => ?_ ⟩
+  simp only [sub_zero, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm]
+  exact lt_of_le_of_lt  (by simpa only [right_distrib] using (mul_le_mul_of_nonneg_right
+    (norm_add_le (coeff R n f) (coeff R n g)) (pow_nonneg (abs_nonneg c) n)))
+    (by simpa only [add_halves] using (add_lt_add (hfN n (le_of_max_le_left hn))
+    (hgN n (le_of_max_le_right hn))))
+
+lemma neg {f : PowerSeries R} (hf : IsRestricted R f c) : IsRestricted R (-f) c := by
+  simpa only [IsRestricted, map_neg, norm_neg] using hf
+
+/-- The set of restricted power series over `R` for a parameter `c` forms an additive subgroup of
+    power series over `R`. -/
+def addsubgroup : AddSubgroup (PowerSeries R) where
+  carrier := (SetOf R c)
+  zero_mem' := zero R c
+  add_mem' := add R c
+  neg_mem' := neg R c
+
+/-- The restricted power series over a normed ring `R` for a parameter `c ∈ ℝ` forms an additive
+    group. -/
+instance IsGroup : AddGroup (SetOf R c) :=
+  AddSubgroup.toAddGroup (addsubgroup R c)
+
+/-- The set of `‖coeff R i f‖ * c^i` for a given power series `f` and parameter `c`. -/
+def convergenceSet (f : PowerSeries R) : Set ℝ :=
+  {‖coeff R i f‖ * c^i | i : ℕ}
+
+lemma BddAbove {f : PowerSeries R} (hf : IsRestricted R f c) : BddAbove (convergenceSet R c f) := by
+  simp_rw [IsRestricted, NormedAddCommGroup.tendsto_atTop] at hf
+  obtain ⟨N, hf⟩ := by simpa only [zero_lt_one, sub_zero, norm_mul, norm_norm, norm_pow,
+    Real.norm_eq_abs, forall_const, abs_norm] using (hf 1)
+  simp_rw [bddAbove_def, convergenceSet]
+  use max 1 (Finset.max' (Finset.image (fun i => ‖coeff R i f‖ * c^i) (Finset.range (N+1)))
+    (by simp only [Finset.image_nonempty, Finset.nonempty_range_iff, ne_eq,
+    AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false,
+    not_false_eq_true]))
+  simp only [Set.mem_setOf_eq, le_sup_iff, forall_exists_index, forall_apply_eq_imp_iff]
+  intro i
+  rcases (Nat.le_total i N) with h | h
+  · right
+    apply Finset.le_max'
+    simp only [Finset.mem_image, Finset.mem_range]
+    exact ⟨i, by exact Order.lt_add_one_iff.mpr h, rfl⟩
+  · exact Or.inl (le_of_lt (lt_of_le_of_lt (mul_le_mul_of_nonneg_left
+      (by simpa only [abs_pow] using le_abs_self (c ^ i)) (norm_nonneg _)) (hf i h)))
+
+lemma BddAbove_nneg {f : PowerSeries R} (hf : IsRestricted R f c) :
+     ∃ A, A > 0 ∧ ∀ i, ‖coeff R i f‖ * c^i ≤ A := by
+  obtain ⟨n, hn⟩ := by simpa only [bddAbove_def] using (BddAbove R c hf)
+  simp_rw [convergenceSet, Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at hn
+  rcases (eq_zero_or_neZero n) with h | h
+  · refine ⟨n + 1, ⟨by simp_rw [h, zero_add, gt_iff_lt, zero_lt_one], fun i => le_trans (hn i)
+    (by simp_rw [h, zero_add, zero_le_one])⟩⟩
+  · exact ⟨|n|, by simpa only [gt_iff_lt, abs_pos] using Ne.symm (NeZero.ne' n),
+    fun i => le_trans (hn i) (le_abs_self n)⟩
+
+variable [IsUltrametricDist R]
+
+open IsUltrametricDist
+
+lemma mul {f g : PowerSeries R} (hf : IsRestricted R f c) (hg : IsRestricted R g c) :
+    IsRestricted R (f * g) c := by
+  simp_rw [IsRestricted] at hf hg ⊢
+  obtain ⟨a, ha, fBound1⟩ := BddAbove_nneg R |c| ((Equiv_cToAbs R c f).mp hf)
+  obtain ⟨b, hb, gBound1⟩ := BddAbove_nneg R |c| ((Equiv_cToAbs R c g).mp hg)
+  rw [NormedAddCommGroup.tendsto_atTop] at hf hg ⊢
+  intro ε hε
+  simp only [sub_zero, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at hf hg ⊢
+  simp_rw [PowerSeries.coeff_mul]
+  obtain ⟨Nf, fBound2⟩ := (hf (ε/ (max a b))) (div_pos hε (lt_sup_of_lt_left ha))
+  obtain ⟨Ng, gBound2⟩ := (hg (ε/ (max a b))) (div_pos hε (lt_sup_of_lt_left ha))
+  refine ⟨2 * max Nf Ng,  fun n hn => ?_⟩
+  obtain ⟨i, hi, ultrametric⟩ := exists_norm_finset_sum_le (Finset.antidiagonal n)
+    (fun a => (coeff R a.1) f * (coeff R a.2) g)
+  have hi := by simpa only [Finset.mem_antidiagonal] using hi (⟨(0,n), by simp only
+    [Finset.mem_antidiagonal, zero_add]⟩)
+  have InterimBound1 := mul_le_mul_of_nonneg_right ultrametric (pow_nonneg (abs_nonneg c) n)
+  have InterimBound2 := mul_le_mul_of_nonneg_right
+    (NormedRing.norm_mul_le ((coeff R i.1) f) ((coeff R i.2) g)) (pow_nonneg (abs_nonneg c) n)
+  have : ‖(coeff R i.1) f‖ * ‖(coeff R i.2) g‖ * |c|^n =
+      ‖(coeff R i.1) f‖ * |c|^i.1 * (‖(coeff R i.2) g‖ * |c|^i.2) := by
+    ring_nf
+    simp_rw [mul_assoc, ← npow_add, hi]
+  simp only [this] at InterimBound2
+  have : i.1 ≥ max Nf Ng ∨ i.2 ≥ max Nf Ng := by
+    omega
+  rcases this with this | this
+  · have FinalBound := mul_lt_mul_of_lt_of_le_of_nonneg_of_pos ((fBound2 i.1)
+      (le_of_max_le_left this)) (gBound1 i.2) (Left.mul_nonneg (norm_nonneg ((coeff R i.1) f))
+      (pow_nonneg (abs_nonneg c) i.1)) hb
+    exact lt_of_lt_of_le (lt_of_le_of_lt (le_trans InterimBound1 InterimBound2) FinalBound)
+      (by simpa only [div_mul_comm] using ((mul_le_iff_le_one_left hε).mpr
+      ((div_le_one₀ (lt_sup_of_lt_left ha)).mpr (le_max_right a b))))
+  · have FinalBound := mul_lt_mul_of_le_of_lt_of_nonneg_of_pos (fBound1 i.1) ((gBound2 i.2)
+      (le_of_max_le_right this)) (Left.mul_nonneg (norm_nonneg ((coeff R i.2) g))
+      (pow_nonneg (abs_nonneg c) i.2)) ha
+    exact lt_of_lt_of_le (lt_of_le_of_lt (le_trans InterimBound1 InterimBound2) FinalBound)
+      (by simpa only [mul_div_left_comm] using ((mul_le_iff_le_one_right hε).mpr
+      ((div_le_one₀ (lt_sup_of_lt_left ha)).mpr (le_max_left a b))))
+
+/-- The set of restricted power series over `R` for a parameter `c` are a subring of power series
+    over `R`. -/
+def subring : Subring (PowerSeries R) where
+  carrier := SetOf R c
+  zero_mem' := zero R c
+  add_mem' := add R c
+  neg_mem' := neg R c
+  one_mem' := one R c
+  mul_mem' := mul R c
+
+/-- The restricted power series over a normed ring `R` with the ultrametric property forms a
+    ring. -/
+noncomputable
+instance IsRing : Ring (SetOf R c) :=
+    Subring.toRing (subring R c)
+
+end Restricted
+end PowerSeries

README.md

@@ -1,198 +1,3 @@
-# Lean 4 Project Template
+Ongoing PhD project to formalise quaternionic modular forms and results on the slopes of compact Hecke operator.
 
-[![License: Apache 2.0](https://img.shields.io/badge/License-Apache_2.0-lightblue.svg)](https://opensource.org/licenses/Apache-2.0)
-[![Zulip : Topic](https://img.shields.io/badge/Zulip-Topic-%237E57C2.svg?logo=zulip&logoColor=white)](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Tutorial.3A.20Getting.20Started.20with.20Blueprint-Driven.20Projects)
-[![YouTube : Tutorial](https://img.shields.io/badge/YouTube-Tutorial-%23FF0000.svg?logo=youtube&logoColor=white)](https://youtu.be/KyuyTsLgkMY)
-
-This repository contains a template for blueprint-driven formalization projects in Lean 4.
-
-## Install Lean 4
-
-Ensure that you have a functioning Lean 4 installation. If you do not, please follow
-the [Lean installation guide](https://leanprover-community.github.io/get_started.html).
-
-## Use this Template
-
-To create a new repository using this template, ensure you are on the correct repository page
-([LeanProject](https://github.com/pitmonticone/LeanProject)) and then follow these steps:
-
-1. Click the **Use this template** button located at the top right of the repository page.
-2. Click the **Create a new repository** button.
-3. Select the account or organization where you want to create it, choose a name for the new
-repository, and click the **Create repository** button.
-
-## Clone this Repository
-
-To clone this repository to your local machine, please refer to the relevant section of the
-GitHub documentation [here](https://docs.github.com/en/repositories/creating-and-managing-repositories/cloning-a-repository).
-
-## Customize this Template
-
-To tailor this template to your specific project, follow these steps:
-
-1. If you don't have a Python environment, you can install one by following the instructions in the
-[Python installation guide](https://www.python.org/downloads/).
-1. Verify your Python installation by running:
-    ```bash
-    python3 --version
-    ```
-1. Verify your Pip installation by running:
-    ```bash
-    pip3 --version
-    ```
-1. Ensure your terminal is in the project directory by running the following command:
-    ```bash
-    cd path/to/your/project
-    ```
-1.	Execute the customization script by running:
-    ```bash
-    scripts/customize_template.py NewProject
-    ```
-    where `NewProject` must be replaced by the name of your project.
-
-The script [`customize_template.py`](scripts/customize_template.py) will automatically rename the
-project folder and update the necessary files and configurations to match the new project name.
-
-## Configure GitHub Pages
-
-To set up GitHub Pages for your repository, follow these steps:
-
-1. Go to the **Settings** tab of your repository.
-2. In the left sidebar, click on the **Pages** section.
-3. In the **Source** dropdown, select `GitHub Actions`.
-
-## Repository Layout
-
-The template repository is organized as follows (listing the main folders and files):
-
-- [`.github`](.github) contains GitHub-specific configuration files and workflows.
-    - [`workflows`](.github/workflows) contains GitHub Actions workflow files.
-        - [`build-project.yml`](.github/workflows/build-project.yml) defines the workflow for building
-        the Lean project on pushes, pull requests, and manual triggers. This is a minimalistic build
-        workflow which is not necessary if you decide to generate a blueprint (see instructions below)
-        and can be manually disabled by clicking on the **Actions** tab, selecting **Build Project**
-        in the left sidebar, then clicking the horizontal triple dots (⋯) on the right,
-        and choosing **Disable workflow**.
-        - [`create-release.yml`](.github/workflows/create-release.yml): defines the workflow for creating a new Git tag and GitHub release when the `lean-toolchain` file is updated in the `main` branch. Ensure the following settings are configured under **Settings > Actions > General > Workflow permissions**: "Read and write permissions" and "Allow GitHub Actions to create and approve pull requests".
-        - [`update.yml`](.github/workflows/update.yml) is the dependency
-        update workflow to be triggered manually by default. [It's not documented yet, but it will be soon.]
-    - [`dependabot.yml`](.github/dependabot.yml) is the configuration file to automate CI dependency updates.
-- [`.vscode`](.vscode) contains Visual Studio Code configuration files
-    - [`extensions.json`](.vscode/extensions.json) recommends VS Code extensions for the project.
-    - [`settings.json`](.vscode/settings.json) defines the project-specific settings for VS Code.
-- [`Project`](Project) should contain the Lean code files.
-    - [`Mathlib`](Project/Mathlib) should contain `.lean` files with declarations missing from the
-    current version of Mathlib.
-    - [`Example.lean`](Project/Example.lean) is a sample Lean file.
-- [`scripts`](scripts) contains scripts to update Mathlib ensuring that the latest version is
-fetched and integrated into the development environment.
-- [`.gitignore`](.gitignore) specifies files and folders to be ignored by Git.
-and environment.
-- [`CODE_OF_CONDUCT.md`](CODE_OF_CONDUCT.md) should contain the code of conduct for the project.
-- [`CONTRIBUTING.md`](CONTRIBUTING.md) should provide the guidelines for contributing to the
-project.
-- [`lakefile.toml`](lakefile.toml) is the configuration file for the Lake build system used in
-Lean projects.
-- [`lean-toolchain`](lean-toolchain) specifies the Lean version and toolchain used for the project.
-
-## Blueprint
-
-### 0. Selected Collaborative Projects
-
-- [Fermat's Last Theorem for Exponent 3](https://pitmonticone.github.io/FLT3/) by Riccardo Brasca et al.
-- [Polynomial Freiman-Ruzsa Conjecture](https://github.com/teorth/pfr) by Terence Tao et al.
-- [Fermat's Last Theorem](https://imperialcollegelondon.github.io/FLT/) by Kevin Buzzard et al.
-- [Carleson Operators on Doubling Metric Measure Spaces](http://florisvandoorn.com/carleson/) by Floris van Doorn et al.
-- [Bonn Collaborative Formalization Seminar Series in Analysis](https://github.com/fpvandoorn/BonnAnalysis) by Floris van Doorn et al.
-- [Prime Number Theorem and More](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd) by Alex Kontorovich et al.
-- [Infinity Cosmos](https://github.com/emilyriehl/infinity-cosmos) by Emily Riehl et al.
-- [Analytic Number Theory Exponent Database](https://github.com/teorth/expdb) by Terence Tao et al.
-- [Groupoid Model of Homotopy Type Theory](https://github.com/sinhp/GroupoidModelofHoTTinLean4) by Sina Hazratpour et al.
-- [Equational Theories](https://github.com/teorth/equational_theories) by Terence Tao et al.
-
-For more examples of completed and ongoing Lean projects and libraries, please
-see the [Lean Reservoir](https://reservoir.lean-lang.org).
-
-### 1. Install Dependencies
-
-To install the necessary dependencies, follow the instructions in the
-[PyGraphViz installation guide](https://pygraphviz.github.io/documentation/stable/install.html).
-
-### 2. Install LeanBlueprint Package
-
-Assuming you have a properly configured Python environment, install LeanBlueprint by running:
-
-```bash
-pip install leanblueprint
-```
-
-If you have an existing installation of LeanBlueprint, you can upgrade to the latest version by
-running:
-
-```bash
-pip install -U leanblueprint
-```
-
-### 3. Configure Blueprint
-
-To set up the blueprint for your project, run:
-
-```bash
-leanblueprint new
-```
-
-Then, follow the prompts and answer the questions as you like, except for a few specific
-questions which should be answered as indicated below to ensure compatibility with this template.
-
-Respond affirmatively with `y` to the following prompt:
-
-```console
-Proceed with blueprint creation? [y/n]
-```
-
-Respond affirmatively with `y` to the following prompt:
-
-```console
-Modify lakefile and lake-manifest to allow checking declarations exist? [y/n] (y)
-```
-
-Respond affirmatively with `y` to the following prompt:
-
-```console
-Modify lakefile and lake-manifest to allow building the documentation? [y/n] (y):
-```
-
-If you want to generate a Jekyll-based home page for the project, respond
-affirmatively with `y` to the following prompt:
-
-```console
-Do you want to create a home page for the project, with links to the blueprint, the API documentation and the repository? [y/n]:
-```
-
-Respond affirmatively with `y` to the following prompt:
-
-```console
-Configure continuous integration to compile blueprint? [y/n] (y):
-```
-
-For more details about the LeanBlueprint package and its commands, please refer to its
-[documentation](https://github.com/PatrickMassot/leanblueprint/tree/master#starting-a-blueprint).
-
-After configuring the blueprint, please wait for the GitHub Action workflow to finish.
-You can keep track of the progress in the **Actions** tab of your repository.
-
-## Selected Projects Using this Template
-
-If you have used this template to create your own Lean project and would like to share it with the community, please consider opening a [PR](https://github.com/pitmonticone/LeanProject/pulls) to add your project to this list:
-
-- [Infinity Cosmos](https://github.com/emilyriehl/infinity-cosmos) by Emily Riehl et al.
-- [Analytic Number Theory Exponent Database](https://github.com/teorth/expdb) by Terence Tao et al.
-- [Equational Theories](https://github.com/teorth/equational_theories) by Terence Tao et al.
-- [Groupoid Model of Homotopy Type Theory](https://github.com/sinhp/GroupoidModelofHoTTinLean4) by Sina Hazratpour et al.
-- [Soundness of FRI](https://github.com/BoltonBailey/FRISoundness) by Bolton Bailey et al.
-- [Weil's Converse Theorem](https://github.com/CBirkbeck/WeilConverse) by Chris Birkbeck et al.
-- [Proofs from THE BOOK](https://github.com/mo271/FormalBook) by Moritz Firsching et al.
-- [Automata Theory](https://github.com/shetzl/autth) by Stefan Hetzl et al.
-- [Dirichlet Nonvanishing](https://github.com/CBirkbeck/DirichletNonvanishing) by Chris Birkbeck et al.
-- [Seymour's Decomposition Theorem](https://github.com/Ivan-Sergeyev/seymour) by Ivan Sergeyev et al.
-- [Spectral Theorem](https://github.com/oliver-butterley/SpectralThm) by Oliver Butterley and Yoh Tanimoto.
+More information and progress can be found in the [blueprint](https://williamcoram.github.io/PhD/blueprint/sect0001.html).