From adf405032e36b9749d607a61c6a237a3ab9e06c5 Mon Sep 17 00:00:00 2001 From: pfaffelh Date: Wed, 14 Jan 2026 22:13:29 +0100 Subject: [PATCH 01/26] run mk_all --- Mathlib.lean | 1 + Mathlib/Data/Set/Dissipate.lean | 144 ++++++++++++++++++++++++++++++++ 2 files changed, 145 insertions(+) create mode 100644 Mathlib/Data/Set/Dissipate.lean diff --git a/Mathlib.lean b/Mathlib.lean index eb8d20cf89f142..126e2b9490901b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3968,6 +3968,7 @@ public import Mathlib.Data.Set.Constructions public import Mathlib.Data.Set.Countable public import Mathlib.Data.Set.Defs public import Mathlib.Data.Set.Disjoint +public import Mathlib.Data.Set.Dissipate public import Mathlib.Data.Set.Enumerate public import Mathlib.Data.Set.Equitable public import Mathlib.Data.Set.Finite.Basic diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean new file mode 100644 index 00000000000000..dab5d439281991 --- /dev/null +++ b/Mathlib/Data/Set/Dissipate.lean @@ -0,0 +1,144 @@ +/- +Copyright (c) 2025 Peter Pfaffelhuber. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Peter Pfaffelhuber +-/ +module + +public import Mathlib.Data.Set.Accumulate +public import Mathlib.MeasureTheory.PiSystem + +/-! +# Dissipate + +The function `dissipate` takes `s : α → Set β` with `LE α` and returns `⋂ y ≤ x, s y`. + +In large parts, this file is parallel to `Mathlib.Data.Set.Accumulate`, where +`Accumulate s := ⋃ y ≤ x, s y` is defined. + +-/ + +@[expose] public section + +open Nat + +variable {α β : Type*} {s : α → Set β} + +namespace Set + +/-- `dissipate s` is the intersection of `s y` for `y ≤ x`. -/ +def dissipate [LE α] (s : α → Set β) (x : α) : Set β := + ⋂ y ≤ x, s y + +theorem dissipate_def [LE α] {x : α} : dissipate s x = ⋂ y ≤ x, s y := rfl + +theorem dissipate_eq {s : ℕ → Set β} {n : ℕ} : dissipate s n = ⋂ k < n + 1, s k := by + simp_rw [Nat.lt_add_one_iff, dissipate] + +@[simp] +theorem dissipate_eq_accumulate_compl [LE α] {s : α → Set β} {x : α} : + (Set.accumulate (fun y ↦ (s y)ᶜ) x)ᶜ = dissipate s x := by + simp [accumulate_def, dissipate_def] + +@[simp] +theorem accumulate_eq_dissipate_compl [LE α] {s : α → Set β} {x : α} : + (Set.dissipate (fun y ↦ (s y)ᶜ) x)ᶜ = accumulate s x := by + simp [accumulate_def, dissipate_def] + +@[simp] +theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by + simp [dissipate_def] + +theorem dissipate_subset [LE α] {x y : α} (hy : y ≤ x) : dissipate s x ⊆ s y := + biInter_subset_of_mem hy + +theorem iInter_subset_dissipate [LE α] (x : α) : ⋂ i, s i ⊆ dissipate s x := by + simp only [dissipate, subset_iInter_iff] + exact fun x h ↦ iInter_subset_of_subset x fun ⦃a⦄ a ↦ a + +theorem antitone_dissipate [Preorder α] : Antitone (dissipate s) := + fun _ _ hab ↦ biInter_subset_biInter_left fun _ hz => le_trans hz hab + +@[gcongr] +theorem dissipate_subset_dissipate [Preorder α] {x y} (h : y ≤ x) : + dissipate s x ⊆ dissipate s y := + antitone_dissipate h + +@[simp] +theorem dissipate_dissipate [Preorder α] {s : α → Set β} {x : α} : + ⋂ y, ⋂ (_ : y ≤ x), dissipate s y = dissipate s x := by + apply Subset.antisymm + · apply iInter_mono fun z y hy ↦ ?_ + simp only [mem_iInter, mem_dissipate] at * + exact fun h ↦ hy h z (le_refl z) + · simp only [subset_iInter_iff] + exact fun i j ↦ dissipate_subset_dissipate j + +@[simp] +theorem iInter_dissipate [Preorder α] : ⋂ x, dissipate s x = ⋂ x, s x := by + apply Subset.antisymm <;> simp_rw [subset_def, dissipate_def, mem_iInter] + · exact fun z h x' ↦ h x' x' (le_refl x') + · exact fun z h x' y hy ↦ h y + +@[simp] +lemma dissipate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : dissipate s ⊥ = s ⊥ := by + simp [dissipate_def] + +open Nat + +@[simp] +theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) : + dissipate s (n + 1) = (dissipate s n) ∩ s (n + 1) + := by + ext x + simp_all only [dissipate_def, mem_iInter, mem_inter_iff] + grind + +@[simp] +lemma dissipate_zero (s : ℕ → Set β) : dissipate s 0 = s 0 := by + simp [dissipate_def] + +/-- For a directed set of sets `s : ℕ → Set α` (i.e. `∀ i j, ∃ k, s k ⊆ s i ∩ s j`) and `n : ℕ`, +there exists `m : ℕ` (maybe larger than `n`) such that `s m ⊆ dissipate s n`. -/ +lemma exists_subset_dissipate_of_directed {s : ℕ → Set α} + (hd : Directed (fun (x y : Set α) => y ⊆ x) s) (n : ℕ) : ∃ m, s m ⊆ dissipate s n := by + induction n with + | zero => use 0; simp [dissipate_def] + | succ n hn => + obtain ⟨m, hm⟩ := hn + simp_rw [dissipate_succ] + obtain ⟨k, hk⟩ := hd m (n+1) + simp only at hk + use k + simp only [subset_inter_iff] + exact ⟨le_trans hk.1 hm, hk.2⟩ + +lemma directed_dissipate {s : ℕ → Set α} : + Directed (fun (x y : Set α) => y ⊆ x) (dissipate s) := + antitone_dissipate.directed_ge + +lemma exists_dissipate_eq_empty_iff_of_directed (C : ℕ → Set α) + (hd : Directed (fun (x y : Set α) => y ⊆ x) C) : + (∃ n, dissipate C n = ∅) ↔ (∃ n, C n = ∅) := by + refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n, ?_⟩⟩ + · rw [← not_imp_not] + push_neg + intro h n + obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n + exact Set.Nonempty.mono hm (h m) + · exact subset_eq_empty (dissipate_subset (Nat.le_refl n)) hn + +/-- For a ∩-stable set of sets `p` on `α` and a sequence of sets `s` with this attribute, +`dissipate s n` belongs to `p`. -/ +lemma IsPiSystem.dissipate_mem {s : ℕ → Set α} {p : Set (Set α)} + (hp : IsPiSystem p) (h : ∀ n, s n ∈ p) (n : ℕ) (h' : (dissipate s n).Nonempty) : + (dissipate s n) ∈ p := by + induction n with + | zero => + simp only [dissipate_def, le_zero_eq, iInter_iInter_eq_left] + exact h 0 + | succ n hn => + rw [dissipate_succ] at * + apply hp (dissipate s n) (hn (Nonempty.left h')) (s (n+1)) (h (n+1)) h' + +end Set From 3fffde0d8cbd644c6ae8af7fa6c90b52e0deace7 Mon Sep 17 00:00:00 2001 From: pfaffelh Date: Mon, 2 Mar 2026 23:50:56 +0100 Subject: [PATCH 02/26] like pfaffelh_compactSystem but in the module system --- Mathlib/Data/Set/Dissipate.lean | 47 +++ .../Topology/Compactness/CompactSystem.lean | 286 ++++++++++++++++++ 2 files changed, 333 insertions(+) create mode 100644 Mathlib/Topology/Compactness/CompactSystem.lean diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index ee403dacb2b95f..8757e7fe156b31 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -7,6 +7,7 @@ Authors: Peter Pfaffelhuber module public import Mathlib.Data.Set.Accumulate +public import Mathlib.MeasureTheory.PiSystem /-! # Dissipate @@ -28,6 +29,9 @@ def dissipate [LE α] (s : α → Set β) (x : α) : Set β := theorem dissipate_def [LE α] {x : α} : dissipate s x = ⋂ y ≤ x, s y := rfl +theorem dissipate_eq {s : ℕ → Set β} {n : ℕ} : dissipate s n = ⋂ k < n + 1, s k := by + simp_rw [Nat.lt_add_one_iff, dissipate] + @[simp] theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by simp [dissipate_def] @@ -80,4 +84,47 @@ theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) : simp_all only [dissipate_def, mem_iInter, mem_inter_iff] grind +/-- For a directed set of sets `s : ℕ → Set α` and `n : ℕ`, there exists `m : ℕ` (maybe +larger than `n`)such that `s m ⊆ dissipate s n`. -/ +lemma exists_subset_dissipate_of_directed {s : ℕ → Set α} + (hd : Directed (fun (x y : Set α) => y ⊆ x) s) (n : ℕ) : ∃ m, s m ⊆ dissipate s n := by + induction n with + | zero => use 0; simp [dissipate_def] + | succ n hn => + obtain ⟨m, hm⟩ := hn + simp_rw [dissipate_succ] + obtain ⟨k, hk⟩ := hd m (n+1) + simp only at hk + use k + simp only [subset_inter_iff] + exact ⟨le_trans hk.1 hm, hk.2⟩ + +lemma directed_dissipate {s : ℕ → Set α} : + Directed (fun (x y : Set α) => y ⊆ x) (dissipate s) := + antitone_dissipate.directed_ge + +lemma exists_dissipate_eq_empty_iff_of_directed (C : ℕ → Set α) + (hd : Directed (fun (x y : Set α) => y ⊆ x) C) : + (∃ n, C n = ∅) ↔ (∃ n, dissipate C n = ∅) := by + refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, ?_⟩ , ?_⟩ + · exact subset_eq_empty (dissipate_subset (Nat.le_refl n)) hn + · rw [← not_imp_not] + push_neg + intro h n + obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n + exact Set.Nonempty.mono hm (h m) + +/-- For a ∩-stable set of sets `p` on `α` and a sequence of sets `s` with this attribute, +`dissipate s n` belongs to `p`. -/ +lemma IsPiSystem.dissipate_mem {s : ℕ → Set α} {p : Set (Set α)} + (hp : IsPiSystem p) (h : ∀ n, s n ∈ p) (n : ℕ) (h' : (dissipate s n).Nonempty) : + (dissipate s n) ∈ p := by + induction n with + | zero => + simp only [dissipate_def, Nat.le_zero_eq, iInter_iInter_eq_left] + exact h 0 + | succ n hn => + rw [dissipate_succ] at * + apply hp (dissipate s n) (hn (Nonempty.left h')) (s (n+1)) (h (n+1)) h' + end Set diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean new file mode 100644 index 00000000000000..9c35597af62d23 --- /dev/null +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -0,0 +1,286 @@ +/- +Copyright (c) 2025 Peter Pfaffelhuber. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne, Peter Pfaffelhuber +-/ +module + +public import Mathlib.Data.Set.Dissipate +public import Mathlib.Topology.Separation.Hausdorff + +/-! +# Compact systems. + +This file defines compact systems of sets. + +## Main definitions + +* `IsCompactSystem`: A set of sets is a compact system if, whenever a countable subfamily has empty + intersection, then finitely many of them already have empty intersection. + +## Main results + +* `IsCompactSystemiff_isCompactSystem_of_or_univ`: A set system is a compact +system iff inserting `univ` gives a compact system. +* `IsClosedCompact.isCompactSystem`: The set of closed and compact sets is a compact system. +* `IsClosedCompact.isCompactSystem_of_T2Space`: In a `T2Space α`, the set of compact sets + is a compact system in a `T2Space`. +-/ + +@[expose] public section + +open Set Finset Nat + +variable {α : Type*} {p : Set α → Prop} {C : ℕ → Set α} + +section definition + +/-- A set of sets is a compact system if, whenever a countable subfamily has empty intersection, +then finitely many of them already have empty intersection. -/ +def IsCompactSystem (p : Set α → Prop) : Prop := + ∀ C : ℕ → Set α, (∀ i, p (C i)) → ⋂ i, C i = ∅ → ∃ (n : ℕ), dissipate C n = ∅ + +end definition + +namespace IsCompactSystem + +open Classical in +/-- In a compact system, given a countable family with `⋂ i, C i = ∅`, we choose the smallest `n` +with `⋂ (i ≤ n), C i = ∅`. -/ +noncomputable +def finite_of_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i)) + (hC_empty : ⋂ i, C i = ∅) : ℕ := + Nat.find (hp C hC hC_empty) + +open Classical in +lemma dissipate_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i)) + (hC_empty : ⋂ i, C i = ∅) : + dissipate C (hp.finite_of_empty hC hC_empty) = ∅ := by + apply Nat.find_spec (hp C hC hC_empty) + +theorem iff_nonempty_iInter (p : Set α → Prop) : + IsCompactSystem p ↔ (∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ), + (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) := by + refine ⟨fun h C hC hn ↦ ?_, fun h C hC ↦ ?_⟩ <;> have h2 := not_imp_not.mpr <| h C hC + · push_neg at h2 + exact h2 hn + · push_neg at h2 + exact h2 + +/-- In this equivalent formulation for a compact system, +note that we use `⋂ k < n, C k` rather than `⋂ k ≤ n, C k`. -/ +lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : IsCompactSystem p ↔ + ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by + simp_rw [iff_nonempty_iInter] + refine ⟨fun h C hi h'↦ ?_, fun h C hi h' ↦ ?_⟩ + · apply h C hi + exact fun n ↦ dissipate_eq ▸ (h' (n + 1)) + · apply h C hi + intro n + simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢ + intro g + apply h' n + simp_rw [← subset_empty_iff, dissipate] at g ⊢ + apply le_trans _ g + intro x + rw [mem_iInter₂, mem_iInter₂] + exact fun h i hi ↦ h i hi.le + +/-- Any subset of a compact system is a compact system. -/ +theorem mono {C D : (Set α) → Prop} (hD : IsCompactSystem D) (hCD : ∀ s, C s → D s) : + IsCompactSystem C := fun s hC hs ↦ hD s (fun i ↦ hCD (s i) (hC i)) hs + +/-- A set system is a compact system iff adding `∅` gives a compact system. -/ +lemma iff_isCompactSystem_of_or_empty : IsCompactSystem p ↔ + IsCompactSystem (fun s ↦ (p s ∨ (s = ∅))) := by + refine ⟨fun h s h' hd ↦ ?_, fun h ↦ mono h (fun s ↦ fun a ↦ Or.symm (Or.inr a))⟩ + by_cases g : ∃ n, s n = ∅ + · use g.choose + rw [← subset_empty_iff] at hd ⊢ + exact le_trans (dissipate_subset (by rfl)) g.choose_spec.le + · push_neg at g + have hj (i : _) : p (s i) := by + rcases h' i with a | b + · exact a + · exfalso + revert g i + simp_rw [← Set.not_nonempty_iff_eq_empty] + simp_rw [imp_false, not_not] + exact fun h i ↦ h i + exact h s hj hd + +lemma of_IsEmpty (h : IsEmpty α) (p : Set α → Prop) : IsCompactSystem p := + fun s _ _ ↦ ⟨0, Set.eq_empty_of_isEmpty (dissipate s 0)⟩ + +/-- A set system is a compact system iff adding `univ` gives a compact system. -/ +lemma iff_isCompactSystem_of_or_univ : IsCompactSystem p ↔ + IsCompactSystem (fun s ↦ (p s ∨ s = univ)) := by + refine ⟨fun h ↦ ?_, fun h ↦ mono h (fun s ↦ fun a ↦ Or.symm (Or.inr a))⟩ + wlog ht : Nonempty α + · rw [not_nonempty_iff] at ht + apply of_IsEmpty ht + · rw [iff_nonempty_iInter] at h ⊢ + intro s h' hd + classical + by_cases h₀ : ∀ n, ¬p (s n) + · simp only [h₀, false_or] at h' + simp_rw [h', iInter_univ, Set.univ_nonempty] + · push_neg at h₀ + let n := Nat.find h₀ + let s' := fun i ↦ if p (s i) then s i else s n + have h₁ : ∀ i, p (s' i) := by + intro i + by_cases h₁ : p (s i) + · simp only [h₁, ↓reduceIte, s'] + · simp only [h₁, ↓reduceIte, Nat.find_spec h₀, s', n] + have h₃ : ∀ i, (p (s i) → s' i = s i) := fun i h ↦ if_pos h + have h₄ : ∀ i, (¬p (s i) → s' i = s n) := fun i h ↦ if_neg h + have h₂ : ⋂ i, s i = ⋂ i, s' i := by + simp only [s'] at * + ext x + simp only [mem_iInter] + refine ⟨fun h i ↦ ?_, fun h i ↦ ?_⟩ + · by_cases h' : p (s i) <;> simp only [h', ↓reduceIte, h, n] + · specialize h' i + specialize h i + rcases h' with a | b + · simp only [a, ↓reduceIte] at h + exact h + · simp only [b, Set.mem_univ] + apply h₂ ▸ h s' h₁ + by_contra! a + obtain ⟨j, hj⟩ := a + have h₂ (v : ℕ) (hv : n ≤ v) : dissipate s v = dissipate s' v:= by + ext x + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ <;> simp only [dissipate_def, mem_iInter] at h ⊢ <;> + intro i hi + · by_cases h₅ : p (s i) + · exact (h₃ i h₅) ▸ h i hi + · exact (h₄ i h₅) ▸ h n hv + · by_cases h₅ : p (s i) + · exact (h₃ i h₅) ▸ h i hi + · have h₆ : s i = univ := by + specialize h' i + simp only [h₅, false_or] at h' + exact h' + simp only [h₆, Set.mem_univ] + have h₇ : dissipate s' (max j n) = ∅ := by + rw [← subset_empty_iff] at hj ⊢ + exact le_trans (antitone_dissipate (Nat.le_max_left j n)) hj + specialize h₂ (max j n) (Nat.le_max_right j n) + specialize hd (max j n) + rw [h₂, Set.nonempty_iff_ne_empty, h₇] at hd + exact hd rfl + +theorem iff_directed (hpi : IsPiSystem p) : + IsCompactSystem p ↔ + ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) → + ⋂ i, C i = ∅ → ∃ (n : ℕ), C n = ∅ := by + rw [iff_isCompactSystem_of_or_empty] + refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩ + · rw [exists_dissipate_eq_empty_iff_of_directed C hdi] + apply h C + exact fun i ↦ Or.inl (hi i) + · have hpi' : IsPiSystem (fun s ↦ p s ∨ s = ∅) := by + intro a ha b hb hab + rcases ha with ha₁ | ha₂ + · rcases hb with hb₁ | hb₂ + · left + exact hpi a ha₁ b hb₁ hab + · right + exact hb₂ ▸ (Set.inter_empty a) + · simp only [ha₂, Set.empty_inter] + right + rfl + rw [← biInter_le_eq_iInter] at h2 + obtain h' := h (dissipate C) directed_dissipate + have h₀ : (∀ (n : ℕ), p (dissipate C n) ∨ dissipate C n = ∅) → ⋂ n, dissipate C n = ∅ → + ∃ n, dissipate C n = ∅ := by + intro h₀ h₁ + by_cases f : ∀ n, p (dissipate C n) + · apply h' f h₁ + · push_neg at f + obtain ⟨n, hn⟩ := f + use n + specialize h₀ n + simp_all only [false_or] + obtain h'' := IsPiSystem.dissipate_mem hpi' h1 + have h₁ : ∀ (n : ℕ), p (dissipate C n) ∨ dissipate C n = ∅ := by + intro n + by_cases g : (dissipate C n).Nonempty + · exact h'' n g + · right + exact Set.not_nonempty_iff_eq_empty.mp g + apply h₀ h₁ h2 + + +theorem iff_directed' (hpi : IsPiSystem p) : + IsCompactSystem p ↔ + ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) → + (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty := by + rw [IsCompactSystem.iff_directed hpi] + refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩ <;> rw [← not_imp_not] <;> push_neg + · exact h1 C h3 h4 + · exact h1 C h3 s + +section IsCompactIsClosed + +variable (α : Type*) [TopologicalSpace α] + +/-- The set of compact and closed sets is a compact system. -/ +theorem of_isCompact_isClosed : + IsCompactSystem (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by + let p := fun (s : Set α) ↦ IsCompact s ∧ IsClosed s + have h2 : IsPiSystem p := by + intro s hs t ht _ + refine ⟨IsCompact.inter_left ht.1 hs.2, IsClosed.inter hs.2 ht.2⟩ + rw [IsCompactSystem.iff_directed' h2] + intro s hs h1 h2 + let s' := fun (i : { j : ℕ | s j ≠ univ}) ↦ s i + have hs' : Directed (fun x1 x2 ↦ x1 ⊇ x2) s' := by + intro a b + obtain ⟨z, hz1, hz2⟩ := hs a.val b.val + have hz : s z ≠ univ := fun h ↦ a.prop <| eq_univ_of_subset hz1 h + use ⟨z, hz⟩ + have htcl : ∀ (i : { j : ℕ | s j ≠ univ}), IsClosed (s i) := + fun i ↦ (h1 i).2 + have htco : ∀ (i : { j : ℕ | s j ≠ univ}), IsCompact (s i) := + fun i ↦ (h1 i).1 + haveI f : Nonempty α := by + apply Exists.nonempty _ + · exact fun x ↦ x ∈ s 0 + · exact h2 0 + by_cases h : Nonempty ↑{j | s j ≠ Set.univ} + · have g : (⋂ i, s' i).Nonempty → (⋂ i, s i).Nonempty := by + rw [Set.nonempty_iInter, Set.nonempty_iInter] + rintro ⟨x, hx⟩ + use x + intro i + by_cases g : s i ≠ univ + · exact hx ⟨i, g⟩ + · simp only [ne_eq, not_not] at g + rw [g] + simp only [Set.mem_univ] + apply g <| IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed s' hs' + (fun j ↦ h2 j) htco htcl + · simp only [ne_eq, coe_setOf, nonempty_subtype, not_exists, not_not] at h + simp [h] + +/-- The set of sets which are either compact and closed, or `univ`, is a compact system. -/ +theorem of_isCompact_isClosed_or_univ : + IsCompactSystem (fun s : Set α ↦ (IsCompact s ∧ IsClosed s) ∨ (s = univ)) := by + rw [← iff_isCompactSystem_of_or_univ] + apply of_isCompact_isClosed + +/-- In a `T2Space` the set of compact sets is a compact system. -/ +theorem of_isCompact [T2Space α] : + IsCompactSystem (fun s : Set α ↦ IsCompact s) := by + have h : (fun s : Set α ↦ IsCompact s) = (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by + ext s + refine ⟨fun h' ↦ ⟨h', h'.isClosed⟩, fun h ↦ h.1⟩ + rw [h] + apply (of_isCompact_isClosed) + +end IsCompactIsClosed + +end IsCompactSystem From aea7a8538bb0452aa77c74bc47bb449223503888 Mon Sep 17 00:00:00 2001 From: pfaffelh Date: Tue, 3 Mar 2026 00:13:08 +0100 Subject: [PATCH 03/26] update one lemma --- .../Topology/Compactness/CompactSystem.lean | 22 ++++++++----------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 9c35597af62d23..d4dd9483891cba 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -72,19 +72,15 @@ note that we use `⋂ k < n, C k` rather than `⋂ k ≤ n, C k`. -/ lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : IsCompactSystem p ↔ ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by simp_rw [iff_nonempty_iInter] - refine ⟨fun h C hi h'↦ ?_, fun h C hi h' ↦ ?_⟩ - · apply h C hi - exact fun n ↦ dissipate_eq ▸ (h' (n + 1)) - · apply h C hi - intro n - simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢ - intro g - apply h' n - simp_rw [← subset_empty_iff, dissipate] at g ⊢ - apply le_trans _ g - intro x - rw [mem_iInter₂, mem_iInter₂] - exact fun h i hi ↦ h i hi.le + refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq ▸ (h' (n + 1))), fun h C hi h' ↦ h C hi ?_⟩ + simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢ + intro n g + apply h' n + simp_rw [← subset_empty_iff, dissipate] at g ⊢ + apply le_trans _ g + intro x + rw [mem_iInter₂, mem_iInter₂] + exact fun h i hi ↦ h i hi.le /-- Any subset of a compact system is a compact system. -/ theorem mono {C D : (Set α) → Prop} (hD : IsCompactSystem D) (hCD : ∀ s, C s → D s) : From 00181ac889421299ce3026323f2f0f19b20050f0 Mon Sep 17 00:00:00 2001 From: pfaffelh Date: Tue, 3 Mar 2026 00:13:59 +0100 Subject: [PATCH 04/26] update one lemma2 --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 3d0097ea74ddf6..74419b89532705 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -7262,6 +7262,7 @@ public import Mathlib.Topology.Compactification.OnePoint.Sphere public import Mathlib.Topology.Compactification.StoneCech public import Mathlib.Topology.Compactness.Bases public import Mathlib.Topology.Compactness.Compact +public import Mathlib.Topology.Compactness.CompactSystem public import Mathlib.Topology.Compactness.CompactlyCoherentSpace public import Mathlib.Topology.Compactness.CompactlyGeneratedSpace public import Mathlib.Topology.Compactness.DeltaGeneratedSpace From 47ab101dcf3283fd3e33659ac576cd0e65e41714 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Mar 2026 10:19:20 +0100 Subject: [PATCH 05/26] golf; revert an import --- Mathlib/Data/Set/Dissipate.lean | 14 - Mathlib/MeasureTheory/PiSystem.lean | 14 + .../Topology/Compactness/CompactSystem.lean | 263 +++++++----------- 3 files changed, 116 insertions(+), 175 deletions(-) diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index 8757e7fe156b31..c42b516a38ebf4 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -7,7 +7,6 @@ Authors: Peter Pfaffelhuber module public import Mathlib.Data.Set.Accumulate -public import Mathlib.MeasureTheory.PiSystem /-! # Dissipate @@ -114,17 +113,4 @@ lemma exists_dissipate_eq_empty_iff_of_directed (C : ℕ → Set α) obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n exact Set.Nonempty.mono hm (h m) -/-- For a ∩-stable set of sets `p` on `α` and a sequence of sets `s` with this attribute, -`dissipate s n` belongs to `p`. -/ -lemma IsPiSystem.dissipate_mem {s : ℕ → Set α} {p : Set (Set α)} - (hp : IsPiSystem p) (h : ∀ n, s n ∈ p) (n : ℕ) (h' : (dissipate s n).Nonempty) : - (dissipate s n) ∈ p := by - induction n with - | zero => - simp only [dissipate_def, Nat.le_zero_eq, iInter_iInter_eq_left] - exact h 0 - | succ n hn => - rw [dissipate_succ] at * - apply hp (dissipate s n) (hn (Nonempty.left h')) (s (n+1)) (h (n+1)) h' - end Set diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean index 768a1832c37b38..1ec23e26462add 100644 --- a/Mathlib/MeasureTheory/PiSystem.lean +++ b/Mathlib/MeasureTheory/PiSystem.lean @@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Martin Zinkevich, Rémy Degenne -/ module +public import Mathlib.Data.Set.Dissipate public import Mathlib.Logic.Encodable.Lattice public import Mathlib.MeasureTheory.MeasurableSpace.Defs public import Mathlib.Order.Disjointed @@ -695,3 +696,16 @@ theorem induction_on_inter {m : MeasurableSpace α} {C : ∀ s : Set α, Measura | @iUnion f hfd hf ihf => exact iUnion f hfd (eq ▸ hf) ihf end MeasurableSpace + +/-- For a ∩-stable set of sets `p` on `α` and a sequence of sets `s` with this attribute, +`dissipate s n` belongs to `p`. -/ +lemma IsPiSystem.dissipate_mem {s : ℕ → Set α} {p : Set (Set α)} + (hp : IsPiSystem p) (h : ∀ n, s n ∈ p) (n : ℕ) (h' : (dissipate s n).Nonempty) : + (dissipate s n) ∈ p := by + induction n with + | zero => + simp only [dissipate_def, Nat.le_zero_eq, iInter_iInter_eq_left] + exact h 0 + | succ n hn => + rw [dissipate_succ] at * + apply hp (dissipate s n) (hn (Nonempty.left h')) (s (n+1)) (h (n+1)) h' diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index d4dd9483891cba..bdc30ac9d50dcc 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -6,6 +6,7 @@ Authors: Rémy Degenne, Peter Pfaffelhuber module public import Mathlib.Data.Set.Dissipate +public import Mathlib.MeasureTheory.PiSystem public import Mathlib.Topology.Separation.Hausdorff /-! @@ -58,19 +59,38 @@ lemma dissipate_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i)) dissipate C (hp.finite_of_empty hC hC_empty) = ∅ := by apply Nat.find_spec (hp C hC hC_empty) +lemma of_nonempty_iInter + (h : ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) : + IsCompactSystem p := by + intro C hC + contrapose! + exact h C hC + +lemma nonempty_iInter (hp : IsCompactSystem p) {C : ℕ → Set α} (hC : ∀ i, p (C i)) + (h_nonempty : ∀ n, (dissipate C n).Nonempty) : + (⋂ i, C i).Nonempty := by + revert h_nonempty + contrapose! + exact hp C hC + theorem iff_nonempty_iInter (p : Set α → Prop) : IsCompactSystem p ↔ (∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ), - (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) := by - refine ⟨fun h C hC hn ↦ ?_, fun h C hC ↦ ?_⟩ <;> have h2 := not_imp_not.mpr <| h C hC - · push_neg at h2 - exact h2 hn - · push_neg at h2 - exact h2 + (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) := + ⟨nonempty_iInter, of_nonempty_iInter⟩ + +@[simp] +lemma of_IsEmpty [IsEmpty α] (p : Set α → Prop) : IsCompactSystem p := + fun s _ _ ↦ ⟨0, Set.eq_empty_of_isEmpty (dissipate s 0)⟩ + +/-- Any subset of a compact system is a compact system. -/ +theorem mono {C D : (Set α) → Prop} (hD : IsCompactSystem D) (hCD : ∀ s, C s → D s) : + IsCompactSystem C := fun s hC hs ↦ hD s (fun i ↦ hCD (s i) (hC i)) hs /-- In this equivalent formulation for a compact system, note that we use `⋂ k < n, C k` rather than `⋂ k ≤ n, C k`. -/ -lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : IsCompactSystem p ↔ - ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by +lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : + IsCompactSystem p ↔ + ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by simp_rw [iff_nonempty_iInter] refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq ▸ (h' (n + 1))), fun h C hi h' ↦ h C hi ?_⟩ simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢ @@ -82,138 +102,82 @@ lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : IsCompactSystem p ↔ rw [mem_iInter₂, mem_iInter₂] exact fun h i hi ↦ h i hi.le -/-- Any subset of a compact system is a compact system. -/ -theorem mono {C D : (Set α) → Prop} (hD : IsCompactSystem D) (hCD : ∀ s, C s → D s) : - IsCompactSystem C := fun s hC hs ↦ hD s (fun i ↦ hCD (s i) (hC i)) hs - /-- A set system is a compact system iff adding `∅` gives a compact system. -/ -lemma iff_isCompactSystem_of_or_empty : IsCompactSystem p ↔ - IsCompactSystem (fun s ↦ (p s ∨ (s = ∅))) := by - refine ⟨fun h s h' hd ↦ ?_, fun h ↦ mono h (fun s ↦ fun a ↦ Or.symm (Or.inr a))⟩ +lemma iff_isCompactSystem_of_or_empty : + IsCompactSystem p ↔ IsCompactSystem (fun s ↦ (p s ∨ (s = ∅))) := by + refine ⟨fun h s h' hd ↦ ?_, fun h ↦ mono h (fun s ↦ fun a ↦ (Or.inr a).symm)⟩ by_cases g : ∃ n, s n = ∅ · use g.choose rw [← subset_empty_iff] at hd ⊢ - exact le_trans (dissipate_subset (by rfl)) g.choose_spec.le + exact (dissipate_subset le_rfl).trans g.choose_spec.le · push_neg at g - have hj (i : _) : p (s i) := by - rcases h' i with a | b - · exact a - · exfalso - revert g i - simp_rw [← Set.not_nonempty_iff_eq_empty] - simp_rw [imp_false, not_not] - exact fun h i ↦ h i - exact h s hj hd - -lemma of_IsEmpty (h : IsEmpty α) (p : Set α → Prop) : IsCompactSystem p := - fun s _ _ ↦ ⟨0, Set.eq_empty_of_isEmpty (dissipate s 0)⟩ + refine h s (fun i ↦ ?_) hd + specialize g i + specialize h' i + rw [Set.nonempty_iff_ne_empty] at g + simpa [g] using h' /-- A set system is a compact system iff adding `univ` gives a compact system. -/ -lemma iff_isCompactSystem_of_or_univ : IsCompactSystem p ↔ - IsCompactSystem (fun s ↦ (p s ∨ s = univ)) := by +lemma iff_isCompactSystem_of_or_univ : + IsCompactSystem p ↔ IsCompactSystem (fun s ↦ (p s ∨ s = univ)) := by refine ⟨fun h ↦ ?_, fun h ↦ mono h (fun s ↦ fun a ↦ Or.symm (Or.inr a))⟩ - wlog ht : Nonempty α - · rw [not_nonempty_iff] at ht - apply of_IsEmpty ht - · rw [iff_nonempty_iInter] at h ⊢ - intro s h' hd - classical - by_cases h₀ : ∀ n, ¬p (s n) - · simp only [h₀, false_or] at h' - simp_rw [h', iInter_univ, Set.univ_nonempty] - · push_neg at h₀ - let n := Nat.find h₀ - let s' := fun i ↦ if p (s i) then s i else s n - have h₁ : ∀ i, p (s' i) := by - intro i - by_cases h₁ : p (s i) - · simp only [h₁, ↓reduceIte, s'] - · simp only [h₁, ↓reduceIte, Nat.find_spec h₀, s', n] - have h₃ : ∀ i, (p (s i) → s' i = s i) := fun i h ↦ if_pos h - have h₄ : ∀ i, (¬p (s i) → s' i = s n) := fun i h ↦ if_neg h - have h₂ : ⋂ i, s i = ⋂ i, s' i := by - simp only [s'] at * - ext x - simp only [mem_iInter] - refine ⟨fun h i ↦ ?_, fun h i ↦ ?_⟩ - · by_cases h' : p (s i) <;> simp only [h', ↓reduceIte, h, n] - · specialize h' i - specialize h i - rcases h' with a | b - · simp only [a, ↓reduceIte] at h - exact h - · simp only [b, Set.mem_univ] - apply h₂ ▸ h s' h₁ - by_contra! a - obtain ⟨j, hj⟩ := a - have h₂ (v : ℕ) (hv : n ≤ v) : dissipate s v = dissipate s' v:= by - ext x - refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ <;> simp only [dissipate_def, mem_iInter] at h ⊢ <;> - intro i hi - · by_cases h₅ : p (s i) - · exact (h₃ i h₅) ▸ h i hi - · exact (h₄ i h₅) ▸ h n hv - · by_cases h₅ : p (s i) - · exact (h₃ i h₅) ▸ h i hi - · have h₆ : s i = univ := by - specialize h' i - simp only [h₅, false_or] at h' - exact h' - simp only [h₆, Set.mem_univ] - have h₇ : dissipate s' (max j n) = ∅ := by - rw [← subset_empty_iff] at hj ⊢ - exact le_trans (antitone_dissipate (Nat.le_max_left j n)) hj - specialize h₂ (max j n) (Nat.le_max_right j n) - specialize hd (max j n) - rw [h₂, Set.nonempty_iff_ne_empty, h₇] at hd - exact hd rfl - -theorem iff_directed (hpi : IsPiSystem p) : + rcases isEmpty_or_nonempty α with hα | _ + · simp + rw [iff_nonempty_iInter] at h ⊢ + intro s h' hd + by_cases h₀ : ∀ n, ¬ p (s n) + · simp only [h₀, false_or] at h' + simp [h'] + push_neg at h₀ + classical + let n := Nat.find h₀ + let s' := fun i ↦ if p (s i) then s i else s n + have h₁ : ∀ i, p (s' i) := by simp [s']; grind + have h₂ : ⋂ i, s i = ⋂ i, s' i := by ext; simp; grind + apply h₂ ▸ h s' h₁ + by_contra! h_exists_empty + obtain ⟨j, hj⟩ := h_exists_empty + have h₃ (v : ℕ) (hv : n ≤ v) : dissipate s v = dissipate s' v:= by ext; simp; grind + have h₇ : dissipate s' (max j n) = ∅ := by + rw [← subset_empty_iff] at hj ⊢ + exact (antitone_dissipate (Nat.le_max_left j n)).trans hj + specialize h₃ (max j n) (Nat.le_max_right j n) + specialize hd (max j n) + simp [h₃, h₇] at hd + +theorem iff_directed (hpi : IsPiSystem {x |p x}) : IsCompactSystem p ↔ - ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) → - ⋂ i, C i = ∅ → ∃ (n : ℕ), C n = ∅ := by + ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, p (C i)) → ⋂ i, C i = ∅ → + ∃ n, C n = ∅ := by rw [iff_isCompactSystem_of_or_empty] refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩ · rw [exists_dissipate_eq_empty_iff_of_directed C hdi] - apply h C - exact fun i ↦ Or.inl (hi i) - · have hpi' : IsPiSystem (fun s ↦ p s ∨ s = ∅) := by - intro a ha b hb hab - rcases ha with ha₁ | ha₂ - · rcases hb with hb₁ | hb₂ - · left - exact hpi a ha₁ b hb₁ hab - · right - exact hb₂ ▸ (Set.inter_empty a) - · simp only [ha₂, Set.empty_inter] - right - rfl + exact h C (by simp [hi]) + · have hpi' : IsPiSystem {s | p s ∨ s = ∅} := by + convert IsPiSystem.insert_empty hpi using 1 + ext + simp + grind rw [← biInter_le_eq_iInter] at h2 obtain h' := h (dissipate C) directed_dissipate - have h₀ : (∀ (n : ℕ), p (dissipate C n) ∨ dissipate C n = ∅) → ⋂ n, dissipate C n = ∅ → - ∃ n, dissipate C n = ∅ := by - intro h₀ h₁ - by_cases f : ∀ n, p (dissipate C n) + have h₀ (h₀ : ∀ n, p (dissipate C n) ∨ dissipate C n = ∅) (h₁ : ⋂ n, dissipate C n = ∅) : + ∃ n, dissipate C n = ∅ := by + by_cases! f : ∀ n, p (dissipate C n) · apply h' f h₁ - · push_neg at f - obtain ⟨n, hn⟩ := f - use n - specialize h₀ n - simp_all only [false_or] + · obtain ⟨n, hn⟩ := f + exact ⟨n, by simpa [hn] using h₀ n⟩ obtain h'' := IsPiSystem.dissipate_mem hpi' h1 - have h₁ : ∀ (n : ℕ), p (dissipate C n) ∨ dissipate C n = ∅ := by + have h₁ : ∀ n, p (dissipate C n) ∨ dissipate C n = ∅ := by intro n by_cases g : (dissipate C n).Nonempty · exact h'' n g - · right - exact Set.not_nonempty_iff_eq_empty.mp g + · exact .inr (Set.not_nonempty_iff_eq_empty.mp g) apply h₀ h₁ h2 - theorem iff_directed' (hpi : IsPiSystem p) : IsCompactSystem p ↔ - ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) → - (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty := by + ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, p (C i)) → (∀ n, (C n).Nonempty) → + (⋂ i, C i).Nonempty := by rw [IsCompactSystem.iff_directed hpi] refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩ <;> rw [← not_imp_not] <;> push_neg · exact h1 C h3 h4 @@ -226,41 +190,27 @@ variable (α : Type*) [TopologicalSpace α] /-- The set of compact and closed sets is a compact system. -/ theorem of_isCompact_isClosed : IsCompactSystem (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by - let p := fun (s : Set α) ↦ IsCompact s ∧ IsClosed s - have h2 : IsPiSystem p := by - intro s hs t ht _ - refine ⟨IsCompact.inter_left ht.1 hs.2, IsClosed.inter hs.2 ht.2⟩ - rw [IsCompactSystem.iff_directed' h2] - intro s hs h1 h2 - let s' := fun (i : { j : ℕ | s j ≠ univ}) ↦ s i - have hs' : Directed (fun x1 x2 ↦ x1 ⊇ x2) s' := by - intro a b - obtain ⟨z, hz1, hz2⟩ := hs a.val b.val - have hz : s z ≠ univ := fun h ↦ a.prop <| eq_univ_of_subset hz1 h - use ⟨z, hz⟩ - have htcl : ∀ (i : { j : ℕ | s j ≠ univ}), IsClosed (s i) := - fun i ↦ (h1 i).2 - have htco : ∀ (i : { j : ℕ | s j ≠ univ}), IsCompact (s i) := - fun i ↦ (h1 i).1 - haveI f : Nonempty α := by - apply Exists.nonempty _ - · exact fun x ↦ x ∈ s 0 - · exact h2 0 - by_cases h : Nonempty ↑{j | s j ≠ Set.univ} - · have g : (⋂ i, s' i).Nonempty → (⋂ i, s i).Nonempty := by - rw [Set.nonempty_iInter, Set.nonempty_iInter] - rintro ⟨x, hx⟩ - use x - intro i - by_cases g : s i ≠ univ - · exact hx ⟨i, g⟩ - · simp only [ne_eq, not_not] at g - rw [g] - simp only [Set.mem_univ] - apply g <| IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed s' hs' - (fun j ↦ h2 j) htco htcl - · simp only [ne_eq, coe_setOf, nonempty_subtype, not_exists, not_not] at h - simp [h] + intro C hC_cc hC_inter + by_contra! h_nonempty + refine absurd hC_inter ?_ + rw [← ne_eq, ← Set.nonempty_iff_ne_empty, ← Set.iInter_dissipate] + refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed (Set.dissipate C) + (fun n ↦ ?_) (fun n ↦ ?_) ?_ (fun n ↦ ?_) + · exact Set.antitone_dissipate (by lia) + · exact h_nonempty _ + · simp only [Set.dissipate_zero_nat] + exact (hC_cc 0).1 + · induction n with + | zero => simp only [Set.dissipate_zero_nat]; exact (hC_cc 0).2 + | succ n hn => + rw [Set.dissipate_succ] + exact hn.inter (hC_cc (n + 1)).2 + +/-- In a `T2Space` the set of compact sets is a compact system. -/ +theorem of_isCompact [T2Space α] : + IsCompactSystem (fun s : Set α ↦ IsCompact s) := by + convert of_isCompact_isClosed α with s + exact ⟨fun hs ↦ ⟨hs, hs.isClosed⟩, fun hs ↦ hs.1⟩ /-- The set of sets which are either compact and closed, or `univ`, is a compact system. -/ theorem of_isCompact_isClosed_or_univ : @@ -268,15 +218,6 @@ theorem of_isCompact_isClosed_or_univ : rw [← iff_isCompactSystem_of_or_univ] apply of_isCompact_isClosed -/-- In a `T2Space` the set of compact sets is a compact system. -/ -theorem of_isCompact [T2Space α] : - IsCompactSystem (fun s : Set α ↦ IsCompact s) := by - have h : (fun s : Set α ↦ IsCompact s) = (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by - ext s - refine ⟨fun h' ↦ ⟨h', h'.isClosed⟩, fun h ↦ h.1⟩ - rw [h] - apply (of_isCompact_isClosed) - end IsCompactIsClosed end IsCompactSystem From 4ee793da46bf002a785798ec1689e327c898b76f Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Mar 2026 10:28:58 +0100 Subject: [PATCH 06/26] golf --- Mathlib/Data/Set/Dissipate.lean | 25 +++++++------------ .../Topology/Compactness/CompactSystem.lean | 3 +-- 2 files changed, 10 insertions(+), 18 deletions(-) diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index c42b516a38ebf4..940a33d8b55831 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -28,7 +28,7 @@ def dissipate [LE α] (s : α → Set β) (x : α) : Set β := theorem dissipate_def [LE α] {x : α} : dissipate s x = ⋂ y ≤ x, s y := rfl -theorem dissipate_eq {s : ℕ → Set β} {n : ℕ} : dissipate s n = ⋂ k < n + 1, s k := by +theorem dissipate_eq_iInter_lt {s : ℕ → Set β} {n : ℕ} : dissipate s n = ⋂ k < n + 1, s k := by simp_rw [Nat.lt_add_one_iff, dissipate] @[simp] @@ -91,26 +91,19 @@ lemma exists_subset_dissipate_of_directed {s : ℕ → Set α} | zero => use 0; simp [dissipate_def] | succ n hn => obtain ⟨m, hm⟩ := hn - simp_rw [dissipate_succ] obtain ⟨k, hk⟩ := hd m (n+1) - simp only at hk - use k - simp only [subset_inter_iff] - exact ⟨le_trans hk.1 hm, hk.2⟩ + exact ⟨k, by simp; grind⟩ -lemma directed_dissipate {s : ℕ → Set α} : - Directed (fun (x y : Set α) => y ⊆ x) (dissipate s) := +lemma directed_dissipate {s : ℕ → Set α} : Directed (fun x y ↦ y ⊆ x) (dissipate s) := antitone_dissipate.directed_ge lemma exists_dissipate_eq_empty_iff_of_directed (C : ℕ → Set α) - (hd : Directed (fun (x y : Set α) => y ⊆ x) C) : + (hd : Directed (fun x y ↦ y ⊆ x) C) : (∃ n, C n = ∅) ↔ (∃ n, dissipate C n = ∅) := by - refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, ?_⟩ , ?_⟩ - · exact subset_eq_empty (dissipate_subset (Nat.le_refl n)) hn - · rw [← not_imp_not] - push_neg - intro h n - obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n - exact Set.Nonempty.mono hm (h m) + refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, subset_eq_empty (dissipate_subset le_rfl) hn⟩ , ?_⟩ + contrapose! + intro h n + obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n + exact (h m).mono hm end Set diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index bdc30ac9d50dcc..26a466cf0077ee 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -5,7 +5,6 @@ Authors: Rémy Degenne, Peter Pfaffelhuber -/ module -public import Mathlib.Data.Set.Dissipate public import Mathlib.MeasureTheory.PiSystem public import Mathlib.Topology.Separation.Hausdorff @@ -21,7 +20,7 @@ This file defines compact systems of sets. ## Main results -* `IsCompactSystemiff_isCompactSystem_of_or_univ`: A set system is a compact +* `IsCompactSystem.iff_isCompactSystem_of_or_univ`: A set system is a compact system iff inserting `univ` gives a compact system. * `IsClosedCompact.isCompactSystem`: The set of closed and compact sets is a compact system. * `IsClosedCompact.isCompactSystem_of_T2Space`: In a `T2Space α`, the set of compact sets From e778b5e633afb102b57ffc549cbab13b27c44de9 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Mar 2026 10:32:25 +0100 Subject: [PATCH 07/26] move and golf --- Mathlib/MeasureTheory/PiSystem.lean | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean index 1ec23e26462add..68ebda266c65d1 100644 --- a/Mathlib/MeasureTheory/PiSystem.lean +++ b/Mathlib/MeasureTheory/PiSystem.lean @@ -108,6 +108,17 @@ theorem IsPiSystem.comap {α β} {S : Set (Set β)} (h_pi : IsPiSystem S) (f : rw [← Set.preimage_inter] at hst ⊢ exact ⟨s ∩ t, h_pi s hs_mem t ht_mem (nonempty_of_nonempty_preimage hst), rfl⟩ +/-- For a ∩-stable set of sets `C` on `α` and a sequence of sets `s` with this attribute, +`dissipate s n` belongs to `C`. -/ +lemma IsPiSystem.dissipate_mem {s : ℕ → Set α} {C : Set (Set α)} + (hC : IsPiSystem C) (h : ∀ n, s n ∈ C) (n : ℕ) (h' : (dissipate s n).Nonempty) : + dissipate s n ∈ C := by + induction n with + | zero => simpa using h 0 + | succ n hn => + rw [dissipate_succ] at h' ⊢ + exact hC (dissipate s n) (hn h'.left) (s (n + 1)) (h (n + 1)) h' + theorem isPiSystem_iUnion_of_directed_le {α ι} (p : ι → Set (Set α)) (hp_pi : ∀ n, IsPiSystem (p n)) (hp_directed : Directed (· ≤ ·) p) : IsPiSystem (⋃ n, p n) := by @@ -696,16 +707,3 @@ theorem induction_on_inter {m : MeasurableSpace α} {C : ∀ s : Set α, Measura | @iUnion f hfd hf ihf => exact iUnion f hfd (eq ▸ hf) ihf end MeasurableSpace - -/-- For a ∩-stable set of sets `p` on `α` and a sequence of sets `s` with this attribute, -`dissipate s n` belongs to `p`. -/ -lemma IsPiSystem.dissipate_mem {s : ℕ → Set α} {p : Set (Set α)} - (hp : IsPiSystem p) (h : ∀ n, s n ∈ p) (n : ℕ) (h' : (dissipate s n).Nonempty) : - (dissipate s n) ∈ p := by - induction n with - | zero => - simp only [dissipate_def, Nat.le_zero_eq, iInter_iInter_eq_left] - exact h 0 - | succ n hn => - rw [dissipate_succ] at * - apply hp (dissipate s n) (hn (Nonempty.left h')) (s (n+1)) (h (n+1)) h' From c4c2236bdee8828d129a0185f8fb9c0d1acca744 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Mar 2026 10:37:07 +0100 Subject: [PATCH 08/26] golf --- Mathlib/Topology/Compactness/CompactSystem.lean | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 26a466cf0077ee..42f3d195b8087d 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -91,15 +91,12 @@ lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : IsCompactSystem p ↔ ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by simp_rw [iff_nonempty_iInter] - refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq ▸ (h' (n + 1))), fun h C hi h' ↦ h C hi ?_⟩ + refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq_iInter_lt ▸ (h' (n + 1))), + fun h C hi h' ↦ h C hi ?_⟩ simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢ - intro n g - apply h' n + refine fun n g ↦ h' n ?_ simp_rw [← subset_empty_iff, dissipate] at g ⊢ - apply le_trans _ g - intro x - rw [mem_iInter₂, mem_iInter₂] - exact fun h i hi ↦ h i hi.le + exact le_trans (fun x ↦ by simp; grind) g /-- A set system is a compact system iff adding `∅` gives a compact system. -/ lemma iff_isCompactSystem_of_or_empty : From a2feb8f863deabc27eca92bc0cf569f135b8258b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Mar 2026 10:46:07 +0100 Subject: [PATCH 09/26] follow in-person review: switch to sets of sets --- .../Topology/Compactness/CompactSystem.lean | 82 +++++++++---------- 1 file changed, 39 insertions(+), 43 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 42f3d195b8087d..449b48fde4da9d 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -9,7 +9,7 @@ public import Mathlib.MeasureTheory.PiSystem public import Mathlib.Topology.Separation.Hausdorff /-! -# Compact systems. +# Compact systems This file defines compact systems of sets. @@ -31,14 +31,14 @@ system iff inserting `univ` gives a compact system. open Set Finset Nat -variable {α : Type*} {p : Set α → Prop} {C : ℕ → Set α} +variable {α : Type*} {S : Set (Set α)} {C : ℕ → Set α} section definition /-- A set of sets is a compact system if, whenever a countable subfamily has empty intersection, then finitely many of them already have empty intersection. -/ -def IsCompactSystem (p : Set α → Prop) : Prop := - ∀ C : ℕ → Set α, (∀ i, p (C i)) → ⋂ i, C i = ∅ → ∃ (n : ℕ), dissipate C n = ∅ +def IsCompactSystem (S : Set (Set α)) : Prop := + ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → ⋂ i, C i = ∅ → ∃ (n : ℕ), dissipate C n = ∅ end definition @@ -48,48 +48,48 @@ open Classical in /-- In a compact system, given a countable family with `⋂ i, C i = ∅`, we choose the smallest `n` with `⋂ (i ≤ n), C i = ∅`. -/ noncomputable -def finite_of_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i)) +def finite_of_empty (hp : IsCompactSystem S) (hC : ∀ i, C i ∈ S) (hC_empty : ⋂ i, C i = ∅) : ℕ := Nat.find (hp C hC hC_empty) open Classical in -lemma dissipate_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i)) +lemma dissipate_eq_empty (hp : IsCompactSystem S) (hC : ∀ i, C i ∈ S) (hC_empty : ⋂ i, C i = ∅) : dissipate C (hp.finite_of_empty hC hC_empty) = ∅ := by apply Nat.find_spec (hp C hC hC_empty) lemma of_nonempty_iInter - (h : ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) : - IsCompactSystem p := by + (h : ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → (∀ n, (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) : + IsCompactSystem S := by intro C hC contrapose! exact h C hC -lemma nonempty_iInter (hp : IsCompactSystem p) {C : ℕ → Set α} (hC : ∀ i, p (C i)) +lemma nonempty_iInter (hp : IsCompactSystem S) {C : ℕ → Set α} (hC : ∀ i, C i ∈ S) (h_nonempty : ∀ n, (dissipate C n).Nonempty) : (⋂ i, C i).Nonempty := by revert h_nonempty contrapose! exact hp C hC -theorem iff_nonempty_iInter (p : Set α → Prop) : - IsCompactSystem p ↔ (∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ), - (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) := +theorem iff_nonempty_iInter (S : Set (Set α)) : + IsCompactSystem S ↔ + ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → (∀ n, (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty := ⟨nonempty_iInter, of_nonempty_iInter⟩ @[simp] -lemma of_IsEmpty [IsEmpty α] (p : Set α → Prop) : IsCompactSystem p := +lemma of_IsEmpty [IsEmpty α] (S : Set (Set α)) : IsCompactSystem S := fun s _ _ ↦ ⟨0, Set.eq_empty_of_isEmpty (dissipate s 0)⟩ /-- Any subset of a compact system is a compact system. -/ -theorem mono {C D : (Set α) → Prop} (hD : IsCompactSystem D) (hCD : ∀ s, C s → D s) : +theorem mono {C D : Set (Set α)} (hD : IsCompactSystem D) (hCD : ∀ s, s ∈ C → s ∈ D) : IsCompactSystem C := fun s hC hs ↦ hD s (fun i ↦ hCD (s i) (hC i)) hs /-- In this equivalent formulation for a compact system, note that we use `⋂ k < n, C k` rather than `⋂ k ≤ n, C k`. -/ -lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : - IsCompactSystem p ↔ - ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by +lemma iff_nonempty_iInter_of_lt (S : Set (Set α)) : + IsCompactSystem S ↔ + ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by simp_rw [iff_nonempty_iInter] refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq_iInter_lt ▸ (h' (n + 1))), fun h C hi h' ↦ h C hi ?_⟩ @@ -100,8 +100,8 @@ lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : /-- A set system is a compact system iff adding `∅` gives a compact system. -/ lemma iff_isCompactSystem_of_or_empty : - IsCompactSystem p ↔ IsCompactSystem (fun s ↦ (p s ∨ (s = ∅))) := by - refine ⟨fun h s h' hd ↦ ?_, fun h ↦ mono h (fun s ↦ fun a ↦ (Or.inr a).symm)⟩ + IsCompactSystem S ↔ IsCompactSystem (insert ∅ S) := by + refine ⟨fun h s h' hd ↦ ?_, fun h ↦ mono h (fun s hs ↦ Set.mem_insert_of_mem ∅ hs)⟩ by_cases g : ∃ n, s n = ∅ · use g.choose rw [← subset_empty_iff] at hd ⊢ @@ -115,20 +115,20 @@ lemma iff_isCompactSystem_of_or_empty : /-- A set system is a compact system iff adding `univ` gives a compact system. -/ lemma iff_isCompactSystem_of_or_univ : - IsCompactSystem p ↔ IsCompactSystem (fun s ↦ (p s ∨ s = univ)) := by - refine ⟨fun h ↦ ?_, fun h ↦ mono h (fun s ↦ fun a ↦ Or.symm (Or.inr a))⟩ + IsCompactSystem S ↔ IsCompactSystem (insert univ S) := by + refine ⟨fun h ↦ ?_, fun h ↦ mono h (fun s hs ↦ Set.mem_insert_of_mem univ hs)⟩ rcases isEmpty_or_nonempty α with hα | _ · simp rw [iff_nonempty_iInter] at h ⊢ intro s h' hd - by_cases h₀ : ∀ n, ¬ p (s n) - · simp only [h₀, false_or] at h' + by_cases h₀ : ∀ n, s n ∉ S + · simp only [mem_insert_iff, h₀, or_false] at h' simp [h'] push_neg at h₀ classical let n := Nat.find h₀ - let s' := fun i ↦ if p (s i) then s i else s n - have h₁ : ∀ i, p (s' i) := by simp [s']; grind + let s' := fun i ↦ if s i ∈ S then s i else s n + have h₁ : ∀ i, s' i ∈ S := by simp [s']; grind have h₂ : ⋂ i, s i = ⋂ i, s' i := by ext; simp; grind apply h₂ ▸ h s' h₁ by_contra! h_exists_empty @@ -141,38 +141,34 @@ lemma iff_isCompactSystem_of_or_univ : specialize hd (max j n) simp [h₃, h₇] at hd -theorem iff_directed (hpi : IsPiSystem {x |p x}) : - IsCompactSystem p ↔ - ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, p (C i)) → ⋂ i, C i = ∅ → +theorem iff_directed (hpi : IsPiSystem S) : + IsCompactSystem S ↔ + ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅ := by rw [iff_isCompactSystem_of_or_empty] refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩ · rw [exists_dissipate_eq_empty_iff_of_directed C hdi] exact h C (by simp [hi]) - · have hpi' : IsPiSystem {s | p s ∨ s = ∅} := by - convert IsPiSystem.insert_empty hpi using 1 - ext - simp - grind + · have hpi' : IsPiSystem (insert ∅ S) := hpi.insert_empty rw [← biInter_le_eq_iInter] at h2 obtain h' := h (dissipate C) directed_dissipate - have h₀ (h₀ : ∀ n, p (dissipate C n) ∨ dissipate C n = ∅) (h₁ : ⋂ n, dissipate C n = ∅) : + have h₀ (h₀ : ∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅) (h₁ : ⋂ n, dissipate C n = ∅) : ∃ n, dissipate C n = ∅ := by - by_cases! f : ∀ n, p (dissipate C n) + by_cases! f : ∀ n, dissipate C n ∈ S · apply h' f h₁ · obtain ⟨n, hn⟩ := f exact ⟨n, by simpa [hn] using h₀ n⟩ obtain h'' := IsPiSystem.dissipate_mem hpi' h1 - have h₁ : ∀ n, p (dissipate C n) ∨ dissipate C n = ∅ := by + have h₁ : ∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅ := by intro n by_cases g : (dissipate C n).Nonempty - · exact h'' n g + · simpa [or_comm] using h'' n g · exact .inr (Set.not_nonempty_iff_eq_empty.mp g) apply h₀ h₁ h2 -theorem iff_directed' (hpi : IsPiSystem p) : - IsCompactSystem p ↔ - ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, p (C i)) → (∀ n, (C n).Nonempty) → +theorem iff_directed' (hpi : IsPiSystem S) : + IsCompactSystem S ↔ + ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, C i ∈ S) → (∀ n, (C n).Nonempty) → (⋂ i, C i).Nonempty := by rw [IsCompactSystem.iff_directed hpi] refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩ <;> rw [← not_imp_not] <;> push_neg @@ -185,7 +181,7 @@ variable (α : Type*) [TopologicalSpace α] /-- The set of compact and closed sets is a compact system. -/ theorem of_isCompact_isClosed : - IsCompactSystem (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by + IsCompactSystem {s : Set α | IsCompact s ∧ IsClosed s} := by intro C hC_cc hC_inter by_contra! h_nonempty refine absurd hC_inter ?_ @@ -204,13 +200,13 @@ theorem of_isCompact_isClosed : /-- In a `T2Space` the set of compact sets is a compact system. -/ theorem of_isCompact [T2Space α] : - IsCompactSystem (fun s : Set α ↦ IsCompact s) := by + IsCompactSystem {s : Set α | IsCompact s} := by convert of_isCompact_isClosed α with s exact ⟨fun hs ↦ ⟨hs, hs.isClosed⟩, fun hs ↦ hs.1⟩ /-- The set of sets which are either compact and closed, or `univ`, is a compact system. -/ theorem of_isCompact_isClosed_or_univ : - IsCompactSystem (fun s : Set α ↦ (IsCompact s ∧ IsClosed s) ∨ (s = univ)) := by + IsCompactSystem (insert univ {s : Set α | IsCompact s ∧ IsClosed s}) := by rw [← iff_isCompactSystem_of_or_univ] apply of_isCompact_isClosed From 41caa5ae49a7c0b4ed7f267c4245cd34520f674f Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Mar 2026 11:04:47 +0100 Subject: [PATCH 10/26] extract lemmas --- .../Topology/Compactness/CompactSystem.lean | 112 ++++++++---------- 1 file changed, 48 insertions(+), 64 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 449b48fde4da9d..1fea1859b81671 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -20,11 +20,10 @@ This file defines compact systems of sets. ## Main results -* `IsCompactSystem.iff_isCompactSystem_of_or_univ`: A set system is a compact -system iff inserting `univ` gives a compact system. -* `IsClosedCompact.isCompactSystem`: The set of closed and compact sets is a compact system. -* `IsClosedCompact.isCompactSystem_of_T2Space`: In a `T2Space α`, the set of compact sets - is a compact system in a `T2Space`. +* `isCompactSystem_insert_univ_iff`: A set system is a compact system iff inserting `univ` + gives a compact system. +* `isCompactSystem_isCompact_isClosed`: The set of closed and compact sets is a compact system. +* `isCompactSystem_isCompact`: In a `T2Space`, the set of compact sets is a compact system. -/ @[expose] public section @@ -44,20 +43,6 @@ end definition namespace IsCompactSystem -open Classical in -/-- In a compact system, given a countable family with `⋂ i, C i = ∅`, we choose the smallest `n` -with `⋂ (i ≤ n), C i = ∅`. -/ -noncomputable -def finite_of_empty (hp : IsCompactSystem S) (hC : ∀ i, C i ∈ S) - (hC_empty : ⋂ i, C i = ∅) : ℕ := - Nat.find (hp C hC hC_empty) - -open Classical in -lemma dissipate_eq_empty (hp : IsCompactSystem S) (hC : ∀ i, C i ∈ S) - (hC_empty : ⋂ i, C i = ∅) : - dissipate C (hp.finite_of_empty hC hC_empty) = ∅ := by - apply Nat.find_spec (hp C hC hC_empty) - lemma of_nonempty_iInter (h : ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → (∀ n, (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) : IsCompactSystem S := by @@ -85,23 +70,9 @@ lemma of_IsEmpty [IsEmpty α] (S : Set (Set α)) : IsCompactSystem S := theorem mono {C D : Set (Set α)} (hD : IsCompactSystem D) (hCD : ∀ s, s ∈ C → s ∈ D) : IsCompactSystem C := fun s hC hs ↦ hD s (fun i ↦ hCD (s i) (hC i)) hs -/-- In this equivalent formulation for a compact system, -note that we use `⋂ k < n, C k` rather than `⋂ k ≤ n, C k`. -/ -lemma iff_nonempty_iInter_of_lt (S : Set (Set α)) : - IsCompactSystem S ↔ - ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by - simp_rw [iff_nonempty_iInter] - refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq_iInter_lt ▸ (h' (n + 1))), - fun h C hi h' ↦ h C hi ?_⟩ - simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢ - refine fun n g ↦ h' n ?_ - simp_rw [← subset_empty_iff, dissipate] at g ⊢ - exact le_trans (fun x ↦ by simp; grind) g - -/-- A set system is a compact system iff adding `∅` gives a compact system. -/ -lemma iff_isCompactSystem_of_or_empty : - IsCompactSystem S ↔ IsCompactSystem (insert ∅ S) := by - refine ⟨fun h s h' hd ↦ ?_, fun h ↦ mono h (fun s hs ↦ Set.mem_insert_of_mem ∅ hs)⟩ +/-- Inserting `∅` into a compact system gives a compact system. -/ +lemma insert_empty (h : IsCompactSystem S) : IsCompactSystem (insert ∅ S) := by + intro s h' hd by_cases g : ∃ n, s n = ∅ · use g.choose rw [← subset_empty_iff] at hd ⊢ @@ -113,13 +84,11 @@ lemma iff_isCompactSystem_of_or_empty : rw [Set.nonempty_iff_ne_empty] at g simpa [g] using h' -/-- A set system is a compact system iff adding `univ` gives a compact system. -/ -lemma iff_isCompactSystem_of_or_univ : - IsCompactSystem S ↔ IsCompactSystem (insert univ S) := by - refine ⟨fun h ↦ ?_, fun h ↦ mono h (fun s hs ↦ Set.mem_insert_of_mem univ hs)⟩ +/-- Inserting `univ` into a compact system gives a compact system. -/ +lemma insert_univ (h : IsCompactSystem S) : IsCompactSystem (insert univ S) := by rcases isEmpty_or_nonempty α with hα | _ · simp - rw [iff_nonempty_iInter] at h ⊢ + rw [IsCompactSystem.iff_nonempty_iInter] at h ⊢ intro s h' hd by_cases h₀ : ∀ n, s n ∉ S · simp only [mem_insert_iff, h₀, or_false] at h' @@ -141,11 +110,35 @@ lemma iff_isCompactSystem_of_or_univ : specialize hd (max j n) simp [h₃, h₇] at hd -theorem iff_directed (hpi : IsPiSystem S) : +end IsCompactSystem + +/-- In this equivalent formulation for a compact system, +note that we use `⋂ k < n, C k` rather than `⋂ k ≤ n, C k`. -/ +lemma isCompactSystem_iff_nonempty_iInter_of_lt (S : Set (Set α)) : + IsCompactSystem S ↔ + ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by + simp_rw [IsCompactSystem.iff_nonempty_iInter] + refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq_iInter_lt ▸ (h' (n + 1))), + fun h C hi h' ↦ h C hi ?_⟩ + simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢ + refine fun n g ↦ h' n ?_ + simp_rw [← subset_empty_iff, dissipate] at g ⊢ + exact le_trans (fun x ↦ by simp; grind) g + +/-- A set system is a compact system iff adding `∅` gives a compact system. -/ +lemma isCompactSystem_insert_empty_iff : + IsCompactSystem (insert ∅ S) ↔ IsCompactSystem S := + ⟨fun h ↦ h.mono (fun _ hs ↦ Set.mem_insert_of_mem ∅ hs), fun h ↦ h.insert_empty⟩ + +/-- A set system is a compact system iff adding `univ` gives a compact system. -/ +lemma isCompactSystem_insert_univ_iff : IsCompactSystem (insert univ S) ↔ IsCompactSystem S := + ⟨fun h ↦ h.mono (fun _ hs ↦ Set.mem_insert_of_mem univ hs), fun h ↦ h.insert_univ⟩ + +theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅ := by - rw [iff_isCompactSystem_of_or_empty] + rw [← isCompactSystem_insert_empty_iff] refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩ · rw [exists_dissipate_eq_empty_iff_of_directed C hdi] exact h C (by simp [hi]) @@ -166,32 +159,26 @@ theorem iff_directed (hpi : IsPiSystem S) : · exact .inr (Set.not_nonempty_iff_eq_empty.mp g) apply h₀ h₁ h2 -theorem iff_directed' (hpi : IsPiSystem S) : +theorem isCompactSystem_iff_directed' (hpi : IsPiSystem S) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, C i ∈ S) → (∀ n, (C n).Nonempty) → (⋂ i, C i).Nonempty := by - rw [IsCompactSystem.iff_directed hpi] + rw [isCompactSystem_iff_directed hpi] refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩ <;> rw [← not_imp_not] <;> push_neg · exact h1 C h3 h4 · exact h1 C h3 s section IsCompactIsClosed -variable (α : Type*) [TopologicalSpace α] - /-- The set of compact and closed sets is a compact system. -/ -theorem of_isCompact_isClosed : +theorem isCompactSystem_isCompact_isClosed (α : Type*) [TopologicalSpace α] : IsCompactSystem {s : Set α | IsCompact s ∧ IsClosed s} := by - intro C hC_cc hC_inter - by_contra! h_nonempty - refine absurd hC_inter ?_ - rw [← ne_eq, ← Set.nonempty_iff_ne_empty, ← Set.iInter_dissipate] + refine IsCompactSystem.of_nonempty_iInter fun C hC_cc h_nonempty ↦ ?_ + rw [← Set.iInter_dissipate] refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed (Set.dissipate C) - (fun n ↦ ?_) (fun n ↦ ?_) ?_ (fun n ↦ ?_) + (fun n ↦ ?_) h_nonempty ?_ (fun n ↦ ?_) · exact Set.antitone_dissipate (by lia) - · exact h_nonempty _ - · simp only [Set.dissipate_zero_nat] - exact (hC_cc 0).1 + · simpa using (hC_cc 0).1 · induction n with | zero => simp only [Set.dissipate_zero_nat]; exact (hC_cc 0).2 | succ n hn => @@ -199,17 +186,14 @@ theorem of_isCompact_isClosed : exact hn.inter (hC_cc (n + 1)).2 /-- In a `T2Space` the set of compact sets is a compact system. -/ -theorem of_isCompact [T2Space α] : +theorem isCompactSystem_isCompact (α : Type*) [TopologicalSpace α] [T2Space α] : IsCompactSystem {s : Set α | IsCompact s} := by - convert of_isCompact_isClosed α with s + convert isCompactSystem_isCompact_isClosed α with s exact ⟨fun hs ↦ ⟨hs, hs.isClosed⟩, fun hs ↦ hs.1⟩ /-- The set of sets which are either compact and closed, or `univ`, is a compact system. -/ -theorem of_isCompact_isClosed_or_univ : - IsCompactSystem (insert univ {s : Set α | IsCompact s ∧ IsClosed s}) := by - rw [← iff_isCompactSystem_of_or_univ] - apply of_isCompact_isClosed +theorem isCompactSystem_insert_univ_isCompact_isClosed (α : Type*) [TopologicalSpace α] : + IsCompactSystem (insert univ {s : Set α | IsCompact s ∧ IsClosed s}) := + (isCompactSystem_isCompact_isClosed α).insert_univ end IsCompactIsClosed - -end IsCompactSystem From 11115229ab78f6cbfaaa6331487dcebc50863913 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 4 Mar 2026 12:11:29 +0100 Subject: [PATCH 11/26] Apply suggestions from code review Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com> --- Mathlib/Data/Set/Dissipate.lean | 13 ++-- Mathlib/MeasureTheory/PiSystem.lean | 2 +- .../Topology/Compactness/CompactSystem.lean | 63 +++++++------------ 3 files changed, 30 insertions(+), 48 deletions(-) diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index 940a33d8b55831..70cd2d18ad71c4 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -28,7 +28,7 @@ def dissipate [LE α] (s : α → Set β) (x : α) : Set β := theorem dissipate_def [LE α] {x : α} : dissipate s x = ⋂ y ≤ x, s y := rfl -theorem dissipate_eq_iInter_lt {s : ℕ → Set β} {n : ℕ} : dissipate s n = ⋂ k < n + 1, s k := by +theorem dissipate_eq_biInter_lt {s : ℕ → Set β} {n : ℕ} : dissipate s n = ⋂ k < n + 1, s k := by simp_rw [Nat.lt_add_one_iff, dissipate] @[simp] @@ -84,22 +84,21 @@ theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) : grind /-- For a directed set of sets `s : ℕ → Set α` and `n : ℕ`, there exists `m : ℕ` (maybe -larger than `n`)such that `s m ⊆ dissipate s n`. -/ +larger than `n`) such that `s m ⊆ dissipate s n`. -/ lemma exists_subset_dissipate_of_directed {s : ℕ → Set α} (hd : Directed (fun (x y : Set α) => y ⊆ x) s) (n : ℕ) : ∃ m, s m ⊆ dissipate s n := by induction n with | zero => use 0; simp [dissipate_def] | succ n hn => obtain ⟨m, hm⟩ := hn - obtain ⟨k, hk⟩ := hd m (n+1) + obtain ⟨k, hk⟩ := hd m (n + 1) exact ⟨k, by simp; grind⟩ -lemma directed_dissipate {s : ℕ → Set α} : Directed (fun x y ↦ y ⊆ x) (dissipate s) := +lemma directed_dissipate {s : ℕ → Set α} : Directed (· ⊇ ·) (dissipate s) := antitone_dissipate.directed_ge -lemma exists_dissipate_eq_empty_iff_of_directed (C : ℕ → Set α) - (hd : Directed (fun x y ↦ y ⊆ x) C) : - (∃ n, C n = ∅) ↔ (∃ n, dissipate C n = ∅) := by +lemma exists_dissipate_eq_empty_iff_of_directed {s : ℕ → Set α} (hd : Directed (· ⊇ ·) s) : + (∃ n, s n = ∅) ↔ (∃ n, dissipate s n = ∅) := by refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, subset_eq_empty (dissipate_subset le_rfl) hn⟩ , ?_⟩ contrapose! intro h n diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean index 68ebda266c65d1..1d87a02b957680 100644 --- a/Mathlib/MeasureTheory/PiSystem.lean +++ b/Mathlib/MeasureTheory/PiSystem.lean @@ -108,7 +108,7 @@ theorem IsPiSystem.comap {α β} {S : Set (Set β)} (h_pi : IsPiSystem S) (f : rw [← Set.preimage_inter] at hst ⊢ exact ⟨s ∩ t, h_pi s hs_mem t ht_mem (nonempty_of_nonempty_preimage hst), rfl⟩ -/-- For a ∩-stable set of sets `C` on `α` and a sequence of sets `s` with this attribute, +/-- For a `π`-system `C` over `α` and a sequence of sets `s` belonging to `C`, `dissipate s n` belongs to `C`. -/ lemma IsPiSystem.dissipate_mem {s : ℕ → Set α} {C : Set (Set α)} (hC : IsPiSystem C) (h : ∀ n, s n ∈ C) (n : ℕ) (h' : (dissipate s n).Nonempty) : diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 1fea1859b81671..da2b24280f6ad9 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -67,8 +67,8 @@ lemma of_IsEmpty [IsEmpty α] (S : Set (Set α)) : IsCompactSystem S := fun s _ _ ↦ ⟨0, Set.eq_empty_of_isEmpty (dissipate s 0)⟩ /-- Any subset of a compact system is a compact system. -/ -theorem mono {C D : Set (Set α)} (hD : IsCompactSystem D) (hCD : ∀ s, s ∈ C → s ∈ D) : - IsCompactSystem C := fun s hC hs ↦ hD s (fun i ↦ hCD (s i) (hC i)) hs +theorem mono {T : Set (Set α)} (hT : IsCompactSystem T) (hST : S ⊆ T) : + IsCompactSystem S := fun C hC1 hC2 ↦ hT C (fun i ↦ hST (hC1 i)) hC2 /-- Inserting `∅` into a compact system gives a compact system. -/ lemma insert_empty (h : IsCompactSystem S) : IsCompactSystem (insert ∅ S) := by @@ -78,11 +78,7 @@ lemma insert_empty (h : IsCompactSystem S) : IsCompactSystem (insert ∅ S) := b rw [← subset_empty_iff] at hd ⊢ exact (dissipate_subset le_rfl).trans g.choose_spec.le · push_neg at g - refine h s (fun i ↦ ?_) hd - specialize g i - specialize h' i - rw [Set.nonempty_iff_ne_empty] at g - simpa [g] using h' + exact h s (fun i ↦ (mem_of_mem_insert_of_ne (h' i) (g i).ne_empty)) hd /-- Inserting `univ` into a compact system gives a compact system. -/ lemma insert_univ (h : IsCompactSystem S) : IsCompactSystem (insert univ S) := by @@ -91,8 +87,7 @@ lemma insert_univ (h : IsCompactSystem S) : IsCompactSystem (insert univ S) := b rw [IsCompactSystem.iff_nonempty_iInter] at h ⊢ intro s h' hd by_cases h₀ : ∀ n, s n ∉ S - · simp only [mem_insert_iff, h₀, or_false] at h' - simp [h'] + · simp_all push_neg at h₀ classical let n := Nat.find h₀ @@ -100,9 +95,8 @@ lemma insert_univ (h : IsCompactSystem S) : IsCompactSystem (insert univ S) := b have h₁ : ∀ i, s' i ∈ S := by simp [s']; grind have h₂ : ⋂ i, s i = ⋂ i, s' i := by ext; simp; grind apply h₂ ▸ h s' h₁ - by_contra! h_exists_empty - obtain ⟨j, hj⟩ := h_exists_empty - have h₃ (v : ℕ) (hv : n ≤ v) : dissipate s v = dissipate s' v:= by ext; simp; grind + by_contra! ⟨j, hj⟩ + have h₃ (v : ℕ) (hv : n ≤ v) : dissipate s v = dissipate s' v := by ext; simp; grind have h₇ : dissipate s' (max j n) = ∅ := by rw [← subset_empty_iff] at hj ⊢ exact (antitone_dissipate (Nat.le_max_left j n)).trans hj @@ -128,11 +122,11 @@ lemma isCompactSystem_iff_nonempty_iInter_of_lt (S : Set (Set α)) : /-- A set system is a compact system iff adding `∅` gives a compact system. -/ lemma isCompactSystem_insert_empty_iff : IsCompactSystem (insert ∅ S) ↔ IsCompactSystem S := - ⟨fun h ↦ h.mono (fun _ hs ↦ Set.mem_insert_of_mem ∅ hs), fun h ↦ h.insert_empty⟩ + ⟨fun h ↦ h.mono (subset_insert _ _), fun h ↦ h.insert_empty⟩ /-- A set system is a compact system iff adding `univ` gives a compact system. -/ lemma isCompactSystem_insert_univ_iff : IsCompactSystem (insert univ S) ↔ IsCompactSystem S := - ⟨fun h ↦ h.mono (fun _ hs ↦ Set.mem_insert_of_mem univ hs), fun h ↦ h.insert_univ⟩ + ⟨fun h ↦ h.mono (subset_insert _ _), .insert_univ⟩ theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) : IsCompactSystem S ↔ @@ -142,24 +136,18 @@ theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) : refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩ · rw [exists_dissipate_eq_empty_iff_of_directed C hdi] exact h C (by simp [hi]) - · have hpi' : IsPiSystem (insert ∅ S) := hpi.insert_empty - rw [← biInter_le_eq_iInter] at h2 - obtain h' := h (dissipate C) directed_dissipate - have h₀ (h₀ : ∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅) (h₁ : ⋂ n, dissipate C n = ∅) : - ∃ n, dissipate C n = ∅ := by - by_cases! f : ∀ n, dissipate C n ∈ S - · apply h' f h₁ - · obtain ⟨n, hn⟩ := f - exact ⟨n, by simpa [hn] using h₀ n⟩ - obtain h'' := IsPiSystem.dissipate_mem hpi' h1 - have h₁ : ∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅ := by - intro n - by_cases g : (dissipate C n).Nonempty - · simpa [or_comm] using h'' n g - · exact .inr (Set.not_nonempty_iff_eq_empty.mp g) - apply h₀ h₁ h2 - -theorem isCompactSystem_iff_directed' (hpi : IsPiSystem S) : + rw [← biInter_le_eq_iInter] at h2 + suffices (∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ (⋂ n, dissipate C n = ∅) by + by_cases! f : ∀ n, dissipate C n ∈ S + · exact h (dissipate C) directed_dissipate f this.2 + · obtain ⟨n, hn⟩ := f + exact ⟨n, by simpa [hn] using this.1 n⟩ + refine ⟨fun n ↦ ?_, h2⟩ + by_cases g : (dissipate C n).Nonempty + · simpa [or_comm] using hpi.insert_empty.dissipate_mem h1 n g + · exact .inr (Set.not_nonempty_iff_eq_empty.mp g) + +theorem isCompactSystem_iff_directed_of_nonempty (hpi : IsPiSystem S) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, C i ∈ S) → (∀ n, (C n).Nonempty) → (⋂ i, C i).Nonempty := by @@ -174,22 +162,17 @@ section IsCompactIsClosed theorem isCompactSystem_isCompact_isClosed (α : Type*) [TopologicalSpace α] : IsCompactSystem {s : Set α | IsCompact s ∧ IsClosed s} := by refine IsCompactSystem.of_nonempty_iInter fun C hC_cc h_nonempty ↦ ?_ - rw [← Set.iInter_dissipate] + rw [← iInter_dissipate] refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed (Set.dissipate C) - (fun n ↦ ?_) h_nonempty ?_ (fun n ↦ ?_) + (fun n ↦ ?_) h_nonempty ?_ (fun n ↦ isClosed_biInter (fun i _ ↦ (hC_cc i).2)) · exact Set.antitone_dissipate (by lia) · simpa using (hC_cc 0).1 - · induction n with - | zero => simp only [Set.dissipate_zero_nat]; exact (hC_cc 0).2 - | succ n hn => - rw [Set.dissipate_succ] - exact hn.inter (hC_cc (n + 1)).2 /-- In a `T2Space` the set of compact sets is a compact system. -/ theorem isCompactSystem_isCompact (α : Type*) [TopologicalSpace α] [T2Space α] : IsCompactSystem {s : Set α | IsCompact s} := by convert isCompactSystem_isCompact_isClosed α with s - exact ⟨fun hs ↦ ⟨hs, hs.isClosed⟩, fun hs ↦ hs.1⟩ + simpa using IsCompact.isClosed /-- The set of sets which are either compact and closed, or `univ`, is a compact system. -/ theorem isCompactSystem_insert_univ_isCompact_isClosed (α : Type*) [TopologicalSpace α] : From c109d6cadadf23e103b3de457898658f69f21eb0 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 12:14:50 +0100 Subject: [PATCH 12/26] fix --- Mathlib/Data/Set/Dissipate.lean | 2 +- Mathlib/Topology/Compactness/CompactSystem.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index 70cd2d18ad71c4..b9ddf39f338018 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -86,7 +86,7 @@ theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) : /-- For a directed set of sets `s : ℕ → Set α` and `n : ℕ`, there exists `m : ℕ` (maybe larger than `n`) such that `s m ⊆ dissipate s n`. -/ lemma exists_subset_dissipate_of_directed {s : ℕ → Set α} - (hd : Directed (fun (x y : Set α) => y ⊆ x) s) (n : ℕ) : ∃ m, s m ⊆ dissipate s n := by + (hd : Directed (· ⊇ ·) s) (n : ℕ) : ∃ m, s m ⊆ dissipate s n := by induction n with | zero => use 0; simp [dissipate_def] | succ n hn => diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index da2b24280f6ad9..3c726fc9bfbfd7 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -112,7 +112,7 @@ lemma isCompactSystem_iff_nonempty_iInter_of_lt (S : Set (Set α)) : IsCompactSystem S ↔ ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by simp_rw [IsCompactSystem.iff_nonempty_iInter] - refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq_iInter_lt ▸ (h' (n + 1))), + refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq_biInter_lt ▸ (h' (n + 1))), fun h C hi h' ↦ h C hi ?_⟩ simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢ refine fun n g ↦ h' n ?_ @@ -134,7 +134,7 @@ theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) : ∃ n, C n = ∅ := by rw [← isCompactSystem_insert_empty_iff] refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩ - · rw [exists_dissipate_eq_empty_iff_of_directed C hdi] + · rw [exists_dissipate_eq_empty_iff_of_directed hdi] exact h C (by simp [hi]) rw [← biInter_le_eq_iInter] at h2 suffices (∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ (⋂ n, dissipate C n = ∅) by From 37cd1521fe2301d3eed2794a1decabe95787c8cc Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 12:16:41 +0100 Subject: [PATCH 13/26] review --- Mathlib/Topology/Compactness/CompactSystem.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 3c726fc9bfbfd7..0c4b42cc946566 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -122,7 +122,7 @@ lemma isCompactSystem_iff_nonempty_iInter_of_lt (S : Set (Set α)) : /-- A set system is a compact system iff adding `∅` gives a compact system. -/ lemma isCompactSystem_insert_empty_iff : IsCompactSystem (insert ∅ S) ↔ IsCompactSystem S := - ⟨fun h ↦ h.mono (subset_insert _ _), fun h ↦ h.insert_empty⟩ + ⟨fun h ↦ h.mono (subset_insert _ _), .insert_empty⟩ /-- A set system is a compact system iff adding `univ` gives a compact system. -/ lemma isCompactSystem_insert_univ_iff : IsCompactSystem (insert univ S) ↔ IsCompactSystem S := @@ -130,8 +130,7 @@ lemma isCompactSystem_insert_univ_iff : IsCompactSystem (insert univ S) ↔ IsCo theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) : IsCompactSystem S ↔ - ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, C i ∈ S) → ⋂ i, C i = ∅ → - ∃ n, C n = ∅ := by + ∀ (C : ℕ → Set α), Directed (· ⊇ ·) C → (∀ i, C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅ := by rw [← isCompactSystem_insert_empty_iff] refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩ · rw [exists_dissipate_eq_empty_iff_of_directed hdi] From 9286ee29b5106bb9ee56a33248e145cff55c16f9 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 12:22:15 +0100 Subject: [PATCH 14/26] names --- Mathlib/Topology/Compactness/CompactSystem.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 0c4b42cc946566..8f8429971d5ec5 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -128,7 +128,7 @@ lemma isCompactSystem_insert_empty_iff : lemma isCompactSystem_insert_univ_iff : IsCompactSystem (insert univ S) ↔ IsCompactSystem S := ⟨fun h ↦ h.mono (subset_insert _ _), .insert_univ⟩ -theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) : +theorem isCompactSystem_iff_of_directed (hpi : IsPiSystem S) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), Directed (· ⊇ ·) C → (∀ i, C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅ := by rw [← isCompactSystem_insert_empty_iff] @@ -146,11 +146,11 @@ theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) : · simpa [or_comm] using hpi.insert_empty.dissipate_mem h1 n g · exact .inr (Set.not_nonempty_iff_eq_empty.mp g) -theorem isCompactSystem_iff_directed_of_nonempty (hpi : IsPiSystem S) : +theorem isCompactSystem_iff_nonempty_iInter_of_directed (hpi : IsPiSystem S) : IsCompactSystem S ↔ - ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, C i ∈ S) → (∀ n, (C n).Nonempty) → + ∀ (C : ℕ → Set α), (Directed (· ⊇ ·) C) → (∀ i, C i ∈ S) → (∀ n, (C n).Nonempty) → (⋂ i, C i).Nonempty := by - rw [isCompactSystem_iff_directed hpi] + rw [isCompactSystem_iff_of_directed hpi] refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩ <;> rw [← not_imp_not] <;> push_neg · exact h1 C h3 h4 · exact h1 C h3 s From 7eee760f8288c465a53adcd2dcf310e25a0c8df1 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 12:27:00 +0100 Subject: [PATCH 15/26] review --- Mathlib/Data/Set/Accumulate.lean | 3 +++ Mathlib/Topology/Compactness/CompactSystem.lean | 4 ++++ 2 files changed, 7 insertions(+) diff --git a/Mathlib/Data/Set/Accumulate.lean b/Mathlib/Data/Set/Accumulate.lean index 624341f03ef2d2..8bae818150f0d9 100644 --- a/Mathlib/Data/Set/Accumulate.lean +++ b/Mathlib/Data/Set/Accumulate.lean @@ -35,6 +35,9 @@ def accumulate [LE α] (s : α → Set β) (x : α) : Set β := theorem accumulate_def [LE α] {x : α} : accumulate s x = ⋃ y ≤ x, s y := rfl +theorem accumulate_eq_biInter_lt {s : ℕ → Set β} {n : ℕ} : accumulate s n = ⋃ k < n + 1, s k := by + simp_rw [Nat.lt_add_one_iff, accumulate] + @[simp] theorem mem_accumulate [LE α] {x : α} {z : β} : z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y := by simp_rw [accumulate_def, mem_iUnion₂, exists_prop] diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 8f8429971d5ec5..963949292db39f 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -128,6 +128,8 @@ lemma isCompactSystem_insert_empty_iff : lemma isCompactSystem_insert_univ_iff : IsCompactSystem (insert univ S) ↔ IsCompactSystem S := ⟨fun h ↦ h.mono (subset_insert _ _), .insert_univ⟩ +/-- To prove that a set of sets is a compact system, it suffices to consider directed families of +sets. -/ theorem isCompactSystem_iff_of_directed (hpi : IsPiSystem S) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), Directed (· ⊇ ·) C → (∀ i, C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅ := by @@ -146,6 +148,8 @@ theorem isCompactSystem_iff_of_directed (hpi : IsPiSystem S) : · simpa [or_comm] using hpi.insert_empty.dissipate_mem h1 n g · exact .inr (Set.not_nonempty_iff_eq_empty.mp g) +/-- To prove that a set of sets is a compact system, it suffices to consider directed families of +sets. -/ theorem isCompactSystem_iff_nonempty_iInter_of_directed (hpi : IsPiSystem S) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), (Directed (· ⊇ ·) C) → (∀ i, C i ∈ S) → (∀ n, (C n).Nonempty) → From 0161fd7bcef5a570b56908330dce5497d185087a Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 12:30:35 +0100 Subject: [PATCH 16/26] add accumulate versions --- Mathlib/Data/Set/Accumulate.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Mathlib/Data/Set/Accumulate.lean b/Mathlib/Data/Set/Accumulate.lean index 8bae818150f0d9..19d8485ca34991 100644 --- a/Mathlib/Data/Set/Accumulate.lean +++ b/Mathlib/Data/Set/Accumulate.lean @@ -85,6 +85,7 @@ theorem disjoint_accumulate [Preorder α] (hs : Pairwise (Disjoint on s)) {i j : rcases hx with ⟨k, hk, hx⟩ exact disjoint_left.1 (hs (hk.trans_lt hij).ne) hx +@[simp] theorem accumulate_succ (u : ℕ → Set α) (n : ℕ) : accumulate u (n + 1) = accumulate u n ∪ u (n + 1) := biUnion_le_succ u n @@ -93,4 +94,19 @@ lemma partialSups_eq_accumulate (f : ℕ → Set α) : ext n simp [partialSups_eq_sup_range, accumulate, Nat.lt_succ_iff] +/-- For a directed set of sets `s : ℕ → Set α` and `n : ℕ`, there exists `m : ℕ` (maybe +larger than `n`) such that `accumulate s n ⊆ s m`. -/ +lemma exists_subset_accumulate_of_directed {s : ℕ → Set α} + (hd : Directed (· ⊆ ·) s) (n : ℕ) : ∃ m, accumulate s n ⊆ s m := by + induction n with + | zero => use 0; simp [accumulate_def] + | succ n hn => + obtain ⟨m, hm⟩ := hn + obtain ⟨k, hk⟩ := hd m (n + 1) + simp at hk + exact ⟨k, by simp; grind⟩ + +lemma directed_accumulate {s : ℕ → Set α} : Directed (· ⊆ ·) (accumulate s) := + monotone_accumulate.directed_le + end Set From 82693239f7c8e17287adb48e91ac397afe8a9398 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 12:31:56 +0100 Subject: [PATCH 17/26] flip iff --- Mathlib/Data/Set/Dissipate.lean | 4 ++-- Mathlib/Topology/Compactness/CompactSystem.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index b9ddf39f338018..0d2b153f30f149 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -98,8 +98,8 @@ lemma directed_dissipate {s : ℕ → Set α} : Directed (· ⊇ ·) (dissipate antitone_dissipate.directed_ge lemma exists_dissipate_eq_empty_iff_of_directed {s : ℕ → Set α} (hd : Directed (· ⊇ ·) s) : - (∃ n, s n = ∅) ↔ (∃ n, dissipate s n = ∅) := by - refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, subset_eq_empty (dissipate_subset le_rfl) hn⟩ , ?_⟩ + (∃ n, dissipate s n = ∅) ↔ (∃ n, s n = ∅) := by + refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n, subset_eq_empty (dissipate_subset le_rfl) hn⟩⟩ contrapose! intro h n obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 963949292db39f..439102fe321e0e 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -135,7 +135,7 @@ theorem isCompactSystem_iff_of_directed (hpi : IsPiSystem S) : ∀ (C : ℕ → Set α), Directed (· ⊇ ·) C → (∀ i, C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅ := by rw [← isCompactSystem_insert_empty_iff] refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩ - · rw [exists_dissipate_eq_empty_iff_of_directed hdi] + · rw [← exists_dissipate_eq_empty_iff_of_directed hdi] exact h C (by simp [hi]) rw [← biInter_le_eq_iInter] at h2 suffices (∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ (⋂ n, dissipate C n = ∅) by From a17c917659e171e3e7c352229ed79df4fed3e490 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 14:27:48 +0100 Subject: [PATCH 18/26] add accumulate lemma --- Mathlib/Data/Set/Accumulate.lean | 9 +++++++++ Mathlib/Data/Set/Dissipate.lean | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Set/Accumulate.lean b/Mathlib/Data/Set/Accumulate.lean index 19d8485ca34991..749df4d76567f9 100644 --- a/Mathlib/Data/Set/Accumulate.lean +++ b/Mathlib/Data/Set/Accumulate.lean @@ -109,4 +109,13 @@ lemma exists_subset_accumulate_of_directed {s : ℕ → Set α} lemma directed_accumulate {s : ℕ → Set α} : Directed (· ⊆ ·) (accumulate s) := monotone_accumulate.directed_le +lemma exists_accumulate_eq_univ_iff_of_directed {s : ℕ → Set α} (hd : Directed (· ⊆ ·) s) : + (∃ n, accumulate s n = univ) ↔ ∃ n, s n = univ := by + refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n, + subset_antisymm (subset_univ _) (hn.symm.le.trans subset_accumulate)⟩⟩ + contrapose! + intro h n + obtain ⟨m, hm⟩ := exists_subset_accumulate_of_directed hd n + grind + end Set diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index 0d2b153f30f149..f0d281c104912e 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -98,7 +98,7 @@ lemma directed_dissipate {s : ℕ → Set α} : Directed (· ⊇ ·) (dissipate antitone_dissipate.directed_ge lemma exists_dissipate_eq_empty_iff_of_directed {s : ℕ → Set α} (hd : Directed (· ⊇ ·) s) : - (∃ n, dissipate s n = ∅) ↔ (∃ n, s n = ∅) := by + (∃ n, dissipate s n = ∅) ↔ ∃ n, s n = ∅ := by refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n, subset_eq_empty (dissipate_subset le_rfl) hn⟩⟩ contrapose! intro h n From e7ba393095cc681213c0025b595a6036e8a81644 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 4 Mar 2026 14:29:00 +0100 Subject: [PATCH 19/26] Update Mathlib/Topology/Compactness/CompactSystem.lean Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com> --- Mathlib/Topology/Compactness/CompactSystem.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 439102fe321e0e..46cdbb9783e203 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -86,9 +86,8 @@ lemma insert_univ (h : IsCompactSystem S) : IsCompactSystem (insert univ S) := b · simp rw [IsCompactSystem.iff_nonempty_iInter] at h ⊢ intro s h' hd - by_cases h₀ : ∀ n, s n ∉ S + by_cases! h₀ : ∀ n, s n ∉ S · simp_all - push_neg at h₀ classical let n := Nat.find h₀ let s' := fun i ↦ if s i ∈ S then s i else s n From ecab847135462675363401ce0b6166918dca9d12 Mon Sep 17 00:00:00 2001 From: pfaffelh Date: Thu, 5 Mar 2026 23:01:00 +0100 Subject: [PATCH 20/26] init --- .../Topology/Compactness/CompactSystem.lean | 63 +++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 46cdbb9783e203..fe3bde0836b344 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -24,6 +24,8 @@ This file defines compact systems of sets. gives a compact system. * `isCompactSystem_isCompact_isClosed`: The set of closed and compact sets is a compact system. * `isCompactSystem_isCompact`: In a `T2Space`, the set of compact sets is a compact system. +* `IsCompactSystem.inter.isCompactSystem`: If `S` is a compact system, then the set of countable +intersections of sets in `S` is a compact system. -/ @[expose] public section @@ -182,3 +184,64 @@ theorem isCompactSystem_insert_univ_isCompact_isClosed (α : Type*) [Topological (isCompactSystem_isCompact_isClosed α).insert_univ end IsCompactIsClosed + +section Inter + +namespace IsCompactSystem + +/-- Countable intersections of sets in a compact system. -/ +def inter (S : Set (Set α)) : Set (Set α) := + sInter '' { L : Set (Set α) | L.Countable ∧ L ⊆ S} + +lemma inter.mem_iff (s : Set α) : + s ∈ inter S ↔ ∃ L : Set (Set α), L.Countable ∧ s = ⋂₀ L ∧ ↑L ⊆ S := by + refine ⟨fun ⟨L, hL⟩ ↦ ?_, fun h ↦ ?_⟩ + · simp only [mem_setOf_eq] at hL + use L + simp [hL] + · obtain ⟨L, hL⟩ := h + use L + simp [hL.1, hL.2] + +/- If `IsCompactSystem S`, the set of countable intersections of sets in `S` is also a compact +system. -/ +theorem inter.isCompactSystem (S : Set (Set α)) (hS : IsCompactSystem S) : + IsCompactSystem (inter S) := by + by_cases h : Nonempty α + · rw [IsCompactSystem] at hS ⊢ + intro D hD₁ hD₂ + simp_rw [inter.mem_iff] at hD₁ + choose E hE₁ using hD₁ + simp only [hE₁] at hD₂ + rw [← sInter_iUnion] at hD₂ + have hE₃ : (⋃ i, E i).Countable := by + simp [hE₁] + have hE₄ : (⋃ i, E i) ⊆ S := by + simp [hE₁] + haveI : Nonempty (⋃ i, E i) := by + contrapose! hD₂ + rw [Set.eq_empty_of_isEmpty (⋃ i, E i)] + simp only [sInter_empty] + refine nonempty_iff_univ_nonempty.mp h + let ⟨x, hx⟩ := this + rw [← range_enumerateCountable_of_mem hE₃ hx, sInter_range] at hD₂ + specialize hS (enumerateCountable hE₃ x) + obtain ⟨n, hn⟩ := hS (fun i ↦ hE₄ (enumerateCountable_mem hE₃ hx i)) hD₂ + have g (i : ℕ) : ∃ j, enumerateCountable hE₃ x i ∈ E j := by + rw [← mem_iUnion] + exact enumerateCountable_mem hE₃ hx i + choose g hg using g + use (Finset.range (n + 1)).sup g + refine subset_eq_empty ?_ hn + simp only [dissipate, subset_iInter_iff] + intro i hi + apply le_trans (b := D (g i)) _ ((hE₁ (g i)).2.1 ▸ sInter_subset_of_mem (hg i)) + apply biInter_subset_of_mem + change g i ≤ (Finset.range (n + 1)).sup g + exact le_sup (mem_range_succ_iff.mpr hi) + · simp only [not_nonempty_iff] at h + exact of_IsEmpty (inter S) + +end IsCompactSystem + +end Inter From ef088e6c37a5018892f7206bc09e0a6fc4b8a3f5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mar=C3=ADa=20In=C3=A9s=20de=20Frutos-Fern=C3=A1ndez?= <88536493+mariainesdff@users.noreply.github.com> Date: Wed, 18 Mar 2026 07:57:00 +0000 Subject: [PATCH 21/26] feat(NumberTheory/RatFunc/Ostrowski): prove Ostrowski's theorem for K(X) (#30505) We prove Ostrowski's theorem for the field of rational functions `K(X)`, where `K` is any field. Co-authored-by: @xgenereux Co-authored-by: mariainesdff Co-authored-by: mariainesdff --- Mathlib.lean | 1 + Mathlib/FieldTheory/RatFunc/AsPolynomial.lean | 35 ++- Mathlib/FieldTheory/RatFunc/Degree.lean | 6 + Mathlib/NumberTheory/FunctionField.lean | 3 + Mathlib/NumberTheory/RatFunc/Ostrowski.lean | 285 ++++++++++++++++++ docs/1000.yaml | 6 +- 6 files changed, 316 insertions(+), 20 deletions(-) create mode 100644 Mathlib/NumberTheory/RatFunc/Ostrowski.lean diff --git a/Mathlib.lean b/Mathlib.lean index 9982e285aa34ed..dd8378ddde6791 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5625,6 +5625,7 @@ public import Mathlib.NumberTheory.RamificationInertia.Basic public import Mathlib.NumberTheory.RamificationInertia.Galois public import Mathlib.NumberTheory.RamificationInertia.HilbertTheory public import Mathlib.NumberTheory.RamificationInertia.Unramified +public import Mathlib.NumberTheory.RatFunc.Ostrowski public import Mathlib.NumberTheory.Rayleigh public import Mathlib.NumberTheory.Real.GoldenRatio public import Mathlib.NumberTheory.Real.Irrational diff --git a/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean b/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean index 681a7d2b3a474b..77dbf9a59c00ba 100644 --- a/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean +++ b/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean @@ -87,6 +87,10 @@ theorem aeval_X_left_eq_algebraMap (p : K[X]) : p.aeval (X : K⟮X⟯) = algebraMap K[X] K⟮X⟯ p := by induction p using Polynomial.induction_on' <;> simp_all +@[simp] +theorem coePolynomial_eq_algebraMap (p : K[X]) : + (p : RatFunc K) = algebraMap (Polynomial K) (RatFunc K) p := rfl + @[simp] lemma liftRingHom_C {L : Type*} [Field L] (φ : K[X] →+* L) (hφ : K[X]⁰ ≤ L⁰.comap φ) (x : K) : liftRingHom φ hφ (C x) = φ (.C x) := @@ -308,18 +312,15 @@ variable {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] section Algebra -variable (L : Type*) [Field L] [Algebra K L] {v : Valuation L Γ} - (hv : ∀ a : K, a ≠ 0 → v (algebraMap K L a) = 1) - -include hv +variable (L : Type*) [Field L] [Algebra K L] {v : Valuation L Γ} [hv : v.IsTrivialOn K] lemma valuation_aeval_monomial_eq_valuation_pow (w : L) (n : ℕ) {a : K} (ha : a ≠ 0) : v ((monomial n a).aeval w) = (v w) ^ n := by - simp [← C_mul_X_pow_eq_monomial, map_mul, map_pow, one_mul, hv a ha] + simp [← C_mul_X_pow_eq_monomial, map_mul, map_pow, one_mul, hv.eq_one a ha] theorem valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X (w : L) (hpos : 1 < v w) {p : Polynomial K} (hp : p ≠ 0) : v (p.aeval w) = v w ^ p.natDegree := by - rw [← valuation_aeval_monomial_eq_valuation_pow _ _ hv _ _ (leadingCoeff_ne_zero.mpr hp)] + rw [← valuation_aeval_monomial_eq_valuation_pow _ _ _ _ ((leadingCoeff_ne_zero).mpr hp)] nth_rw 1 [as_sum_range p, map_sum] apply Valuation.map_sum_eq_of_lt _ (by simp) intro i hi @@ -327,32 +328,30 @@ theorem valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X (w : ← lt_iff_le_and_ne] at hi simp only [← C_mul_X_pow_eq_monomial, map_mul, aeval_C, map_pow, aeval_X, coeff_natDegree] by_cases h0 : (p.coeff i) = 0 - · simp [h0, map_zero, zero_mul, one_mul, hv p.leadingCoeff (leadingCoeff_ne_zero.mpr hp), + · simp [h0, map_zero, zero_mul, one_mul, hv.eq_one p.leadingCoeff (leadingCoeff_ne_zero.mpr hp), pow_pos (lt_trans zero_lt_one hpos) p.natDegree] - · simp [one_mul, hv p.leadingCoeff (leadingCoeff_ne_zero.mpr hp), - hv _ h0, one_mul, pow_lt_pow_right₀ hpos hi] + · simp [one_mul, hv.eq_one p.leadingCoeff ((leadingCoeff_ne_zero).mpr hp), + hv.eq_one _ h0, one_mul, pow_lt_pow_right₀ hpos hi] end Algebra -variable {v : Valuation K⟮X⟯ Γ} (hv : ∀ a : K, a ≠ 0 → v (C a) = 1) +variable {v : Valuation K⟮X⟯ Γ} [hv : v.IsTrivialOn K] open Valuation -include hv - /-- If a valuation `v` is trivial on constants then for every `n : ℕ` the valuation of `(monomial n a)` is equal to `(v RatFunc.X) ^ n`. -/ lemma valuation_monomial_eq_valuation_X_pow (n : ℕ) {a : K} (ha : a ≠ 0) : v (monomial n a) = v RatFunc.X ^ n := by - simp_all [RatFunc.coePolynomial, ← C_mul_X_pow_eq_monomial] + simp_all [← RatFunc.algebraMap_eq_C, hv.eq_one] /-- If a valuation `v` is trivial on constants and `1 < v RatFunc.X` then for every polynomial `p`, `v p = v RatFunc.X ^ p.natDegree`. Note: The condition `1 < v RatFunc.X` is typically satisfied by the valuation at infinity. -/ -theorem valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X (hlt : 1 < v RatFunc.X) - {p : K[X]} (hp : p ≠ 0) : v p = v RatFunc.X ^ p.natDegree := by - convert valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X K K⟮X⟯ hv +theorem valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X + (hlt : 1 < v RatFunc.X) {p : K[X]} (hp : p ≠ 0) : v p = v RatFunc.X ^ p.natDegree := by + convert valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X K K⟮X⟯ RatFunc.X hlt hp ext p nth_rw 1 [RatFunc.X, ← aeval_X_left_apply p (R := K)] @@ -368,14 +367,14 @@ theorem valuation_le_one_of_valuation_X_le_one (hle : v RatFunc.X ≤ 1) (p : K[ by_cases h0 : p.coeff i = 0 · simp_all · rw [← RatFunc.coePolynomial] - simp_all [valuation_monomial_eq_valuation_X_pow, pow_le_one'] + simp_all [pow_le_one', ← RatFunc.algebraMap_eq_C, hv.eq_one _ h0] /-- If a valuation `v` is trivial on constants then for every `n : ℕ` the valuation of `1 / (monomial n a)` (as an element of the field of rational functions) is equal to `(v RatFunc.X) ^ (- n)`. -/ lemma valuation_inv_monomial_eq_valuation_X_zpow (n : ℕ) {a : K} (ha : a ≠ 0) : v (1 / monomial n a) = v RatFunc.X ^ (-(n : ℤ)) := by - simpa using valuation_monomial_eq_valuation_X_pow _ hv n ha + simp [← RatFunc.algebraMap_eq_C, hv.eq_one _ ha] end TrivialOnConstants diff --git a/Mathlib/FieldTheory/RatFunc/Degree.lean b/Mathlib/FieldTheory/RatFunc/Degree.lean index b585e642b6874c..3a50b92aaa10bf 100644 --- a/Mathlib/FieldTheory/RatFunc/Degree.lean +++ b/Mathlib/FieldTheory/RatFunc/Degree.lean @@ -82,6 +82,12 @@ theorem intDegree_mul {x y : K⟮X⟯} (hx : x ≠ 0) (hy : y ≠ 0) : theorem intDegree_inv (x : K⟮X⟯) : intDegree (x⁻¹) = - intDegree x := by by_cases hx : x = 0 <;> simp [hx, eq_neg_iff_add_eq_zero, ← intDegree_mul (inv_ne_zero hx) hx] +set_option backward.isDefEq.respectTransparency false in +lemma intDegree_div {x y : RatFunc K} (hx : x ≠ 0) (hy : y ≠ 0) : + (x / y).intDegree = x.intDegree - y.intDegree := by + rw [div_eq_mul_inv, intDegree_mul, intDegree_inv, ← sub_eq_add_neg] <;> grind + +set_option backward.isDefEq.respectTransparency false in @[simp] theorem intDegree_neg (x : K⟮X⟯) : intDegree (-x) = intDegree x := by by_cases hx : x = 0 diff --git a/Mathlib/NumberTheory/FunctionField.lean b/Mathlib/NumberTheory/FunctionField.lean index bdd65eed1eea37..af71fedeb637ca 100644 --- a/Mathlib/NumberTheory/FunctionField.lean +++ b/Mathlib/NumberTheory/FunctionField.lean @@ -222,6 +222,9 @@ theorem inftyValuation.polynomial {p : Fq[X]} (hp : p ≠ 0) : instance : Valuation.IsNontrivial (inftyValuation Fq) := ⟨RatFunc.X, by simp⟩ +instance : Valuation.IsTrivialOn Fq (inftyValuation Fq) := + ⟨fun _ hx ↦ by simp [inftyValuation.C _ hx]⟩ + /-- The valued field `Fq(t)` with the valuation at infinity. -/ @[implicit_reducible] def inftyValuedFqt : Valued (RatFunc Fq) ℤᵐ⁰ := diff --git a/Mathlib/NumberTheory/RatFunc/Ostrowski.lean b/Mathlib/NumberTheory/RatFunc/Ostrowski.lean new file mode 100644 index 00000000000000..0a3050efe7e8d4 --- /dev/null +++ b/Mathlib/NumberTheory/RatFunc/Ostrowski.lean @@ -0,0 +1,285 @@ +/- +Copyright (c) 2025 María Inés de Frutos-Fernández & Xavier Généreux. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: María Inés de Frutos-Fernández, Xavier Généreux +-/ +module + +public import Mathlib.FieldTheory.Finite.Valuation +public import Mathlib.NumberTheory.FunctionField +public import Mathlib.RingTheory.Valuation.Discrete.Basic + +/-! +# Ostrowski's theorem for `K(X)` + +This file proves Ostrowski's theorem for the field of rational functions `K(X)`, where `K` is any +field: if `v` is a discrete valuation on `K(X)` which is trivial on elements of `K`, then `v` is +equivalent to either the `I`-adic valuation for some `I : HeightOneSpectrum K[X]`, or to the +valuation at infinity `FunctionField.inftyValuation K`. + +## Main results +- `RatFunc.valuation_isEquiv_infty_or_adic`: Ostrowski's theorem for `K(X)`. +-/ + +@[expose] public noncomputable section + + +open Multiplicative WithZero + +variable {K Γ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} + +namespace RatFunc + +section Infinity + +open FunctionField Polynomial Valuation + +lemma valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X {f : RatFunc K} + [v.IsTrivialOn K] (hlt : 1 < v X) (hf : f ≠ 0) : v f = v RatFunc.X ^ f.intDegree := by + induction f using RatFunc.induction_on with + | f p q hq => + rw [intDegree_div (by grind only) (by grind only), v.map_div, zpow_sub₀ (ne_zero_of_lt hlt)] + simp_rw [intDegree_polynomial, zpow_natCast, ← coePolynomial_eq_algebraMap] + have hp : p ≠ 0 := by contrapose! hf; simp [hf] + rw [valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt hp, + valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt hq] + +variable [DecidableEq (RatFunc K)] + +lemma valuation_isEquiv_inftyValuation_of_one_lt_valuation_X [v.IsTrivialOn K] (hlt : 1 < v X) : + v.IsEquiv (inftyValuation K) := by + refine isEquiv_iff_val_lt_one.mpr fun {f} ↦ ?_ + rcases eq_or_ne f 0 with rfl | hf + · simp + · have hlt' : 1 < inftyValuation K X := by simp [← exp_zero] + rw [valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X hlt hf, + valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X hlt' hf] + grind [one_le_zpow_iff_right₀] + +end Infinity + +open IsDedekindDomain HeightOneSpectrum Set Valuation FunctionField Polynomial + +lemma setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty [v.IsNontrivial] [v.IsTrivialOn K] + (hle : v RatFunc.X ≤ 1) : {p : K[X] | v p < 1 ∧ p ≠ 0}.Nonempty := by + obtain ⟨w , h0, h1⟩ := IsNontrivial.exists_lt_one (v := v) + induction w using RatFunc.induction_on with + | f p q => + simp only [ne_eq, _root_.div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or, + map_div₀] at * + have hor : ¬v ↑p = 1 ∨ ¬v ↑q = 1 := by rw [← not_and_or]; aesop + suffices ∀ r : K[X], v (↑r) ≠ 1 → r ≠ 0 → {p : K[X] | v ↑p < 1 ∧ ¬p = 0}.Nonempty by + exact Or.elim hor (fun hp ↦ this p hp h0.1) (fun hq ↦ this q hq h0.2) + exact fun r hr hr0 ↦ ⟨r, lt_iff_le_and_ne.mpr + ⟨Polynomial.valuation_le_one_of_valuation_X_le_one _ hle r, hr⟩, hr0⟩ + +private lemma one_le_valuation_factor (hne : {p : K[X] | v p < 1 ∧ p ≠ 0}.Nonempty) {a b : K[X]} + (hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0) (hπᵥ : degree_lt_wf.min _ hne = a * b) + (hb : ¬IsUnit b) : 1 ≤ v ↑a := by + set πᵥ := degree_lt_wf.min _ hne + have hda : a.degree < πᵥ.degree := by + have hbpos := degree_pos_of_ne_zero_of_nonunit hab.2.2 hb + simp_rw [hπᵥ, degree_mul, degree_eq_natDegree hab.2.1, degree_eq_natDegree hab.2.2] at hbpos ⊢ + norm_cast + simpa using hbpos + have hlea := imp_not_comm.mp (degree_lt_wf.not_lt_min _) hda + grind + +lemma irreducible_min_polynomial_valuation_lt_one_and_ne_zero [v.IsTrivialOn K] + (hne : {p : K[X] | v p < 1 ∧ p ≠ 0}.Nonempty) : + Irreducible (degree_lt_wf.min {p : K[X] | v p < 1 ∧ p ≠ 0} hne) := by + set πᵥ := degree_lt_wf.min _ hne + have hπᵥ : v πᵥ < 1 ∧ πᵥ ≠ 0 := degree_lt_wf.min_mem _ hne + refine irreducible_iff.mpr ⟨?_, fun a b hab ↦ ?_⟩ + · simp only [Polynomial.isUnit_iff, isUnit_iff_ne_zero] + intro ⟨a, ha0, ha⟩ + rw [← ha, coePolynomial, algebraMap_C, ← algebraMap_eq_C] at hπᵥ + grind + · by_contra! H + simp only [hab, ne_eq, mul_eq_zero, not_or] at hπᵥ + have hva := one_le_valuation_factor hne hπᵥ hab H.2 + simp only [mul_comm a b, @and_comm (¬a = 0)] at hπᵥ hab + have := Right.one_le_mul (one_le_valuation_factor hne hπᵥ hab H.1) hva + simp only [coePolynomial_eq_algebraMap, map_mul] at hπᵥ this + grind + +section valuation_X_le_one + +variable [v.IsNontrivial] [v.IsTrivialOn K] (hle : v RatFunc.X ≤ 1) + +/-- A uniformizing element for the valuation `v`, as a polynomial in `K[X]`. -/ +abbrev uniformizingPolynomial : K[X] := + WellFounded.min degree_lt_wf _ (setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty hle) + +@[inherit_doc] +local notation "πᵥ" => uniformizingPolynomial hle + +lemma uniformizingPolynomial_ne_zero : πᵥ ≠ 0 := by + have := degree_lt_wf.min_mem _ (setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty hle) + simp_all [uniformizingPolynomial] + +lemma valuation_uniformizingPolynomial_lt_one : v πᵥ < 1 := by + simpa using (degree_lt_wf.min_mem _ + (setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty hle)).1 + +open Ideal in +/-- The maximal ideal of `K[X]` generated by the `uniformizingPolynomial` for `v`. -/ +def valuationIdeal : HeightOneSpectrum K[X] where + asIdeal := Submodule.span K[X] {πᵥ} + isPrime := IsMaximal.isPrime (PrincipalIdealRing.isMaximal_of_irreducible + (irreducible_min_polynomial_valuation_lt_one_and_ne_zero + (setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty hle))) + ne_bot := by simpa using uniformizingPolynomial_ne_zero hle + +@[inherit_doc] +local notation "Pᵥ" => RatFunc.valuationIdeal hle + +section Associates + +open EuclideanDomain in +lemma valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one {p : K[X]} + (hp : p ≠ 0) : + v (algebraMap K[X] (RatFunc K) p) = v (πᵥ ^ ((Associates.mk (Pᵥ).asIdeal).count + (Associates.mk (Ideal.span {p})).factors)) := by + set π := πᵥ + have hne := setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty hle + have hπirr : Irreducible π := irreducible_min_polynomial_valuation_lt_one_and_ne_zero hne + obtain ⟨k, q, hnq, heq⟩ := WfDvdMonoid.max_power_factor hp hπirr + have hπ : π ∈ _ := degree_lt_wf.min_mem _ hne + simp only [ne_eq, mem_setOf] at hπ + nth_rw 1 [heq] + simp only [map_mul, map_pow] + suffices v (algebraMap K[X] (RatFunc K) q) = 1 by + simp only [this, mul_one] + congr + exact (Ideal.count_associates_eq (irreducible_iff_prime.mp hπirr) hnq heq).symm + rw [← mod_add_div q π, map_add] + rw [← mod_eq_zero] at hnq + suffices v (algebraMap K[X] (RatFunc K) (q % π)) = 1 ∧ + v (algebraMap K[X] (RatFunc K) (π * (q / π))) < 1 by + obtain ⟨h₁, h₂⟩ := this + rw [← h₁] at h₂ ⊢ + exact Valuation.map_add_eq_of_lt_left _ h₂ + constructor + · rw [← coePolynomial_eq_algebraMap] + have hnπ : q % π ∉ {p : K[X] | v ↑p < 1 ∧ p ≠ 0} := + imp_not_comm.mp (degree_lt_wf.not_lt_min _) (EuclideanDomain.remainder_lt q hπ.2) + have := Polynomial.valuation_le_one_of_valuation_X_le_one _ hle (q % π) + grind + · simpa only [map_mul, ← coePolynomial_eq_algebraMap] + using mul_lt_one_of_lt_of_le hπ.1 <| (q / π).valuation_le_one_of_valuation_X_le_one _ hle + +lemma exists_zpow_uniformizingPolynomial {f : RatFunc K} (hf : f ≠ 0) : + ∃ (z : ℤ), v f = v πᵥ ^ z:= by + have h0 : v πᵥ ≠ 0 := by simpa using uniformizingPolynomial_ne_zero hle + induction f using RatFunc.induction_on with + | f p q hq => + use (Associates.mk (Pᵥ).asIdeal).count (Associates.mk (Ideal.span {p})).factors - + (Associates.mk (Pᵥ).asIdeal).count (Associates.mk (Ideal.span {q})).factors + simp only [map_div₀, map_pow, zpow_sub₀ h0, zpow_natCast, + valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq, + valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle + (p := p) (by aesop)] + +set_option backward.isDefEq.respectTransparency false in +lemma uniformizingPolynomial_isUniformizer [hv : IsRankOneDiscrete v] : + v.IsUniformizer πᵥ := by + have h0 : v πᵥ ≠ 0 := by simpa using uniformizingPolynomial_ne_zero hle + rw [IsUniformizer, ← hv.valueGroup_genLTOne_eq_generator, ← h0.isUnit.unit_spec, Units.val_inj] + apply LinearOrderedCommGroup.Subgroup.genLTOne_unique + · rw [← Units.val_lt_val, h0.isUnit.unit_spec, Units.val_one] + exact valuation_uniformizingPolynomial_lt_one hle + · ext γ + simp only [coePolynomial_eq_algebraMap, MonoidWithZeroHom.mem_valueGroup_iff_of_comm, ne_eq, + map_eq_zero, Subgroup.mem_zpowers_iff] + refine ⟨fun ⟨k, hk⟩ ↦ ?_, fun ⟨a, ha, b, hab⟩ ↦ ?_⟩ + · use 1, one_ne_zero, πᵥ ^ k + simp only [← Units.val_inj, Units.val_zpow_eq_zpow_val, h0.isUnit.unit_spec] at hk + simp [← hk] + · obtain ⟨ka, hka⟩ := exists_zpow_uniformizingPolynomial hle ha + obtain ⟨kb, hkb⟩ := exists_zpow_uniformizingPolynomial hle (f := b) (by aesop) + rw [hka, hkb] at hab + use kb - ka + have : v ↑πᵥ ^ ka ≠ 0 := zpow_ne_zero _ h0 + simp only [zpow_sub, ← Units.val_inj, Units.val_mul, Units.val_zpow_eq_zpow_val, + h0.isUnit.unit_spec, Units.val_inv_eq_inv_val, ← hab, field] + +lemma valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one [IsRankOneDiscrete v] : + v.IsEquiv ((Pᵥ).valuation (RatFunc K)) := by + rw [isEquiv_iff_val_le_one] + intro f + rcases eq_or_ne f 0 with rfl | hf0 + · simp + · induction f using RatFunc.induction_on with + | f p q hq0 => + have hp0 : p ≠ 0 := by simp_all + set pi := πᵥ with hpi_def + have hpi : v.IsUniformizer (pi : RatFunc K) := uniformizingPolynomial_isUniformizer hle + simp only [map_div₀, valuation_of_algebraMap, intValuation_def, exp_neg, if_neg hp0, + if_neg hq0, div_inv_eq_mul] + rw [valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hp0, + valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq0] + simp_all [div_le_one₀, inv_mul_le_one₀, + (pow_le_pow_iff_right_of_lt_one₀ (by simp_all) (IsRankOneDiscrete.generator_lt_one v))] + +end Associates + +end valuation_X_le_one + +lemma adicValuation_not_isEquiv_infty_valuation [DecidableEq (RatFunc K)] + (p : IsDedekindDomain.HeightOneSpectrum K[X]) : + ¬ (p.valuation (RatFunc K)).IsEquiv (inftyValuation K) := by + simp only [isEquiv_iff_val_le_one] + push Not + refine ⟨X, .inl ⟨p.valuation_le_one _, ?_⟩⟩ + rw [inftyValuation.X, ← log_lt_iff_lt_exp one_ne_zero, log_one] + exact zero_lt_one + +lemma adicValuation_ne_inftyValuation [DecidableEq (RatFunc K)] + (p : IsDedekindDomain.HeightOneSpectrum K[X]) : + p.valuation (RatFunc K) ≠ inftyValuation K := by + by_contra h + exact absurd Valuation.IsEquiv.refl (h ▸ adicValuation_not_isEquiv_infty_valuation p) + +section Discrete + +variable [IsRankOneDiscrete v] + +section IsTrivialOn + +variable [v.IsTrivialOn K] + +lemma valuation_isEquiv_adic_of_valuation_X_le_one (hle : v X ≤ 1) : + ∃ (u : HeightOneSpectrum K[X]), v.IsEquiv (u.valuation _) := + ⟨_, valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one hle⟩ + +/-- **Ostrowski's Theorem** for `K(X)` with `K` any field: +A discrete valuation of rank 1 that is trivial on `K` is equivalent either to the valuation +at infinity or to the `p`-adic valuation for a unique maximal ideal `p` of `K[X]`. -/ +theorem valuation_isEquiv_infty_or_adic [DecidableEq (RatFunc K)] : + Xor' (v.IsEquiv (FunctionField.inftyValuation K)) + (∃! (u : HeightOneSpectrum K[X]), v.IsEquiv (u.valuation _)) := by + rcases lt_or_ge 1 (v X) with hlt | hge + /- Infinity case -/ + · have hv := valuation_isEquiv_inftyValuation_of_one_lt_valuation_X hlt + refine .inl ⟨hv, ?_⟩ + simp only [ExistsUnique, not_exists, not_and, not_forall] + intro pw hw + exact absurd (hw.symm.trans hv) (adicValuation_not_isEquiv_infty_valuation pw) + /- Prime case -/ + · obtain ⟨pw, hw⟩ := valuation_isEquiv_adic_of_valuation_X_le_one hge + exact .inr ⟨⟨pw, hw, fun pw' hw' ↦ eq_of_valuation_isEquiv_valuation (hw'.symm.trans hw)⟩, + fun hv ↦ absurd (hw.symm.trans hv) (adicValuation_not_isEquiv_infty_valuation pw)⟩ + +lemma valuation_isEquiv_adic_of_not_isEquiv_infty [DecidableEq (RatFunc K)] + (hni : ¬ v.IsEquiv (FunctionField.inftyValuation K)) : + ∃! (u : HeightOneSpectrum K[X]), v.IsEquiv (u.valuation _) := + valuation_isEquiv_infty_or_adic.or.resolve_left hni + +end IsTrivialOn + +end Discrete + +end RatFunc + +end diff --git a/docs/1000.yaml b/docs/1000.yaml index 1a4c3a297db446..88c13448812ca7 100644 --- a/docs/1000.yaml +++ b/docs/1000.yaml @@ -2266,8 +2266,10 @@ Q2916568: Q2919401: title: Ostrowski's theorem - decl: Rat.AbsoluteValue.equiv_real_or_padic - authors: David Kurniadi Angdinata, Fabrizio Barroero, Laura Capuano, Nirvana Coppola, María Inés de Frutos-Fernández, Sam van Gool, Silvain Rideau-Kikuchi, Amos Turchet, Francesco Veneziano + decls: + - Rat.AbsoluteValue.equiv_real_or_padic + - RatFunc.valuation_isEquiv_infty_or_adic + authors: David Kurniadi Angdinata, Fabrizio Barroero, Laura Capuano, Nirvana Coppola, María Inés de Frutos-Fernández, Sam van Gool, Silvain Rideau-Kikuchi, Amos Turchet, Francesco Veneziano, Xavier Généreux date: 2024 Q2981012: From 941639847c2a8d215d7504954da19d425cf7d90d Mon Sep 17 00:00:00 2001 From: euprunin <178733547+euprunin@users.noreply.github.com> Date: Wed, 18 Mar 2026 08:30:55 +0000 Subject: [PATCH 22/26] chore: replace `aesop` with `grind` where the latter is significantly faster (#35947) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This experiment investigates the impact of replacing particularly heavy `aesop` calls with `grind`, specifically how this change affects the instruction count as measured by the benchmarking infrastructure. Trace profiling results (differences <30 ms considered measurement noise): * `Submonoid.mem_closure_image_one_lt_iff`: 125 ms before, 61 ms after 🎉 * `SimpleGraph.Connected.connected_delete_edge_of_not_isBridge`: 230 ms before, 51 ms after 🎉 * `SimpleGraph.Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv`: 899 ms before, 666 ms after 🎉 * `SimpleGraph.IsCycles.existsUnique_ne_adj`: 855 ms before, 599 ms after 🎉 * `SimpleGraph.Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge`: 962 ms before, 619 ms after 🎉 * `SimpleGraph.IsAlternating.sup_edge`: 2854 ms before, 1615 ms after 🎉 * `SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_of_isAlternating`: 3103 ms before, 1734 ms after 🎉 * `SimpleGraph.edgeSet_replaceVertex_of_not_adj`: 1525 ms before, 933 ms after 🎉 * `SimpleGraph.edgeSet_replaceVertex_of_adj`: 2194 ms before, 1605 ms after 🎉 * `SimpleGraph.tutte_exists_isPerfectMatching_of_near_matchings`: 3161 ms before, 1652 ms after 🎉 * `RootPairing.Base.sub_notMem_range_root`: 1025 ms before, 978 ms after 🎉 * `RootPairing.EmbeddedG2.mem_allRoots`: 3832 ms before, 3255 ms after 🎉 * `RootSystem.GeckConstruction.Lemmas.0.RootPairing.chainBotCoeff_mul_chainTopCoeff.aux_2`: 3572 ms before, 2631 ms after 🎉 * `isCompact_generateFrom`: 1987 ms before, 763 ms after 🎉 * `IsCompactOpenCovered.of_isCompact_of_forall_exists_isCompactOpenCovered`: 2279 ms before, 2009 ms after 🎉 * `UniformContinuousOn.comp_tendstoUniformly_eventually`: 416 ms before, 151 ms after 🎉 Profiled using `set_option trace.profiler true in`. --- .../Group/Irreducible/Indecomposable.lean | 2 +- .../SimpleGraph/Connectivity/Connected.lean | 4 ++-- Mathlib/Combinatorics/SimpleGraph/Matching.lean | 16 ++++++++-------- .../Combinatorics/SimpleGraph/Operations.lean | 4 ++-- Mathlib/Combinatorics/SimpleGraph/Tutte.lean | 4 ++-- Mathlib/LinearAlgebra/RootSystem/Base.lean | 2 +- Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean | 2 +- .../RootSystem/GeckConstruction/Lemmas.lean | 10 +++++----- Mathlib/Topology/Compactness/Compact.lean | 2 +- Mathlib/Topology/Sets/CompactOpenCovered.lean | 2 +- .../UniformSpace/UniformConvergenceTopology.lean | 6 +++--- 11 files changed, 27 insertions(+), 27 deletions(-) diff --git a/Mathlib/Algebra/Group/Irreducible/Indecomposable.lean b/Mathlib/Algebra/Group/Irreducible/Indecomposable.lean index 674dff3d487665..ef97f0b2b4d67a 100644 --- a/Mathlib/Algebra/Group/Irreducible/Indecomposable.lean +++ b/Mathlib/Algebra/Group/Irreducible/Indecomposable.lean @@ -199,7 +199,7 @@ lemma Submonoid.mem_closure_image_one_lt_iff [CommMonoid S] [IsOrderedCancelMono v i ∈ closure (v '' {i | 1 < f (v i)}) ↔ 1 < f (v i) := by refine ⟨fun hi ↦ ?_, fun hi ↦ subset_closure <| mem_image_of_mem v hi⟩ suffices v i = 1 ∨ 1 < f (v i) from this.resolve_left hv_one - refine closure_induction (by aesop) (by simp) (fun x y _ _ hx hy ↦ ?_) hi + refine closure_induction (by grind) (by simp) (fun x y _ _ hx hy ↦ ?_) hi rcases hx with rfl | hx; · simpa rcases hy with rfl | hy; · right; simpa right diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean index 5bc4c5725297ce..76c05ed98287e1 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean @@ -830,12 +830,12 @@ lemma Connected.connected_delete_edge_of_not_isBridge (hG : G.Connected) {x y : refine (connected_iff_exists_forall_reachable _).2 ⟨x, fun w ↦ ?_⟩ obtain ⟨P, hP⟩ := hG.exists_isPath w x obtain heP | heP := em' <| s(x, y) ∈ P.edges - · exact ⟨(P.toDeleteEdges {s(x, y)} (by aesop)).reverse⟩ + · exact ⟨(P.toDeleteEdges {s(x, y)} (by grind)).reverse⟩ have hyP := P.snd_mem_support_of_mem_edges heP let P₁ := P.takeUntil y hyP have hxP₁ := Walk.endpoint_notMem_support_takeUntil hP hyP hxy.ne have heP₁ : s(x, y) ∉ P₁.edges := fun h ↦ hxP₁ <| P₁.fst_mem_support_of_mem_edges h - exact (h hxy).trans (Reachable.symm ⟨P₁.toDeleteEdges {s(x, y)} (by aesop)⟩) + exact (h hxy).trans (Reachable.symm ⟨P₁.toDeleteEdges {s(x, y)} (by grind)⟩) /-- If `e` is an edge in `G` and is a bridge in a larger graph `G'`, then it's a bridge in `G`. -/ theorem IsBridge.anti_of_mem_edgeSet {G' : SimpleGraph V} {e : Sym2 V} (hle : G ≤ G') diff --git a/Mathlib/Combinatorics/SimpleGraph/Matching.lean b/Mathlib/Combinatorics/SimpleGraph/Matching.lean index b91bc49150dcd4..82017418d947c0 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Matching.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Matching.lean @@ -172,7 +172,7 @@ lemma IsMatching.exists_of_disjoint_sets_of_equiv {s t : Set V} (h : Disjoint s obtain (⟨hv, rfl⟩ | ⟨hw, rfl⟩) := h · exact hadj ⟨v, _⟩ · exact (hadj ⟨w, _⟩).symm - edge_vert := by aesop } + edge_vert := by grind } simp only [Subgraph.IsMatching, Set.mem_union, true_and] intro v hv rcases hv with hl | hr @@ -368,7 +368,7 @@ lemma IsCycles.existsUnique_ne_adj (h : G.IsCycles) (hadj : G.Adj v w) : intro y ⟨hwy, hwy'⟩ obtain ⟨x, y', hxy'⟩ := Set.ncard_eq_two.mp (h ⟨w, hadj⟩) simp_rw [← SimpleGraph.mem_neighborSet] at * - aesop + grind lemma IsCycles.toSimpleGraph (c : G.ConnectedComponent) (h : G.IsCycles) : c.toSimpleGraph.spanningCoe.IsCycles := by @@ -394,7 +394,7 @@ lemma Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge {u v} {p : G.Walk u v ext w x simp only [sup_adj, Subgraph.spanningCoe_adj, completeGraph_eq_top, edge_adj, c, Walk.toSubgraph, Subgraph.sup_adj, subgraphOfAdj_adj, adj_toSubgraph_mapLe] - aesop + grind exact this ▸ IsCycle.isCycles_spanningCoe_toSubgraph (by simp [Walk.cons_isCycle_iff, c, hp, hs]) lemma Walk.IsCycle.adj_toSubgraph_iff_of_isCycles [LocallyFinite G] {u} {p : G.Walk u u} @@ -562,19 +562,19 @@ lemma IsAlternating.sup_edge {u x : V} (halt : G.IsAlternating G') (hnadj : ¬G' simp only [sup_adj, edge_adj] at hvw hvv' obtain hl | hr := hvw <;> obtain h1 | h2 := hvv' · exact halt hww' hl h1 - · rw [G'.adj_congr_of_sym2 (by aesop : s(v, w') = s(u, x))] + · rw [G'.adj_congr_of_sym2 (by grind : s(v, w') = s(u, x))] simp only [hnadj, not_false_eq_true, iff_true] rcases h2.1 with ⟨h2l1, h2l2⟩ | ⟨h2r1, h2r2⟩ · subst h2l1 h2l2 exact (hx' _ hww' hl.symm).symm · simp_all - · rw [G'.adj_congr_of_sym2 (by aesop : s(v, w) = s(u, x))] + · rw [G'.adj_congr_of_sym2 (by grind : s(v, w) = s(u, x))] simp only [hnadj, false_iff, not_not] rcases hr.1 with ⟨hrl1, hrl2⟩ | ⟨hrr1, hrr2⟩ · subst hrl1 hrl2 exact (hx' _ hww'.symm h1.symm).symm - · aesop - · aesop + · grind + · grind set_option backward.isDefEq.respectTransparency false in lemma Subgraph.IsPerfectMatching.symmDiff_of_isAlternating (hM : M.IsPerfectMatching) @@ -591,7 +591,7 @@ lemma Subgraph.IsPerfectMatching.symmDiff_of_isAlternating (hM : M.IsPerfectMatc simp only [Subgraph.top_adj, SimpleGraph.sup_adj, sdiff_adj, Subgraph.spanningCoe_adj, hmadj.mp hw.1, hw'.2, not_true_eq_false, and_self, not_false_eq_true, or_true, true_and] rintro y (hl | hr) - · aesop + · grind · obtain ⟨w'', hw''⟩ := hG'cyc.other_adj_of_adj hr.1 by_contra! hc simp_all [show M.Adj v y ↔ ¬M.Adj v w' from by simpa using hG' hc hr.1 hw'.2] diff --git a/Mathlib/Combinatorics/SimpleGraph/Operations.lean b/Mathlib/Combinatorics/SimpleGraph/Operations.lean index e109a411cefabc..fc72b7a761745f 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Operations.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Operations.lean @@ -72,13 +72,13 @@ theorem edgeSet_replaceVertex_of_not_adj (hn : ¬G.Adj s t) : (G.replaceVertex s G.edgeSet \ G.incidenceSet t ∪ (s(·, t)) '' (G.neighborSet s) := by ext e; refine e.inductionOn ?_ simp only [replaceVertex, mem_edgeSet, Set.mem_union, Set.mem_diff, mk'_mem_incidenceSet_iff] - intros; split_ifs; exacts [by simp_all, by aesop, by rw [adj_comm]; aesop, by aesop] + intros; split_ifs; exacts [by simp_all, by aesop, by rw [adj_comm]; aesop, by grind] theorem edgeSet_replaceVertex_of_adj (ha : G.Adj s t) : (G.replaceVertex s t).edgeSet = (G.edgeSet \ G.incidenceSet t ∪ (s(·, t)) '' (G.neighborSet s)) \ {s(t, t)} := by ext e; refine e.inductionOn ?_ simp only [replaceVertex, mem_edgeSet, Set.mem_union, Set.mem_diff, mk'_mem_incidenceSet_iff] - intros; split_ifs; exacts [by simp_all, by aesop, by rw [adj_comm]; aesop, by aesop] + intros; split_ifs; exacts [by simp_all, by aesop, by rw [adj_comm]; aesop, by grind] variable [Fintype V] [DecidableRel G.Adj] diff --git a/Mathlib/Combinatorics/SimpleGraph/Tutte.lean b/Mathlib/Combinatorics/SimpleGraph/Tutte.lean index 4d45d65d9c1e6c..e3237438877822 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Tutte.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Tutte.lean @@ -169,7 +169,7 @@ private theorem tutte_exists_isPerfectMatching_of_near_matchings {x a b c : V} -- Neither matching contains the edge that would make the other matching of G perfect have hM1nac : ¬M1.Adj a c := fun h ↦ by simpa [hnGac, edge_adj, hnac, hxa.ne, hnbc.symm, hab.ne] using h.adj_sub - have hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = (G ⊔ edge a c) ⊔ edge x b := by aesop + have hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = (G ⊔ edge a c) ⊔ edge x b := by grind -- We state conditions for our cycle that hold in all cases and show that this suffices suffices ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c by @@ -228,7 +228,7 @@ private theorem tutte_exists_isPerfectMatching_of_near_matchings {x a b c : V} have : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd := by apply Walk.toSubgraph_adj_snd rw [Walk.nil_takeUntil] - aesop + grind rwa [Walk.snd_takeUntil, hp'.2.1] at this simp only [Finset.mem_insert, Finset.mem_singleton] at hx' obtain rfl | rfl := hx' diff --git a/Mathlib/LinearAlgebra/RootSystem/Base.lean b/Mathlib/LinearAlgebra/RootSystem/Base.lean index 2dd04b73c5cc3b..3421deb5ef6f56 100644 --- a/Mathlib/LinearAlgebra/RootSystem/Base.lean +++ b/Mathlib/LinearAlgebra/RootSystem/Base.lean @@ -258,7 +258,7 @@ lemma sub_notMem_range_root have hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j := by have : {i, j} ⊆ b.support := by aesop (add simp Finset.insert_subset_iff) rw [← Finset.sum_subset (s₁ := {i, j}) (s₂ := b.support) (by lia) (by aesop), - Finset.sum_insert (by aesop), Finset.sum_singleton] + Finset.sum_insert (by grind), Finset.sum_singleton] simp [f, hij, sub_eq_add_neg] intro contra rcases b.pos_or_neg_of_sum_smul_root_mem f (by rwa [hf]) (by aesop) with pos | neg diff --git a/Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean b/Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean index 8c68dcaf3cadae..96d7e6637691ca 100644 --- a/Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean +++ b/Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean @@ -560,7 +560,7 @@ lemma mem_allRoots (i : ι) : simp only [LinearMap.zero_apply] induction hx using Submodule.span_induction with | zero => simp - | mem => aesop + | mem => grind | add => simp_all | smul => simp_all simpa using LinearMap.congr_fun key (P.root i) diff --git a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean index a3a76acb6c8e01..33513d59325d6c 100644 --- a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean +++ b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean @@ -236,7 +236,7 @@ private lemma chainBotCoeff_mul_chainTopCoeff.aux_1 have key₁ : P.pairingIn ℤ i k = 0 := by rwa [pairingIn_eq_zero_iff] have key₂ : P.pairingIn ℤ i m = 0 := P.pairingIn_eq_zero_iff.mp <| by simpa [aux₁] using aux₀ have key₃ : P.pairingIn ℤ j k = 2 := by - suffices 2 ≤ P.pairingIn ℤ j k by have := IsNotG2.pairingIn_mem_zero_one_two (P := P) j k; aesop + suffices 2 ≤ P.pairingIn ℤ j k by have := IsNotG2.pairingIn_mem_zero_one_two (P := P) j k; grind have hn₁ : P.pairingIn ℤ n k = 2 + P.pairingIn ℤ i k - P.pairingIn ℤ j k := by apply algebraMap_injective ℤ R simp only [map_add, map_sub, algebraMap_pairingIn, ← root_coroot_eq_pairing, hn] @@ -249,7 +249,7 @@ private lemma chainBotCoeff_mul_chainTopCoeff.aux_1 rw [pairing_eq_zero_iff, ← P.algebraMap_pairingIn ℤ, aux₁, map_zero] have hkj : P.pairing k j = 1 := by rw [← P.algebraMap_pairingIn ℤ] - have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' j k (by aesop) (by aesop) + have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' j k (by grind) (by grind) aesop apply algebraMap_injective ℤ R rw [algebraMap_pairingIn, ← root_coroot_eq_pairing, ← h₁] @@ -305,14 +305,14 @@ private lemma chainBotCoeff_mul_chainTopCoeff.aux_2 algebraMap_injective ℤ R <| by simpa only [algebraMap_pairingIn, map_add] simp [← P.root_coroot_eq_pairing l, ← h₁, add_comm] · have := IsNotG2.pairingIn_mem_zero_one_two (P := P) k j - aesop + grind /- Choose a positive invariant form. -/ obtain B : RootPositiveForm ℤ P := have : Fintype ι := Fintype.ofFinite ι; P.posRootForm ℤ /- Calculate root length relationships implied by the pairings calculated above. -/ have ⟨aux₃, aux₄⟩ : B.rootLength i = B.rootLength j ∧ B.rootLength j < B.rootLength k := by have hij_le : B.rootLength i ≤ B.rootLength j := B.rootLength_le_of_pairingIn_eq <| Or.inl aux₁ have hjk_lt : B.rootLength j < B.rootLength k := - B.rootLength_lt_of_pairingIn_notMem (by aesop) hkj_ne.2 <| by aesop + B.rootLength_lt_of_pairingIn_notMem (by grind) hkj_ne.2 <| by grind refine ⟨?_, hjk_lt⟩ simpa [posForm, rootLength] using (B.toInvariantForm.apply_eq_or_of_apply_ne (i := j) (j := k) (by simpa [posForm, rootLength] using hjk_lt.ne) i).resolve_right @@ -323,7 +323,7 @@ private lemma chainBotCoeff_mul_chainTopCoeff.aux_2 have aux : B.toInvariantForm.form (P.root i) (P.root i) = B.toInvariantForm.form (P.root j) (P.root j) := by simpa [posForm, rootLength] using aux₃ have := P.pairingIn_pairingIn_mem_set_of_length_eq_of_ne aux hij (b.root_ne_neg_of_ne hi hj hij) - aesop + grind /- Use the newly calculated pairing result to obtain further information about root lengths. -/ have aux₆ : B.rootLength k ≤ B.rootLength i := B.rootLength_le_of_pairingIn_eq <| Or.inl aux₅ /- We now have contradictory information about root lengths. -/ diff --git a/Mathlib/Topology/Compactness/Compact.lean b/Mathlib/Topology/Compactness/Compact.lean index 56b38d9d613411..2a3b92c151dbed 100644 --- a/Mathlib/Topology/Compactness/Compact.lean +++ b/Mathlib/Topology/Compactness/Compact.lean @@ -539,7 +539,7 @@ theorem isCompact_generateFrom [T : TopologicalSpace X] have hSF : ∀ x ∈ s, ∃ t, x ∈ t ∧ t ∈ S ∧ t ∉ F := by simpa [nhds_generateFrom] using hF choose! U hxU hSU hUF using hSF obtain ⟨Q, hQU, hQ, hsQ⟩ := h (U '' s) (by simpa [Set.subset_def]) - (fun x hx ↦ Set.mem_sUnion_of_mem (hxU _ hx) (by aesop)) + (fun x hx ↦ Set.mem_sUnion_of_mem (hxU _ hx) (by grind)) have : ∀ s ∈ Q, s ∉ F := fun s hsQ ↦ (hQU hsQ).choose_spec.2 ▸ hUF _ (hQU hsQ).choose_spec.1 have hQF : ⋂₀ (compl '' Q) ∈ F.sets := by simpa [Filter.biInter_mem hQ, F.compl_mem_iff_notMem] have : ⋃₀ Q ∉ F := by diff --git a/Mathlib/Topology/Sets/CompactOpenCovered.lean b/Mathlib/Topology/Sets/CompactOpenCovered.lean index f91e918c54fe46..047f37915ffcfc 100644 --- a/Mathlib/Topology/Sets/CompactOpenCovered.lean +++ b/Mathlib/Topology/Sets/CompactOpenCovered.lean @@ -111,7 +111,7 @@ lemma of_isCompact_of_forall_exists_isCompactOpenCovered [TopologicalSpace S] {U refine of_biUnion_eq_of_isCompact hU { Us x h | (x : S) (h : x ∈ U) } ?_ ?_ · refine subset_antisymm (fun x ↦ ?_) fun x hx ↦ ?_ · simp [Opens.forall] - aesop + grind · simpa using ⟨⟨Us x hx, hUo _ _⟩, ⟨x, by simpa⟩, hUx _ _⟩ · grind diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean index cfc0576c0ffc83..59c35a54a8d7ea 100644 --- a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean +++ b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean @@ -1187,13 +1187,13 @@ theorem UniformContinuousOn.comp_tendstoUniformly_eventually let F' : ι → α → β := fun i x => if i ∈ s' then F i x else f x have hF : F =ᶠ[p] F' := by rw [eventuallyEq_iff_exists_mem] - refine ⟨s', hs', fun y hy => by aesop⟩ + refine ⟨s', hs', fun y hy => by grind⟩ have h' : TendstoUniformly F' f p := by rwa [tendstoUniformly_congr hF] at h apply (tendstoUniformly_congr _).mpr - (UniformContinuousOn.comp_tendstoUniformly (by aesop) hf hg h') + (UniformContinuousOn.comp_tendstoUniformly (by grind) hf hg h') rw [eventuallyEq_iff_exists_mem] - refine ⟨s', hs', fun i hi => by aesop⟩ + refine ⟨s', hs', fun i hi => by grind⟩ theorem UniformContinuousOn.comp_tendstoUniformlyOn_eventually {t : Set α} (hF : ∀ᶠ i in p, ∀ x ∈ t, F i x ∈ s) (hf : ∀ x ∈ t, f x ∈ s) From 78dd61f6dbcb137b2226d793d7bc6d5d3592f811 Mon Sep 17 00:00:00 2001 From: Harald Husum Date: Wed, 18 Mar 2026 09:00:56 +0000 Subject: [PATCH 23/26] doc(AlgebraicTopology/DoldKan): fix typos (#36765) Issues were spotted and fixed by Codex. --- .../DoldKan/Compatibility.lean | 20 +++++++++---------- .../DoldKan/Equivalence.lean | 2 +- .../DoldKan/EquivalencePseudoabelian.lean | 2 +- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean b/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean index a3ea4b2df5ba83..25181e78eaac1b 100644 --- a/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean +++ b/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean @@ -13,17 +13,17 @@ The purpose of this file is to introduce tools which will enable the construction of the Dold-Kan equivalence `SimplicialObject C ≌ ChainComplex C ℕ` for a pseudoabelian category `C` from the equivalence `Karoubi (SimplicialObject C) ≌ Karoubi (ChainComplex C ℕ)` and the two -equivalences `simplicial_object C ≅ Karoubi (SimplicialObject C)` and -`ChainComplex C ℕ ≅ Karoubi (ChainComplex C ℕ)`. +equivalences `SimplicialObject C ≌ Karoubi (SimplicialObject C)` and +`ChainComplex C ℕ ≌ Karoubi (ChainComplex C ℕ)`. It is certainly possible to get an equivalence `SimplicialObject C ≌ ChainComplex C ℕ` using a composition of the three equivalences above, but then neither the functor nor the inverse would have good definitional properties. For example, it would be better if the inverse functor of the equivalence was exactly the functor -`Γ₀ : SimplicialObject C ⥤ ChainComplex C ℕ` which was constructed in `FunctorGamma.lean`. +`Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C` which was constructed in `FunctorGamma.lean`. -In this file, given four categories `A`, `A'`, `B`, `B'`, equivalences `eA : A ≅ A'`, -`eB : B ≅ B'`, `e' : A' ≅ B'`, functors `F : A ⥤ B'`, `G : B ⥤ A` equipped with certain +In this file, given four categories `A`, `A'`, `B`, `B'`, equivalences `eA : A ≌ A'`, +`eB : B ≌ B'`, `e' : A' ≌ B'`, functors `F : A ⥤ B'`, `G : B ⥤ A` equipped with certain compatibilities, we construct successive equivalences: - `equivalence₀` from `A` to `B'`, which is the composition of `eA` and `e'`. - `equivalence₁` from `A` to `B'`, with the same inverse functor as `equivalence₀`, @@ -55,14 +55,14 @@ variable {A A' B B' : Type*} [Category* A] [Category* A'] [Category* B] [Categor (eB : B ≌ B') (e' : A' ≌ B') {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) {G : B ⥤ A} (hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor) -/-- A basic equivalence `A ≅ B'` obtained by composing `eA : A ≅ A'` and `e' : A' ≅ B'`. -/ +/-- A basic equivalence `A ≌ B'` obtained by composing `eA : A ≌ A'` and `e' : A' ≌ B'`. -/ @[simps! functor inverse unitIso_hom_app] def equivalence₀ : A ≌ B' := eA.trans e' variable {eA} {e'} -/-- An intermediate equivalence `A ≅ B'` whose functor is `F` and whose inverse is +/-- An intermediate equivalence `A ≌ B'` whose functor is `F` and whose inverse is `e'.inverse ⋙ eA.inverse`. -/ @[simps! functor] def equivalence₁ : A ≌ B' := (equivalence₀ eA e').changeFunctor hF @@ -104,7 +104,7 @@ theorem equivalence₁UnitIso_eq : (equivalence₁ hF).unitIso = equivalence₁U ext X simp [equivalence₁] -/-- An intermediate equivalence `A ≅ B` obtained as the composition of `equivalence₁` and +/-- An intermediate equivalence `A ≌ B` obtained as the composition of `equivalence₁` and the inverse of `eB : B ≌ B'`. -/ @[simps! functor] def equivalence₂ : A ≌ B := @@ -155,8 +155,8 @@ theorem equivalence₂UnitIso_eq : (equivalence₂ eB hF).unitIso = equivalence variable {eB} -/-- The equivalence `A ≅ B` whose functor is `F ⋙ eB.inverse` and -whose inverse is `G : B ≅ A`. -/ +/-- The equivalence `A ≌ B` whose functor is `F ⋙ eB.inverse` and +whose inverse functor is `G : B ⥤ A`. -/ @[simps! inverse] def equivalence : A ≌ B := ((equivalence₂ eB hF).changeInverse diff --git a/Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean b/Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean index 99c18780fb26e3..97716a6dda8fd9 100644 --- a/Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean +++ b/Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean @@ -91,7 +91,7 @@ obtained by composing the previous equivalence with the equivalences `Karoubi (ChainComplex C ℕ) ≌ ChainComplex C ℕ`. Instead, we polish this construction in `Compatibility.lean` by ensuring good definitional properties of the equivalence (e.g. the inverse functor is definitionally equal to -`Γ₀' : ChainComplex C ℕ ⥤ SimplicialObject C`) and +`Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C`, which is induced by `Γ₀'`) and showing compatibilities for the unit and counit isomorphisms. In this file `Equivalence.lean`, assuming the category `A` is abelian, we obtain diff --git a/Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean b/Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean index 15a0be4973b860..783057f7abc920 100644 --- a/Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean +++ b/Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean @@ -60,7 +60,7 @@ of the equivalence `ChainComplex C ℕ ≌ Karoubi (ChainComplex C ℕ)`. -/ def N [IsIdempotentComplete C] [HasFiniteCoproducts C] : SimplicialObject C ⥤ ChainComplex C ℕ := N₁ ⋙ (toKaroubiEquivalence _).inverse -/-- The functor `Γ` for the equivalence is `Γ'`. -/ +/-- The functor `Γ` for the equivalence is `Γ₀`. -/ @[simps!, nolint unusedArguments] def Γ [IsIdempotentComplete C] [HasFiniteCoproducts C] : ChainComplex C ℕ ⥤ SimplicialObject C := Γ₀ From bfb1623d82dd5fa283dca04796ad14bcf7b6f1de Mon Sep 17 00:00:00 2001 From: Etienne Marion <66847262+EtienneC30@users.noreply.github.com> Date: Wed, 18 Mar 2026 09:21:07 +0000 Subject: [PATCH 24/26] feat: processes with independent increments (#36718) Define a predicate stating that a stochastic process has independent increments. Prove an equivalent definition using sequences instead of `Fin`. Prove some basic invariance properties. Co-authored-by: @jvanwinden --- Mathlib.lean | 3 +- .../IsGaussianProcess/Independence.lean | 2 +- .../BoundedContinuousFunction.lean | 2 +- .../{Process.lean => Process/Basic.lean} | 0 .../Process/HasIndepIncrements.lean | 132 ++++++++++++++++++ 5 files changed, 136 insertions(+), 3 deletions(-) rename Mathlib/Probability/Independence/{Process.lean => Process/Basic.lean} (100%) create mode 100644 Mathlib/Probability/Independence/Process/HasIndepIncrements.lean diff --git a/Mathlib.lean b/Mathlib.lean index dd8378ddde6791..a3afd8e9c52620 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5998,7 +5998,8 @@ public import Mathlib.Probability.Independence.Integration public import Mathlib.Probability.Independence.Kernel public import Mathlib.Probability.Independence.Kernel.Indep public import Mathlib.Probability.Independence.Kernel.IndepFun -public import Mathlib.Probability.Independence.Process +public import Mathlib.Probability.Independence.Process.Basic +public import Mathlib.Probability.Independence.Process.HasIndepIncrements public import Mathlib.Probability.Independence.ZeroOne public import Mathlib.Probability.Kernel.Basic public import Mathlib.Probability.Kernel.CompProdEqIff diff --git a/Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Independence.lean b/Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Independence.lean index fe0a12387a8f16..b790e91ebfad67 100644 --- a/Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Independence.lean +++ b/Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Independence.lean @@ -10,7 +10,7 @@ public import Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def import Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic import Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence import Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic -import Mathlib.Probability.Independence.Process +import Mathlib.Probability.Independence.Process.Basic /-! # Independence of Gaussian processes diff --git a/Mathlib/Probability/Independence/BoundedContinuousFunction.lean b/Mathlib/Probability/Independence/BoundedContinuousFunction.lean index 2726dfa2bbb8c8..ee5a8244a1c172 100644 --- a/Mathlib/Probability/Independence/BoundedContinuousFunction.lean +++ b/Mathlib/Probability/Independence/BoundedContinuousFunction.lean @@ -6,7 +6,7 @@ Authors: Etienne Marion module public import Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd -public import Mathlib.Probability.Independence.Process +public import Mathlib.Probability.Independence.Process.Basic public import Mathlib.Probability.Notation /-! diff --git a/Mathlib/Probability/Independence/Process.lean b/Mathlib/Probability/Independence/Process/Basic.lean similarity index 100% rename from Mathlib/Probability/Independence/Process.lean rename to Mathlib/Probability/Independence/Process/Basic.lean diff --git a/Mathlib/Probability/Independence/Process/HasIndepIncrements.lean b/Mathlib/Probability/Independence/Process/HasIndepIncrements.lean new file mode 100644 index 00000000000000..b62be7fb5b6801 --- /dev/null +++ b/Mathlib/Probability/Independence/Process/HasIndepIncrements.lean @@ -0,0 +1,132 @@ +/- +Copyright (c) 2025 Etienne Marion. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Etienne Marion, Joris van Winden +-/ +module + +public import Mathlib.Probability.Independence.Basic + +import Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap + +/-! +# Stochastic processes with independent increments + +A stochastic process `X : T → Ω → E` has independent increments if for any `n ≥ 1` and +`t₁ ≤ ... ≤ tₙ`, the random variables `X t₂ - X t₁, ..., X tₙ - X tₙ₋₁` are independent. +Equivalently, for any monotone sequence `(tₙ)`, the random variables `(X tₙ₊₁ - X tₙ)` +are independent. + +## Main definition + +* `HasIndepIncrements`: A stochastic process `X : T → Ω → E` has independent increments if for any + `n ≥ 1` and `t₁ ≤ ... ≤ tₙ`, the random variables `X t₂ - X t₁, ..., X tₙ - X tₙ₋₁` are + independent. + +## Main statement + +* `hasIndepIncrements_iff_nat`: A stochastic process `X : T → Ω → E` has independent increments if + and only if for any monotone sequence `(tₙ)`, the random variables `(X tₙ₊₁ - X tₙ)` are + independent. + +## Tags + +independent increments +-/ + +@[expose] public section + +open MeasureTheory Filter + +namespace ProbabilityTheory + +variable {T Ω E : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : T → Ω → E} + [Preorder T] [MeasurableSpace E] + +section Def + +variable [Sub E] + +/-- A stochastic process `X : T → Ω → E` has independent increments if for any `n ≥ 1` and +`t₁ ≤ ... ≤ tₙ`, the random variables `X t₂ - X t₁, ..., X tₙ - X tₙ₋₁` are independent. + +Although this corresponds to the standard definition, dealing with `Fin` might make things +complicated in some cases. Therefore we provide `HasIndepIncrements.of_nat` which instead requires +to prove that for any monotone sequence `(tₙ)` that is eventually constant, +the random variables `X tₙ₊₁ - X tₙ` are independent. -/ +def HasIndepIncrements (X : T → Ω → E) (P : Measure Ω := by volume_tac) : Prop := + ∀ n, ∀ t : Fin (n + 1) → T, Monotone t → + iIndepFun (fun (i : Fin n) ω ↦ X (t i.succ) ω - X (t i.castSucc) ω) P + +protected lemma HasIndepIncrements.nat + (hX : HasIndepIncrements X P) {t : ℕ → T} (ht : Monotone t) : + iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P := by + refine iIndepFun_iff_finset.2 fun s ↦ ?_ + obtain rfl | hs := s.eq_empty_or_nonempty + · have := (hX 0 (fun _ ↦ t 0) (fun _ ↦ by grind)).isProbabilityMeasure + exact iIndepFun.of_subsingleton + · let g (x : s) : Fin (s.max' hs + 1) := ⟨x.1, Nat.lt_add_one_of_le (s.le_max' x.1 x.2)⟩ + refine iIndepFun.precomp (g := g) ?_ (hX (s.max' hs + 1) (fun m ↦ t m) ?_) + · simp [g, Function.Injective] + · exact ht.comp Fin.val_strictMono.monotone + +protected lemma HasIndepIncrements.of_nat + (h : ∀ t : ℕ → T, Monotone t → EventuallyConst t atTop → + iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P) : + HasIndepIncrements X P := by + intro n t ht + let t' k := t ⟨min n k, by grind⟩ + convert (h t' ?_ ?_).precomp Fin.val_injective with i ω + · grind + · grind + · exact fun a b hab ↦ ht (by grind) + · exact eventuallyConst_atTop.2 ⟨n, by grind⟩ + +lemma hasIndepIncrements_iff_nat : + HasIndepIncrements X P ↔ + ∀ t : ℕ → T, Monotone t → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P where + mp h _ ht := h.nat ht + mpr h := .of_nat (fun t ht _ ↦ h t ht) + +end Def + +lemma HasIndepIncrements.indepFun_sub_sub [Sub E] (hX : HasIndepIncrements X P) {r s t : T} + (hrs : r ≤ s) (hst : s ≤ t) : + (X s - X r) ⟂ᵢ[P] (X t - X s) := by + let τ : ℕ → T + | 0 => r + | 1 => s + | _ => t + exact hX.nat (t := τ) (fun _ ↦ by grind) |>.indepFun (by grind : 0 ≠ 1) + +lemma HasIndepIncrements.indepFun_eval_sub [SubNegZeroMonoid E] (hX : HasIndepIncrements X P) + {r s t : T} (hrs : r ≤ s) (hst : s ≤ t) (h : ∀ᵐ ω ∂P, X r ω = 0) : + (X s) ⟂ᵢ[P] (X t - X s) := by + refine (hX.indepFun_sub_sub hrs hst).congr ?_ .rfl + filter_upwards [h] with ω hω using by simp [hω] + +protected lemma HasIndepIncrements.map' {F G : Type*} [MeasurableSpace G] [FunLike F E G] + [AddGroup E] [SubtractionMonoid G] [AddMonoidHomClass F E G] {f : F} (hf : Measurable f) + (hX : HasIndepIncrements X P) : + HasIndepIncrements (fun t ω ↦ f (X t ω)) P := by + intro n t ht + simp_rw [← map_sub] + exact (hX n t ht).comp (fun _ ↦ f) (fun _ ↦ hf) + +protected lemma HasIndepIncrements.map {R F : Type*} [Semiring R] [SeminormedAddCommGroup E] + [Module R E] [OpensMeasurableSpace E] [SeminormedAddCommGroup F] [Module R F] + [MeasurableSpace F] [BorelSpace F] (L : E →L[R] F) (hX : HasIndepIncrements X P) : + HasIndepIncrements (fun t ω ↦ L (X t ω)) P := + hX.map' L.measurable + +protected lemma HasIndepIncrements.smul {R : Type*} [AddGroup E] [DistribSMul R E] + [MeasurableConstSMul R E] (hX : HasIndepIncrements X P) (c : R) : + HasIndepIncrements (fun t ω ↦ c • (X t ω)) P := + hX.map' (f := DistribSMul.toAddMonoidHom E c) (MeasurableConstSMul.measurable_const_smul c) + +protected lemma HasIndepIncrements.neg [AddCommGroup E] [MeasurableNeg E] + (hX : HasIndepIncrements X P) : + HasIndepIncrements (-X) P := + hX.map' (f := negAddMonoidHom) measurable_neg + +end ProbabilityTheory From 223dcbd3fe023d784e56df7913c650278dff534d Mon Sep 17 00:00:00 2001 From: Louis Liu Date: Wed, 18 Mar 2026 09:33:20 +0000 Subject: [PATCH 25/26] feat(MeasureTheory): add `continuousWithinAt_Ici/Iic_primitive_Ioi/Iio` and `continuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic` (#34966) This PR proves: - `continuousWithinAt_Ici/Iic_primitive_Ioi/Iio` - `continuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic` - `integral_Ioi_sub_Ioi`, `integral_Ioi_sub_Ioi'`, `integral_Iio_sub_Iio`, `integral_Iio_sub_Iio'` - `Ioi_diff_Ioc` Co-authored-by: Deep0Thinking --- .../MeasureTheory/Integral/Bochner/Set.lean | 3 + .../Integral/DominatedConvergence.lean | 97 ++++++++++++++++++- .../Integral/IntervalIntegral/Basic.lean | 24 +++++ Mathlib/Order/Interval/Set/LinearOrder.lean | 4 + 4 files changed, 125 insertions(+), 3 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/Bochner/Set.lean b/Mathlib/MeasureTheory/Integral/Bochner/Set.lean index f943dd8505c383..4f08bfaed1ac42 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner/Set.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner/Set.lean @@ -693,6 +693,9 @@ theorem integral_Ioc_eq_integral_Ioo : ∫ t in Ioc x y, f t ∂μ = ∫ t in Io theorem integral_Ico_eq_integral_Ioo : ∫ t in Ico x y, f t ∂μ = ∫ t in Ioo x y, f t ∂μ := integral_Ico_eq_integral_Ioo' <| measure_singleton x +theorem integral_Ico_eq_integral_Ioc : ∫ t in Ico x y, f t ∂μ = ∫ t in Ioc x y, f t ∂μ := by + rw [integral_Ico_eq_integral_Ioo, integral_Ioc_eq_integral_Ioo] + theorem integral_Icc_eq_integral_Ioo : ∫ t in Icc x y, f t ∂μ = ∫ t in Ioo x y, f t ∂μ := by rw [integral_Icc_eq_integral_Ico, integral_Ico_eq_integral_Ioo] diff --git a/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean b/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean index 7530413f38f51d..3aeb4ace15863c 100644 --- a/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean +++ b/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2019 Zhouhang Zhou. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Zhouhang Zhou, Yury Kudryashov, Patrick Massot +Authors: Zhouhang Zhou, Yury Kudryashov, Patrick Massot, Louis (Yiyang) Liu -/ module @@ -472,8 +472,7 @@ theorem continuousOn_primitive (h_int : IntegrableOn f (Icc a b) μ) : rw [continuousOn_congr this] intro x₀ _ refine continuousWithinAt_primitive (measure_singleton x₀) ?_ - simp only [intervalIntegrable_iff_integrableOn_Ioc_of_le, max_eq_right, h, - min_self] + simp only [intervalIntegrable_iff_integrableOn_Ioc_of_le, max_eq_right, h, min_self] exact h_int.mono Ioc_subset_Icc_self le_rfl · rw [Icc_eq_empty h] exact continuousOn_empty _ @@ -637,4 +636,96 @@ end ContinuousPrimitive end intervalIntegral +namespace MeasureTheory + +namespace IntegrableOn + +open intervalIntegral + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure ℝ} {f : ℝ → E} + +theorem continuousWithinAt_Ici_primitive_Ioi {a₀ : ℝ} (hf : IntegrableOn f (Ioi a₀) μ) : + ContinuousWithinAt (fun b ↦ ∫ x in Ioi b, f x ∂μ) (Ici a₀) a₀ := by + simp_rw [← integral_indicator measurableSet_Ioi] + apply tendsto_integral_filter_of_dominated_convergence ((Ioi a₀).indicator (norm ∘ f)) + · filter_upwards [self_mem_nhdsWithin] with a ha + rw [aestronglyMeasurable_indicator_iff measurableSet_Ioi] + exact (hf.mono_set (Ioi_subset_Ioi ha)).aestronglyMeasurable + · filter_upwards [self_mem_nhdsWithin] with a ha + refine ae_of_all _ fun x ↦ ?_ + rw [norm_indicator_eq_indicator_norm] + apply indicator_le_indicator_of_subset (Ioi_subset_Ioi (by grind)) (fun a ↦ norm_nonneg (f a)) + · simpa [integrable_indicator_iff measurableSet_Ioi] using hf.norm + · refine ae_of_all _ fun x ↦ ?_ + simp only [indicator_apply, mem_Ioi] + by_cases hx : a₀ < x <;> apply tendsto_const_nhds.congr' + · filter_upwards [mem_nhdsWithin_of_mem_nhds (Iio_mem_nhds hx)] with a ha using by grind + · filter_upwards [self_mem_nhdsWithin] with a ha using by grind + +theorem continuousOn_Ici_primitive_Ioi [NoAtoms μ] {a₀ : ℝ} (hf : IntegrableOn f (Ioi a₀) μ) : + ContinuousOn (fun b ↦ ∫ x in Ioi b, f x ∂μ) (Ici a₀) := by + intro a (ha : a₀ ≤ a) + rw [continuousWithinAt_iff_continuous_left_right] + constructor + · rw [Ici_inter_Iic] + have h_int : IntervalIntegrable f μ a₀ a := + (intervalIntegrable_iff_integrableOn_Ioc_of_le ha).2 <| hf.mono_set Ioc_subset_Ioi_self + have h_split : ∀ b ∈ Icc a₀ a, ∫ x in Ioi b, f x ∂μ = + (∫ x in Ioi a₀, f x ∂μ) - ∫ x in a₀..b, f x ∂μ := by + intro b hb + simp [← integral_Ioi_sub_Ioi hf hb.1] + have h_cwa : ContinuousWithinAt (fun b ↦ ∫ x in a₀..b, f x ∂μ) (Icc a₀ a) a := + continuousWithinAt_primitive (measure_singleton a) (by simpa [ha]) + exact (continuousWithinAt_const.sub h_cwa).congr h_split (h_split a (right_mem_Icc.2 ha)) + · simpa [ha] using (hf.mono_set (Ioi_subset_Ioi ha)).continuousWithinAt_Ici_primitive_Ioi + +theorem continuousWithinAt_Iic_primitive_Iio {a₀ : ℝ} (hf : IntegrableOn f (Iio a₀) μ) : + ContinuousWithinAt (fun b ↦ ∫ x in Iio b, f x ∂μ) (Iic a₀) a₀ := by + simp_rw [← integral_indicator measurableSet_Iio] + apply tendsto_integral_filter_of_dominated_convergence ((Iio a₀).indicator (norm ∘ f)) + · filter_upwards [self_mem_nhdsWithin] with a ha + rw [aestronglyMeasurable_indicator_iff measurableSet_Iio] + exact (hf.mono_set (Iio_subset_Iio ha)).aestronglyMeasurable + · filter_upwards [self_mem_nhdsWithin] with a ha + refine ae_of_all _ fun x ↦ ?_ + rw [norm_indicator_eq_indicator_norm] + apply indicator_le_indicator_of_subset (Iio_subset_Iio (by grind)) (fun a ↦ norm_nonneg (f a)) + · simpa [integrable_indicator_iff measurableSet_Iio] using hf.norm + · refine ae_of_all _ fun x ↦ ?_ + simp only [indicator_apply, mem_Iio] + by_cases hx : x < a₀ <;> apply tendsto_const_nhds.congr' + · filter_upwards [mem_nhdsWithin_of_mem_nhds (Ioi_mem_nhds hx)] with a ha using by grind + · filter_upwards [self_mem_nhdsWithin] with a ha using by grind + +theorem continuousOn_Iic_primitive_Iio [NoAtoms μ] {a₀ : ℝ} (hf : IntegrableOn f (Iio a₀) μ) : + ContinuousOn (fun b ↦ ∫ x in Iio b, f x ∂μ) (Iic a₀) := by + intro a (ha : a ≤ a₀) + rw [continuousWithinAt_iff_continuous_left_right] + constructor + · simpa [ha] using (hf.mono_set (Iio_subset_Iio ha)).continuousWithinAt_Iic_primitive_Iio + · rw [Iic_inter_Ici] + have h_int : IntervalIntegrable f μ a a₀ := + (intervalIntegrable_iff_integrableOn_Ico_of_le ha).2 <| hf.mono_set Ico_subset_Iio_self + have h_split : ∀ b ∈ Icc a a₀, ∫ x in Iio b, f x ∂μ = + (∫ x in Iio a₀, f x ∂μ) + ∫ x in a₀..b, f x ∂μ := by + intro b hb + simp [integral_symm b a₀, ← integral_Iio_sub_Iio' hf (hf.mono_set (Iio_subset_Iio hb.2))] + have h_cwa : ContinuousWithinAt (fun b ↦ ∫ x in a₀..b, f x ∂μ) (Icc a a₀) a := + continuousWithinAt_primitive (measure_singleton a) (by simpa [ha]) + exact (continuousWithinAt_const.add h_cwa).congr h_split (h_split a (left_mem_Icc.2 ha)) + +theorem continuousOn_Ici_primitive_Ici [NoAtoms μ] {a₀ : ℝ} (hf : IntegrableOn f (Ici a₀) μ) : + ContinuousOn (fun b ↦ ∫ x in Ici b, f x ∂μ) (Ici a₀) := by + simp_rw [integral_Ici_eq_integral_Ioi] + exact (hf.mono_set Ioi_subset_Ici_self).continuousOn_Ici_primitive_Ioi + +theorem continuousOn_Iic_primitive_Iic [NoAtoms μ] {a₀ : ℝ} (hf : IntegrableOn f (Iic a₀) μ) : + ContinuousOn (fun b ↦ ∫ x in Iic b, f x ∂μ) (Iic a₀) := by + simp_rw [integral_Iic_eq_integral_Iio] + exact (hf.mono_set Iio_subset_Iic_self).continuousOn_Iic_primitive_Iio + +end IntegrableOn + +end MeasureTheory + end DominatedConvergenceTheorem diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean index 6e2461079cbd7c..27d17ca7e66c3d 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean @@ -1128,6 +1128,30 @@ theorem integral_interval_add_Ioi' (ha : IntervalIntegrable f μ a b) ((intervalIntegrable_iff_integrableOn_Ioc_of_le h).1 ha) hb · exact hb.mono_set <| Ioi_subset_Ioi h.le +theorem integral_Ioi_sub_Ioi (hf : IntegrableOn f (Ioi a) μ) (hab : a ≤ b) : + ∫ x in Ioi a, f x ∂μ - ∫ x in Ioi b, f x ∂μ = ∫ x in a..b, f x ∂μ := + sub_eq_of_eq_add (integral_interval_add_Ioi hf (hf.mono_set (Ioi_subset_Ioi hab))).symm + +theorem integral_Ioi_sub_Ioi' (hf : IntegrableOn f (Ioi a) μ) (hg : IntegrableOn f (Ioi b) μ) : + ∫ x in Ioi a, f x ∂μ - ∫ x in Ioi b, f x ∂μ = ∫ x in a..b, f x ∂μ := by + wlog! hab : a ≤ b generalizing a b + · rw [integral_symm, ← this hg hf hab.le, neg_sub] + exact integral_Ioi_sub_Ioi hf hab + +theorem integral_Iio_sub_Iio (hf : IntegrableOn f (Iio b) μ) (hab : a ≤ b) : + ∫ x in Iio b, f x ∂μ - ∫ x in Iio a, f x ∂μ = ∫ x in Ico a b, f x ∂μ := by + have ha : IntegrableOn f (Iio a) μ := hf.mono_set (Iio_subset_Iio hab) + have h : IntegrableOn f (Ico a b) μ := hf.mono_set Ico_subset_Iio_self + rw [sub_eq_iff_eq_add', ← setIntegral_union (by grind) measurableSet_Ico ha h, + Iio_union_Ico_eq_Iio hab] + +theorem integral_Iio_sub_Iio' [NoAtoms μ] (hf : IntegrableOn f (Iio b) μ) + (hg : IntegrableOn f (Iio a) μ) : + ∫ x in Iio b, f x ∂μ - ∫ x in Iio a, f x ∂μ = ∫ x in a..b, f x ∂μ := by + wlog! hab : a ≤ b generalizing a b + · rw [integral_symm, ← this hg hf hab.le, neg_sub] + rw [integral_Iio_sub_Iio hf hab, integral_of_le hab, integral_Ico_eq_integral_Ioc] + theorem integral_Iic_add_Ioi (h_left : IntegrableOn f (Iic b) μ) (h_right : IntegrableOn f (Ioi b) μ) : (∫ x in Iic b, f x ∂μ) + (∫ x in Ioi b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ := by diff --git a/Mathlib/Order/Interval/Set/LinearOrder.lean b/Mathlib/Order/Interval/Set/LinearOrder.lean index 26a2a8cf18a9d7..b238400c16e73f 100644 --- a/Mathlib/Order/Interval/Set/LinearOrder.lean +++ b/Mathlib/Order/Interval/Set/LinearOrder.lean @@ -565,6 +565,10 @@ theorem compl_Ioc : (Ioc a b)ᶜ = Iic a ∪ Ioi b := by theorem Iic_diff_Ioc : Iic b \ Ioc a b = Iic (a ⊓ b) := by grind +@[simp] +theorem Ioi_diff_Ioc : Ioi a \ Ioc a b = Ioi (max a b) := by + grind + theorem Iic_diff_Ioc_self_of_le (hab : a ≤ b) : Iic b \ Ioc a b = Iic a := by grind From 4292dc8d1d55a20f9a88d5368b3332d9ece73fb0 Mon Sep 17 00:00:00 2001 From: pfaffelh Date: Wed, 18 Mar 2026 11:53:34 +0100 Subject: [PATCH 26/26] update indicator --- Mathlib/Algebra/Order/Group/Indicator.lean | 14 ++++++++++++++ Mathlib/Analysis/Normed/Group/Indicator.lean | 15 +++++++++++++++ 2 files changed, 29 insertions(+) diff --git a/Mathlib/Algebra/Order/Group/Indicator.lean b/Mathlib/Algebra/Order/Group/Indicator.lean index ad1e7fbf03bbe4..cd3983be2cf161 100644 --- a/Mathlib/Algebra/Order/Group/Indicator.lean +++ b/Mathlib/Algebra/Order/Group/Indicator.lean @@ -168,6 +168,20 @@ lemma mulIndicator_iUnion_apply (h1 : (⊥ : M) = 1) (s : ι → Set α) (f : α simp only [mem_iUnion, not_exists] at hx simp [hx, ← h1] +lemma Set.indicator_iUnion_of_disjoint [AddCommMonoid M] [TopologicalSpace M] (s : δ → Set α) (hs : Pairwise (Disjoint on s)) (f : α → M) (i : α) : (⋃ d, s d).indicator f i = tsum d, (s d).indicator f i := by + simp only [Set.indicator, Set.mem_iUnion] + by_cases h₀ : ∃ d, i ∈ s d <;> simp only [Set.mem_iUnion, h₀, ↓reduceIte] + · obtain ⟨j, hj⟩ := h₀ + rw [ENNReal.tsum_eq_add_tsum_ite j] + simp only [hj, ↓reduceIte] + nth_rw 1 [← add_zero (f i)] ; congr + apply (ENNReal.tsum_eq_zero.mpr ?_).symm + simp only [ite_eq_left_iff, ite_eq_right_iff] + exact fun k hk hb ↦ False.elim <| Disjoint.notMem_of_mem_left (hs (id (Ne.symm hk))) hj hb + · refine (ENNReal.tsum_eq_zero.mpr (fun j ↦ ?_)).symm + push_neg at h₀ + simp [h₀ j] + variable [Nonempty ι] @[to_additive] diff --git a/Mathlib/Analysis/Normed/Group/Indicator.lean b/Mathlib/Analysis/Normed/Group/Indicator.lean index c307ef50f4e45e..39d00b0789a447 100644 --- a/Mathlib/Analysis/Normed/Group/Indicator.lean +++ b/Mathlib/Analysis/Normed/Group/Indicator.lean @@ -42,6 +42,21 @@ theorem enorm_indicator_le_enorm_self : ‖indicator s f a‖ₑ ≤ ‖f a‖ rw [enorm_indicator_eq_indicator_enorm] apply indicator_enorm_le_enorm_self + +lemma Set.indicator_iUnion_of_disjoint (s : δ → Set α) (hs : Pairwise (Disjoint on s)) (f : α → ε) (i : α) : (⋃ d, s d).indicator f i = 1 --∑' (d : α), (s d).indicator f i := by + simp only [Set.indicator, Set.mem_iUnion] + by_cases h₀ : ∃ d, i ∈ s d <;> simp only [Set.mem_iUnion, h₀, ↓reduceIte] + · obtain ⟨j, hj⟩ := h₀ + rw [ENNReal.tsum_eq_add_tsum_ite j] + simp only [hj, ↓reduceIte] + nth_rw 1 [← add_zero (f i)] ; congr + apply (ENNReal.tsum_eq_zero.mpr ?_).symm + simp only [ite_eq_left_iff, ite_eq_right_iff] + exact fun k hk hb ↦ False.elim <| Disjoint.notMem_of_mem_left (hs (id (Ne.symm hk))) hj hb + · refine (ENNReal.tsum_eq_zero.mpr (fun j ↦ ?_)).symm + push_neg at h₀ + simp [h₀ j] + end ESeminormedAddMonoid section SeminormedAddGroup