From 033f29165e7977a33db52cc41302aedc3ba22066 Mon Sep 17 00:00:00 2001 From: WilliamCoram Date: Fri, 31 Oct 2025 11:43:05 +0000 Subject: [PATCH 1/4] bump --- PhD/Mathlib/PR'd/RPS.lean | 153 ++++++++++++ PhD/RPS/RestrictedMV.lean | 375 ++++++++++++++++++++++++++++ PhD/RPS/def.lean | 273 ++++++++------------ blueprint/src/chapter/GaussNorm.tex | 7 +- blueprint/src/chapter/RPS.tex | 92 +++---- blueprint/src/macro/print.tex | 2 + blueprint/src/macro/web.tex | 2 + lake-manifest.json | 36 +-- lean-toolchain | 2 +- 9 files changed, 712 insertions(+), 230 deletions(-) create mode 100644 PhD/Mathlib/PR'd/RPS.lean create mode 100644 PhD/RPS/RestrictedMV.lean diff --git a/PhD/Mathlib/PR'd/RPS.lean b/PhD/Mathlib/PR'd/RPS.lean new file mode 100644 index 0000000..96508bf --- /dev/null +++ b/PhD/Mathlib/PR'd/RPS.lean @@ -0,0 +1,153 @@ +/- +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.Analysis.Normed.Group.Ultra +import Mathlib.Analysis.RCLike.Basic +import Mathlib.RingTheory.PowerSeries.Basic +import Mathlib.Tactic.Bound + +/-! +# Restricted power series + +`IsRestricted` : We say a power series over a normed ring `R` is restricted for a parameter `c` if +`‖coeff R i f‖ * c ^ i → 0`. + +-/ + +namespace PowerSeries + +variable {R : Type*} [NormedRing R] (c : ℝ) + +open PowerSeries Filter +open scoped Topology + +/-- A power series over `R` is restricted of paramerter `c` if we have +`‖coeff R i f‖ * c ^ i → 0`. -/ +def IsRestricted (f : PowerSeries R) := + Tendsto (fun (i : ℕ) ↦ (norm (coeff i f)) * c ^ i) atTop (𝓝 0) + +namespace IsRestricted + +lemma isRestricted_iff {f : PowerSeries R} : IsRestricted c f ↔ + ∀ ε, 0 < ε → ∃ N, ∀ n, N ≤ n → ‖‖(coeff n) f‖ * c ^ n‖ < ε := by + simp [IsRestricted, NormedAddCommGroup.tendsto_atTop] + +lemma isRestricted_iff_abs (f : PowerSeries R) : IsRestricted c f ↔ IsRestricted |c| f := by + simp [isRestricted_iff] + +lemma zero : IsRestricted c (0 : PowerSeries R) := by + simp [IsRestricted] + +lemma one : IsRestricted c (1 : PowerSeries R) := by + simp only [isRestricted_iff, coeff_one, norm_mul, norm_pow, Real.norm_eq_abs] + refine fun _ _ ↦ ⟨1, fun n hn ↦ ?_ ⟩ + split + · omega + · simpa + +lemma monomial (n : ℕ) (a : R) : IsRestricted c (monomial n a) := by + simp only [monomial_eq_mk, isRestricted_iff, coeff_mk, norm_mul, norm_pow, + Real.norm_eq_abs, abs_norm] + refine fun _ _ ↦ ⟨n + 1, fun _ _ ↦ ?_⟩ + split + · omega + · simpa + +lemma C (a : R) : IsRestricted c (C a) := by + simpa [monomial_zero_eq_C_apply] using monomial c 0 a + +lemma add {f g : PowerSeries R} (hf : IsRestricted c f) (hg : IsRestricted c g) : + IsRestricted c (f + g) := by + simp only [isRestricted_iff, map_add, norm_mul, norm_pow, Real.norm_eq_abs] at ⊢ hf hg + intro ε hε + obtain ⟨fN, hfN⟩ := hf (ε / 2) (by positivity) + obtain ⟨gN, hgN⟩ := hg (ε / 2) (by positivity) + simp only [abs_norm] at hfN hgN ⊢ + refine ⟨max fN gN, fun n hn ↦ ?_ ⟩ + calc _ ≤ ‖(coeff n) f‖ * |c| ^ n + ‖(coeff n) g‖ * |c| ^ n := by grw [norm_add_le, add_mul] + _ < ε / 2 + ε / 2 := by gcongr <;> grind + _ = ε := by ring + +lemma neg {f : PowerSeries R} (hf : IsRestricted c f) : IsRestricted c (-f) := by + simpa [isRestricted_iff] using hf + +lemma smul {f : PowerSeries R} (hf : IsRestricted c f) (r : R) : IsRestricted c (r • f) := by + if h : r = 0 then (simpa [h] using zero c) else + simp_rw [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at ⊢ hf + intro ε _ + obtain ⟨n, hn⟩ := hf (ε / ‖r‖) (by positivity) + refine ⟨n, fun N hN ↦ ?_⟩ + calc _ ≤ ‖r‖ * ‖(coeff N) f‖ * |c| ^ N := + mul_le_mul_of_nonneg (norm_mul_le _ _) (by simp) (by simp) (by simp) + _ < ‖r‖ * (ε / ‖r‖) := by + rw [mul_assoc]; aesop + _ = ε := mul_div_cancel₀ _ (by aesop) + + +/-- 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 i f‖ * c^i | i : ℕ} + +open Finset in +lemma convergenceSet_BddAbove {f : PowerSeries R} (hf : IsRestricted c f) : + BddAbove (convergenceSet c f) := by + simp_rw [isRestricted_iff] at hf + obtain ⟨N, hf⟩ := by simpa using (hf 1) + rw [bddAbove_def, convergenceSet] + use max 1 (max' (image (fun i ↦ ‖coeff i f‖ * c ^ i) (range (N + 1))) (by simp)) + simp only [Set.mem_setOf_eq, le_sup_iff, forall_exists_index, forall_apply_eq_imp_iff] + intro i + rcases le_total i N with h | h + · right + apply le_max' + simp only [mem_image, mem_range] + exact ⟨i, by omega, rfl⟩ + · left + calc _ ≤ ‖(coeff i) f‖ * |c ^ i| := by bound + _ ≤ 1 := by simpa using (hf i h).le + +variable [IsUltrametricDist R] + +open IsUltrametricDist + +lemma mul {f g : PowerSeries R} (hf : IsRestricted c f) (hg : IsRestricted c g) : + IsRestricted c (f * g) := by + obtain ⟨a, ha, fBound1⟩ := (bddAbove_iff_exists_ge 1).mp (convergenceSet_BddAbove _ + ((isRestricted_iff_abs c f).mp hf)) + obtain ⟨b, hb, gBound1⟩ := (bddAbove_iff_exists_ge 1).mp (convergenceSet_BddAbove _ + ((isRestricted_iff_abs c g).mp hg)) + simp only [convergenceSet, Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] + at fBound1 gBound1 + simp only [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm, + PowerSeries.coeff_mul] at ⊢ hf hg + intro ε hε + obtain ⟨Nf, fBound2⟩ := (hf (ε / (max a b))) (by positivity) + obtain ⟨Ng, gBound2⟩ := (hg (ε / (max a b))) (by positivity) + refine ⟨2 * max Nf Ng, fun n hn ↦ ?_⟩ + obtain ⟨⟨fst, snd⟩, hi, ultrametric⟩ := exists_norm_finset_sum_le (Finset.antidiagonal n) + (fun a ↦ (coeff a.1) f * (coeff a.2) g) + obtain ⟨rfl⟩ := by simpa using hi (⟨(0, n), by simp⟩) + calc _ ≤ ‖(coeff fst) f * (coeff snd) g‖ * |c| ^ (fst + snd) := by bound + _ ≤ ‖(coeff fst) f‖ * |c| ^ fst * (‖(coeff snd) g‖ * |c| ^ snd) := by + grw [norm_mul_le]; grind + have : max Nf Ng ≤ fst ∨ max Nf Ng ≤ snd := by omega + rcases this with this | this + · calc _ < ε / max a b * b := by + grw [gBound1 snd] + gcongr + exact fBound2 fst (by omega) + _ ≤ ε := by + rw [div_mul_comm, mul_le_iff_le_one_left ‹_›] + bound + · calc _ < a * (ε / max a b) := by + grw [fBound1 fst] + gcongr + exact gBound2 snd (by omega) + _ ≤ ε := by + rw [mul_div_left_comm, mul_le_iff_le_one_right ‹_›] + bound + +end IsRestricted +end PowerSeries diff --git a/PhD/RPS/RestrictedMV.lean b/PhD/RPS/RestrictedMV.lean new file mode 100644 index 0000000..6f7361b --- /dev/null +++ b/PhD/RPS/RestrictedMV.lean @@ -0,0 +1,375 @@ +import Mathlib + +namespace MvPowerSeries + +open MvPowerSeries Filter +open scoped Topology + +abbrev range_sum {σ : Type*} [Fintype σ] : (σ →₀ ℕ) → ℕ := + fun n ↦ ∑ i : σ, n i + +lemma range_sum_add {σ : Type*} [Fintype σ] (a b : σ →₀ ℕ) : + range_sum (a + b) = range_sum (a) + range_sum (b) := by + exact Finset.sum_add_distrib + +lemma range_sum_smul {σ : Type*} [Fintype σ] (a : σ →₀ ℕ) (n : ℕ) : + range_sum (n • a) = n * range_sum a := by + unfold range_sum + simp only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul] + rw [Finset.mul_sum] + +instance {σ : Type*} [Fintype σ] : LE (σ →₀ ℕ) where le f g := (range_sum f) ≤ (range_sum g) + +lemma le_def {σ : Type*} [Fintype σ] {f g : σ →₀ ℕ} : f ≤ g ↔ (range_sum f) ≤ (range_sum g) := .rfl + +instance {σ : Type*} [Fintype σ] : LT (σ →₀ ℕ) where lt f g := (range_sum f) < (range_sum g) + +lemma lt_def {σ : Type*} [Fintype σ] {f g : σ →₀ ℕ} : f < g ↔ (range_sum f) < (range_sum g) := .rfl + +instance preorder {σ : Type*} [Fintype σ] : Preorder (σ →₀ ℕ) where + le_refl _ := by + rw [le_def] + le_trans _ _ _ := by + exact Nat.le_trans + lt_iff_le_not_ge a b := by + simp_rw [le_def, lt_def, not_le, iff_and_self] + exact Nat.le_of_succ_le + +def le_total {σ : Type*} [Fintype σ] (a b : σ →₀ ℕ) : a ≤ b ∨ b ≤ a := by + simp_rw [le_def] + exact Nat.le_total _ _ + +instance {σ : Type*} [Fintype σ] : IsDirected (σ →₀ ℕ) (fun (a b : (σ →₀ ℕ)) ↦ (a ≤ b)) where + directed a b := by + rcases le_total a b with h | h + · use b + · use a + +def IsRestricted {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] + (f : MvPowerSeries σ R) := + Tendsto (fun (t : σ →₀ ℕ) ↦ (norm (coeff t f)) * c^(range_sum t)) atTop (𝓝 0) + +namespace IsRestricted + +lemma isRestricted_iff {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] + {f : MvPowerSeries σ R} : IsRestricted c f ↔ ∀ ε, 0 < ε → ∃ (N : σ →₀ ℕ), + ∀ (n : σ →₀ ℕ), N ≤ n → ‖‖(coeff n) f‖ * c^(range_sum n)‖ < ε := by + simp [IsRestricted, NormedAddCommGroup.tendsto_atTop] + +lemma isRestricted_iff_abs {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] + (f : MvPowerSeries σ R) : IsRestricted c f ↔ IsRestricted |c| f := by + simp [isRestricted_iff] + +lemma zero {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] : + IsRestricted c (0 : MvPowerSeries σ R) := by + simp [IsRestricted] + +lemma monomial {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] (n : σ →₀ ℕ) + (a : R) : IsRestricted c (monomial n a) := by + let I := Classical.typeDecidableEq σ + simp_rw [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm, coeff_monomial] + · obtain ⟨m, hm⟩ : ∃ m : σ →₀ ℕ, n < m := by + use n + (Finsupp.equivFunOnFinite.symm (fun (i : σ) ↦ 1)) + simp_rw [lt_def, range_sum_add, lt_add_iff_pos_right, range_sum, + Finsupp.equivFunOnFinite_symm_apply_toFun, Finset.sum_const, Finset.card_univ, smul_eq_mul, + mul_one] + exact Fintype.card_pos + refine fun _ _ ↦ ⟨m, fun N hN ↦ ?_⟩ + split + · grind + · aesop + +lemma one {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] : + IsRestricted c (1 : MvPowerSeries σ R) := by + exact monomial c 0 1 + +lemma C {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] (a : R) : + IsRestricted c (C (σ := σ) a) := by + simpa [monomial_zero_eq_C_apply] using monomial c 0 a + +lemma add {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] + {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) : + IsRestricted c (f + g) := by + simp only [isRestricted_iff, map_add, norm_mul, norm_pow, Real.norm_eq_abs] at ⊢ hf hg + intro ε hε + obtain ⟨fN, hfN⟩ := hf (ε / 2) (by positivity) + obtain ⟨gN, hgN⟩ := hg (ε / 2) (by positivity) + simp only [abs_norm] at hfN hgN ⊢ + -- at this point I want to be using max fN gN... but I have not defined it properly, could do this + -- if prefered; this also causes a similar use of rcases in mul... + rcases le_total fN gN with h | h + · refine ⟨gN, fun n hn ↦ ?_ ⟩ + calc _ ≤ ‖(coeff n) f‖ * |c| ^ (range_sum n) + ‖(coeff n) g‖ * |c| ^ (range_sum n) := by + grw [norm_add_le, add_mul] + _ < ε / 2 + ε / 2 := by + have := Preorder.le_trans fN gN n h hn + gcongr <;> aesop + _ = ε := by ring + · refine ⟨fN, fun n hn ↦ ?_ ⟩ + calc _ ≤ ‖(coeff n) f‖ * |c| ^ (range_sum n) + ‖(coeff n) g‖ * |c| ^ (range_sum n) := by + grw [norm_add_le, add_mul] + _ < ε / 2 + ε / 2 := by + have := Preorder.le_trans gN fN n h hn + gcongr <;> aesop + _ = ε := by ring + +lemma smul {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] + {f : MvPowerSeries σ R} (hf : IsRestricted c f) (r : R) : IsRestricted c (r • f) := by + if h : r = 0 then simpa [h] using zero c else + simp_rw [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at ⊢ hf + intro ε _ + obtain ⟨n, hn⟩ := hf (ε / ‖r‖) (by positivity) + refine ⟨n, fun N hN ↦ ?_⟩ + calc _ ≤ ‖r‖ * ‖(coeff N) f‖ * |c| ^ (range_sum N) := + mul_le_mul_of_nonneg (norm_mul_le _ _) (by simp) (by simp) (by simp) + _ < ‖r‖ * (ε / ‖r‖) := by + rw [mul_assoc]; aesop + _ = ε := mul_div_cancel₀ _ (by aesop) + +lemma nsmul {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] (n : ℕ) + (f : MvPowerSeries σ R) (hf : IsRestricted c f) : IsRestricted c (n • f) := by + convert IsRestricted.smul c hf (n : R) + ext _ _ + simp_rw [map_smul, smul_eq_mul, map_nsmul, nsmul_eq_mul] + +lemma zsmul {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] (n : ℤ) + (f : MvPowerSeries σ R) (hf : IsRestricted c f) : IsRestricted c (n • f) := by + convert IsRestricted.smul c hf (n : R) + ext _ _ + simp_rw [map_smul, smul_eq_mul, map_zsmul, zsmul_eq_mul] + +/-- The set of `‖coeff n f‖ * c ^ (range_sum n)` for a given power series `f` and parameter `c`. -/ +def convergenceSet {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] + (f : MvPowerSeries σ R) : Set ℝ := {‖(coeff n) f‖ * c^(range_sum n) | n : (σ →₀ ℕ)} + +def set_lt {σ : Type*} [Fintype σ] (n : σ →₀ ℕ) : Set (σ →₀ ℕ) := + {a : σ →₀ ℕ | a ≤ n} + +lemma set_lt_isFinite {σ : Type*} [Fintype σ] (n : σ →₀ ℕ) : Finite (set_lt n) := by + let I := Classical.typeDecidableEq σ + simp only [set_lt, le_def, Set.coe_setOf] + have : { a : σ →₀ ℕ // range_sum a ≤ range_sum n } = + ⋃ i : Finset.range ((range_sum n) + 1), {a : σ →₀ ℕ | range_sum a = i} := by + simp_rw [Set.coe_eq_subtype, Set.mem_iUnion, Set.mem_setOf_eq, Subtype.exists, Finset.mem_range, + exists_prop, exists_eq_right', Nat.lt_add_one_iff] + rw [this] + have (i : Finset.range ((range_sum n) + 1)) : Finite {a : σ →₀ ℕ | range_sum a = i} := by + simp only [Set.coe_setOf] + have (a : σ →₀ ℕ) (t : ℕ) (h : range_sum a = t) : ∀ i, a i ≤ t := by + intro i + unfold range_sum at h + rw [← h] + have : ∑ n, a n = a i + ∑ n with n ≠ i, a n := by + have : a i = ∑ i ∈ {i}, a i := by + rfl + rw [this] + have h : {i} ∪ ({n | n ≠ i} : (Finset σ)) = + Finset.univ := by + ext j + simpa using eq_or_ne j i + have : ∑ n, a n = ∑ n ∈ {i} ∪ ({n | n ≠ i} : (Finset σ)), a n := by + exact congrFun (congrArg Finset.sum (id (Eq.symm h))) fun n ↦ a n + simp_rw [this] + simp only [ne_eq, Finset.singleton_union, Finset.mem_filter, Finset.mem_univ, + not_true_eq_false, and_false, not_false_eq_true, Finset.sum_insert, Finset.sum_singleton] + -- has to be a better way to do this + simp_rw [this] + grind + have incl : {a : σ →₀ ℕ | range_sum a = i} ⊆ {a : σ →₀ ℕ | ∀ x, a x ≤ i} := by + exact fun ⦃a⦄ ↦ this a ↑i + have incl_fin : Finite {a : σ →₀ ℕ | ∀ x, a x ≤ i} := by + -- we show this injects into functions (σ → Fin (i + 1)); which is of finite cardinality + let J : {a : σ →₀ ℕ | ∀ x, a x ≤ i} → (σ → Fin (i + 1)) := + fun b ↦ fun j ↦ ⟨b.1 j, Nat.lt_succ_of_le (b.2 j)⟩ + have inj : Function.Injective J := by + exact injective_of_le_imp_le J fun {x y} a ↦ a -- no idea how this works... + exact Finite.of_injective J inj + exact Finite.Set.subset ({a : σ →₀ ℕ | ∀ x, a x ≤ i}) incl + exact Set.finite_iUnion this + +lemma set_lt_Nonempty {σ : Type*} [Fintype σ] (n : σ →₀ ℕ) : Nonempty (set_lt n) := by + use n + simp [set_lt] + +open Finset in +lemma convergenceSet_BddAbove {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] + [Nonempty σ] {f : MvPowerSeries σ R} (hf : IsRestricted c f) : + BddAbove (convergenceSet c f) := by + simp_rw [isRestricted_iff] at hf + obtain ⟨N, hf⟩ := by simpa using (hf 1) + rw [bddAbove_def, convergenceSet] + use max 1 (max' (image (fun i ↦ ‖coeff i f‖ * c ^ (range_sum i)) + ((Set.Finite.toFinset (set_lt_isFinite N)))) (by simpa using set_lt_Nonempty N)) + simp only [Set.mem_setOf_eq, le_sup_iff, forall_exists_index, forall_apply_eq_imp_iff] + intro i + rcases le_total i N with h | h + · right + apply le_max' + simp only [mem_image] + exact ⟨i, by aesop, rfl⟩ + · left + calc _ ≤ ‖(coeff i) f‖ * |c ^ (range_sum i)| := by bound + _ ≤ 1 := by simpa using (hf i h).le + +lemma lt_ineq {σ : Type*} [Fintype σ] (n a b : σ →₀ ℕ) (h : 2 • n ≤ a + b) : + n ≤ a ∨ n ≤ b := by + simp_rw [le_def, range_sum_add, range_sum_smul] at ⊢ h + have (a b c : ℕ) (h : 2 * a ≤ b + c) : a ≤ b ∨ a ≤ c := by + grind + exact this (∑ i, n i) (∑ i, a i) (∑ i, b i) h + +open IsUltrametricDist + +lemma mul {R : Type*} [NormedRing R] [IsUltrametricDist R] (c : ℝ) {σ : Type*} [Fintype σ] + [Nonempty σ] {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) : + IsRestricted c (f * g) := by + let I := Classical.typeDecidableEq σ + obtain ⟨a, ha, fBound1⟩ := (bddAbove_iff_exists_ge 1).mp (convergenceSet_BddAbove _ + ((isRestricted_iff_abs c f).mp hf)) + obtain ⟨b, hb, gBound1⟩ := (bddAbove_iff_exists_ge 1).mp (convergenceSet_BddAbove _ + ((isRestricted_iff_abs c g).mp hg)) + simp only [convergenceSet, Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] + at fBound1 gBound1 + simp only [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm, coeff_mul] at ⊢ hf hg + intro ε hε + obtain ⟨Nf, fBound2⟩ := (hf (ε / (max a b))) (by positivity) + obtain ⟨Ng, gBound2⟩ := (hg (ε / (max a b))) (by positivity) + rcases le_total Nf Ng with h | h + · refine ⟨2 • Ng, fun n hn ↦ ?_⟩ + obtain ⟨⟨fst, snd⟩, hi, ultrametric⟩ := exists_norm_finset_sum_le (M := R) + (Finset.antidiagonal n) (fun a ↦ (coeff a.1) f * (coeff a.2) g) + obtain ⟨rfl⟩ := by simpa using hi (⟨(0, n), by simp⟩) + calc _ ≤ ‖(coeff fst) f * (coeff snd) g‖ * |c| ^ (range_sum (fst + snd)) := by bound + _ ≤ ‖(coeff fst) f‖ * |c| ^ (range_sum fst) * (‖(coeff snd) g‖ * |c| ^ (range_sum snd)) := by + grw [norm_mul_le, range_sum_add]; grind + have : Ng ≤ fst ∨ Ng ≤ snd := lt_ineq Ng fst snd hn + rcases this with this | this + · calc _ < ε / max a b * b := by + grw [gBound1 snd] + gcongr + exact fBound2 fst (Preorder.le_trans Nf Ng fst h this) + _ ≤ ε := by + rw [div_mul_comm, mul_le_iff_le_one_left ‹_›] + bound + · calc _ < a * (ε / max a b) := by + grw [fBound1 fst] + gcongr + exact gBound2 snd this + _ ≤ ε := by + rw [mul_div_left_comm, mul_le_iff_le_one_right ‹_›] + bound + · refine ⟨(Finsupp.equivFunOnFinite.symm (fun (i : σ) ↦ 2 * Nf i)), fun n hn ↦ ?_⟩ + obtain ⟨⟨fst, snd⟩, hi, ultrametric⟩ := exists_norm_finset_sum_le (M := R) + (Finset.antidiagonal n) (fun a ↦ (coeff a.1) f * (coeff a.2) g) + obtain ⟨rfl⟩ := by simpa using hi (⟨(0, n), by simp⟩) + calc _ ≤ ‖(coeff fst) f * (coeff snd) g‖ * |c| ^ (range_sum (fst + snd)) := by bound + _ ≤ ‖(coeff fst) f‖ * |c| ^ (range_sum fst) * (‖(coeff snd) g‖ * |c| ^ (range_sum snd)) := by + grw [norm_mul_le, range_sum_add]; grind + have : Nf ≤ fst ∨ Nf ≤ snd := lt_ineq Nf fst snd hn + rcases this with this | this + · calc _ < ε / max a b * b := by + grw [gBound1 snd] + gcongr + exact fBound2 fst this + _ ≤ ε := by + rw [div_mul_comm, mul_le_iff_le_one_left ‹_›] + bound + · calc _ < a * (ε / max a b) := by + grw [fBound1 fst] + gcongr + exact gBound2 snd (Preorder.le_trans Ng Nf snd h this) + _ ≤ ε := by + rw [mul_div_left_comm, mul_le_iff_le_one_right ‹_›] + bound + -- can probably clean this proof up if I bother to include max; as opposed to breaking into two + -- steps + +end IsRestricted +end MvPowerSeries + + + +/- +-- not sure if this definition works as we use this instance of < +-- instance instLE : LE (ι →₀ M) where le f g := ∀ i, f i ≤ g i +-- which is not the correct definition. + +-- so I need to define a new ordering of f ≤ g when range_sum f ≤ range_sum g + +-- the nonempty is required as the definition does not work for σ = ∅... it would give it to be {0}. +-- and fintype is required for the sum +def IsRestricted {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] + (f : MvPowerSeries σ R) := + Tendsto (fun (t : σ →₀ ℕ) ↦ (norm (coeff t f)) * c^(∑ i : σ, t i)) atTop (𝓝 0) + +namespace IsRestricted + +lemma isRestricted_iff {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] + {f : MvPowerSeries σ R} : IsRestricted c f ↔ ∀ ε, 0 < ε → ∃ (N : σ →₀ ℕ), + ∀ (n : σ →₀ ℕ), N ≤ n → ‖‖(coeff n) f‖ * c^(∑ i : σ, n i)‖ < ε := by + simp [IsRestricted, NormedAddCommGroup.tendsto_atTop] + +lemma isRestricted_iff_abs {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] + (f : MvPowerSeries σ R) : IsRestricted c f ↔ IsRestricted |c| f := by + simp [isRestricted_iff] + +lemma zero {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] : + IsRestricted c (0 : MvPowerSeries σ R) := by + simp [IsRestricted] + +lemma monomial {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] (n : σ →₀ ℕ) + (a : R) : IsRestricted c (monomial n a) := by + let I := Classical.typeDecidableEq σ + simp_rw [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm, coeff_monomial] + · obtain ⟨m, hm⟩ : ∃ m : σ →₀ ℕ, n < m := by + use n + (Finsupp.equivFunOnFinite.symm (fun (i : σ) ↦ 1)) + simp only [lt_add_iff_pos_right] + refine Finsupp.lt_def.mpr ?_ + exact ⟨zero_le (Finsupp.equivFunOnFinite.symm fun i ↦ 1), by simp?⟩ + refine fun _ _ ↦ ⟨m, fun N hN ↦ ?_⟩ + split + · grind + · aesop + +lemma one {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] : + IsRestricted c (1 : MvPowerSeries σ R) := by + exact monomial c 0 1 + +lemma C {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] (a : R) : + IsRestricted c (C (σ := σ) a) := by + simpa [monomial_zero_eq_C_apply] using monomial c 0 a + +lemma add {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] + {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) : + IsRestricted c (f + g) := by + simp only [isRestricted_iff, map_add, norm_mul, norm_pow, Real.norm_eq_abs] at ⊢ hf hg + intro ε hε + obtain ⟨fN, hfN⟩ := hf (ε / 2) (by positivity) + obtain ⟨gN, hgN⟩ := hg (ε / 2) (by positivity) + simp only [abs_norm] at hfN hgN ⊢ + refine ⟨max fN gN, fun n hn ↦ ?_ ⟩ + calc _ ≤ ‖(coeff n) f‖ * |c| ^ (∑ i, n i) + ‖(coeff n) g‖ * |c| ^ (∑ i, n i) := by + grw [norm_add_le, add_mul] + _ < ε / 2 + ε / 2 := by gcongr <;> aesop + _ = ε := by ring + +lemma neg {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] + {f : MvPowerSeries σ R} (hf : IsRestricted c f) : IsRestricted c (-f) := by + simpa [isRestricted_iff] using hf + +-- the ordering seems wrong... need to change this + +lemma smul {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] + {f : MvPowerSeries σ R} (hf : IsRestricted c f) (r : R) : IsRestricted c (r • f) := by + if h : r = 0 then simpa [h] using zero c else + simp_rw [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at ⊢ hf + intro ε _ + obtain ⟨n, hn⟩ := hf (ε / ‖r‖) (by positivity) + refine ⟨n, fun N hN ↦ ?_⟩ + calc _ ≤ ‖r‖ * ‖(coeff N) f‖ * |c| ^ (∑ i, n i) := + mul_le_mul_of_nonneg (norm_mul_le _ _) (by sorry) (by simp) (by simp) + _ < ‖r‖ * (ε / ‖r‖) := by + rw [mul_assoc]; sorry + _ = ε := mul_div_cancel₀ _ (by aesop) + +-/ diff --git a/PhD/RPS/def.lean b/PhD/RPS/def.lean index 4ea9dfa..af780d8 100644 --- a/PhD/RPS/def.lean +++ b/PhD/RPS/def.lean @@ -4,178 +4,125 @@ 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 +import Mathlib -/-! -# Restricted power series +open PowerSeries -We say a powerseries over a normed ring `R` is restricted for a parameter `c` if -`‖coeff R i f‖ * c^i → 0`. +namespace IsRestricted -## Main results +open IsRestricted -- `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. +variable {R : Type*} [NormedRing R] (c : ℝ) --/ +lemma nsmul (n : ℕ) (f : PowerSeries R) (hf : IsRestricted c f) : IsRestricted c (n • f) := by + have h := IsRestricted.smul c hf (n : R) + convert h + ext _ _ + simp_rw [map_smul, smul_eq_mul, map_nsmul, nsmul_eq_mul] + +lemma zsmul (n : ℤ) (f : PowerSeries R) (hf : IsRestricted c f) : IsRestricted c (n • f) := by + have h := IsRestricted.smul c hf (n : R) + convert h + ext _ _ + simp_rw [map_smul, smul_eq_mul, map_zsmul, zsmul_eq_mul] + +end IsRestricted 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 {R : Type*} [NormedRing R] (c : ℝ) -variable [IsUltrametricDist R] +local instance : AddSubgroup (PowerSeries R) where + carrier := IsRestricted c + zero_mem' := IsRestricted.zero c + add_mem' := IsRestricted.add c + neg_mem' := IsRestricted.neg c + +def Crestricted : Type _ := + Subtype (IsRestricted (R := R) c) + +variable (f g : Crestricted (R := R) c) + +#check f + g -- something is not working... do I need to adjust the definition of turning it to a type + +namespace Ultrametric + +local instance [IsUltrametricDist R] : Subring (PowerSeries R) where + toAddSubgroup := by infer_instance + one_mem' := IsRestricted.one c + mul_mem' := IsRestricted.mul c + +/--/ +-- Method 2 + +structure cRestricted where + series : PowerSeries R + convergence : IsRestricted c series -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) +instance : AddCommGroup (cRestricted R c) where + add f g :=⟨f.1 + g.1, IsRestricted.add c f.2 g.2⟩ + add_assoc f g h := by + rw [cRestricted.mk.injEq] + exact add_assoc f.1 g.1 h.1 + add_comm f g := by + rw [cRestricted.mk.injEq] + exact add_comm f.1 g.1 + zero := ⟨0, IsRestricted.zero c⟩ + zero_add f := by + rw [cRestricted.mk.injEq] + exact zero_add f.series + add_zero f := by + rw [cRestricted.mk.injEq] + exact add_zero f.series + neg f := ⟨-f.1, IsRestricted.neg c f.2⟩ + neg_add_cancel f := by + rw [cRestricted.mk.injEq] + exact neg_add_cancel f.1 + nsmul n f := ⟨n • f.1, (IsRestricted.nsmul c n f.1) f.2⟩ + nsmul_zero _ := by + simp only [zero_nsmul] + rfl + nsmul_succ _ _ := by + simp_rw [nsmul_eq_mul, Nat.cast_add, Nat.cast_one, add_mul, one_mul] + rfl + zsmul n f := ⟨n • f.1, (IsRestricted.zsmul c n f.1) f.2⟩ + zsmul_neg' _ _ := by + simp only [zsmul_eq_mul, Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, + Nat.succ_eq_add_one, Int.cast_add, Int.cast_natCast, Int.cast_one, add_mul, neg_mul, one_mul, + neg_add_rev] + zsmul_succ' _ _ := by + simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, zsmul_eq_mul, Int.cast_add, + Int.cast_natCast, Int.cast_one, add_mul, one_mul] + rfl + zsmul_zero' _ := by + simp only [zero_smul] + rfl -end Restricted -end PowerSeries +variable [IsUltrametricDist R] + +noncomputable +instance : Ring (cRestricted R c) where + one := ⟨1, IsRestricted.one c⟩ + mul f g := ⟨f.1 * g.1, IsRestricted.mul c f.2 g.2⟩ + zero_mul f := by + rw [cRestricted.mk.injEq] + exact zero_mul f.1 + mul_zero f := by + rw [cRestricted.mk.injEq] + exact mul_zero f.1 + one_mul f := by + rw [cRestricted.mk.injEq] + exact one_mul f.1 + mul_one f := by + rw [cRestricted.mk.injEq] + exact mul_one f.1 + mul_assoc f g h := by + rw [cRestricted.mk.injEq] + exact mul_assoc f.1 g.1 h.1 + left_distrib f g h := by + rw [cRestricted.mk.injEq] + exact left_distrib f.1 g.1 h.1 + right_distrib f g h := by + rw [cRestricted.mk.injEq] + exact right_distrib f.1 g.1 h.1 diff --git a/blueprint/src/chapter/GaussNorm.tex b/blueprint/src/chapter/GaussNorm.tex index 339a4d7..9ffc383 100644 --- a/blueprint/src/chapter/GaussNorm.tex +++ b/blueprint/src/chapter/GaussNorm.tex @@ -1,10 +1,11 @@ \chapter{Gauss Norm} Thus far we have shown restricted power series over a non-archimedean normed ring $R$ for a -parameter $c$ forms a ring. Let us denote this ring by $\mathcal{F}$. Next, let us consider the -following function $| \cdot |_c : \mathcal{F} \to \R$ with $f = \sum a_n x^n$ +parameter $c$ forms a ring. Let us again denote this ring by $\mathcal{F}$. + +We consider the following function $| \cdot |_c : \mathcal{F} \to \R$ with $f = \sum a_n x^n$ \[ - |f|_c = \sup_{i \in \N} |a_n|c^n + |f|_c = \sup_{i \in \N} |a_n|c^n. \] \begin{lemma} diff --git a/blueprint/src/chapter/RPS.tex b/blueprint/src/chapter/RPS.tex index eae0337..2201727 100644 --- a/blueprint/src/chapter/RPS.tex +++ b/blueprint/src/chapter/RPS.tex @@ -1,61 +1,39 @@ \chapter{Restricted Power Series} -Recall formal power series over a set $K$ in one variable, written $K [ \! [ x ] \! ] $, are +Formal power series over a set $K$ in one variable, written $K [ \! [ x ] \! ] $, are infinite sums \[ f(x) = \sum_{n=0}^\infty a_n x^n, \quad \forall i, \; a_i \in K. \] -This can be generalized to multivariate formal power series as -\[ -\sum a_{(n)} x^{(n)} -\] -where $x^{(n)} = x_1^{n_1} \cdots x_m^{n_m}$ with $n = \sum_{i = 1}^m n_i$, and the sum is taken -over all tuples $(n) = (n_1,\dots,n_m)$ of non-negative integers. +When $K$ is a ring, we can show power series over $K$ form a ring, and we will often refer to them +as the ring of power series over $K$, denoted by $\mathcal{F}_K$. -When $K$ is a ring, it is not hard to see that power series over $K$ form a ring, and we will often -refer to them as the ring of power series over $K$. +We define a subset of $\mathcal{F}$ that consists of power series whose coefficeients approach zero, +to do this we first better make sure $K$ is a normed ring -We want to introduce a convergence property on the terms $a_n x^n$, to do this we need a norm. -Towards this we recall the definition of a normed ring: we say a ring $R$ is a normed ring if we can -equip it with a norm. +\begin{definition*} +A normed ring is a pair $(R,\lvert \cdot \rvert)$, of a ring and a norm. +\end{definition*} - -We now restrict ourselves to normed rings $R$ and define a subset of power series with a convergence -property. +With this we define, \begin{definition} \label{PowerSeries.IsRestricted} \lean{PowerSeries.IsRestricted} \leanok - Let $f$ be a power series over $R$ in one variable, write $f = \sum_{n=0}^\infty a_n x^n$, and - let $c$ be a real number. We say $f$ is a restricted power series of parameter $c$ over $K$ if + Let $f$ be a power series over a normed ring $R$ in one variable, write + $f = \sum_{n=0}^\infty a_n x^n$, and let $c$ be a real number. + We say $f$ is a restricted power series of parameter $c$ over $K$ if \[ \lim_{n \to \infty} \lvert a_n \rvert c^n = 0. \] \end{definition} -It would be nice if restricted power series of weight $c$ were a ring, that is if we added, or -multiplied, two restricted power series the resulting power series would also be restricted of -weight $c$. - -If the norm of $R$ has the non-archimedean property, it indeed turns out this is true. -The non-archimedean property is key here; restricted power series form an additive group regardless -of the norm on $K$, but a stronger bound than the triangle inequality is necessary for the -multiplication to be closed. This can be seen by the following example: +Note this is not the same as convergent power series in the usual sense unless $R$ is complete, +since in complete spaces Cauchy sequences converge. -Let $f = \sum_{n=0}^\infty \frac{(-1)^n}{\sqrt{n+1}}x^n$ be a power series over $\mathbb{R}$ -equipped with the standard norm. Then it is trivial to see that $f$ is a restricted power series for -the parameter 1. However, the product $f^2$ has coefficients -\[ -b_n = (-1)^n \sum_{k=0}^n \frac{1}{(n - k -1)(k+1)}, -\] -and it can be shown that -\[ -\lvert b_n\rvert \geq \sum_{k = 0}^n \frac{2}{n + 2} = \frac{2 (n + 1)}{(n + 2)}. -\] -Therefore $\lim_{n \to \infty} \lvert b_n \rvert \geq \lim_{n \to \infty} \frac{2(n+1)}{(n+2)}=2$, -that is $f^2$ is not a restricted power series for parameter 1, and we see multiplication is not -closed. +It turns out that restricted power series of parameter $c$ are not just a set, in fact we have the +following. \begin{theorem} \label{PowerSeries.Restricted.IsGroup} @@ -64,9 +42,17 @@ \chapter{Restricted Power Series} Restricted power series over a normed ring $R$ form an additive group. \end{theorem} -\begin{proof} - \leanok -\end{proof} +Moreover, if the norm of $R$ has the non-archimedean property, + +\begin{definition*} + We say a norm is non-archimedean if + \[ + \lvert a + b \rvert \leq \max \{ \lvert a \rvert, \lvert b \rvert\}. + \] + Else the norm is archimedean. +\end{definition*} + +we can strengthen this lemma. \begin{theorem} \label{PowerSeries.Restricted.IsRing} @@ -75,15 +61,31 @@ \chapter{Restricted Power Series} Restricted power series over a non-archimedean normed ring $R$ form a ring. \end{theorem} -\begin{proof} - \leanok -\end{proof} +The importance of the non-archimedean property can be seen in the following example. + +Let $f = \sum_{n=0}^\infty \frac{(-1)^n}{\sqrt{n+1}}x^n$ be a power series over $\mathbb{R}$ +equipped with the standard norm. Then it is immediate to see that $f$ is a restricted power series +for the parameter 1. However, the product $f^2$ has coefficients +\[ +b_n = (-1)^n \sum_{k=0}^n \frac{1}{(n - k -1)(k+1)}, +\] +and it can be shown that +\[ +\lvert b_n\rvert \geq \sum_{k = 0}^n \frac{2}{n + 2} = \frac{2 (n + 1)}{(n + 2)}. +\] +Therefore $\lim_{n \to \infty} \lvert b_n \rvert \geq \lim_{n \to \infty} \frac{2(n+1)}{(n+2)}=2$, +that is $f^2$ is not a restricted power series for parameter 1, and we see multiplication is not +closed. We now suppose that $K$ is a non-archimedean complete field; that is a field equipped with a metric -that is complete and whose metric has the non-archimedean property as defined earlier, like $\Q_p$. +that is complete and whose metric has the non-archimedean property as defined earlier. We give a +new name to restricted power series with these $K$. \begin{definition} When $K$ is a non-archimedean complete field we denote the ring of restricted power series with parameter $c$ over $K$ by $\mathcal{A}_c(K)$ and call it the Tate algebra over $K$ of parameter $c$. \end{definition} + +As mentioned earlier, this set is equivalent to power series that converge on the ball of radius +$c$, and so sometimes in literature the Tate algebra may be referenced as convergent power series. diff --git a/blueprint/src/macro/print.tex b/blueprint/src/macro/print.tex index cbdcce5..6c1daf8 100644 --- a/blueprint/src/macro/print.tex +++ b/blueprint/src/macro/print.tex @@ -17,6 +17,8 @@ \declaretheorem[sibling=theorem]{definition} \declaretheorem[sibling=theorem]{example} +\newtheorem*{definition*}{Definition} + % Dummy macros that make sense only for web version. \newcommand{\uses}[1]{} diff --git a/blueprint/src/macro/web.tex b/blueprint/src/macro/web.tex index d58daaa..4132eb9 100644 --- a/blueprint/src/macro/web.tex +++ b/blueprint/src/macro/web.tex @@ -7,6 +7,8 @@ \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} +\newtheorem*{definition*}{Definition} + \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newtheorem{example}[theorem]{Example} diff --git a/lake-manifest.json b/lake-manifest.json index cd9f4db..31f0713 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "1b489cdbe4bc57a6acdddb9a5dc5699acacdecdd", + "rev": "8ad38b989576a3244a70f249ba4ee7d62f550a94", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "75d7aea6c81efeb68701164edaaa9116f06b91ba", + "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", "name": "checkdecls", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -25,37 +25,37 @@ "type": "git", "subDir": null, "scope": "", - "rev": "eab98761167237d45662033394ebd5ee28613aac", + "rev": "7f43b3a97f3fa978255945f532011c3065d72ad9", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/mhuisi/lean4-cli", + {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925", + "rev": "f75f4926aff7ba19949e16c19094d7298806b1a6", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/jcommelin/lean4-unicode-basic", + {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, "scope": "", - "rev": "458e2d3feda3999490987eabee57b8bb88b1949c", + "rev": "fae4fbc11a6076475940e0d4c43aea77d65d5898", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", - "inputRev": "bump_to_v4.18.0-rc1", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/dupuisf/BibtexQuery", "type": "git", "subDir": null, "scope": "", - "rev": "c07de335d35ed6b118e084ec48cffc39b40d29d2", + "rev": "29a4b34f8caa7c95934ab4494d8866fde1850c0b", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7cf25ec0edf7a72830379ee227eefdaa96c48cfb", + "rev": "66aefec2852d3e229517694e642659f316576591", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a", + "rev": "7607162f5a1c1eb23c23027629a418b3a160670e", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ba020ed434b9c5877eb62ff072a28f5ec56eb871", + "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c96401869916619b86e2e54dbb8e8488bd6dd19c", + "rev": "e5c37730d22634ee0169c164f25dac49918ed951", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,17 +105,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8", + "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.53", + "inputRev": "v0.0.77", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ec060e0e10c685be8af65f288e23d026c9fde245", + "rev": "cbe864cd5177966c9e005418cfdc1fb36db62e13", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -125,7 +125,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73", + "rev": "593aa51c4aa07ee81e9233b53e1f61a5b4d9f761", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -135,7 +135,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5105c4f21aae2d8dc15b4568951810140e6027cd", + "rev": "5bd478197f2e5d2a4fde527cf3581d83f49baa9b", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index ee45541..2264e7f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.18.0-rc1 \ No newline at end of file +leanprover/lean4:v4.25.0-rc1 \ No newline at end of file From 120502c0dc592afb33e99f44dc3f8d6409ea508e Mon Sep 17 00:00:00 2001 From: WilliamCoram Date: Tue, 25 Nov 2025 11:47:31 +0000 Subject: [PATCH 2/4] new restrictedMV work --- PhD/Other work/FLT/ringHaarCharwork.lean | 277 +++++++++++++ PhD/RPS/RestrictedMV.lean | 3 + PhD/RPS/RestrictedMV2.lean | 498 +++++++++++++++++++++++ PhD/RPS/restrictedMV3.lean | 463 +++++++++++++++++++++ 4 files changed, 1241 insertions(+) create mode 100644 PhD/Other work/FLT/ringHaarCharwork.lean create mode 100644 PhD/RPS/RestrictedMV2.lean create mode 100644 PhD/RPS/restrictedMV3.lean diff --git a/PhD/Other work/FLT/ringHaarCharwork.lean b/PhD/Other work/FLT/ringHaarCharwork.lean new file mode 100644 index 0000000..9726c99 --- /dev/null +++ b/PhD/Other work/FLT/ringHaarCharwork.lean @@ -0,0 +1,277 @@ +/- + +Old work on FLT; which was made redundent via a quicker method + +import Mathlib +import FLT.HaarMeasure.HaarChar.Ring + +section basics + +variable {T R : Type*} [Ring R] [Nontrivial R] + +lemma ex_ne_zero_coeff_one [Semiring T] [Module T R] + (B : Module.Basis (Fin (Module.finrank T R)) T R) : ∃ i, B.coord i 1 ≠ 0 := by + by_contra t + simp only [Module.Basis.coord_apply, ne_eq, not_exists] at t + have w (a b : R) : (∀ x, (B.coord x) a = (B.coord x) b) → + (a = b) := (Module.Basis.ext_elem_iff B).mpr + specialize w 1 0 + have (x : Fin (Module.finrank T R)) : (B.coord x) 1 = + (B.coord x) 0 := by + simpa using t x + apply w at this + contrapose this + exact one_ne_zero + +/-- The basis change map mapping `B i ↦ B i - (∑ x, B x - 1)` where `i` is from + `ex_ne_zero_coeff_one`. -/ +noncomputable +def basis_change_map [Semiring T] [Module T R] : + Module.Basis (Fin (Module.finrank T R)) T R → (Fin (Module.finrank T R) → R) := + fun B i => + if i = Classical.choose (ex_ne_zero_coeff_one B) + then B i - (∑ x, B x - 1) + else B i + +section Module + +variable [Field T] [Module T R] + +lemma basis_change_map_spans + (B : Module.Basis (Fin (Module.finrank T R)) T R) : + ⊤ ≤ Submodule.span T (Set.range (basis_change_map B)) := by + obtain ⟨a, ha⟩ : ∃ a, Classical.choose (ex_ne_zero_coeff_one B) = a := by + exact exists_eq' + suffices h : B a ∈ Submodule.span T (Set.range (basis_change_map B)) by + have (i : Fin (Module.finrank T R)) : + B i ∈ Submodule.span T (Set.range (basis_change_map B)) := by + rcases (eq_or_ne i a) with h | h + · aesop + · refine (Submodule.mem_span_range_iff_exists_fun T).mpr ?_ + use (fun j => if j = i then 1 else 0) + simp_rw [basis_change_map, ite_smul, one_smul, zero_smul, Finset.sum_ite_eq', + Finset.mem_univ, reduceIte] + aesop + simp only [← Module.Basis.span_eq B] + refine Submodule.span_le.mpr ?_ + intro x hx + aesop + refine (Submodule.mem_span_range_iff_exists_fun T).mpr ?_ + simp_rw [basis_change_map, ha, smul_ite] + have h : {a} ∪ ({i | i ≠ a} : (Finset (Fin (Module.finrank T R)))) = + Set.univ (α := (Fin (Module.finrank T R))) := by + ext i + simpa using eq_or_ne i a + simp_rw [← Set.toFinset_univ, ← h] + simp only [ne_eq, Finset.singleton_union, Finset.coe_insert, Finset.coe_filter, Finset.mem_univ, + true_and, Set.toFinset_insert, Set.toFinset_setOf, Finset.mem_filter, not_true_eq_false, + and_false, not_false_eq_true, Finset.sum_insert, ↓reduceIte] + have s (c : Fin (Module.finrank T R) → T) : ∑ x with ¬x = a, c x • B x = + ∑ x with ¬x = a, if x = a then c x • (B x - (B a + + ∑ x with ¬x = a, B x - 1)) else c x • B x := + Finset.sum_congr rfl (by aesop) + -- probably should take these two haves (h,s) out as private theorems + simp_rw [← s] + have : (B a - (B a + ∑ x with ¬x = a, B x - 1)) = 1 - ∑ x with ¬x = a, B x := by grind + rw [this, ← (Module.Basis.sum_equivFun B 1), Module.Basis.equivFun_apply] + simp_rw [sub_eq_add_neg, smul_add, smul_neg, Finset.smul_sum, ← sub_eq_add_neg, ← mul_smul] + nth_rw 1 [← Set.toFinset_univ] + simp only [←h, ne_eq, Finset.singleton_union, Finset.coe_insert, Finset.coe_filter, + Finset.mem_univ, true_and, Set.toFinset_insert, Set.toFinset_setOf, Finset.mem_filter, + not_true_eq_false, and_false, not_false_eq_true, Finset.sum_insert] + simp_rw [sub_eq_add_neg, add_assoc, neg_add_eq_sub] + use (fun i => if i = a then (1 : T) / (B.repr 1 a) + else - ((B.repr 1 i) / (B.repr 1 a)) + ((1 : T) / (B.repr 1 a))) + simp only [↓reduceIte, one_div] + have : (∑ x with ¬x = a, (if x = a then ((B.repr 1) a)⁻¹ + else -((B.repr 1) x / (B.repr 1) a) + ((B.repr 1) a)⁻¹) • B x) = + (∑ x with ¬x = a, (-((B.repr 1) x / (B.repr 1) a) + ((B.repr 1) a)⁻¹) • B x) := by + refine Finset.sum_congr rfl ?_ + intro x hx + have : x ≠ a := by + simpa using hx + simp only [this, reduceIte] + rw [this] + simp_rw [Eq.symm (Finset.sum_sub_distrib _ _)] + simp_rw [Eq.symm (@Finset.sum_add_distrib _ _ _ _ _ _)] + have : ((B.repr 1) a) ≠ 0 := by + simpa [← ha, ← Module.Basis.coord_apply] using Classical.choose_spec (ex_ne_zero_coeff_one B) + simp only [ne_eq, this, not_false_eq_true, inv_mul_cancel₀, one_smul, add_eq_left] + refine Finset.sum_eq_zero ?_ + intro i hi + simp_rw [← sub_smul, ← add_smul] + ring_nf + exact zero_smul T (B i) + +lemma basis_change_map_lin_independent (B : Module.Basis (Fin (Module.finrank T R)) T R) : + LinearIndependent T (basis_change_map B) := by + apply linearIndependent_of_top_le_span_of_card_eq_finrank + · exact basis_change_map_spans B + · exact Fintype.card_fin (Module.finrank T R) + +/-- For any basis `a`, `basis_change_map a` is a basis. -/ +noncomputable +def basis_change_map_is_basis (a : Module.Basis (Fin (Module.finrank T R)) T R) : + Module.Basis (Fin (Module.finrank T R)) T R := + Module.Basis.mk (v := basis_change_map a) (basis_change_map_lin_independent a) + (basis_change_map_spans a) + +variable [Module.Finite T R] + +-- This could probably go in Mathlib.LinearAlgebra.Basic; or create a new file? +lemma ex_basis_sum_basis_eq_one : + ∃ b : Module.Basis (Fin (Module.finrank T R)) T R, ∑ x, b x = 1 := by + use basis_change_map_is_basis (Module.finBasis T R) + obtain ⟨a, ha⟩ : ∃ a, Classical.choose (ex_ne_zero_coeff_one (Module.finBasis T R)) = a := by + exact exists_eq' + have h : {a} ∪ ({i | i ≠ a} : (Finset (Fin (Module.finrank T R)))) = + Set.univ (α := (Fin (Module.finrank T R))) := by + ext i + simpa using eq_or_ne i a + simp_rw [basis_change_map_is_basis, Module.Basis.coe_mk, ← Set.toFinset_univ, ← h] + simp only [ne_eq, Finset.singleton_union, Finset.coe_insert, Finset.coe_filter, Finset.mem_univ, + true_and, Set.toFinset_insert, Set.toFinset_setOf, Finset.mem_filter, not_true_eq_false, + and_false, not_false_eq_true, Finset.sum_insert, basis_change_map, ha, reduceIte] + nth_rw 1 [← Set.toFinset_univ] + simp only [← h, ne_eq, Finset.singleton_union, Finset.coe_insert, Finset.coe_filter, + Finset.mem_univ, true_and, Set.toFinset_insert, Set.toFinset_setOf, Finset.mem_filter, + not_true_eq_false, and_false, not_false_eq_true, Finset.sum_insert] + have r : (Module.finBasis T R) a - ((Module.finBasis T R) a + + ∑ x with ¬x = a, (Module.finBasis T R) x - 1) = + 1 - ∑ x with ¬x = a, (Module.finBasis T R) x := by grind + have s : ∑ x with ¬x = a, (Module.finBasis T R) x = ∑ x with ¬x = a, + if x = a then (Module.finBasis T R) x - (∑ x, (Module.finBasis T R) x - 1) + else (Module.finBasis T R) x := Finset.sum_congr rfl (by aesop) + simp_rw [r, s, sub_add_cancel] -- this proof is horrible + + +/- +I need to break the file here. +iso should go in FLT.Mathlib.Topology.Module.ModuleTopology +ringHaarChar_eq should go in the HaarMeasure files somewhere + maybe make a new file where I can also include the results of ℝ → ℝ^d. +-/ + +variable [TopologicalSpace T] [TopologicalSpace R] [IsModuleTopology T R] [IsTopologicalRing T] + +/-- The topological equivalence of `R` and `ℝ^(dim ℝ R)` as additive groups. -/ +noncomputable +abbrev iso (b : Module.Basis (Fin (Module.finrank T R)) T R) : + R ≃ₜ+ (Fin (Module.finrank T R) → T) where + toFun := Module.Basis.equivFun b + invFun := (Module.Basis.equivFun _).symm + map_add' _ _ := LinearEquiv.map_add _ _ _ + left_inv _ := LinearEquiv.symm_apply_apply _ _ + right_inv _ := LinearEquiv.apply_symm_apply _ _ + continuous_toFun := by + convert IsModuleTopology.continuous_of_linearMap _ + all_goals infer_instance + continuous_invFun := by + convert IsModuleTopology.continuous_of_linearMap _ + all_goals try infer_instance + · exact IsModuleTopology.toContinuousAdd T R + +end Module + +section Algebra + +variable [Field T] [Algebra T R] [Module.Finite T R] [TopologicalSpace T] [TopologicalSpace R] + [IsModuleTopology T R] [IsTopologicalRing T] [IsTopologicalRing R] [LocallyCompactSpace T] + [LocallyCompactSpace R] + +-- I now need Algebra and not module to get that smul is associative... maybe there is a nicer way +-- to show this rather than changing assumption to algebra... +-- maybe [IsScalarTower T R R]? + +local instance : MeasurableSpace R := by + exact borel R -- I can probably use the Borelize tactic but not sure how it works. + +local instance : BorelSpace R := by + exact { measurable_eq := rfl } + +instance : MeasurableSpace (Fin (Module.finrank T R) → T) := by + exact borel (Fin (Module.finrank T R) → T) + +instance : BorelSpace (Fin (Module.finrank T R) → T) := by + exact { measurable_eq := rfl } + +lemma ringHaarChar_eq (y : (Fin (Module.finrank T R) → T)ˣ) + (hy : ∃ a : T, y.val = algebraMap T (Fin (Module.finrank T R) → T) a) + (hy' : IsUnit ((Module.Basis.equivFun + (Classical.choose (ex_basis_sum_basis_eq_one (T := T) (R := R)))).symm y)) : + MeasureTheory.ringHaarChar y = MeasureTheory.ringHaarChar (R := R) (IsUnit.unit hy') := by + apply MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv + (iso (Classical.choose (ex_basis_sum_basis_eq_one))).symm + intro x + obtain ⟨a, ha⟩ := hy + have h1 : (iso (Classical.choose (ex_basis_sum_basis_eq_one))).symm x = + ∑ j, x j • (Classical.choose (ex_basis_sum_basis_eq_one)) j := + Module.Basis.equivFun_symm_apply _ _ + have h2 : (iso (Classical.choose (ex_basis_sum_basis_eq_one (T := T) (R := R)))).symm (↑y * x) = + ∑ j, (↑y * x) j • (Classical.choose (ex_basis_sum_basis_eq_one)) j := + Module.Basis.equivFun_symm_apply _ _ + have : a • (∑ x, (Classical.choose (ex_basis_sum_basis_eq_one)) x) = + (∑ x, a • (Classical.choose (ex_basis_sum_basis_eq_one (T := T))) x) := + Finset.smul_sum (N := R) + simp_rw [ContinuousAddEquiv.mulLeft_apply, IsUnit.unit_spec, h1, h2, + Module.Basis.equivFun_symm_apply, ha, Pi.mul_apply, Pi.algebraMap_apply, + Algebra.algebraMap_self, RingHom.id_apply] + simp_rw [← this] + simp_rw [smul_mul_assoc, Classical.choose_spec (ex_basis_sum_basis_eq_one), + one_mul, Finset.smul_sum, ← IsScalarTower.smul_assoc, smul_eq_mul] + +theorem foo (t : Tˣ) : MeasureTheory.ringHaarChar (Units.map (algebraMap T R).toMonoidHom t) = + (MeasureTheory.ringHaarChar t) ^ (Module.finrank T R) := by + let t' := (MulEquiv.piUnits (ι := Fin (Module.finrank T R)) (M := fun _ => T)).symm + (fun (i : Fin (Module.finrank T R)) => t) + have h : IsUnit ((Module.Basis.equivFun + (Classical.choose (ex_basis_sum_basis_eq_one (T := T) (R := R)))).symm t') := by + simp only [Module.Basis.equivFun_symm_apply] + refine isUnit_iff_exists.mpr ?_ + let t'inv := (MulEquiv.piUnits (ι := Fin (Module.finrank T R)) (M := fun _ => T)).symm + (fun (i : Fin (Module.finrank T R)) => t⁻¹) + use ((Module.Basis.equivFun + (Classical.choose (ex_basis_sum_basis_eq_one (T := T) (R := R)))).symm t'inv) + simp only [Module.Basis.equivFun_symm_apply] + simp_rw [Algebra.smul_def] + have : ∑ i, (Classical.choose (ex_basis_sum_basis_eq_one (T := T) (R := R))) i = 1 := by + exact Classical.choose_spec (ex_basis_sum_basis_eq_one (T := T) (R := R)) + + sorry + have hmm1 := ringHaarChar_eq (T := T) (R := R) t' ⟨t.val, rfl⟩ h + have hmm2 : MeasureTheory.ringHaarChar h.unit = + MeasureTheory.ringHaarChar (Units.map (algebraMap T R).toMonoidHom t) := by + have : h.unit = (Units.map (algebraMap T R).toMonoidHom t) := by + ext + simp only [Module.Basis.equivFun_symm_apply, IsUnit.unit_spec, RingHom.toMonoidHom_eq_coe, + Units.coe_map, MonoidHom.coe_coe] + unfold t' + simp only [MulEquiv.val_piUnits_symm_apply] + have (x : Fin (Module.finrank T R)) : + t.val • (Classical.choose (ex_basis_sum_basis_eq_one (T := T) (R := R))) x = + (algebraMap T R) t.val * Classical.choose (ex_basis_sum_basis_eq_one (T := T) (R := R)) x + := by + exact Algebra.smul_def (R := T) (A := R) _ _ + simp_rw [this] + rw [← @Finset.mul_sum] + have : ∑ i, (Classical.choose (ex_basis_sum_basis_eq_one (T := T) (R := R))) i = 1 := by + exact Classical.choose_spec (ex_basis_sum_basis_eq_one (T := T) (R := R)) + simp [this] + simp_rw [this] + rw [hmm2] at hmm1 + rw [← hmm1] + unfold t' + have : MeasureTheory.ringHaarChar (MulEquiv.piUnits.symm (fun (i : Fin (Module.finrank T R)) ↦ t)) + = ∏ (i : Fin (Module.finrank T R)), MeasureTheory.ringHaarChar ((fun i ↦ t) i) := by + have := MeasureTheory.ringHaarChar_pi (ι := Fin (Module.finrank T R)) + (A := fun _ : Fin (Module.finrank T R) => T) (fun (i : Fin (Module.finrank T R)) ↦ t) + simp only [Finset.prod_const, Finset.card_univ, Fintype.card_fin] at this ⊢ + exact this + simp_rw [this] + simp only [Finset.prod_const, Finset.card_univ, Fintype.card_fin] + +end Algebra + +end basics + +-/ diff --git a/PhD/RPS/RestrictedMV.lean b/PhD/RPS/RestrictedMV.lean index 6f7361b..82a6287 100644 --- a/PhD/RPS/RestrictedMV.lean +++ b/PhD/RPS/RestrictedMV.lean @@ -45,6 +45,9 @@ instance {σ : Type*} [Fintype σ] : IsDirected (σ →₀ ℕ) (fun (a b : (σ · use b · use a +-- For infinite variables, could add the condition that the max of the convergence set is bounded... +-- so vacously solves our problem + def IsRestricted {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] (f : MvPowerSeries σ R) := Tendsto (fun (t : σ →₀ ℕ) ↦ (norm (coeff t f)) * c^(range_sum t)) atTop (𝓝 0) diff --git a/PhD/RPS/RestrictedMV2.lean b/PhD/RPS/RestrictedMV2.lean new file mode 100644 index 0000000..d67abba --- /dev/null +++ b/PhD/RPS/RestrictedMV2.lean @@ -0,0 +1,498 @@ +import Mathlib + +import Mathlib + +namespace RestrictedMvPowerSeries + +open MvPowerSeries Filter +open scoped Topology + +abbrev range_sum {σ : Type*} : (σ →₀ ℕ) → ℕ := + fun n ↦ ∑ i ∈ n.support, n i + +lemma foo {σ : Type*} (a b : σ →₀ ℕ) [DecidableEq σ] : + (a + b).support = a.support ∪ (b.support \ a.support) := by + apply Finset.Subset.antisymm_iff.mpr ?_ + constructor + · simpa using Finsupp.support_add + · intro i hi + simp only [Finsupp.mem_support_iff, Finsupp.coe_add, Pi.add_apply, ne_eq, Nat.add_eq_zero, + not_and] + simp only [Finset.mem_union, Finsupp.mem_support_iff, ne_eq] at hi + aesop + +lemma foo' {σ : Type*} (a b : σ →₀ ℕ) [DecidableEq σ] : + (a + b).support = (a.support \ b.support) ∪ b.support := by + apply Finset.Subset.antisymm_iff.mpr ?_ + constructor + · simp only [Finset.sdiff_union_self_eq_union] + exact Finsupp.support_add + · intro i hi + simp only [Finsupp.mem_support_iff, Finsupp.coe_add, Pi.add_apply, ne_eq, Nat.add_eq_zero, + not_and] + simp only [Finset.sdiff_union_self_eq_union, Finset.mem_union, Finsupp.mem_support_iff, + ne_eq] at hi + aesop + +lemma test {σ : Type*} (a b : σ →₀ ℕ) [DecidableEq σ] : ∑ i ∈ (a + b).support, a i = + ∑ i ∈ a.support, a i + ∑ i ∈ (b.support \ a.support) , a i := by + rw [foo, Finset.sum_union] + exact Finset.disjoint_sdiff + +lemma test2 {σ : Type*} (a b : σ →₀ ℕ) [DecidableEq σ] : ∑ i ∈ (a + b).support, b i = + ∑ i ∈ (a.support \ b.support), b i + ∑ i ∈ b.support, b i := by + rw [foo', Finset.sum_union] + exact Finset.sdiff_disjoint + +lemma range_sum_add {σ : Type*} [DecidableEq σ] (a b : σ →₀ ℕ) : + range_sum (a + b) = range_sum (a) + range_sum (b) := by + unfold range_sum + simp only [Finsupp.coe_add, Pi.add_apply] + rw [Finset.sum_add_distrib, test, test2] + have h1 : ∑ i ∈ a.support \ b.support, b i = 0 := by + aesop + have h2 : ∑ i ∈ b.support \ a.support, a i = 0 := by + aesop + simp_rw [h1, h2] + ring + +lemma range_sum_smul {σ : Type*} (a : σ →₀ ℕ) (n : ℕ) : + range_sum (n • a) = n * range_sum a := by + unfold range_sum + simp only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul] + rw [Finset.mul_sum] + rcases Nat.eq_zero_or_pos n with h | h + · simp_rw [h] + simp only [zero_mul, Finset.sum_const_zero] + · have : (n • a).support = a.support := by + refine Finsupp.support_smul_eq ?_ + exact Nat.ne_zero_of_lt h + grw [this] + +instance {σ : Type*} : LE (σ →₀ ℕ) where le f g := (range_sum f) ≤ (range_sum g) + +lemma le_def {σ : Type*} {f g : σ →₀ ℕ} : f ≤ g ↔ (range_sum f) ≤ (range_sum g) := .rfl + +instance {σ : Type*} : LT (σ →₀ ℕ) where lt f g := (range_sum f) < (range_sum g) + +lemma lt_def {σ : Type*} {f g : σ →₀ ℕ} : f < g ↔ (range_sum f) < (range_sum g) := .rfl + +instance preorder {σ : Type*} : Preorder (σ →₀ ℕ) where + le_refl _ := by + rw [le_def] + le_trans _ _ _ := by + exact Nat.le_trans + lt_iff_le_not_ge a b := by + simp_rw [le_def, lt_def, not_le, iff_and_self] + exact Nat.le_of_succ_le + +def le_total {σ : Type*} (a b : σ →₀ ℕ) : a ≤ b ∨ b ≤ a := by + simp_rw [le_def] + exact Nat.le_total _ _ + +instance {σ : Type*} : IsDirected (σ →₀ ℕ) (fun (a b : (σ →₀ ℕ)) ↦ (a ≤ b)) where + directed a b := by + rcases le_total a b with h | h + · use b + · use a + +-- need to change this to the cofinite filter +-- This is the proposed new definition!! +def IsRestricted_limit' {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] + (f : MvPowerSeries σ R) := + Tendsto (fun (t : σ →₀ ℕ) ↦ (norm (coeff t f)) * c^(range_sum t)) Filter.cofinite (𝓝 0) + +def IsRestricted_limit {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] + (f : MvPowerSeries σ R) := + Tendsto (fun (t : σ →₀ ℕ) ↦ (norm (coeff t f)) * c^(range_sum t)) atTop (𝓝 0) + +lemma isRestricted_limit_iff {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] + {f : MvPowerSeries σ R} : IsRestricted_limit c f ↔ ∀ ε, 0 < ε → ∃ (N : σ →₀ ℕ), + ∀ (n : σ →₀ ℕ), N ≤ n → ‖‖(coeff n) f‖ * c^(range_sum n)‖ < ε := by + simp [IsRestricted_limit, NormedAddCommGroup.tendsto_atTop] + +lemma isRestricted_limit_iff_abs {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] + (f : MvPowerSeries σ R) : IsRestricted_limit c f ↔ IsRestricted_limit |c| f := by + simp [isRestricted_limit_iff] + +/- + Originally, I did not have |c| - rather just c - in this definition... however consider + f = ∑_n (-n) x_n, g = ∑_n (1/n) x_n^n ... + f * g has terms of the form x_n^{n+1} i.e. for all degrees of monomoials, there is a term of + coeff 1; i.e. f * g will not be restricted + + Thus we really need the |c| in convergenceSet +-/ + +/-- The set of `‖coeff n f‖ * c ^ (range_sum n)` for a given power series `f` and parameter `c`. -/ +def convergenceSet {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] + (f : MvPowerSeries σ R) : Set ℝ := {‖(coeff n) f‖ * |c|^(range_sum n) | n : (σ →₀ ℕ)} + +def IsRestricted_bdd {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] + (f : MvPowerSeries σ R) := BddAbove (convergenceSet c f) + +-- This definition comes from a discussion of what restricted power series in infinitly many +-- variables should be. +-- I need BddAbove in the proof of Mul... so having the statement vacously allows me to use my proof +-- Rest of BddAbove should follow from Non-archimedean property (hopefully). + +structure IsRestricted {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] + (f : MvPowerSeries σ R) : Prop where + limit : IsRestricted_limit c f + bdd : IsRestricted_bdd c f + +lemma zero {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] : + IsRestricted c (0 : MvPowerSeries σ R) where + limit := by + simp [IsRestricted_limit] + bdd := by + rw [IsRestricted_bdd, convergenceSet] + simp only [coeff_zero, norm_zero, zero_mul, exists_const, Set.setOf_eq_eq_singleton', + bddAbove_singleton] + +lemma monomial {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] (n : σ →₀ ℕ) + (a : R) : IsRestricted c (monomial n a) where + limit := by + let I := Classical.typeDecidableEq σ + simp_rw [isRestricted_limit_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] + obtain ⟨m, hm⟩ : ∃ m : σ →₀ ℕ, n < m := by + use n + Finsupp.single (Classical.choice (inferInstance : Nonempty σ)) 1 + simp_rw [lt_def, range_sum_add] + simp only [lt_add_iff_pos_right] + simp_rw [range_sum] + have : ∑ i ∈ (fun₀ | Classical.choice (inferInstance : Nonempty σ) => 1).support, + (fun₀ | Classical.choice (inferInstance : Nonempty σ) => 1) ↑i = 1 := by + have : (fun₀ | Classical.choice (inferInstance : Nonempty σ) => 1).support = + {Classical.choice (inferInstance : Nonempty σ)} := by + ext i + constructor + · intro hi + simp only [Finsupp.mem_support_iff, ne_eq] at hi + simp only [Finset.mem_singleton] + contrapose hi + simp only [Decidable.not_not] + aesop + · aesop + simp_rw [this] + simp only [Finset.sum_singleton, Finsupp.single_eq_same] + positivity + refine fun _ _ ↦ ⟨m, fun N hN ↦ ?_⟩ + rw [coeff_monomial] + split + · grind + · aesop + bdd := by + let I := Classical.typeDecidableEq σ + rw [IsRestricted_bdd, convergenceSet] + have : {x | ∃ n_1, ‖(coeff n_1) ((MvPowerSeries.monomial n) a)‖ * |c| ^ range_sum n_1 = x} = + {0, ‖a‖ * |c|^(range_sum n)} := by + refine Set.ext ?_ + intro x + constructor + · intro hx + simp only [Set.mem_insert_iff, Set.mem_singleton_iff] + simp only [Set.mem_setOf_eq] at hx + obtain ⟨n', hn'⟩ := hx + rw [coeff_monomial] at hn' + rcases eq_or_ne n' n with h | h + · simp only [h, ↓reduceIte] at hn' + right + exact hn'.symm + · simp only [h, ↓reduceIte, norm_zero, zero_mul] at hn' + left + exact hn'.symm + · intro hx + simp only [Set.mem_setOf_eq] + simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hx + rcases hx with h | h + · simp_rw [coeff_monomial] + obtain ⟨n', hn'⟩ : ∃ a : σ →₀ ℕ, a ≠ n := exists_ne n + use n' + simp only [hn', ↓reduceIte, norm_zero, zero_mul] + exact h.symm + · use n + simp only [coeff_monomial_same] + exact h.symm + simp_rw [this] + simp only [bddAbove_insert, bddAbove_singleton] + +lemma one {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] : + IsRestricted c (1 : MvPowerSeries σ R) := by + exact monomial c 0 1 + +lemma C {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] (a : R) : + IsRestricted c (C (σ := σ) a) := by + simpa [monomial_zero_eq_C_apply] using monomial c 0 a + +-- I should be pulling these two things out (also see literally every other proof) +lemma add {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] + {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) : + IsRestricted c (f + g) where + limit := by + obtain ⟨hf1, hf2⟩ := hf + obtain ⟨hg1, hg2⟩ := hg + simp only [isRestricted_limit_iff, map_add, norm_mul, norm_pow, Real.norm_eq_abs] at ⊢ hf1 hg1 + intro ε hε + obtain ⟨fN, hfN⟩ := hf1 (ε / 2) (by positivity) + obtain ⟨gN, hgN⟩ := hg1 (ε / 2) (by positivity) + simp only [abs_norm] at hfN hgN ⊢ + rcases le_total fN gN with h | h + · refine ⟨gN, fun n hn ↦ ?_ ⟩ + calc _ ≤ ‖(coeff n) f‖ * |c| ^ (range_sum n) + ‖(coeff n) g‖ * |c| ^ (range_sum n) := by + grw [norm_add_le, add_mul] + _ < ε / 2 + ε / 2 := by + have := Preorder.le_trans fN gN n h hn + gcongr <;> aesop + _ = ε := by ring + · refine ⟨fN, fun n hn ↦ ?_ ⟩ + calc _ ≤ ‖(coeff n) f‖ * |c| ^ (range_sum n) + ‖(coeff n) g‖ * |c| ^ (range_sum n) := by + grw [norm_add_le, add_mul] + _ < ε / 2 + ε / 2 := by + have := Preorder.le_trans gN fN n h hn + gcongr <;> aesop + _ = ε := by ring + bdd := by + obtain ⟨hf1, hf2⟩ := hf + obtain ⟨hg1, hg2⟩ := hg + simp_rw [IsRestricted_bdd, convergenceSet] at ⊢ hf2 hg2 + obtain ⟨A, hA⟩ := hf2 + obtain ⟨B, hB⟩ := hg2 + simp_rw [mem_upperBounds] at hA hB + use A + B + simp only [map_add] + refine mem_upperBounds.mpr ?_ + simp only [Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at ⊢ hA hB + intro n + calc _ ≤ ‖(coeff n) f‖ * |c| ^ (range_sum n) + ‖(coeff n) g‖ * |c| ^ (range_sum n) := by + grw [norm_add_le, add_mul] + _ ≤ A + B := by + exact add_le_add (hA n) (hB n) + +lemma smul {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] + {f : MvPowerSeries σ R} (hf : IsRestricted c f) (r : R) : IsRestricted c (r • f) where + limit := by + if h : r = 0 then simpa [h] using (zero c).limit else + obtain ⟨hf, _⟩ := hf + simp_rw [isRestricted_limit_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at ⊢ hf + intro ε _ + obtain ⟨n, hn⟩ := hf (ε / ‖r‖) (by positivity) + refine ⟨n, fun N hN ↦ ?_⟩ + calc _ ≤ ‖r‖ * ‖(coeff N) f‖ * |c| ^ (range_sum N) := + mul_le_mul_of_nonneg (norm_mul_le _ _) (by simp) (by simp) (by simp) + _ < ‖r‖ * (ε / ‖r‖) := by + rw [mul_assoc]; aesop + _ = ε := mul_div_cancel₀ _ (by aesop) + bdd := by + obtain ⟨_, hf⟩ := hf + simp_rw [IsRestricted_bdd, convergenceSet] at ⊢ hf + obtain ⟨A, hA⟩ := hf + simp_rw [mem_upperBounds] at hA + simp only [Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at hA + use ‖r‖ * A + simp only [map_smul, smul_eq_mul] + refine mem_upperBounds.mpr ?_ + intro x hx + simp only [Set.mem_setOf_eq] at hx + obtain ⟨n, rfl⟩ := hx + grw [norm_mul_le, mul_assoc] + exact mul_le_mul_of_nonneg_left (hA n) (by simp) + +lemma nsmul {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] (n : ℕ) + (f : MvPowerSeries σ R) (hf : IsRestricted c f) : IsRestricted c (n • f) := by + convert smul c hf (n : R) + ext _ _ + simp_rw [map_smul, smul_eq_mul, map_nsmul, nsmul_eq_mul] + +lemma zsmul {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] [Nonempty σ] (n : ℤ) + (f : MvPowerSeries σ R) (hf : IsRestricted c f) : IsRestricted c (n • f) := by + convert smul c hf (n : R) + ext _ _ + simp_rw [map_smul, smul_eq_mul, map_zsmul, zsmul_eq_mul] + +open IsUltrametricDist + +lemma lt_ineq {σ : Type*} (n a b : σ →₀ ℕ) (h : 2 • n ≤ a + b) : + n ≤ a ∨ n ≤ b := by + let I := Classical.typeDecidableEq σ + simp_rw [le_def, range_sum_add, range_sum_smul] at ⊢ h + have (a b c : ℕ) (h : 2 * a ≤ b + c) : a ≤ b ∨ a ≤ c := by + grind + exact this (range_sum n) (range_sum a) (range_sum b) h + +lemma mul {R : Type*} [NormedRing R] [IsUltrametricDist R] (c : ℝ) {σ : Type*} [Fintype σ] + [Nonempty σ] {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) : + IsRestricted c (f * g) where + limit := by + let I := Classical.typeDecidableEq σ + obtain ⟨hf1, fBound1⟩ := hf + obtain ⟨hg1, gBound1⟩ := hg + obtain ⟨a, ha, fBound1⟩ := (bddAbove_iff_exists_ge 1).mp fBound1 + obtain ⟨b, hb, gBound1⟩ := (bddAbove_iff_exists_ge 1).mp gBound1 + simp only [convergenceSet, Set.mem_setOf_eq, forall_exists_index, + forall_apply_eq_imp_iff] at fBound1 gBound1 + simp only [isRestricted_limit_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm, + coeff_mul] at ⊢ hf1 hg1 + intro ε hε + obtain ⟨Nf, fBound2⟩ := (hf1 (ε / (max a b))) (by positivity) + obtain ⟨Ng, gBound2⟩ := (hg1 (ε / (max a b))) (by positivity) + rcases le_total Nf Ng with h | h + · refine ⟨2 • Ng, fun n hn ↦ ?_⟩ + obtain ⟨⟨fst, snd⟩, hi, ultrametric⟩ := exists_norm_finset_sum_le (M := R) + (Finset.antidiagonal n) (fun a ↦ (coeff a.1) f * (coeff a.2) g) + obtain ⟨rfl⟩ := by simpa using hi (⟨(0, n), by simp⟩) + calc _ ≤ ‖(coeff fst) f * (coeff snd) g‖ * |c| ^ (range_sum (fst + snd)) := by bound + _ ≤ ‖(coeff fst) f‖ * |c| ^ (range_sum fst) * (‖(coeff snd) g‖ * |c| ^ (range_sum snd)) := by + grw [norm_mul_le, range_sum_add]; grind + have : Ng ≤ fst ∨ Ng ≤ snd := lt_ineq Ng fst snd hn + rcases this with this | this + · calc _ < ε / max a b * b := by + grw [gBound1 snd] + gcongr + exact fBound2 fst (Preorder.le_trans Nf Ng fst h this) + _ ≤ ε := by + rw [div_mul_comm, mul_le_iff_le_one_left ‹_›] + bound + · calc _ < a * (ε / max a b) := by + grw [fBound1 fst] + gcongr + exact gBound2 snd this + _ ≤ ε := by + rw [mul_div_left_comm, mul_le_iff_le_one_right ‹_›] + bound + · refine ⟨2 • Nf, fun n hn ↦ ?_⟩ + obtain ⟨⟨fst, snd⟩, hi, ultrametric⟩ := exists_norm_finset_sum_le (M := R) + (Finset.antidiagonal n) (fun a ↦ (coeff a.1) f * (coeff a.2) g) + obtain ⟨rfl⟩ := by simpa using hi (⟨(0, n), by simp⟩) + calc _ ≤ ‖(coeff fst) f * (coeff snd) g‖ * |c| ^ (range_sum (fst + snd)) := by bound + _ ≤ ‖(coeff fst) f‖ * |c| ^ (range_sum fst) * (‖(coeff snd) g‖ * |c| ^ (range_sum snd)) := by + grw [norm_mul_le, range_sum_add]; grind + have : Nf ≤ fst ∨ Nf ≤ snd := lt_ineq Nf fst snd hn + rcases this with this | this + · calc _ < ε / max a b * b := by + grw [gBound1 snd] + gcongr + exact fBound2 fst this + _ ≤ ε := by + rw [div_mul_comm, mul_le_iff_le_one_left ‹_›] + bound + · calc _ < a * (ε / max a b) := by + grw [fBound1 fst] + gcongr + exact gBound2 snd (Preorder.le_trans Ng Nf snd h this) + _ ≤ ε := by + rw [mul_div_left_comm, mul_le_iff_le_one_right ‹_›] + bound + bdd := by + obtain ⟨_, hf⟩ := hf + obtain ⟨_, hg⟩ := hg + simp [IsRestricted_bdd, convergenceSet] at ⊢ hf hg + obtain ⟨a, ha⟩ := hf + obtain ⟨b, hb⟩ := hg + simp_rw [mem_upperBounds] at ha hb + simp only [Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at ha hb + use a * b + refine mem_upperBounds.mpr ?_ + intro x hx + simp only [Set.mem_setOf_eq] at hx + obtain ⟨n, rfl⟩ := hx + let I := Classical.typeDecidableEq σ + simp_rw [coeff_mul] + obtain ⟨⟨fst, snd⟩, hi, ultrametric⟩ := exists_norm_finset_sum_le (M := R) + (Finset.antidiagonal n) (fun a ↦ (coeff a.1) f * (coeff a.2) g) + obtain ⟨rfl⟩ := by simpa using hi (⟨(0, n), by simp⟩) + calc _ ≤ ‖(coeff fst) f * (coeff snd) g‖ * |c| ^ (range_sum (fst + snd)) := by bound + _ ≤ ‖(coeff fst) f‖ * |c| ^ (range_sum fst) * (‖(coeff snd) g‖ * |c| ^ (range_sum snd)) := by + grw [norm_mul_le, range_sum_add]; grind + refine mul_le_mul_of_nonneg (ha fst) (hb snd) (by positivity) ?_ + calc 0 ≤ ‖(coeff fst) g‖ * |c| ^ range_sum fst := by + have h1 : 0 ≤ ‖(coeff fst) g‖ := by + exact norm_nonneg ((coeff fst) g) + have h2 : 0 ≤ |c| ^ range_sum fst := by + simp only [abs_nonneg, pow_nonneg] + exact Left.mul_nonneg h1 h2 + _ ≤ b := by + exact hb fst + +section Finite + +def set_lt {σ : Type*} [Fintype σ] (n : σ →₀ ℕ) : Set (σ →₀ ℕ) := + {a : σ →₀ ℕ | a ≤ n} + +lemma set_lt_isFinite {σ : Type*} [Fintype σ] (n : σ →₀ ℕ) : Finite (set_lt n) := by + let I := Classical.typeDecidableEq σ + simp only [set_lt, le_def, Set.coe_setOf] + have : { a : σ →₀ ℕ // range_sum a ≤ range_sum n } = + ⋃ i : Finset.range ((range_sum n) + 1), {a : σ →₀ ℕ | range_sum a = i} := by + simp_rw [Set.coe_eq_subtype, Set.mem_iUnion, Set.mem_setOf_eq, Subtype.exists, Finset.mem_range, + exists_prop, exists_eq_right', Nat.lt_add_one_iff] + rw [this] + have (i : Finset.range ((range_sum n) + 1)) : Finite {a : σ →₀ ℕ | range_sum a = i} := by + simp only [Set.coe_setOf] + have (a : σ →₀ ℕ) (t : ℕ) (h : range_sum a = t) : ∀ i, a i ≤ t := by + intro i + unfold range_sum at h + rw [← h] + rcases Decidable.em (i ∈ a.support) with H | H + · have : ∑ i ∈ a.support, a i = a i + + ∑ j ∈ ({n | n ∈ a.support ∧ n ≠ i} : (Finset σ)), a j := by + have : ∑ n ∈ a.support, a n = + ∑ n ∈ {i} ∪ ({n | n ∈ a.support ∧ n ≠ i} : (Finset σ)), a n := by + have : {i} ∪ ({n | n ∈ a.support ∧ n ≠ i} : (Finset σ)) = a.support := by + refine Finset.ext_iff.mpr ?_ + intro j + constructor + · aesop + · intro hj + rcases eq_or_ne j i with hjeq | hjneq + · aesop + · simp only [Finsupp.mem_support_iff, ne_eq, Finset.singleton_union, + Finset.mem_insert, Finset.mem_filter, Finset.mem_univ, true_and] + right + aesop + rw [this] + simp [this] + simp [this] + · aesop + have incl : {a : σ →₀ ℕ | range_sum a = i} ⊆ {a : σ →₀ ℕ | ∀ x, a x ≤ i} := by + exact fun ⦃a⦄ ↦ this a ↑i + have incl_fin : Finite {a : σ →₀ ℕ | ∀ x, a x ≤ i} := by + -- we show this injects into functions (σ → Fin (i + 1)); which is of finite cardinality + let J : {a : σ →₀ ℕ | ∀ x, a x ≤ i} → (σ → Fin (i + 1)) := + fun b ↦ fun j ↦ ⟨b.1 j, Nat.lt_succ_of_le (b.2 j)⟩ + have inj : Function.Injective J := by + exact injective_of_le_imp_le J fun {x y} a ↦ a -- no idea how this works... + exact Finite.of_injective J inj + exact Finite.Set.subset ({a : σ →₀ ℕ | ∀ x, a x ≤ i}) incl + exact Set.finite_iUnion this + +lemma set_lt_Nonempty {σ : Type*} [Fintype σ] (n : σ →₀ ℕ) : Nonempty (set_lt n) := by + use n + simp [set_lt] + +open Finset in +lemma convergenceSet_BddAbove {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] + [Nonempty σ] {f : MvPowerSeries σ R} (hf : IsRestricted_limit c f) : + BddAbove (convergenceSet c f) := by + simp_rw [isRestricted_limit_iff] at hf + obtain ⟨N, hf⟩ := by simpa using (hf 1) + rw [bddAbove_def, convergenceSet] + use max 1 (max' (image (fun i ↦ ‖coeff i f‖ * |c| ^ (range_sum i)) + ((Set.Finite.toFinset (set_lt_isFinite N)))) (by simpa using set_lt_Nonempty N)) + simp only [Set.mem_setOf_eq, le_sup_iff, forall_exists_index, forall_apply_eq_imp_iff] + intro i + rcases le_total i N with h | h + · right + apply le_max' + simp only [mem_image] + exact ⟨i, by aesop, rfl⟩ + · left + calc _ ≤ ‖(coeff i) f‖ * |c ^ (range_sum i)| := by bound + _ ≤ 1 := by simpa using (hf i h).le + +theorem IsRestricted_iff_isRestricted_limit {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Fintype σ] + [Nonempty σ] {f : MvPowerSeries σ R} : (IsRestricted c f) ↔ (IsRestricted_limit c f) := by + constructor + · exact fun h ↦ h.1 + · exact fun h ↦ ⟨h, convergenceSet_BddAbove c h⟩ + +end Finite diff --git a/PhD/RPS/restrictedMV3.lean b/PhD/RPS/restrictedMV3.lean new file mode 100644 index 0000000..03e9800 --- /dev/null +++ b/PhD/RPS/restrictedMV3.lean @@ -0,0 +1,463 @@ +import Mathlib + +namespace RestrictedMvPowerSeries + +open MvPowerSeries Filter +open scoped Topology + +abbrev range_sum {σ : Type*} : (σ →₀ ℕ) → ℕ := + fun n ↦ Finsupp.sum n (fun i ↦ n i) + -- seems overcomplicated; not sure if this is prefered over the other definition + +/- +abbrev range_sum' {σ : Type*} : (σ →₀ ℕ) → ℕ := + fun n ↦ ∑ i ∈ n.support, n i + -- could still PR work on range_sum + +lemma test {σ : Type*} (n : σ →₀ ℕ) : range_sum n = range_sum' n := by + unfold range_sum range_sum' + rw [Finsupp.sum] + simp only [Pi.natCast_apply] + simp only [Nat.cast_id] +-/ + +def IsRestricted {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} (f : MvPowerSeries σ R) := + Tendsto (fun (t : σ →₀ ℕ) ↦ (norm (coeff t f)) * c^(range_sum t)) Filter.cofinite (𝓝 0) + +--Dont want to be using this +lemma isRestricted_iff {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} (f : MvPowerSeries σ R) : + IsRestricted c f ↔ ∀ ε > 0, {t | ε ≤ ‖(norm (coeff t f)) * c^(range_sum t)‖}.Finite := by + simp [IsRestricted, NormedAddCommGroup.tendsto_nhds_zero] + + +lemma isRestricted_iff_abs {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} + (f : MvPowerSeries σ R) : IsRestricted c f ↔ IsRestricted |c| f := by + simp [IsRestricted, NormedAddCommGroup.tendsto_nhds_zero] + +lemma zero {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} : + IsRestricted c (0 : MvPowerSeries σ R) := by + simpa [IsRestricted] using tendsto_const_nhds + +/-- The set of `‖coeff n f‖ * c ^ (range_sum n)` for a given power series `f` and parameter `c`. -/ +def convergenceSet {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} (f : MvPowerSeries σ R) : Set ℝ := + {‖(coeff n) f‖ * c^(range_sum n) | n : (σ →₀ ℕ)} + +/- +-- maybe not neccesary; not being used right now +lemma convergenceSet_monomial {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] + (n : σ →₀ ℕ) (a : R) : convergenceSet c (monomial n a) = {‖a‖ * c ^ (range_sum n), 0} := by + letI := Classical.typeDecidableEq σ + simp_rw [convergenceSet] + simp_rw [coeff_monomial] + ext t + constructor <;> intro ht + · obtain ⟨b, hb⟩ := ht + split at hb + · expose_names; aesop + · aesop + · simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at ht + rcases ht with h | h + · aesop + · obtain ⟨m, hm⟩ : ∃ m : σ →₀ ℕ, n ≠ m := by + exact ⟨n + (Finsupp.single (Classical.arbitrary σ) 1), by simp⟩ + exact ⟨m, by aesop⟩ +-/ + +lemma monomial {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} (n : σ →₀ ℕ) (a : R) : + IsRestricted c (monomial n a) := by + letI := Classical.typeDecidableEq σ + simp_rw [IsRestricted, coeff_monomial] + refine tendsto_nhds_of_eventually_eq ?_ + simp only [mul_eq_zero, norm_eq_zero, ite_eq_right_iff, pow_eq_zero_iff', ne_eq, + eventually_cofinite, not_or, Classical.not_imp, not_and, Decidable.not_not] + have : {x | (x = n ∧ ¬a = 0) ∧ (c = 0 → range_sum x = 0)} ⊆ {x | x = n} := by + simp + refine Set.Finite.subset ?_ this + aesop + +/- +-- there has to be a better way +lemma monomial {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} (n : σ →₀ ℕ) (a : R) : + IsRestricted c (monomial n a) := by + letI := Classical.typeDecidableEq σ + rcases eq_or_ne 0 a with h | h + · have : MvPowerSeries.monomial n 0 = (0 : MvPowerSeries σ R) := by + simp only [map_zero] + simpa [←h, this] using zero c + · rw [isRestricted_iff] + intro ε hε + simp only [norm_mul, norm_pow, Real.norm_eq_abs, abs_norm, coeff_monomial] + rcases le_or_gt ε (‖a‖ * |c| ^ range_sum n) with h1 | h1 + · have : {t | ε ≤ ‖if t = n then a else 0‖ * |c| ^ range_sum t} = {n} := by + ext i + simp only [Set.mem_setOf_eq, Set.mem_singleton_iff] + constructor <;> intro hε' + · split at hε' + · aesop + · simp only [norm_zero, zero_mul] at hε' + contrapose hε + exact Std.not_lt.mpr hε' + · aesop + simp only [this, Set.finite_singleton] + · have : {t | ε ≤ ‖if t = n then a else 0‖ * |c| ^ range_sum t} = ∅ := by + aesop + simp only [this, Set.finite_empty] +-/ + +lemma one {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} : + IsRestricted c (1 : MvPowerSeries σ R) := by + exact monomial c 0 1 + +lemma C {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} [Nonempty σ] (a : R) : + IsRestricted c (C (σ := σ) a) := by + simpa [monomial_zero_eq_C_apply] using monomial c 0 a + + +/- +-- maybe see if this API exists, but it will be very useful +lemma subset_function_le {T : Type*} (f g : T → ℝ) (ε : ℝ) : + (∀ b, f b ≤ g b) → {a | ε ≤ f a} ⊆ {a | ε ≤ g a} := by + intro h + simp only [Set.setOf_subset_setOf] + intro a ha + exact Std.IsPreorder.le_trans ε (f a) (g a) ha (h a) +-- definitely should use this to golf add proof +-/ + +lemma add {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} {f g : MvPowerSeries σ R} + (hf : IsRestricted c f) (hg : IsRestricted c g) : IsRestricted c (f + g) := by + rw [isRestricted_iff_abs, IsRestricted] at * + have := hf.add hg + simp at this + have h0 : Tendsto (fun x : σ →₀ ℕ => 0) cofinite (nhds (0 : ℝ)) := by + rw [NormedAddCommGroup.tendsto_nhds_zero] + aesop + apply Filter.Tendsto.squeeze h0 this + <;> refine Pi.le_def.mpr ?_ + <;> intro n + · positivity + · simp only [map_add] + have : ‖(coeff n) f + (coeff n) g‖ * |c| ^ range_sum n ≤ + (‖(coeff n) f‖ + ‖coeff n g‖) * |c| ^ range_sum n := by + exact mul_le_mul_of_nonneg (norm_add_le _ _) (by rfl) (by simp) (by simp) + grind + +/- +-- I reckon I can golf this a ton by combining first set inclusions and using a calc _ ... +-- surely can combine proofs of HF and HG too +lemma add {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} {f g : MvPowerSeries σ R} + (hf : IsRestricted c f) (hg : IsRestricted c g) : IsRestricted c (f + g) := by + rw [isRestricted_iff_abs, isRestricted_iff] + simp only [map_add] + have (t : σ →₀ ℕ) : ‖(coeff t) f + (coeff t) g‖ * |c| ^ range_sum t ≤ + (‖(coeff t) f‖ + ‖coeff t g‖) * |c| ^ range_sum t := by + exact mul_le_mul_of_nonneg (norm_add_le _ _) (by rfl) (by simp) (by simp) + intro ε hε + simp only [norm_mul, norm_pow, Real.norm_eq_abs, abs_abs] + have h : {t | ε ≤ |‖(coeff t) f + (coeff t) g‖| * |c| ^ range_sum t} ⊆ + {t | ε ≤ (‖(coeff t) f‖ + ‖coeff t g‖) * |c| ^ range_sum t} := by + simp only [abs_norm, Set.setOf_subset_setOf] + intro n hn + exact Std.IsPreorder.le_trans ε _ _ hn (this n) + refine Set.Finite.subset ?_ h + have h : {t | ε ≤ (‖(coeff t) f‖ + ‖coeff t g‖) * |c| ^ range_sum t} ⊆ + {t | ε ≤ 2 * (max (‖(coeff t) f‖) (‖coeff t g‖)) * |c| ^ range_sum t} := by + simp only [Set.setOf_subset_setOf] + intro n hn + have : (‖(coeff n) f‖ + ‖coeff n g‖) * |c| ^ range_sum n ≤ + 2 * (max (‖(coeff n) f‖) (‖coeff n g‖)) * |c| ^ range_sum n := by + exact mul_le_mul_of_nonneg (by grind) (by rfl) (add_nonneg (by simp) (by simp)) (by simp) + exact Std.IsPreorder.le_trans ε _ _ hn this + refine Set.Finite.subset ?_ h + have h : {t | ε ≤ 2 * max ‖(coeff t) f‖ ‖(coeff t) g‖ * |c| ^ range_sum t} ⊆ + {t | ε ≤ 2 * ‖(coeff t) f‖ * |c| ^ range_sum t} ∪ + {t | ε ≤ 2 * ‖(coeff t) g‖ * |c| ^ range_sum t} := by + intro n hn + simp only [Set.mem_union, Set.mem_setOf_eq] at hn ⊢ + grind + refine Set.Finite.subset ?_ h + have (h : MvPowerSeries σ R) : {t | ε ≤ 2 * ‖(coeff t) h‖ * |c| ^ range_sum t} = + {t | ε / 2 ≤ ‖(coeff t) h‖ * |c| ^ range_sum t} := by + ext m + simp only [Set.mem_setOf_eq] + field_simp -- poggers + simp_rw [this] + have HF : {t | ε / 2 ≤ ‖(coeff t) f‖ * |c| ^ range_sum t}.Finite := by + rw [isRestricted_iff_abs, isRestricted_iff] at hf + simp only [gt_iff_lt, norm_mul, norm_pow, Real.norm_eq_abs, abs_abs, abs_norm] at hf + exact hf (ε / 2) (by aesop) + have HG : {t | ε / 2 ≤ ‖(coeff t) g‖ * |c| ^ range_sum t}.Finite := by + rw [isRestricted_iff_abs, isRestricted_iff] at hg + simp only [gt_iff_lt, norm_mul, norm_pow, Real.norm_eq_abs, abs_abs, abs_norm] at hg + exact hg (ε / 2) (by aesop) + exact Set.Finite.union HF HG +-/ + +lemma smul {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} {f : MvPowerSeries σ R} + (hf : IsRestricted c f) (r : R) : IsRestricted c (r • f) := by + rw [isRestricted_iff_abs, IsRestricted] at * + have : Tendsto (fun t ↦ ‖r‖ * ‖(coeff t) f‖ * |c| ^ range_sum t) cofinite (𝓝 0) := by + have := Filter.Tendsto.const_mul ‖r‖ hf + grind + have h0 : Tendsto (fun x : σ →₀ ℕ => 0) cofinite (nhds (0 : ℝ)) := by + rw [NormedAddCommGroup.tendsto_nhds_zero] + aesop + apply Filter.Tendsto.squeeze h0 this + <;> refine Pi.le_def.mpr ?_ + <;> intro n + · positivity + · exact mul_le_mul_of_nonneg (norm_mul_le _ _) (by rfl) (by simp) (by simp) + +/- +lemma smul {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} {f : MvPowerSeries σ R} + (hf : IsRestricted c f) (r : R) : IsRestricted c (r • f) := by + if h : r = 0 then simpa [h] using (zero c) else + rw [isRestricted_iff_abs, isRestricted_iff] + simp only [gt_iff_lt, map_smul, smul_eq_mul, norm_mul, norm_pow, Real.norm_eq_abs, + abs_abs, abs_norm] + intro ε hε + have (t : σ →₀ ℕ) : ‖r * (coeff t) f‖ * |c| ^ range_sum t ≤ + ‖r‖ * ‖coeff t f‖ * |c| ^ range_sum t := by + exact mul_le_mul_of_nonneg (norm_mul_le _ _) (by rfl) (by simp) (by simp) + refine Set.Finite.subset ?_ (subset_function_le _ _ ε this) + rw [isRestricted_iff_abs, isRestricted_iff] at hf + specialize hf (ε / ‖r‖) (by aesop) + field_simp at hf + simp only [norm_mul, norm_pow, Real.norm_eq_abs, abs_abs, abs_norm, ← mul_assoc] at hf + exact hf +-/ + +lemma nsmul {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} (n : ℕ) + (f : MvPowerSeries σ R) (hf : IsRestricted c f) : IsRestricted c (n • f) := by + convert smul c hf (n : R) + ext _ _ + simp_rw [map_smul, smul_eq_mul, map_nsmul, nsmul_eq_mul] + +lemma zsmul {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} (n : ℤ) + (f : MvPowerSeries σ R) (hf : IsRestricted c f) : IsRestricted c (n • f) := by + convert smul c hf (n : R) + ext _ _ + simp_rw [map_smul, smul_eq_mul, map_zsmul, zsmul_eq_mul] + + +---- Trying to find a nice way to do the multiplication + +open IsUltrametricDist + +lemma tendsto_antidiagonal {R S : Type*} [AddMonoid R] [Finset.HasAntidiagonal R] + {f g : R → S} [NormedRing S] + (hf : Tendsto (fun i ↦ ‖f i‖) cofinite (𝓝 0)) (hg : Tendsto (fun i ↦ ‖g i‖) cofinite (𝓝 0)) : + Tendsto (fun a ↦ ‖∑ p ∈ Finset.antidiagonal a, (f p.1 * g p.2)‖) cofinite (𝓝 0) := by + rw [@NormedAddCommGroup.tendsto_nhds_zero] at * + simp only [gt_iff_lt, Real.norm_eq_abs, eventually_cofinite, not_lt] at * + + -- this isnt true because we can just consider points + -- x = a + _ where a is in the finite set greater than ε + sorry + +lemma mul' {R : Type*} [NormedRing R] [IsUltrametricDist R] {σ : Type*} + {f g : MvPowerSeries σ R} (hf : IsRestricted 1 f) (hg : IsRestricted 1 g) : + IsRestricted 1 (f * g) := by + letI := Classical.typeDecidableEq σ + letI : Finset.HasAntidiagonal (σ →₀ ℕ) := by + exact Finsupp.instHasAntidiagonal + rw [isRestricted_iff_abs, IsRestricted] at * + simp_rw [coeff_mul] + simp only [abs_one, one_pow, mul_one] at * + have := tendsto_antidiagonal hf hg + exact this + /- + have h0 : Tendsto (fun x : σ →₀ ℕ => 0) cofinite (nhds (0 : ℝ)) := by + rw [NormedAddCommGroup.tendsto_nhds_zero] + aesop + apply Filter.Tendsto.squeeze h0 this + <;> refine Pi.le_def.mpr ?_ + <;> intro n + · positivity + · simp_rw [coeff_mul] + -- do I have the right set up + sorry + -/ + +lemma isRestricted_BddAbove {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} {f : MvPowerSeries σ R} + (hf : IsRestricted c f) : BddAbove (convergenceSet c f) := by + refine bddAbove_def.mpr ?_ + rw [isRestricted_iff] at hf + simp only [gt_iff_lt, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at hf + specialize hf 1 (by simp) + rw [convergenceSet] + letI set := {a | ∃ t ∈ {t | 1 ≤ ‖(coeff t) f‖ * |c| ^ range_sum t}, + a = ‖(coeff t) f‖ * |c| ^ range_sum t} + rcases isEmpty_or_nonempty set with h | h + · use 1 + simp only [Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] + intro a + have : IsEmpty {t | 1 ≤ ‖(coeff t) f‖ * |c| ^ range_sum t} := by + contrapose h + aesop + have : a ∉ {t | 1 ≤ ‖(coeff t) f‖ * |c| ^ range_sum t} := by + contrapose this + aesop + simp only [Set.mem_setOf_eq, not_le] at this + calc _ ≤ ‖(coeff a) f‖ * |c| ^ range_sum a := by + + sorry + _ ≤ 1 := Std.le_of_lt this + · have set_fin : set.Finite := by + simp_rw [set] + letI fun1 := fun n : σ →₀ ℕ ↦ ‖(coeff n) f‖ * |c| ^ range_sum n + have : {a | ∃ t ∈ {t | 1 ≤ ‖(coeff t) f‖ * |c| ^ range_sum t}, + a = ‖(coeff t) f‖ * |c| ^ range_sum t} = fun1 '' {t | 1 ≤ ‖(coeff t) f‖ * |c| ^ range_sum t} + := by + aesop + simp_rw [this] + exact Set.Finite.image fun1 hf + obtain ⟨_, ha⟩ : Nonempty (Set.Finite.toFinset set_fin) := by + aesop + obtain ⟨b, hb⟩ := Finset.max_of_mem ha + use max 1 b + intro a h + simp only [Set.mem_setOf_eq] at h + obtain ⟨n, eq⟩ := h + rw [← eq] + rcases Decidable.em (n ∈ {t | 1 ≤ ‖(coeff t) f‖ * |c| ^ range_sum t}) with h | h + · have : ‖(coeff n) f‖ * |c| ^ range_sum n ∈ set := by + use n + have : ‖(coeff n) f‖ * |c| ^ range_sum n ≤ b := by + + sorry + calc _ ≤ ‖(coeff n) f‖ * |c| ^ range_sum n := by + + sorry + _ ≤ b := this + _ ≤ max 1 b := le_max_right 1 b + · simp only [Set.mem_setOf_eq, not_le] at h + calc _ ≤ ‖(coeff n) f‖ * |c| ^ range_sum n := by + + sorry + _ ≤ 1 := Std.le_of_lt h + _ ≤ max 1 b := le_max_left 1 b + +open IsUltrametricDist + +lemma mul2 {R : Type*} [NormedRing R] [IsUltrametricDist R] (c : ℝ) {σ : Type*} + {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) : + IsRestricted c (f * g) := by + letI := Classical.typeDecidableEq σ + rw [IsRestricted] at * + + have := hf.max hg + have h0 : Tendsto (fun x : σ →₀ ℕ => 0) cofinite (nhds (0 : ℝ)) := by sorry + simp at this + apply Filter.Tendsto.squeeze h0 this + + sorry + refine Pi.le_def.mpr ?_ + intro n + + sorry + + + +lemma mul {R : Type*} [NormedRing R] [IsUltrametricDist R] (c : ℝ) {σ : Type*} + {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) : + IsRestricted c (f * g) := by + letI := Classical.typeDecidableEq σ + + rw [isRestricted_iff_abs, isRestricted_iff] + intro ε hε + simp only [norm_mul, norm_pow, Real.norm_eq_abs, abs_abs, abs_norm] + simp_rw [coeff_mul] + have H (t : σ →₀ ℕ) := exists_norm_finset_sum_le (M := R) (Finset.antidiagonal t) + (fun a ↦ (coeff a.1) f * (coeff a.2) g) + simp only [Finset.mem_antidiagonal, Prod.exists] at H + have (t : σ →₀ ℕ) : ∃ a b, ((Finset.antidiagonal t).Nonempty → a + b = t) ∧ + ‖∑ p ∈ Finset.antidiagonal t, (coeff p.1) f * (coeff p.2) g‖ * + |c| ^ range_sum t ≤ (‖(coeff a) f * (coeff b) g‖) * |c| ^ range_sum t := by + obtain ⟨a, b, heq, h⟩ := H t + use a, b + constructor + · exact heq + · exact mul_le_mul_of_nonneg (by grind) (by rfl) (by simp) (by simp) + have : {t | ε ≤ ‖∑ p ∈ Finset.antidiagonal t, (coeff p.1) f * (coeff p.2) g‖ * |c| ^ range_sum t} + ⊆ {t | IsEmpty (Finset.antidiagonal t)} ∪ + {t | ((Finset.antidiagonal t).Nonempty) ∧ ∃ a b, a + b = t ∧ + ε ≤ (‖(coeff a) f * (coeff b) g‖) * |c| ^ range_sum t} := by + intro n hn + simp only [Set.mem_union, Set.mem_setOf_eq] at ⊢ hn + rcases isEmpty_or_nonempty (Finset.antidiagonal n) with h | h + · aesop + · right + obtain ⟨a, b, heq, h'⟩ := H n + constructor + · exact Finset.nonempty_coe_sort.mp h + use a, b + constructor + · exact heq (Finset.nonempty_coe_sort.mp h) + · exact Std.IsPreorder.le_trans ε _ _ hn + (mul_le_mul_of_nonneg (by grind) (by rfl) (by simp) (by simp)) + refine Set.Finite.subset ?_ this + simp only [Finset.mem_antidiagonal, Set.finite_union] + constructor + · -- think this should just be true vacuously? + have : {t | IsEmpty { x : (σ →₀ ℕ) × (σ →₀ ℕ) // x.1 + x.2 = t }} = ∅ := by + ext i + constructor + · -- not sure if what I have written is nonsense + sorry + · aesop + sorry + · have (a b t : σ →₀ ℕ) (h : a + b = t) : ‖(coeff a) f * (coeff b) g‖ * |c| ^ range_sum t ≤ + ‖(coeff a) f‖ * |c| ^ range_sum a * ‖(coeff b) g‖ * |c| ^ range_sum b := by + calc _ ≤ ‖(coeff a) f‖ * ‖(coeff b) g‖ * |c| ^ range_sum t := by + exact (mul_le_mul_of_nonneg (norm_mul_le _ _)) (by rfl) (by simp) (by simp) + _ = ‖(coeff a) f‖ * |c| ^ range_sum a * ‖(coeff b) g‖ * |c| ^ range_sum b := by + simp_rw [← h] + ring_nf + + sorry + have : {t | (Finset.antidiagonal t).Nonempty ∧ ∃ a b, a + b = t ∧ + ε ≤ ‖(coeff a) f * (coeff b) g‖ * |c| ^ range_sum t} ⊆ + {t | (Finset.antidiagonal t).Nonempty ∧ ∃ a b, a + b = t ∧ + ε ≤ ‖(coeff a) f‖ * |c| ^ range_sum a * ‖(coeff b) g‖ * |c| ^ range_sum b} := by + intro n hn + simp only [Set.mem_setOf_eq] at ⊢ hn + obtain ⟨h', a, b, heq, h⟩ := hn + constructor + · exact h' + · use a, b + constructor + · exact heq + · specialize this a b n heq + exact Std.IsPreorder.le_trans ε _ _ h this + refine Set.Finite.subset ?_ this + refine Set.Finite.subset ?_ (Set.sep_subset_setOf _ _) + rw [isRestricted_iff_abs] at hg + obtain ⟨B, hB1, hB2⟩ := (bddAbove_iff_exists_ge 1).mp (isRestricted_BddAbove |c| hg) + + -- I am not sure if this is the correct method from here + -- may need to break into two cases and take the intersection when I bound each function + + have : {x | ∃ a b, a + b = x ∧ + ε ≤ ‖(coeff a) f‖ * |c| ^ range_sum a * ‖(coeff b) g‖ * |c| ^ range_sum b} ⊆ + {x | ∃ a b, a + b = x ∧ ε ≤ ‖(coeff a) f‖ * |c| ^ range_sum a * B} := by + intro n hn + simp only [Set.mem_setOf_eq, exists_and_right] at hn ⊢ + obtain ⟨a, b, eq, h⟩ := hn + use a + constructor + · use b + · + sorry + refine Set.Finite.subset ?_ this + have : {x | ε ≤ ‖(coeff x) f‖ * |c| ^ range_sum x * B}.Finite := by + rw [isRestricted_iff_abs, isRestricted_iff] at hf + simp only [gt_iff_lt, norm_mul, norm_pow, Real.norm_eq_abs, abs_abs, abs_norm] at hf + specialize hf (ε / B) (by positivity) + field_simp at hf + + sorry + + sorry + +end RestrictedMvPowerSeries From 7cc18b81332d7fb3ac926d081387f939fc52ee38 Mon Sep 17 00:00:00 2001 From: WilliamCoram Date: Wed, 21 Jan 2026 16:28:21 +0000 Subject: [PATCH 3/4] test --- PhD/GaussNorm/GN_new.lean | 112 +++++++ PhD/GaussNorm/GaussNorm.lean | 135 ++++++++ PhD/Newton polygons/NPGeneral.lean | 237 ++++++++++++++ PhD/Newton polygons/NPnew.lean | 124 +++++++ PhD/RPS/OldRestrictedWork/RMV4.lean | 295 +++++++++++++++++ .../{ => OldRestrictedWork}/RestrictedMV.lean | 0 .../RestrictedMV2.lean | 0 PhD/RPS/{ => OldRestrictedWork}/def.lean | 0 .../restrictedMV3.lean | 13 +- blueprint/src/chapter/Fujisaki.tex | 303 ++++++++++++++++++ blueprint/src/chapter/RPS.tex | 148 ++++++++- blueprint/src/print.tex | 3 + blueprint/src/web.tex | 3 + 13 files changed, 1366 insertions(+), 7 deletions(-) create mode 100644 PhD/GaussNorm/GN_new.lean create mode 100644 PhD/GaussNorm/GaussNorm.lean create mode 100644 PhD/Newton polygons/NPGeneral.lean create mode 100644 PhD/Newton polygons/NPnew.lean create mode 100644 PhD/RPS/OldRestrictedWork/RMV4.lean rename PhD/RPS/{ => OldRestrictedWork}/RestrictedMV.lean (100%) rename PhD/RPS/{ => OldRestrictedWork}/RestrictedMV2.lean (100%) rename PhD/RPS/{ => OldRestrictedWork}/def.lean (100%) rename PhD/RPS/{ => OldRestrictedWork}/restrictedMV3.lean (97%) diff --git a/PhD/GaussNorm/GN_new.lean b/PhD/GaussNorm/GN_new.lean new file mode 100644 index 0000000..26a4373 --- /dev/null +++ b/PhD/GaussNorm/GN_new.lean @@ -0,0 +1,112 @@ +import Mathlib.Analysis.Normed.Ring.Basic +import Mathlib.RingTheory.MvPowerSeries.Basic + +open MvPowerSeries + +variable {R F σ : Type*} [Semiring R] [FunLike F R ℝ] (v : F) (c : σ → ℝ) (f : MvPowerSeries σ R) + +/-- Given a multivariate power series `f` in, a function `v : R → ℝ` and a real number `c`, + the Gauss norm is defined as the supremum of the set of all values of + `v (coeff t f) * ∏ i : t.support, c i` for all `t : σ →₀ ℕ`. -/ +noncomputable def gaussNormC : ℝ := + sSup {a : ℝ | ∃ t : σ →₀ ℕ, a = v (coeff t f) * ∏ i ∈ t.support, (c i) ^ (t i)} + +@[simp] +theorem gaussNormC_zero [ZeroHomClass F R ℝ] : gaussNormC v c 0 = 0 := by simp [gaussNormC] + +private lemma gaussNormC_nonempty : + {a | ∃ t : σ →₀ ℕ, a = v (coeff t f) * ∏ i ∈ t.support, (c i) ^ (t i)}.Nonempty := by + use v (f.coeff 0) * ∏ i ∈ (0 : σ →₀ ℕ).support, (c i) ^ ((0 : σ →₀ ℕ) i), 0 + +lemma le_gaussNormC (hbd : BddAbove {a | ∃ t : σ →₀ ℕ, a = v (coeff t f) * + ∏ i ∈ t.support, (c i) ^ (t i)}) (t : σ →₀ ℕ) : + v (coeff t f) * ∏ i ∈ t.support, (c i) ^ (t i) ≤ gaussNormC v c f := by + apply le_csSup hbd + use t + +theorem gaussNormC_nonneg [NonnegHomClass F R ℝ] : 0 ≤ gaussNormC v c f := by + rw [gaussNormC] + by_cases h : BddAbove {a | ∃ t : σ →₀ ℕ, a = v (coeff t f) * ∏ i ∈ t.support,(c i) ^ (t i)} + · simp_rw [Real.le_sSup_iff h <| gaussNormC_nonempty v c f, Set.mem_setOf_eq, zero_add, + existsAndEq, true_and] + intro ε hε + use 0 + simpa using lt_of_lt_of_le hε <| apply_nonneg v (f.constantCoeff) + · simp only [h, not_false_eq_true, csSup_of_not_bddAbove, Real.sSup_empty, le_refl] + +@[simp] +theorem gaussNormC_eq_zero_iff [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] {v : F} + (h_eq_zero : ∀ x : R, v x = 0 → x = 0) (hc : ∀ i, 0 < c i) + (hbd : BddAbove {a | ∃ t : σ →₀ ℕ, a = v (coeff t f) * ∏ i ∈ t.support, (c i) ^ (t i)}) : + gaussNormC v c f = 0 ↔ f = 0 := by + refine ⟨?_, fun hf ↦ by simp [hf]⟩ + contrapose! + intro hf + apply ne_of_gt + obtain ⟨n, hn⟩ := (MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero f).mp hf + calc + 0 < v (f.coeff n) * ∏ i ∈ n.support, (c i) ^ (n i) := by + apply mul_pos _ (by exact Finset.prod_pos fun i a ↦ (fun i ↦ pow_pos (hc ↑i) (n ↑i)) i) + specialize h_eq_zero (f.coeff n) + simp_all only [ne_eq] + positivity + _ ≤ sSup {x | ∃ t, x = v (f.coeff t) * ∏ i ∈ t.support, (c i) ^ (t i)} := by + rw [Real.le_sSup_iff hbd <| gaussNormC_nonempty v c f] + simp only [Set.mem_setOf_eq, ↓existsAndEq, true_and] + intro ε hε + use n + simp [hε] + +@[simp] +theorem gaussNormC_nonarchimedean (f g : MvPowerSeries σ R) (hc : 0 ≤ c) + (hv1 : ∀ x y, v (x + y) ≤ max (v x) (v y)) (hv2 : ∀ x, 0 ≤ v x) + (hbfd : BddAbove {a | ∃ t : σ →₀ ℕ, a = v (coeff t f) * ∏ i ∈ t.support, (c i) ^ (t i)}) + (hbgd : BddAbove {a | ∃ t : σ →₀ ℕ, a = v (coeff t g) * ∏ i ∈ t.support, (c i) ^ (t i)}) : + gaussNormC v c (f + g) ≤ max (gaussNormC v c f) (gaussNormC v c g) := by + have H (t : σ →₀ ℕ) : 0 ≤ ∏ i ∈ t.support, c i ^ t i := + Finset.prod_nonneg (fun i hi ↦ pow_nonneg (hc i) (t i)) + have Final (t : σ →₀ ℕ) : v ((coeff t) (f + g)) * ∏ i ∈ t.support, c ↑i ^ t ↑i ≤ + max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i) + (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by + specialize hv1 (coeff t f) (coeff t g) + rcases max_choice (v ((coeff t) f)) (v ((coeff t) g)) with h | h + · have : max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i) + (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) = + (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by + simp only [sup_eq_left] + exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t) + simp_rw [this] + exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t) + · have : max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i) + (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) = + (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by + simp only [sup_eq_right] + exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t) + simp_rw [this] + exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t) + refine Real.sSup_le ?_ ?_ + · simp only [Set.mem_setOf_eq, forall_exists_index, forall_eq_apply_imp_iff] + refine fun t ↦ calc + _ ≤ _ := Final t + _ ≤ max (sSup {a | ∃ t, a = v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i}) + (sSup {a | ∃ t, a = v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i}) := by + simp only [le_sup_iff] + rcases max_choice (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) + (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) with h | h + · left + simp_rw [h, Real.le_sSup_iff hbfd <| gaussNormC_nonempty v c f, Set.mem_setOf_eq, + existsAndEq, true_and] + intro ε hε + use t + simp [hε] + · right + simp_rw [h, Real.le_sSup_iff hbgd <| gaussNormC_nonempty v c g, Set.mem_setOf_eq, + existsAndEq, true_and] + intro ε hε + use t + simp [hε] + · simp only [le_sup_iff] + left + refine Real.sSup_nonneg ?_ + simp only [Set.mem_setOf_eq, forall_exists_index, forall_eq_apply_imp_iff] + exact fun t ↦ mul_nonneg (hv2 (coeff t f)) (H t) diff --git a/PhD/GaussNorm/GaussNorm.lean b/PhD/GaussNorm/GaussNorm.lean new file mode 100644 index 0000000..e06513d --- /dev/null +++ b/PhD/GaussNorm/GaussNorm.lean @@ -0,0 +1,135 @@ +/- + Copyright (c) 2025 Fabrizio Barroero. All rights reserved. + Released under Apache 2.0 license as described in the file LICENSE. + Authors: Fabrizio Barroero + -/ + import Mathlib.Analysis.Normed.Ring.Basic + import Mathlib.RingTheory.PowerSeries.Order + + /-! + # Gauss norm for power series + This file defines the Gauss norm for power series. Given a power series `f` in `R⟦X⟧`, a function + `v : R → ℝ` and a real number `c`, the Gauss norm is defined as the supremum of the set of all + values of `v (f.coeff R i) * c ^ i` for all `i : ℕ`. + ## Main Definitions and Results + * `PowerSeries.gaussNormC` is the supremum of the set of all values of `v (f.coeff R i) * c ^ i` + for all `i : ℕ`, where `f` is a power series in `R⟦X⟧`, `v : R → ℝ` is a function and `c` is a + real number. + * `PowerSeries.gaussNormC_nonneg`: if `v` is a non-negative function, then the Gauss norm is + non-negative. + * `PowerSeries.gaussNormC_eq_zero_iff`: if `v` is a non-negative function and `v x = 0 ↔ x = 0` for + all `x : R` and `c` is positive, then the Gauss norm is zero if and only if the power series is + zero. + -/ + + namespace PowerSeries + + variable {R F : Type*} [Semiring R] [FunLike F R ℝ] (v : F) (c : ℝ) (f : R⟦X⟧) + + /-- Given a power series `f` in `R⟦X⟧`, a function `v : R → ℝ` and a real number `c`, the Gauss norm + is defined as the supremum of the set of all values of `v (f.coeff R i) * c ^ i` for all `i : ℕ`. -/ + noncomputable def gaussNormC : ℝ := sSup {v (f.coeff i) * c ^ i | (i : ℕ)} + + @[simp] + theorem gaussNormC_zero [ZeroHomClass F R ℝ] : gaussNormC v c 0 = 0 := by simp [gaussNormC] + + private lemma gaussNormC_nonempty : {x | ∃ i, v (f.coeff i) * c ^ i = x}.Nonempty := by + use v (f.coeff 0) * c ^ 0, 0 + + lemma le_gaussNormC (hbd : BddAbove {x | ∃ i, v (f.coeff i) * c ^ i = x}) (i : ℕ) : + v (f.coeff i) * c ^ i ≤ f.gaussNormC v c := by + apply le_csSup hbd + simp + + theorem gaussNormC_nonneg [NonnegHomClass F R ℝ] : 0 ≤ f.gaussNormC v c := by + rw [gaussNormC] + by_cases h : BddAbove {x | ∃ i, v (f.coeff i) * c ^ i = x} + · rw [Real.le_sSup_iff h <| gaussNormC_nonempty v c f] + simp only [Set.mem_setOf_eq, zero_add, exists_exists_eq_and] + intro ε hε + use 0 + simpa using lt_of_lt_of_le hε <| apply_nonneg v (f.constantCoeff) + · simp [h] + + @[simp] + theorem gaussNormC_eq_zero_iff [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] {v : F} + (h_eq_zero : ∀ x : R, v x = 0 → x = 0) {f : R⟦X⟧} {c : ℝ} (hc : 0 < c) + (hbd : BddAbove {x | ∃ i, v (f.coeff i) * c ^ i = x}) : + f.gaussNormC v c = 0 ↔ f = 0 := by + refine ⟨?_, fun hf ↦ by simp [hf]⟩ + contrapose! + intro hf + apply ne_of_gt + obtain ⟨n, hn⟩ := exists_coeff_ne_zero_iff_ne_zero.mpr hf + calc + 0 < v (f.coeff n) * c ^ n := by + apply mul_pos _ (pow_pos hc _) + specialize h_eq_zero (f.coeff n) + simp_all only [ne_eq] + positivity + _ ≤ sSup {x | ∃ i, v (f.coeff i) * c ^ i = x} := by + rw [Real.le_sSup_iff hbd <| gaussNormC_nonempty v c f] + simp only [Set.mem_setOf_eq, exists_exists_eq_and] + intro ε hε + use n + simp [hε] + + + +--- All the above is what has been put into Mathlib... I want to generalise this to MVPowerSeries +--- Then show it forms a norm (absolute value...?) on restricted power series by the below work + +/- +section RestrictedPowerSeries + +variable [NormedRing R] + +lemma gaussNormC_bddabove: BddAbove {x | ∃ i, v (f.coeff i) * c ^ i = x} := by + sorry + + +lemma gaussNormC_existence (hf : IsRestricted R f c) : ∃ j : ℕ, + gaussNormC v c f = v (f.coeff R j) * c ^ j := by + sorry + + + +/-- The Gauss norm of the sum of two restricted power series is less than or equal to the maximum +of the Gauss norms of the two series. -/ +@[simp] +theorem gaussNormC_nonarchimedean (hf : IsRestricted R f c) (hg : IsRestricted R g c) (hc : 0 < c) + (hv : ∀ x y, v (x + y) ≤ max (v x) (v y)) : gaussNormC v c (f + g) ≤ max (gaussNormC v c f) + (gaussNormC v c g) := by + obtain ⟨i, hi⟩ := gaussNormC_existence v c f hf + obtain ⟨j, hj⟩ := gaussNormC_existence v c g hg + obtain ⟨l, hl⟩ := gaussNormC_existence v c (f + g) (PowerSeries.Restricted.add R c hf hg) + simp_rw [hi, hj, hl] + have final : v ((coeff R l) f + (coeff R l) g) * c^l ≤ max (v ((coeff R l) f) * c^l) + (v ((coeff R l) g) * c^l) := by + simpa only [le_sup_iff, hc, pow_pos, mul_le_mul_right, Rat.cast_le] using (hv (f.coeff R l) + (g.coeff R l)) + have hf2 (a : ℝ) (ha : a ∈ {x | ∃ i, v (f.coeff R i) * c ^ i = x}) := + le_csSup (gaussNormC_bddabove v c f) ha + simp only [Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at hf2 + have hg2 (a : ℝ) (ha : a ∈ {x | ∃ i, v (g.coeff R i) * c ^ i = x}) := + le_csSup (gaussNormC_bddabove v c g) ha + simp only [Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at hg2 + have h (a : ℝ) (q : PowerSeries R) (ha : a ∈ {x | ∃ i, v (q.coeff R i) * c ^ i = x}) := + le_csSup (gaussNormC_bddabove v c q) ha + simp only [Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at h + simp_rw [gaussNormC] at hi hj hl + rw [hi] at hf2 + rw [hj] at hg2 + rw [hl] at hl + simp only [le_sup_iff] at final ⊢ + rcases final with le1 | le2 + · left + exact le_trans le1 (hf2 l) + · right + exact le_trans le2 (hg2 l) + +end RestrictedPowerSeries + +-/ + +end PowerSeries diff --git a/PhD/Newton polygons/NPGeneral.lean b/PhD/Newton polygons/NPGeneral.lean new file mode 100644 index 0000000..8b44e44 --- /dev/null +++ b/PhD/Newton polygons/NPGeneral.lean @@ -0,0 +1,237 @@ +import Mathlib + +structure LowerConvexHull (K : Type*) [Field K] [LinearOrder K] [IsStrictOrderedRing K] where + /-- The number of points -/ + n : ℕ + /-- `x j` is the x-coordinate of the `j`th point when `0 ≤ j < n`. -/ + x : ℕ → K --may need to add Top for slope of infinite length + /-- `y j` is the y-coordinate of the `j`th point when `0 ≤ j < n`. -/ + y : ℕ → K + -- also may want to switch the y function to a set of slopes; will still need a first y value + /-- The x-coordinates are strictly increasing -/ + increasing : StrictMonoOn x (Set.Ico 0 n) + /-- The Newton polygon is lower convex. + This considers three successive points with indices `j`, `j+1` and `j+2`. -/ + -- We have a ≤ as we are allowing the slops to be the same for now. + + -- need to change this to < + convex : ∀ j : ℕ, j + 2 ≤ n → + x j * y (j + 2) + x (j + 1) * y j + x (j + 2) * y (j + 1) < + x j * y (j + 1) + x (j + 1) * y (j + 2) + x (j + 2) * y j + +namespace LowerConvexHull + +variable {K : Type*} [Field K] [LinearOrder K] [IsStrictOrderedRing K] + +/-- The slopes of a lower convex hull. -/ +def slope (U : LowerConvexHull K) (j : ℕ) : K := + (U.y (j + 1) - U.y j) / (U.x (j + 1) - U.x j) + +/-- The segments have positive (projected) length. -/ +lemma length_pos (U : LowerConvexHull K) {j : ℕ} (hj : j ∈ Set.Ico 0 (U.n - 1)) : + 0 < U.x (j + 1) - U.x j := by + rw [sub_pos] + simp only [Set.mem_Ico, zero_le, true_and] at hj + refine U.increasing ?_ ?_ (lt_add_one j) <;> simp <;> omega + +/-- The slopes are strictly increasing. -/ +lemma slope_MonotoneOn (U : LowerConvexHull K) : StrictMonoOn U.slope (Set.Ico 0 (U.n - 1)) := by + refine strictMono_of_le_succ Set.ordConnected_Ico ?_ -- find name + intro j hj₁ hj₂ hj₃ + simp only [slope] + have h₁ : 0 < U.x (j + 1) - U.x j := U.length_pos hj₂ + have h₂ : 0 < U.x (j + 2) - U.x (j + 1) := U.length_pos hj₃ + simp +arith only [Nat.succ_eq_succ, Nat.succ_eq_add_one] + rw [div_le_div_iff₀ h₁ h₂, ← sub_nonneg] + have := U.convex j (by simp at hj₃; omega) + rw [← sub_nonneg] at this + convert this using 1 + ring +------------------------------------------------------------------------------------------------ + + +/- +If we denote a finite set S in Prod K K by f_x : ℕ → K and f_y : ℕ → K indexing their +x and y points, with x values ordered, we want to compute its LowerConvexHull +-/ +variable (N : ℕ) -- Size of our finite set, i.e. only care for i < N in f_x and f_y +variable (f_x : ℕ → K) (f_y : ℕ → K) [hx : Fact (StrictMonoOn (f_x) (Set.Ico 0 N))] + +/- The set of slopes out of the point indexed by i -/ +def Set_of_Slopes (i : ℕ) : Set K := + Set.image (fun j => (f_y j - f_y i) / (f_x j - f_x i)) {j | j < N ∧ i < j} + +def Set_of_Slopes_isFinite (i : ℕ): Set.Finite (Set_of_Slopes N f_y f_x i) := by + apply Set.Finite.image + exact Set.Finite.sep (Set.finite_lt_nat N) (LT.lt i) + +noncomputable +def Set_of_Slopes_isFinset (i : ℕ) : Finset K := + Set.Finite.toFinset (Set_of_Slopes_isFinite N f_y f_x i) + +noncomputable +def MinSlope (i : ℕ) (Nonempty : Nonempty (Set_of_Slopes_isFinset N f_y f_x i)) : K := by + refine Finset.min' (Set_of_Slopes_isFinset N f_y f_x i ) ?_ + exact Finset.nonempty_coe_sort.mp Nonempty + +noncomputable +def NextPoint (i : ℕ) : ℕ := + letI := Classical.propDecidable (Nonempty (Set_of_Slopes_isFinset N f_y f_x i)) + if Nonempty : Nonempty (Set_of_Slopes_isFinset N f_y f_x i) then + letI := Classical.propDecidable + (∃ j : ℕ, i < j ∧ j < N ∧ (f_y j - f_y i) / (f_x j - f_x i) = MinSlope N f_x f_y i Nonempty) + if h : ∃ j : ℕ, i < j ∧ j < N ∧ (f_y j - f_y i) / (f_x j - f_x i) = MinSlope N f_x f_y i Nonempty + then Nat.find h -- need to find the maximum + else N - 1 -- only non-empty when we are at the final point (i.e. N - 1) + else N - 1 -- we remain at the final point we are interested in + +noncomputable +def Index_x : ℕ → ℕ + | 0 => 0 + | i + 1 => NextPoint N f_x f_y (Index_x i) + +--the final point will always be at the largest x value in the original set +noncomputable +def LowerConvexHull_n (h : (∃ i, Index_x N f_x f_y i = N - 1)) : ℕ := + Nat.find h + +noncomputable +def LowerConvexHull_set : LowerConvexHull K where + n := have h : (∃ i, Index_x N f_x f_y i = N - 1) := by + + -- by our construction, as the index set is only finite + sorry + LowerConvexHull_n N f_x f_y h + x := fun i => f_x (Index_x N f_x f_y i) + y := fun i => f_y (Index_x N f_x f_y i) + increasing := by + refine StrictMono.strictMonoOn ?_ (Set.Ico 0 (LowerConvexHull_n N f_x f_y sorry)) + refine strictMono_nat_of_lt_succ ?_ + intro r + cases r + · unfold Index_x NextPoint + simp only [nonempty_subtype] + split + · split + · -- need to check constructions + sorry + · -- same as below + sorry + · -- what happens when N = 0... so need to do cases + sorry + · + -- this is only true for n < N, so we have lost information somewhere! + sorry + convex := by + simp only + intro i hi + have h : + (f_y (Index_x N f_x f_y (i+1)) - f_y (Index_x N f_x f_y i)) / + (f_x (Index_x N f_x f_y (i+1)) - f_x (Index_x N f_x f_y i)) ≤ + (f_y (Index_x N f_x f_y (i+2)) - f_y (Index_x N f_x f_y i)) / + (f_x (Index_x N f_x f_y (i+1)) - f_x (Index_x N f_x f_y i)) := by + -- this is just showing the slope to a later point is greater; which worKs as both slopes are in + -- the set of slopes and the first one is the min + -- how to do this in lean? + ring_nf + obtain ⟨hx⟩ := hx + simp only [le_neg_add_iff_add_le, add_sub_cancel] + have : 0 < (f_x (Index_x N f_x f_y (i+1)) - f_x (Index_x N f_x f_y i)):= by + sorry + rw [mul_comm] + simp_rw [← div_eq_inv_mul] + simp only [div_le_div_iff_of_pos_right this] -- why does this not worK? + -- now we just need to show f_y is strictly mono; this is true by construction + + sorry + have h1 : + (f_y (Index_x N f_x f_y (i+1)) - f_y (Index_x N f_x f_y i)) * + (f_x (Index_x N f_x f_y (i+2)) - f_x (Index_x N f_x f_y i)) ≤ + (f_y (Index_x N f_x f_y (i+2)) - f_y (Index_x N f_x f_y i)) * + (f_x (Index_x N f_x f_y (i+1)) - f_x (Index_x N f_x f_y i)) := by + -- multiply out at h + + sorry + field_simp + + + + -- rearrange h1 + sorry + +end LowerConvexHull + +---------------------------------------------------------------------------------------------------- +namespace NewtonPolygons + +open Polynomial LowerConvexHull + +variable {K : Type*} [Field K] [LinearOrder K] [IsStrictOrderedRing K] +variable (f : Polynomial K) + +/- +It thus remains to find `N`, `f_x`, `f_y` for polynomials, and show `f_x` is strictly mono +-/ + +def coeff_set : Set ℕ := + Set.image (fun i => i) {i | i ≤ degree f ∧ coeff f i ≠ 0 } + +def coeff_set_is_finite : Set.Finite (coeff_set f) := by + apply Set.Finite.image + have : {i : ℕ | i ≤ degree f}.Finite := by + cases degree f + · simp only [le_bot_iff, WithBot.natCast_ne_bot, Set.setOf_false, Set.finite_empty] + · -- exact Set.finite_lt_nat ?_ -- i am unsure how to not grey out the a† + sorry + exact Set.Finite.sep this (fun i => coeff f i ≠ 0) + +/-- The number of coefficients that have non-zero coefficients-/ +noncomputable +def Polynomial_N : ℕ := + (coeff_set_is_finite f).toFinset.card + +noncomputable +def fun_x : ℕ → ℕ + | 0 => letI := Classical.propDecidable (∃ n : ℕ, coeff f n ≠ 0) + if h : ∃ n : ℕ, coeff f n ≠ 0 then (Nat.find h) + else 0 + | i + 1 => letI := Classical.propDecidable (∃ n : ℕ, coeff f n ≠ 0 ∧ n > fun_x i) + if h : ∃ n : ℕ, coeff f n ≠ 0 ∧ n > fun_x i then (Nat.find h) + else 0 + +/- There may be a better way to show that this is the inclusion of the function fun_x into K -/ +/-- The function indexing the first coord of the points in the relevant set to consider -/ +noncomputable +def fun_x' : ℕ → K := + fun i => fun_x f i + +/-- fun_x is strictly increasing -/ +def fun_x.isMono : (StrictMonoOn (fun_x' f) (Set.Ico 0 (Polynomial_N f))) := by + -- certainly true by construction; have coeff f fun_x (Polynomial_N f) ≠ 0 as fun_x (Polynomial_N f) = degree f + rw [StrictMonoOn] + simp only [Set.mem_Ico, zero_le, true_and] + intro a ha b hb hab + cases a + · + sorry + · + sorry + + +/-- The function indexing the second coord of the points in the relevant set to consider-/ +noncomputable +def fun_y : ℕ → K := + fun i => coeff f (fun_x f i) + +noncomputable +def NewtonPolygon : LowerConvexHull K := + LowerConvexHull_set (Polynomial_N f) (fun_x' f) (fun_y f) -- I thinK this is missing the requirement of strictly increasing + + + +-- I think I want to change this section... I need Newton polygon to be a function from +-- polynomials (powerseries) to lower convex hull! + + + +end NewtonPolygons diff --git a/PhD/Newton polygons/NPnew.lean b/PhD/Newton polygons/NPnew.lean new file mode 100644 index 0000000..7a0adf7 --- /dev/null +++ b/PhD/Newton polygons/NPnew.lean @@ -0,0 +1,124 @@ +import Mathlib + +structure LowerConvexHull (K : Type*) [Field K] [LinearOrder K] [IsStrictOrderedRing K] where + /-- The number of points -/ + n : ℕ -- we will want to add a withTop ℕ to resolve for powerseries in the future + /-- `x j` is the x-coordinate of the `j`th point when `0 ≤ j < n`. -/ + x : ℕ → K + /-- `y j` is the y-coordinate of the `j`th point when `0 ≤ j < n`. -/ + y : ℕ → K + /-- The x-coordinates are strictly increasing -/ + increasing : StrictMonoOn x (Set.Ico 0 n) + /-- The Newton polygon is lower convex. + This considers three successive points with indices `j`, `j+1` and `j+2`. -/ + -- We have a ≤ as we are allowing the slops to be the same for now. + convex : ∀ j : ℕ, j + 2 ≤ n → + x j * y (j + 2) + x (j + 1) * y j + x (j + 2) * y (j + 1) < + x j * y (j + 1) + x (j + 1) * y (j + 2) + x (j + 2) * y j + +namespace LowerConvexHull + +variable {K : Type*} [Field K] [LinearOrder K] [IsStrictOrderedRing K] + +/-- The slopes of a lower convex hull. -/ +def slope (U : LowerConvexHull K) (j : ℕ) : K := + (U.y (j + 1) - U.y j) / (U.x (j + 1) - U.x j) + +/-- The segments have positive (projected) length. -/ +lemma length_pos (U : LowerConvexHull K) {j : ℕ} (hj : j ∈ Set.Ico 0 (U.n - 1)) : + 0 < U.x (j + 1) - U.x j := by + rw [sub_pos] + simp only [Set.mem_Ico, zero_le, true_and] at hj + refine U.increasing ?_ ?_ (lt_add_one j) <;> simp <;> omega + +/-- The slopes are increasing. -/ +lemma slope_MonotoneOn (U : LowerConvexHull K) : StrictMonoOn U.slope (Set.Ico 0 (U.n - 1)) := by + refine strictMonoOn_of_lt_succ Set.ordConnected_Ico ?_ + intro j hj₁ hj₂ hj₃ + simp only [slope] + have h₁ : 0 < U.x (j + 1) - U.x j := U.length_pos hj₂ + have h₂ : 0 < U.x (j + 2) - U.x (j + 1) := U.length_pos hj₃ + simp +arith only [Nat.succ_eq_succ, Nat.succ_eq_add_one] + rw [div_lt_div_iff₀ h₁ h₂, ← sub_pos] + have := U.convex j (by simp at hj₃; omega) + rw [← sub_pos] at this + convert this using 1 + ring +------------------------------------------------------------------------------------------------ +/- +The goal is to give a function that sends a Polynomial R to a lower convexhull. +To do this I want to write this as a composition of two functions. +Function 1. Sends a Polynomial to a finite set of points + 2. Sends a finite set of points to its lower convex hull + +Function 1 should be straight forward... just do i ↦ (i, v(a_i)) + -- can probably leave it as a general function v for now +-/ + +section fun1 + +variable (M F : Type*) [Field M] [LinearOrder M] [IsStrictOrderedRing M] [FunLike F K M] (v : F) +-- Given a polynomial we want a 3-tuple of a natural number and two functions indexing the wanted points + +structure finset_Prod where -- maybe theres a nicer way to be doing this + n : ℕ -- number of points + x : ℕ → ℕ -- x values + y : ℕ → M -- y values + +-- Note the below will not work for powerseries, so maybe need to think of a better approach + +noncomputable +def Poly_set (f : Polynomial K) : finset_Prod M where + n := Finset.card {b : Fin (f.natDegree + 1) | Polynomial.coeff f b ≠ 0} + x := fun i => ((Finset.sort (· ≤ ·) + {b : Fin (f.natDegree + 1) | Polynomial.coeff f b ≠ 0}).getD i 0).val + -- copilot found this; need to work out if this seems fine practically to use + -- note will not work for infinite set cases + -- is 0 an okay junk value + y := fun i => if i < (Finset.card {b : Fin (f.natDegree + 1) | Polynomial.coeff f b ≠ 0}) + then v (Polynomial.coeff f i) + else 0 -- maybe want a better junk value for this + +end fun1 + + +section fun2 +/- +If we denote a finite set S in Prod K K by f_x : ℕ → K and f_y : ℕ → K indexing their +x and y points, with x values ordered, we want to compute its LowerConvexHull +-/ +variable (N : ℕ) -- Size of our finite set, i.e. only care for i < N in f_x and f_y +variable (f_x : ℕ → K) (f_y : ℕ → K) [hx : Fact (StrictMonoOn (f_x) (Set.Ico 0 N))] + + +noncomputable +def NextPoint (i : ℕ) : ℕ := + + sorry + +end fun2 + +variable (M F : Type*) [Field M] [LinearOrder M] [IsStrictOrderedRing M] [FunLike F K M] (v : F) + +/- +The goal is to give a function that sends a Polynomial R to a lower convexhull. +To do this I want to write this as a composition of two functions. +Function 1. Sends a Polynomial to a finite set of points + 2. Sends a finite set of points to its lower convex hull + +Function 1 should be straight forward... just do i ↦ (i, v(a_i)) + -- can probably leave it as a general function v for now +-/ + +-- will need to add more requirements on the R; i.e. normed ring + +noncomputable +def setOfPoly : Polynomial K → finset_Prod M := + fun f => (Poly_set M F v f) + +def setToLCH : (finset_Prod M) → (LowerConvexHull K) := by + + sorry + +def NewtonPolygon : Polynomial K → LowerConvexHull K := + setToLCH K ∘ (setOfPoly M F v) -- why :( diff --git a/PhD/RPS/OldRestrictedWork/RMV4.lean b/PhD/RPS/OldRestrictedWork/RMV4.lean new file mode 100644 index 0000000..97748d5 --- /dev/null +++ b/PhD/RPS/OldRestrictedWork/RMV4.lean @@ -0,0 +1,295 @@ +import Mathlib + +namespace RestrictedMvPowerSeries + +open MvPowerSeries Filter +open scoped Topology Pointwise + +def IsRestricted {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) (f : MvPowerSeries σ R) := + Tendsto (fun (t : σ →₀ ℕ) ↦ (norm (coeff t f)) * ∏ i ∈ t.support, c i ^ t i) Filter.cofinite (𝓝 0) + +lemma isRestricted_iff_abs {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) + (f : MvPowerSeries σ R) : IsRestricted c f ↔ IsRestricted |c| f := by + simp [IsRestricted, NormedAddCommGroup.tendsto_nhds_zero] + +lemma zero {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) : + IsRestricted c (0 : MvPowerSeries σ R) := by + simpa [IsRestricted] using tendsto_const_nhds + +/-- The set of `‖coeff t f‖ * ∏ i : t.support, c i ^ t i` for a given power series `f` + and tuple `c`. -/ +def convergenceSet {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) (f : MvPowerSeries σ R) : + Set ℝ := {‖(coeff t) f‖ * ∏ i : t.support, c i ^ t i | t : (σ →₀ ℕ)} + +lemma monomial {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) (n : σ →₀ ℕ) (a : R) : + IsRestricted c (monomial n a) := by + letI := Classical.typeDecidableEq σ + simp_rw [IsRestricted, coeff_monomial] + refine tendsto_nhds_of_eventually_eq ?_ + simp only [mul_eq_zero, norm_eq_zero, ite_eq_right_iff, + eventually_cofinite, not_or, Classical.not_imp] + have : {x | (x = n ∧ ¬a = 0) ∧ ¬∏ i ∈ x.support, c i ^ x i = 0} ⊆ {x | x = n} := by + simp only [Set.setOf_eq_eq_singleton, Set.subset_singleton_iff, Set.mem_setOf_eq, and_imp, + forall_eq, implies_true] + refine Set.Finite.subset ?_ this + aesop + +lemma one {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) : + IsRestricted c (1 : MvPowerSeries σ R) := by + exact monomial c 0 1 + +lemma C {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) (a : R) : + IsRestricted c (C (σ := σ) a) := by + simpa [monomial_zero_eq_C_apply] using monomial c 0 a + +lemma add {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) {f g : MvPowerSeries σ R} + (hf : IsRestricted c f) (hg : IsRestricted c g) : IsRestricted c (f + g) := by + rw [isRestricted_iff_abs, IsRestricted] at * + have := hf.add hg + simp only [Pi.abs_apply, add_zero] at this + have h0 : Tendsto (fun x : σ →₀ ℕ => 0) cofinite (nhds (0 : ℝ)) := by + rw [NormedAddCommGroup.tendsto_nhds_zero] + aesop + apply Filter.Tendsto.squeeze h0 this + <;> refine Pi.le_def.mpr ?_ + <;> intro n + · refine mul_nonneg (norm_nonneg _) ?_ + have : ∀ i ∈ n.support, 0 ≤ |c| i ^ n i := by + aesop + exact Finset.prod_nonneg fun i a ↦ this i a + · simp only [map_add] + have : ‖(coeff n) f + (coeff n) g‖ * ∏ i ∈ n.support, |c| i ^ n i ≤ + (‖(coeff n) f‖ + ‖coeff n g‖) * ∏ i ∈ n.support, |c| i ^ n i := by + refine mul_le_mul_of_nonneg (norm_add_le _ _) (by rfl) (by simp) ?_ + have : ∀ i ∈ n.support, 0 ≤ |c| i ^ n i := by + aesop + exact Finset.prod_nonneg fun i a ↦ this i a + simpa only [add_mul] using this + +lemma neg {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) {f : MvPowerSeries σ R} + (hf : IsRestricted c f) : IsRestricted c (- f) := by + rw [isRestricted_iff_abs, IsRestricted] at * + simpa using hf + +instance {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) : + AddSubgroup (MvPowerSeries σ R) where + carrier := IsRestricted c + zero_mem' := zero c + add_mem' := add c + neg_mem' := neg c + +lemma smul {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) {f : MvPowerSeries σ R} + (hf : IsRestricted c f) (r : R) : IsRestricted c (r • f) := by + rw [isRestricted_iff_abs, IsRestricted] at * + have : Tendsto (fun t ↦ ‖r‖ * ‖(coeff t) f‖ * ∏ i ∈ t.support, |c| i ^ t i) cofinite (𝓝 0) := by + have := Filter.Tendsto.const_mul ‖r‖ hf + grind + have h0 : Tendsto (fun x : σ →₀ ℕ => 0) cofinite (nhds (0 : ℝ)) := by + rw [NormedAddCommGroup.tendsto_nhds_zero] + aesop + apply Filter.Tendsto.squeeze h0 this + <;> refine Pi.le_def.mpr ?_ + <;> intro n + · refine mul_nonneg (norm_nonneg _) ?_ + have : ∀ i ∈ n.support, 0 ≤ |c| i ^ n i := by + aesop + exact Finset.prod_nonneg fun i a ↦ this i a + · refine mul_le_mul_of_nonneg (norm_mul_le _ _) (by rfl) (by simp) ?_ + have : ∀ i ∈ n.support, 0 ≤ |c| i ^ n i := by + aesop + exact Finset.prod_nonneg fun i a ↦ this i a + +lemma nsmul {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) (n : ℕ) + (f : MvPowerSeries σ R) (hf : IsRestricted c f) : IsRestricted c (n • f) := by + convert smul c hf (n : R) + ext _ _ + simp_rw [map_smul, smul_eq_mul, map_nsmul, nsmul_eq_mul] + +lemma zsmul {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) (n : ℤ) + (f : MvPowerSeries σ R) (hf : IsRestricted c f) : IsRestricted c (n • f) := by + convert smul c hf (n : R) + ext _ _ + simp_rw [map_smul, smul_eq_mul, map_zsmul, zsmul_eq_mul] + +open IsUltrametricDist + +def foo {S : Type*} [Nonempty S] {f : S → ℝ} (hf : Tendsto (fun i ↦ f i) cofinite (𝓝 0)) : + ∃ F, ∀ i, |f i| ≤ F := by + have ⟨a, ha⟩ := Tendsto.bddAbove_range_of_cofinite hf + have ⟨b, hb⟩ := Tendsto.bddBelow_range_of_cofinite hf + use max |a| |b| + intro i + rw [mem_upperBounds] at ha + specialize ha (f i) (by simp) + rw [mem_lowerBounds] at hb + specialize hb (f i) (by simp) + simp only [le_sup_iff] + rcases lt_or_ge (f i) 0 with h | h + · right + have : b < 0 := by + calc _ ≤ f i := hb + _ < 0 := h + have := le_of_lt this + have h := le_of_lt h + simp_all only [← abs_eq_neg_self] + aesop + · left + have : 0 ≤ a := by + calc _ ≤ f i := h + _ ≤ a := ha + simp_all only [← abs_eq_self] -- perhaps this is already done or can be done easier? + +def cofinite_max {S : Type*} [Nonempty S] {f : S → ℝ} + (hf : Tendsto (fun i ↦ f i) cofinite (𝓝 0)) : + ∃ F, 0 < F ∧ ∀ i : S, |f i| ≤ F := by + obtain ⟨F, hF⟩ := foo hf + use max F 1 + aesop + +lemma tendsto_antidiagonal {M S : Type*} [AddMonoid M] [Finset.HasAntidiagonal M] + {f g : M → S} [NormedRing S] [IsUltrametricDist S] {C : M → ℝ} + (hC : ∀ a b, C (a + b) = C a * C b) -- should this be stated differently? + -- need C to be monoid morphism to ℝ with mult + (hf : Tendsto (fun i ↦ ‖f i‖ * C i ) cofinite (𝓝 0)) + (hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)) : + Tendsto (fun a ↦ ‖∑ p ∈ Finset.antidiagonal a, (f p.1 * g p.2)‖ * C a) cofinite (𝓝 0) := by + obtain ⟨F, Fpos, hF⟩ := cofinite_max hf + have ⟨G, Gpos, hG⟩ := cofinite_max hg + simp only [NormedAddCommGroup.tendsto_nhds_zero, gt_iff_lt, Real.norm_eq_abs, eventually_cofinite, + not_lt] at * + intro ε hε + let I := {x | ε / G ≤ |‖f x‖ * C x|} + let J := {x | ε / F ≤ |‖g x‖ * C x|} + specialize hf (ε / G) (by positivity) + specialize hg (ε / F) (by positivity) + refine Set.Finite.subset (s := I + J) (Set.Finite.add (by aesop) (by aesop)) ?_ + by_contra h + obtain ⟨t, ht, ht'⟩ := Set.not_subset.mp h + simp only [abs_mul, abs_norm] at * + have hh (i j : M) (ht_eq : t = i + j) : i ∉ I ∨ j ∉ J := by + simp_rw [ht_eq] at ht' + contrapose ht' + simp only [not_or, not_not] at * + use i; use ht'.1; use j; use ht'.2 -- must be a nicer way to write this + have hij (i j : M) (ht_eq : t = i + j) : ‖f i * g j‖ * |C t| < ε := by + calc + _ ≤ ‖f i‖ * ‖g j‖ * |C t| := + mul_le_mul_of_nonneg (norm_mul_le _ _) (le_refl _) (norm_nonneg _) (abs_nonneg _) + _ ≤ ‖f i‖ * ‖g j‖ * (|C i| * |C j|) := + mul_le_mul_of_nonneg (le_refl _) (by simp [ht_eq, hC]) (by positivity) (by positivity) + _ = (‖f i‖ * |C i|) * (‖g j‖ * |C j|) := by + ring + _ < ε := by + rcases hh i j ht_eq with hi | hj + · rw [← div_mul_cancel₀ ε (ne_of_lt Gpos).symm] + exact mul_lt_mul_of_nonneg_of_pos (by aesop) (hG j) + (mul_nonneg (by positivity) (by positivity)) Gpos + · rw [← div_mul_cancel₀ ε (ne_of_lt Fpos).symm, mul_comm] + exact mul_lt_mul_of_nonneg_of_pos (by aesop) (hF i) + (mul_nonneg (by positivity) (by positivity)) Fpos + have Final : ‖∑ p ∈ Finset.antidiagonal t, f p.1 * g p.2‖ * |C t| < ε := by + obtain ⟨k, hk, leq⟩ := exists_norm_finset_sum_le (Finset.antidiagonal t) + (fun a ↦ f a.1 * g a.2) + calc + _ ≤ ‖f k.1 * g k.2‖ * |C t| := by + exact mul_le_mul_of_nonneg (leq) (le_refl _) (by positivity) (by positivity) + _ < ε := by + have : (Finset.antidiagonal t).Nonempty := by + refine Finset.nonempty_def.mpr ?_ + use (t, 0); simp + have : t = k.1 + k.2 := by + specialize hk this + simp only [Finset.mem_antidiagonal] at hk + exact hk.symm + exact hij k.1 k.2 this + grind + +-- I should probably change all of this to @[toAdd] as well + +lemma test1 {σ : Type*} (a b : σ →₀ ℕ) [DecidableEq σ] : + (a + b).support = a.support ∪ (b.support \ a.support) := by + apply Finset.Subset.antisymm_iff.mpr ?_ + constructor + · simpa using Finsupp.support_add + · intro i hi + simp only [Finsupp.mem_support_iff, Finsupp.coe_add, Pi.add_apply, ne_eq, Nat.add_eq_zero, + not_and] + simp only [Finset.mem_union, Finsupp.mem_support_iff, ne_eq] at hi + aesop + +lemma test2 {σ : Type*} (a b : σ →₀ ℕ) [DecidableEq σ] : + (a + b).support = (a.support \ b.support) ∪ b.support := by + apply Finset.Subset.antisymm_iff.mpr ?_ + constructor + · simp only [Finset.sdiff_union_self_eq_union] + exact Finsupp.support_add + · intro i hi + simp only [Finsupp.mem_support_iff, Finsupp.coe_add, Pi.add_apply, ne_eq, Nat.add_eq_zero, + not_and] + simp only [Finset.sdiff_union_self_eq_union, Finset.mem_union, Finsupp.mem_support_iff, + ne_eq] at hi + aesop + +lemma test3 {σ : Type*} (a b : σ →₀ ℕ) [DecidableEq σ] (f : σ → ℝ): ∏ i ∈ (a + b).support, f i = + (∏ i ∈ a.support, f i) * ∏ i ∈ (b.support \ a.support) , f i := by + rw [test1, Finset.prod_union] + exact Finset.disjoint_sdiff + +lemma test4 {σ : Type*} (a b : σ →₀ ℕ) [DecidableEq σ] (f : σ → ℝ) : ∏ i ∈ (a + b).support, f i = + (∏ i ∈ (a.support \ b.support), f i) * ∏ i ∈ b.support, f i := by + rw [test2, Finset.prod_union] + exact Finset.sdiff_disjoint + +lemma bar {σ : Type*} [DecidableEq σ] (c : σ → ℝ) (a b : σ →₀ ℕ) : ∏ i ∈ (a + b).support, |c| i ^ (a + b) i = + (∏ i ∈ a.support, |c| i ^ a i) * ∏ i ∈ b.support, |c| ↑i ^ b i := by + simp only [Pi.abs_apply, Finsupp.coe_add, Pi.add_apply] + simp_rw [pow_add, Finset.prod_mul_distrib] + rw [test3, test4] + have h1 : ∏ i ∈ a.support \ b.support, |c i| ^ b i = 1 := by + suffices (∀ i ∈ (a.support \ b.support), b i = 0) by + have : ∀ i ∈ (a.support \ b.support), |c i| ^ b i = 1 := by + aesop + exact Finset.prod_eq_one this + simp + have h2 : ∏ i ∈ b.support \ a.support, |c i| ^ a i = 1 := by + suffices (∀ i ∈ (b.support \ a.support), a i = 0) by + have : ∀ i ∈ (b.support \ a.support), |c i| ^ a i = 1 := by + aesop + exact Finset.prod_eq_one this + simp + simp only [h2, mul_one, h1, one_mul] + +lemma mul {R : Type*} [NormedRing R] [IsUltrametricDist R] {σ : Type*} (c : σ → ℝ) + {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) : + IsRestricted c (f * g) := by + letI := Classical.typeDecidableEq σ + letI : Finset.HasAntidiagonal (σ →₀ ℕ) := by + exact Finsupp.instHasAntidiagonal + rw [isRestricted_iff_abs, IsRestricted] at * + simp_rw [coeff_mul] + have := tendsto_antidiagonal (bar c) hf hg + exact this + +instance {R : Type*} [NormedRing R] [IsUltrametricDist R] {σ : Type*} (c : σ → ℝ) : + Subring (MvPowerSeries σ R) where + toAddSubgroup := RestrictedMvPowerSeries.instAddSubgroupMvPowerSeriesOfReal_phD c + one_mem' := one c + mul_mem' := mul c + + +-- we can use this to get an upper bound on cofinite things +-- Filter.Tendsto.bddAbove_range_of_cofinite hf + + +/- +/-- Promoting restricted mv power series to its own type. -/ +def Crestricted {R : Type*} [NormedRing R] {σ : Type*} (c : σ → ℝ) : Type _ := + Subtype (IsRestricted (R := R) (σ := σ) c) + +variable (R : Type*) [NormedRing R] {σ : Type*} (c : σ → ℝ) (f g : Crestricted (R := R) c) + +instance : AddGroup (Crestricted (R := R) c) := by + have := RestrictedMvPowerSeries.instAddSubgroupMvPowerSeriesOfReal_phD (R := R) c + -- maybe I am not doing this correctly?? + sorry +-/ diff --git a/PhD/RPS/RestrictedMV.lean b/PhD/RPS/OldRestrictedWork/RestrictedMV.lean similarity index 100% rename from PhD/RPS/RestrictedMV.lean rename to PhD/RPS/OldRestrictedWork/RestrictedMV.lean diff --git a/PhD/RPS/RestrictedMV2.lean b/PhD/RPS/OldRestrictedWork/RestrictedMV2.lean similarity index 100% rename from PhD/RPS/RestrictedMV2.lean rename to PhD/RPS/OldRestrictedWork/RestrictedMV2.lean diff --git a/PhD/RPS/def.lean b/PhD/RPS/OldRestrictedWork/def.lean similarity index 100% rename from PhD/RPS/def.lean rename to PhD/RPS/OldRestrictedWork/def.lean diff --git a/PhD/RPS/restrictedMV3.lean b/PhD/RPS/OldRestrictedWork/restrictedMV3.lean similarity index 97% rename from PhD/RPS/restrictedMV3.lean rename to PhD/RPS/OldRestrictedWork/restrictedMV3.lean index 03e9800..13910ae 100644 --- a/PhD/RPS/restrictedMV3.lean +++ b/PhD/RPS/OldRestrictedWork/restrictedMV3.lean @@ -21,6 +21,8 @@ lemma test {σ : Type*} (n : σ →₀ ℕ) : range_sum n = range_sum' n := by simp only [Nat.cast_id] -/ +-- Q : Do I need to change c from ℝ to σ → ℝ, i.e. a tuple instead of just a single value? + def IsRestricted {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} (f : MvPowerSeries σ R) := Tendsto (fun (t : σ →₀ ℕ) ↦ (norm (coeff t f)) * c^(range_sum t)) Filter.cofinite (𝓝 0) @@ -244,15 +246,14 @@ lemma zsmul {R : Type*} [NormedRing R] (c : ℝ) {σ : Type*} (n : ℤ) open IsUltrametricDist -lemma tendsto_antidiagonal {R S : Type*} [AddMonoid R] [Finset.HasAntidiagonal R] - {f g : R → S} [NormedRing S] - (hf : Tendsto (fun i ↦ ‖f i‖) cofinite (𝓝 0)) (hg : Tendsto (fun i ↦ ‖g i‖) cofinite (𝓝 0)) : - Tendsto (fun a ↦ ‖∑ p ∈ Finset.antidiagonal a, (f p.1 * g p.2)‖) cofinite (𝓝 0) := by +lemma tendsto_antidiagonal {R S C: Type*} [AddMonoid R] [Finset.HasAntidiagonal R] + {f g : R → S} [NormedRing S] [IsUltrametricDist S] {C : R → ℝ} -- need C to be monoid morphism to ℝ with mult + (hf : Tendsto (fun i ↦ ‖f i‖ * C i ) cofinite (𝓝 0)) + (hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)) : + Tendsto (fun a ↦ ‖∑ p ∈ Finset.antidiagonal a, (f p.1 * g p.2)‖ * C a) cofinite (𝓝 0) := by rw [@NormedAddCommGroup.tendsto_nhds_zero] at * simp only [gt_iff_lt, Real.norm_eq_abs, eventually_cofinite, not_lt] at * - -- this isnt true because we can just consider points - -- x = a + _ where a is in the finite set greater than ε sorry lemma mul' {R : Type*} [NormedRing R] [IsUltrametricDist R] {σ : Type*} diff --git a/blueprint/src/chapter/Fujisaki.tex b/blueprint/src/chapter/Fujisaki.tex index 76a4f32..80d7e6a 100644 --- a/blueprint/src/chapter/Fujisaki.tex +++ b/blueprint/src/chapter/Fujisaki.tex @@ -1 +1,304 @@ \chapter{Fujisaki's Lemma} + +This section aims to prove a classical result about the finiteness of a certain double coset. This +lemma plays a key role in determining that quaternionic modular forms are finite dimensional. + +This lemma was completed as part of Kevin Buzzard's FLT project; and we will use his blueprint +as reference (reference here!). + +\section{Prerequesites} + +\begin{definition} + A \emph{global field} is one of two types of fields: + \begin{itemize} + \item an algebraic number field; or + \item an irreducible algebraic curve over a finite field, or equivalently a finite extension + of $\mathbb{F}_q(T)$, the field of rational functions in one variable over a finite field + with $q = p^n$ elements. + \end{itemize} +\end{definition} + +\begin{definition} + A \emph{division algebra} is a ring in which every non-zero element has multiplicative inverse. +\end{definition} + +\begin{remark} + Non-split quaternion algebras are division algebras. To see this, recall split quaternion + algebras are isomorphic to $M_2 (K)$ and consider $\begin{pmatrix} 1 & 0 \\ 0 & 0 + \end{pmatrix}$, which clearly has no inverse. +\end{remark} + +For the lemma we let $B$ be a finite-dimensional division algebra over a global field $K$. + +%% May need another chapter where I define quaternion algebras and create such prerequesites... + +We will introduce the following notation: +\begin{align*} + &\underline{B} = B \otimes_K \mathds{A} \\ + &\underline{B}_f = B \otimes_K \mathds{A}_f \\ + &\underline{B}^{(1)} = \left\{ (x_\nu)_\nu \in \underline{B} : \prod_\nu | + \text{nrd}(x_\nu)|_\nu = 1\right\} +\end{align*} + +The main result we need is (reference).%%\cite[Theorem~27.6.14(a)]{Voight}. + +\begin{lemma}\label{Fujisaki} + Let $B$ be a finite-dimensional division algebra over a global field $F$, then the following + statements hold + \begin{itemize} + \item $B^\times \leq \underline{B}^{(1)}$ is cocompact + \item If $U$ is an open subgroup of $(\underline{B}_f )^\times$ + then the double coset space $B^\times \backslash (\underline{B}_f)^\times /U$ is finite. + \end{itemize} +\end{lemma} + + +\section{The proof} + +Within the FLT project we proved this lemma via a series of lemmas - for now directly copied from +his blueprint. + +%% TODO : make the notation consistent - e.g. B and D; differing notation for finite adeles! + +%% Not formalised by me. +\begin{lemma} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.existsE} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.existsE} + \leanok + There's a compact subset $E$ of $D_{\A}$ + with the property that for all $x\in D_{\A}^{(1)}$, + the obvious map $xE\to D\backslash D_{\A}$ is not injective. +\end{lemma} + +\begin{proof} + \leanok + We know that if we pick a $\Q$-basis for $D$ of size $d$ then this identifies $D$ with $\Q^d$, + $D_{\A}$ with $\A_{\Q}^d$, and $D\backslash D_{\A}$ with $(\Q\backslash\A_{\Q})^d$. Now $\Q$ is + discrete in $\A_{\Q}$, and the quotient $\Q\backslash \A_{\Q}$ is compact. + Hence, $D$ is discrete in $D_{\A}$ and the quotient $D\backslash D_{\A}$ is compact. + + Fix a Haar measure $\mu$ on $D_{\A}$ and push it forward to $D\backslash D_{\A}$; by compactness + this quotient has finite and positive measure, say $m\in\R_{>0}$. Choose any compact + $E\subseteq D_{\A}$ with measure $> m$ (for example, choose a $\Z$-lattice $L\cong\Z^d$ in + $D\cong\Q^d$, define $E_f:=\prod_p L_p\in D\otimes_{\Q}\A_{\Q}^\infty$, and define + $E_{\infty}\subseteq D\otimes_{\Q}\R\cong\R^n$ to be a huge closed ball, large enough to ensure + the measure of $E:=E_f\times E_{\infty}$ is bigger than $m$). Then $\mu(xE)=\mu(E)>m$ so the map + can't be injective. +\end{proof} + +\begin{definition} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.E} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.E} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.existsE} + \leanok + We let $E$ denote any compact set satisfying the hypothesis of the previous lemma. +\end{definition} + +\begin{definition} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.X} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.X} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.E} + \leanok +Define $X:=E-E:=\{e-f:e,f\in E\}\subseteq D_{\A}$. +\end{definition} + +\begin{definition} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.Y} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.Y} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.X} + \leanok +Define $Y:=X.X:=\{xy:x,y\in X\}\subseteq D_{\A}$. +\end{definition} + +\begin{lemma} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.X_compact} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.X_compact} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.X} + \leanok + $X$ is a compact subset of $D_{\A}$. +\end{lemma} +\begin{proof} + \leanok + It's the continuous image of the compact set~$E\times E$. +\end{proof} + +\begin{lemma} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.Y} + \leanok + $Y$ is a compact subset of $D_{\A}$. +\end{lemma} +\begin{proof} + \leanok + It's the continuous image of the compact set~$X\times X$. +\end{proof} + +\begin{lemma} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.X, NumberField.AdeleRing.DivisionAlgebra.Aux.E} + \leanok + If $\beta\in D_{\A}^{(1)}$ then +$\beta X\cap D^\times\not=\emptyset$. +\end{lemma} +\begin{proof} + \leanok +The map $\beta E\to D\backslash D_{\A}$ isn't injective, so there are distinct +$\beta e_1,\beta e_2\in \beta E$ with $e_i\in E$ and $\beta e_1-\beta e_2=b\in D$. Now $b\not=0$ +and $D$ is a division algebra, so $b\in D^\times$. And $e_1-e_2\in X$ so $b=\beta(e_1-e_2)\in +\beta X$, so we're done. +\end{proof} + +\begin{lemma} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel'} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel'} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.X} + \leanok + Similarly, if $\beta\in D_{\A}^{(1)}$ then $X\beta^{-1}\cap D^\times\not=\emptyset$. +\end{lemma} +\begin{proof} + \leanok + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.E, addHaarScalarFactor.left_mul_eq_right_mul} + Indeed, $\beta^{-1}\in D_{\A}^{(1)}$, and so left multiplication by $\beta^{-1}$ + doesn't change Haar measure on $D_{\A}$, so neither does right multiplication. + So the same argument works: $E\beta^{-1}\to D\backslash D_{\A}$ is not + injective so choose $e_1\beta^{-1}\not=e_2\beta^{-1}$ with difference $b\in D$ + and then $(e_1-e_2)\beta^{-1}\in D-{0}=D^\times$. +\end{proof} + +\begin{definition} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.T} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.T} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.Y} + \leanok + Let $T:=Y\cap D^\times$. +\end{definition} + +\begin{lemma} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.T} + \leanok + $T$ is finite. +\end{lemma} +\begin{proof} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact} + \leanok + It suffices to prove that $Y\cap D$ is finite. But $D\subseteq D_{\A}$ is a discrete additive + subgroup, and hence closed. And $Y\subseteq D_{\A}$ is compact. So $D\cap Y$ is compact and + discrete, so finite. +\end{proof} + +\begin{definition} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.C} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.C} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.T, NumberField.AdeleRing.DivisionAlgebra.Aux.X} + \leanok + Define $C:= (T^{-1}.X) \times X\subset D_{\A}\times D_{\A}$. +\end{definition} + +\begin{lemma} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.C_compact} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.C_compact} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.C, + NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite, + NumberField.AdeleRing.DivisionAlgebra.Aux.X_compact} + \leanok + $C$ is compact. +\end{lemma} +\begin{proof} + \leanok + $X$ is compact and $T$ is finite. +\end{proof} + +\begin{lemma} + \label{NumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C} + %\lean{NumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C} + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.C} + \leanok + For every $\beta\in D_{\A}^{(1)}$, there exists $b\in D^\times$ + and $\nu\in D_{\A}^{(1)}$ such that $\beta=b\nu$ and $(\nu,\nu^{-1})\in C.$ +\end{lemma} +\begin{proof} + \leanok + \uses{NumberField.AdeleRing.DivisionAlgebra.Aux.E, + NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel, + NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel', + NumberField.AdeleRing.DivisionAlgebra.Aux.C} + We have $\beta X\cap D^\times\not=\emptyset$, and $X\beta^{-1}\cap D^\times\not=\emptyset$, + so we can write $\beta x_1=b_1$ and $x_2\beta^{-1}=b_2$ with $b_i\in D^\times$ and $x_i\in X$. + Note that $\beta\in D_{\A}^{(1)}$ and $b_i\in D^{\times}\subseteq D_{\A}^{(1)}$, so + $x_i\in D_{\A}^{(1)}$ as well. In particular $x_i\in D_{\A}^\times$ so $x_1^{-1}$ makes sense. + + Multiplying the equations defining the $x_i$ and $b_i$ we deduce that + $x_2x_1=b_2b_1\in Y\cap D^\times=T$ (recall that $Y=X.X$ and $T=Y\cap D^\times$ is finite); call + this element $t$. Then $x_1^{-1}=t^{-1}x_2\in T^{-1}.X$, and $x_1\in X$, so if we set + $\nu=x_1^{-1}\in D_{\A}^{(1)}$ and $b=b_1\in D^\times$ then we have $\beta=b\nu$ and + $(\nu,\nu^{-1})\in C := (T^{-1}.X)\times X$. We are done! +\end{proof} + +We can now prove the first part of Fujisaki's lemma. + +\begin{proof} + \proves{NumberField.AdeleRing.DivisionAlgebra.compact_quotient} + \leanok + \uses{MeasureTheory.ringHaarChar_continuous, + NumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C, + NumberField.AdeleRing.DivisionAlgebra.Aux.C_compact} + Indeed, if $M$ is the preimage of $C$ under the inclusion $D_{\A}^{(1)} \to D_{\A}\times D_{\A}$ + sending $\nu$ to $(\nu,\nu^{-1})$, then $M$ is a closed subspace of a compact space so it's + compact (note that $\delta_{D_{\A}}$ is continuous, so $D_{\A}^{(1)}$ is a closed subset of + $D_{\A}^\times$ which is itself a closed subset of $D_{\A}\times D_{\A}$). $M$ surjects onto + $D^\times\backslash D_{\A}^{(1)}$ which is thus also compact. +\end{proof} + +And now the second part. + +\begin{theorem} + \label{NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact} + %\lean{NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact} + \leanok + $D^\times\backslash(D\otimes_K\A_K^\infty)^\times$ is compact. +\end{theorem} +\begin{proof} + \uses{NumberField.AdeleRing.DivisionAlgebra.compact_quotient} + \leanok +There's a natural map $\alpha$ from $D^\times\backslash D_{\A}^{(1)}$ to + $D^\times\backslash (D\otimes_K \A_K^\infty)^\times$. We claim that it's + surjective. Granted this claim, we are home, because if we put the quotient + topology on $D^\times\backslash (D\otimes_K \A_K^\infty)^\times$ coming from + $(D\otimes_K \A_K^\infty)^\times$ then it's readily verified that $\alpha$ + is continuous, and the continuous image of a compact space is compact. + + As for surjectivity: say $x\in (D\otimes_K \A_K^\infty)^\times$. We need to extend + $x$ to an element $(x,y)\in (D\otimes_K \A_K^\infty)^\times\times(D\otimes_K K_\infty)^\times$ + which is in the kernel of $\delta_{D_{\A}}$. Because $\delta_{D_{\A}}(x,1)$ is some positive + real number, it will suffice to show that if $r$ is any positive real number then we can + find $y\in (D\otimes_K \A_K^\infty)^\times=(D\otimes_{\Q}\R)^\times$ with $\delta_{D_{\A}}(1,y)=r$, + or equivalently (setting $D_{\R}=D\otimes_{\Q}\R$) that $\delta_{D_{\R}}(y)=r$. + But $D\not=0$ as it is a division algebra,and hence $\Q\subseteq D$, meaning + $\R\subseteq D_{\R}$, and if + $x\in\R^\times\subseteq D_{\R}^\times$ then $\delta(x)=|x|^d$ with $d=\dim_{\Q}(D)$, + as multiplication by $x$ is just scaling by a factor of $x$ on $D_{\R}\cong\R^d$. + In particular we can set $x=y^{1/d}$. +\end{proof} + +\begin{remark} In this generality the quotient might not be Hausdorff. +\end{remark} + +\begin{theorem} + \label{NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset} + %\lean{NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset} + \uses{NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact} + \leanok + If $U$ is an open subgroup of $(D\otimes_K \A_K^\infty)^\times$ + then the double coset space $D^\times\backslash(D\otimes_K \A_K^\infty)^\times/U$ is finite. +\end{theorem} +\begin{proof} + \leanok + The double cosets give a disjoint open cover of $(D\otimes_K \A_K^\infty)$ + which descends to a disjoint open cover of the quotient space + $D^\times\backslash(D\otimes_K \A_K^\infty)^\times$. However this space is compact + by theorem~\ref{NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact}. +\end{proof} diff --git a/blueprint/src/chapter/RPS.tex b/blueprint/src/chapter/RPS.tex index 2201727..17349f2 100644 --- a/blueprint/src/chapter/RPS.tex +++ b/blueprint/src/chapter/RPS.tex @@ -1,5 +1,144 @@ \chapter{Restricted Power Series} +\section{Definition} + +Recall formal multivariate power series over a set $K$ in $n$ variables, written +$K [ \! [ x_1, \dots, x_n ] \! ]$ are infinite sums +\[ + f(x) = \sum a_{(i_1, \cdots, i_n)} x_1^{i_1} \cdots x_n^{i_n}, +\] +where the sum is taken over all $n$-tuples $(i_1, \cdots i_n)$ with $i_j \in \mathbb{N}$ and +$a_{(i_1, \cdots, i_n)} \in K$. + +When $K$ is a ring, formal multivariate power series in $n$ variables form a ring, and we will refer +to them as the ring of power series over $K$ in $n$ variables. We again denote such +rings using $K [ \! [ x_1, \dots, x_n ] \! ]$. + +We define a subset of $K [ \! [ x_1, \dots, x_n ] \! ]$ that consists of power series whose +coefficeients approach zero in the cofinite filter. + +\begin{definition} + \label{IsRestricted} + \lean{IsRestricted} + \leanok + Let $f$ be a power series over a normed ring $R$ in one variable, write + $f(x) = \sum a_{(i_1, \cdots, i_n)} x_1^{i_1} \cdots x_n^{i_n},$, and let + $c = (c_1, \cdots, c_n)$ be an $n$-tuple of real numbers. + We say $f$ is a restricted power series of parameter $c$ over $R$ in $n$ variables if + \[ + \lim_{n \to \infty} \lvert a_{(i_1, \cdots, i_n)} \rvert \prod_{j=1}^{n} c_j^{i_j} = 0 + \] + in the cofinite topology. + + We denote the set of restricted power series of parameter $c$ over $R$ in $n$ variables by + $R_c [ \! [ x_1, \dots, x_n ] \! ]$. +\end{definition} + +\begin{remark} + Note + \[ + \lim \lvert a_{(i_1, \cdots, i_n)} \rvert \prod_{j=1}^{n} c_j^{i_j} = 0 + \] + in the cofinite topology, if for all $0 < \epsilon$ there are finitely many $n$-tuples that have + $\left \lvert \lvert a_{(i_1, \cdots, i_n)} \rvert \prod_{j=1}^{n} c_j^{i_j} \right \rvert$ + greater than $\varepsilon$. +\end{remark} + +\section{Additive Group} + +It turns out that restricted power series of parameter $c$ over a normed ring $R$ in $n$ variables +are not just a set, in fact they form an additive group. + +\begin{theorem} + For any normed ring $R$, $n \in \mathbb{N}$ and $c \in \mathbb{R}^n$. Then + $R_c [ \! [ x_1, \dots, x_n ] \! ]$ forms an additive group. +\end{theorem} + +Let $R$ be a normed ring, $n \in \N$ and $c \in \mathbb{R}^n$ +We prove this in lean using the following lemmas. + +\begin{lemma} + \label{isRestricted_iff_abs} + \lean{isRestricted_iff_abs} + \leanok + \uses{IsRestricted} %% Do I need to say uses in all the statements? + $f \in R_c [ \! [ x_1, \dots, x_n ] \! ]$ if and only if $f \in R_{\lvert c \rvert} + [ \! [ x_1, \dots, x_n ] \! ]$. + That is we can always consider $c$ to have positive entries. +\end{lemma} + +\begin{proof} + \[ + \left \lvert \lvert a_{(i_1, \cdots, i_n)} \rvert \prod_{j=1}^{j=n} c_j^{i_j} \right \rvert = + \left \lvert \lvert a_{(i_1, \cdots, i_n)} \rvert \prod_{j=1}^{j=n} \lvert c \rvert _j^{i_j} + \right \rvert. + \] +\end{proof} + +\begin{lemma} + \label{zero} + \lean{zero} + \leanok + $0 \in R_c [ \! [ x_1, \dots, x_n ] \! ]$. +\end{lemma} + +\begin{proof} + Substitute the zero power series into the definition - every coefficient is 0, thus we are + immediately done. +\end{proof} + +\begin{lemma} + \label{monomial} + \lean{monomial} + \leanok + Any monomial $m = a_{(i_1, \cdots, i_n)} x_1^{i_1} \cdots x_n^{i_n}$ is restricted. +\end{lemma} + +\begin{proof} + Only one coefficient is non-zero. +\end{proof} + +\begin{lemma} + \label{One} + \lean{One} + \leanok + \uses{monomial} + $1 \in R_c [ \! [ x_1, \dots, x_n ] \! ]$. +\end{lemma} + +\begin{proof} + 1 is a monomial. +\end{proof} + +\begin{lemma} + \label{add} + \lean{add} + \leanok + \uses{IsRestricted, isRestricted_iff_abs} + If $f, g \in R_c [ \! [ x_1, \dots, x_n ] \! ]$ then $f+g \in R_c [ \! [ x_1, \dots, x_n ] \! ]$. +\end{lemma} + +\begin{proof} + Squeeze theorem. +\end{proof} + +\begin{lemma} + \label{neg} + \lean{neg} + \leanok + \uses{IsRestricted, isRestricted_iff_abs} + +\end{lemma} + +\begin{proof} + \[ + \left \lvert \lvert a_{(i_1, \cdots, i_n)} \rvert \prod_{j=1}^{n} c_j^{i_j} \right \rvert = + \left \lvert \lvert - a_{(i_1, \cdots, i_n)} \rvert \prod_{j=1}^{n} c_j^{i_j} \right \rvert. + \] +\end{proof} + +\iffalse + Formal power series over a set $K$ in one variable, written $K [ \! [ x ] \! ] $, are infinite sums \[ @@ -25,8 +164,9 @@ \chapter{Restricted Power Series} $f = \sum_{n=0}^\infty a_n x^n$, and let $c$ be a real number. We say $f$ is a restricted power series of parameter $c$ over $K$ if \[ - \lim_{n \to \infty} \lvert a_n \rvert c^n = 0. + \lim_{n \to \infty} \lvert a_n \rvert c^n = 0 \] + in the cofinite topology. \end{definition} Note this is not the same as convergent power series in the usual sense unless $R$ is complete, @@ -42,6 +182,10 @@ \chapter{Restricted Power Series} Restricted power series over a normed ring $R$ form an additive group. \end{theorem} +\section{Additive Group} + +To prove that they form a ring in + Moreover, if the norm of $R$ has the non-archimedean property, \begin{definition*} @@ -89,3 +233,5 @@ \chapter{Restricted Power Series} As mentioned earlier, this set is equivalent to power series that converge on the ball of radius $c$, and so sometimes in literature the Tate algebra may be referenced as convergent power series. + +\fi diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index 59d9c82..1754832 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -39,6 +39,9 @@ \usepackage{etexcmds} \usepackage{thmtools} +\usepackage{cancel} +\usepackage{dsfont} + \input{macro/print} diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex index f46523b..15b95b6 100644 --- a/blueprint/src/web.tex +++ b/blueprint/src/web.tex @@ -17,6 +17,9 @@ \usepackage{tikz-cd} \usepackage{tikz} +\usepackage{cancel} +\usepackage{dsfont} + \input{macro/common} \input{macro/web} From 635bbec8423d62f0cece63ad3ca498c9185a0754 Mon Sep 17 00:00:00 2001 From: WilliamCoram Date: Wed, 21 Jan 2026 16:36:29 +0000 Subject: [PATCH 4/4] oops --- PhD.lean | 1 - blueprint/src/chapter/RPS.tex | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/PhD.lean b/PhD.lean index c60e64d..e69de29 100644 --- a/PhD.lean +++ b/PhD.lean @@ -1 +0,0 @@ -import PhD.RPS.def diff --git a/blueprint/src/chapter/RPS.tex b/blueprint/src/chapter/RPS.tex index 17349f2..f1cd4aa 100644 --- a/blueprint/src/chapter/RPS.tex +++ b/blueprint/src/chapter/RPS.tex @@ -127,7 +127,7 @@ \section{Additive Group} \lean{neg} \leanok \uses{IsRestricted, isRestricted_iff_abs} - + If $f \in R_c [ \! [ x_1, \dots, x_n ] \! ]$ then $-f \in R_c [ \! [ x_1, \dots, x_n ] \! ]$. \end{lemma} \begin{proof}