From 127de0cf1cfe4388059ffe6945fd866e45792a99 Mon Sep 17 00:00:00 2001
From: Salvatore Mercuri <47568553+smmercuri@users.noreply.github.com>
Date: Sun, 2 Feb 2025 22:30:43 +0000
Subject: [PATCH] Various results useful for weak approximation (#322)

* Weak approximation for infinite places

* Refactor and document weak approximation

* Remove unnecessary limit results

* Fix imports

* Refactor absolute value results

* helper results for weak approximation
---
 FLT/Mathlib/Analysis/Normed/Ring/WithAbs.lean | 17 +++++++++++++++++
 FLT/Mathlib/Data/Fin/Basic.lean               | 13 +++++++++++++
 FLT/Mathlib/Data/Finset/Lattice/Fold.lean     | 17 +++++++++++++++++
 FLT/Mathlib/Topology/Constructions.lean       |  7 +++++++
 4 files changed, 54 insertions(+)
 create mode 100644 FLT/Mathlib/Analysis/Normed/Ring/WithAbs.lean
 create mode 100644 FLT/Mathlib/Data/Fin/Basic.lean
 create mode 100644 FLT/Mathlib/Data/Finset/Lattice/Fold.lean

diff --git a/FLT/Mathlib/Analysis/Normed/Ring/WithAbs.lean b/FLT/Mathlib/Analysis/Normed/Ring/WithAbs.lean
new file mode 100644
index 00000000..1a11a691
--- /dev/null
+++ b/FLT/Mathlib/Analysis/Normed/Ring/WithAbs.lean
@@ -0,0 +1,17 @@
+import Mathlib.Analysis.Normed.Ring.WithAbs
+import Mathlib.NumberTheory.NumberField.Basic
+
+namespace WithAbs
+
+variable {K : Type*} [Field K] {v : AbsoluteValue K ℝ}
+  {L : Type*} [Field L] [Algebra K L] {w : AbsoluteValue L ℝ}
+
+instance : Algebra (WithAbs v) (WithAbs w) := ‹Algebra K L›
+
+instance : Algebra K (WithAbs w) := ‹Algebra K L›
+
+instance [NumberField K] : NumberField (WithAbs v) := ‹NumberField K›
+
+theorem norm_eq_abs (x : WithAbs v) : ‖x‖ = v x := rfl
+
+end WithAbs
diff --git a/FLT/Mathlib/Data/Fin/Basic.lean b/FLT/Mathlib/Data/Fin/Basic.lean
new file mode 100644
index 00000000..3be6dff9
--- /dev/null
+++ b/FLT/Mathlib/Data/Fin/Basic.lean
@@ -0,0 +1,13 @@
+import Mathlib.Data.Fin.Basic
+import Mathlib.Data.Fin.VecNotation
+import Mathlib.Logic.Pairwise
+
+theorem Fin.castPred_ne_zero {n : ℕ} {j : Fin (n + 2)} (h₁ : j ≠ Fin.last (n + 1)) (h₂ : j ≠ 0) :
+    Fin.castPred j h₁ ≠ 0 := by
+  contrapose! h₂
+  rwa [← Fin.castPred_zero, Fin.castPred_inj] at h₂
+
+theorem Fin.pairwise_forall_two {n : ℕ} {r : Fin (n + 2) → Fin (n + 2) → Prop} (h : Pairwise r) :
+    Pairwise (r.onFun ![0, Fin.last _]) := by
+  apply Pairwise.comp_of_injective h
+  simp [Function.Injective, Fin.forall_fin_two]
diff --git a/FLT/Mathlib/Data/Finset/Lattice/Fold.lean b/FLT/Mathlib/Data/Finset/Lattice/Fold.lean
new file mode 100644
index 00000000..7779c430
--- /dev/null
+++ b/FLT/Mathlib/Data/Finset/Lattice/Fold.lean
@@ -0,0 +1,17 @@
+import Mathlib.Data.Finset.Lattice.Fold
+
+ theorem Finset.le_sup_dite_pos {α β : Type*} [SemilatticeSup α] [OrderBot α] {s : Finset β}
+    (p : β → Prop) [DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β}
+    (h₀ : b ∈ s) (h₁ : p b) :
+    f b h₁ ≤ s.sup fun i => if h : p i then f i h else g i h := by
+  have : f b h₁ = (fun i => if h : p i then f i h else g i h) b := by simp [h₁]
+  rw [this]
+  apply Finset.le_sup h₀
+
+  theorem Finset.le_sup_dite_neg {α β : Type*} [SemilatticeSup α] [OrderBot α] {s : Finset β}
+    (p : β → Prop) [DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β}
+    (h₀ : b ∈ s) (h₁ : ¬p b) :
+    g b h₁ ≤ s.sup fun i => if h : p i then f i h else g i h := by
+  have : g b h₁ = (fun i => if h : p i then f i h else g i h) b := by simp [h₁]
+  rw [this]
+  apply Finset.le_sup h₀
diff --git a/FLT/Mathlib/Topology/Constructions.lean b/FLT/Mathlib/Topology/Constructions.lean
index f901723e..100a04ec 100644
--- a/FLT/Mathlib/Topology/Constructions.lean
+++ b/FLT/Mathlib/Topology/Constructions.lean
@@ -1,7 +1,14 @@
 import Mathlib.Topology.Constructions
+import Mathlib.Topology.ContinuousOn
 
 theorem TopologicalSpace.prod_mono {α β : Type*} {σ₁ σ₂ : TopologicalSpace α}
     {τ₁ τ₂ : TopologicalSpace β} (hσ : σ₁ ≤ σ₂) (hτ : τ₁ ≤ τ₂) :
     @instTopologicalSpaceProd α β σ₁ τ₁ ≤ @instTopologicalSpaceProd α β σ₂ τ₂ :=
   le_inf (inf_le_left.trans  <| induced_mono hσ)
          (inf_le_right.trans  <| induced_mono hτ)
+
+theorem DenseRange.piMap {ι : Type*} {X Y : ι → Type*} [∀ i, TopologicalSpace (Y i)]
+    {f : (i : ι) → (X i) → (Y i)} (hf : ∀ i, DenseRange (f i)):
+    DenseRange (Pi.map f) := by
+  rw [DenseRange, Set.range_piMap]
+  exact dense_pi Set.univ (fun i _ => hf i)