Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: port Topology.Algebra.Order.Field (#2626)
I made substantial changes to the proofs. To avoid backporting most of them, in leanprover-community/mathlib#18552 I add `private` to lemmas that are deleted in this PR. Also, I backport `Homeomorph.symm_symm` in leanprover-community/mathlib#18551
- Loading branch information
Showing
6 changed files
with
284 additions
and
12 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,239 @@ | ||
| /- | ||
| Copyright (c) 2022 Benjamin Davidson. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Benjamin Davidson, Devon Tuma, Eric Rodriguez, Oliver Nash | ||
| ! This file was ported from Lean 3 source module topology.algebra.order.field | ||
| ! leanprover-community/mathlib commit 9a59dcb7a2d06bf55da57b9030169219980660cd | ||
| ! Please do not edit these lines, except to modify the commit id | ||
| ! if you have ported upstream changes. | ||
| -/ | ||
| import Mathlib.Tactic.Positivity | ||
| import Mathlib.Topology.Algebra.Order.Group | ||
| import Mathlib.Topology.Algebra.Field | ||
|
|
||
| /-! | ||
| # Topologies on linear ordered fields | ||
| In this file we prove that a linear ordered field with order topology has continuous multiplication | ||
| and division (apart from zero in the denominator). We also prove theorems like | ||
| `Filter.Tendsto.mul_atTop`: if `f` tends to a positive number and `g` tends to positive infinity, | ||
| then `f * g` tends to positive infinity. | ||
| -/ | ||
|
|
||
|
|
||
| open Set Filter TopologicalSpace Function Topology Classical | ||
| open OrderDual (toDual ofDual) | ||
|
|
||
| /-- If a (possibly non-unital and/or non-associative) ring `R` admits a submultiplicative | ||
| nonnegative norm `norm : R → 𝕜`, where `𝕜` is a linear ordered field, and the open balls | ||
| `{ x | norm x < ε }`, `ε > 0`, form a basis of neighborhoods of zero, then `R` is a topological | ||
| ring. -/ | ||
| theorem TopologicalRing.of_norm {R 𝕜 : Type _} [NonUnitalNonAssocRing R] [LinearOrderedField 𝕜] | ||
| [TopologicalSpace R] [TopologicalAddGroup R] (norm : R → 𝕜) | ||
| (norm_nonneg : ∀ x, 0 ≤ norm x) (norm_mul_le : ∀ x y, norm (x * y) ≤ norm x * norm y) | ||
| (nhds_basis : (𝓝 (0 : R)).HasBasis ((0 : 𝕜) < ·) (fun ε ↦ { x | norm x < ε })) : | ||
| TopologicalRing R := by | ||
| have h0 : ∀ f : R → R, ∀ c ≥ (0 : 𝕜), (∀ x, norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0) | ||
| · refine fun f c c0 hf ↦ (nhds_basis.tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_ | ||
| rcases exists_pos_mul_lt ε0 c with ⟨δ, δ0, hδ⟩ | ||
| refine ⟨δ, δ0, fun x hx ↦ (hf _).trans_lt ?_⟩ | ||
| exact (mul_le_mul_of_nonneg_left (le_of_lt hx) c0).trans_lt hδ | ||
| apply TopologicalRing.of_add_group_of_nhds_zero | ||
| case hmul => | ||
| refine ((nhds_basis.prod nhds_basis).tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_ | ||
| refine ⟨(1, ε), ⟨one_pos, ε0⟩, fun (x, y) ⟨hx, hy⟩ => ?_⟩ | ||
| simp only [sub_zero] at * | ||
| calc norm (x * y) ≤ norm x * norm y := norm_mul_le _ _ | ||
| _ < ε := mul_lt_of_le_one_of_lt_of_nonneg hx.le hy (norm_nonneg _) | ||
| case hmul_left => exact fun x => h0 _ (norm x) (norm_nonneg _) (norm_mul_le x) | ||
| case hmul_right => | ||
| exact fun y => h0 (· * y) (norm y) (norm_nonneg y) fun x => | ||
| (norm_mul_le x y).trans_eq (mul_comm _ _) | ||
|
|
||
| variable {𝕜 α : Type _} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] | ||
| {l : Filter α} {f g : α → 𝕜} | ||
|
|
||
| -- see Note [lower instance priority] | ||
| instance (priority := 100) LinearOrderedField.topologicalRing : TopologicalRing 𝕜 := | ||
| .of_norm abs abs_nonneg (fun _ _ ↦ (abs_mul _ _).le) <| by | ||
| simpa using nhds_basis_abs_sub_lt (0 : 𝕜) | ||
|
|
||
| /-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atTop` and `g` | ||
| tends to a positive constant `C` then `f * g` tends to `Filter.atTop`. -/ | ||
| theorem Filter.Tendsto.atTop_mul {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atTop) | ||
| (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop := by | ||
| refine' tendsto_atTop_mono' _ _ (hf.atTop_mul_const (half_pos hC)) | ||
| filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0] | ||
| with x hg hf using mul_le_mul_of_nonneg_left hg.le hf | ||
| #align filter.tendsto.at_top_mul Filter.Tendsto.atTop_mul | ||
|
|
||
| /-- In a linearly ordered field with the order topology, if `f` tends to a positive constant `C` and | ||
| `g` tends to `Filter.atTop` then `f * g` tends to `Filter.atTop`. -/ | ||
| theorem Filter.Tendsto.mul_atTop {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C)) | ||
| (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop := by | ||
| simpa only [mul_comm] using hg.atTop_mul hC hf | ||
| #align filter.tendsto.mul_at_top Filter.Tendsto.mul_atTop | ||
|
|
||
| /-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atTop` and `g` | ||
| tends to a negative constant `C` then `f * g` tends to `Filter.atBot`. -/ | ||
| theorem Filter.Tendsto.atTop_mul_neg {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atTop) | ||
| (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atBot := by | ||
| have := hf.atTop_mul (neg_pos.2 hC) hg.neg | ||
| simpa only [(· ∘ ·), neg_mul_eq_mul_neg, neg_neg] using tendsto_neg_atTop_atBot.comp this | ||
| #align filter.tendsto.at_top_mul_neg Filter.Tendsto.atTop_mul_neg | ||
|
|
||
| /-- In a linearly ordered field with the order topology, if `f` tends to a negative constant `C` and | ||
| `g` tends to `Filter.atTop` then `f * g` tends to `Filter.atBot`. -/ | ||
| theorem Filter.Tendsto.neg_mul_atTop {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (𝓝 C)) | ||
| (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atBot := by | ||
| simpa only [mul_comm] using hg.atTop_mul_neg hC hf | ||
| #align filter.tendsto.neg_mul_at_top Filter.Tendsto.neg_mul_atTop | ||
|
|
||
| /-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atBot` and `g` | ||
| tends to a positive constant `C` then `f * g` tends to `Filter.atBot`. -/ | ||
| theorem Filter.Tendsto.atBot_mul {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atBot) | ||
| (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atBot := by | ||
| have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul hC hg | ||
| simpa [(· ∘ ·)] using tendsto_neg_atTop_atBot.comp this | ||
| #align filter.tendsto.at_bot_mul Filter.Tendsto.atBot_mul | ||
|
|
||
| /-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atBot` and `g` | ||
| tends to a negative constant `C` then `f * g` tends to `Filter.atTop`. -/ | ||
| theorem Filter.Tendsto.atBot_mul_neg {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atBot) | ||
| (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop := by | ||
| have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_neg hC hg | ||
| simpa [(· ∘ ·)] using tendsto_neg_atBot_atTop.comp this | ||
| #align filter.tendsto.at_bot_mul_neg Filter.Tendsto.atBot_mul_neg | ||
|
|
||
| /-- In a linearly ordered field with the order topology, if `f` tends to a positive constant `C` and | ||
| `g` tends to `Filter.atBot` then `f * g` tends to `Filter.atBot`. -/ | ||
| theorem Filter.Tendsto.mul_atBot {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C)) | ||
| (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot := by | ||
| simpa only [mul_comm] using hg.atBot_mul hC hf | ||
| #align filter.tendsto.mul_at_bot Filter.Tendsto.mul_atBot | ||
|
|
||
| /-- In a linearly ordered field with the order topology, if `f` tends to a negative constant `C` and | ||
| `g` tends to `Filter.atBot` then `f * g` tends to `Filter.atTop`. -/ | ||
| theorem Filter.Tendsto.neg_mul_atBot {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (𝓝 C)) | ||
| (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atTop := by | ||
| simpa only [mul_comm] using hg.atBot_mul_neg hC hf | ||
| #align filter.tendsto.neg_mul_at_bot Filter.Tendsto.neg_mul_atBot | ||
|
|
||
| /-- The function `x ↦ x⁻¹` tends to `+∞` on the right of `0`. -/ | ||
| theorem tendsto_inv_zero_atTop : Tendsto (fun x : 𝕜 => x⁻¹) (𝓝[>] (0 : 𝕜)) atTop := by | ||
| refine' (atTop_basis' 1).tendsto_right_iff.2 fun b hb => _ | ||
| have hb' : 0 < b := by positivity | ||
| filter_upwards [Ioc_mem_nhdsWithin_Ioi | ||
| ⟨le_rfl, inv_pos.2 hb'⟩]with x hx using(le_inv hx.1 hb').1 hx.2 | ||
| #align tendsto_inv_zero_at_top tendsto_inv_zero_atTop | ||
|
|
||
| /-- The function `r ↦ r⁻¹` tends to `0` on the right as `r → +∞`. -/ | ||
| theorem tendsto_inv_atTop_zero' : Tendsto (fun r : 𝕜 => r⁻¹) atTop (𝓝[>] (0 : 𝕜)) := by | ||
| refine (atTop_basis.tendsto_iff ⟨fun s => mem_nhdsWithin_Ioi_iff_exists_Ioc_subset⟩).2 ?_ | ||
| refine fun b hb => ⟨b⁻¹, trivial, fun x hx => ?_⟩ | ||
| have : 0 < x := lt_of_lt_of_le (inv_pos.2 hb) hx | ||
| exact ⟨inv_pos.2 this, (inv_le this hb).2 hx⟩ | ||
| #align tendsto_inv_at_top_zero' tendsto_inv_atTop_zero' | ||
|
|
||
| theorem tendsto_inv_atTop_zero : Tendsto (fun r : 𝕜 => r⁻¹) atTop (𝓝 0) := | ||
| tendsto_inv_atTop_zero'.mono_right inf_le_left | ||
| #align tendsto_inv_at_top_zero tendsto_inv_atTop_zero | ||
|
|
||
| theorem Filter.Tendsto.div_atTop {a : 𝕜} (h : Tendsto f l (𝓝 a)) (hg : Tendsto g l atTop) : | ||
| Tendsto (fun x => f x / g x) l (𝓝 0) := by | ||
| simp only [div_eq_mul_inv] | ||
| exact mul_zero a ▸ h.mul (tendsto_inv_atTop_zero.comp hg) | ||
| #align filter.tendsto.div_at_top Filter.Tendsto.div_atTop | ||
|
|
||
| theorem Filter.Tendsto.inv_tendsto_atTop (h : Tendsto f l atTop) : Tendsto f⁻¹ l (𝓝 0) := | ||
| tendsto_inv_atTop_zero.comp h | ||
| #align filter.tendsto.inv_tendsto_at_top Filter.Tendsto.inv_tendsto_atTop | ||
|
|
||
| theorem Filter.Tendsto.inv_tendsto_zero (h : Tendsto f l (𝓝[>] 0)) : Tendsto f⁻¹ l atTop := | ||
| tendsto_inv_zero_atTop.comp h | ||
| #align filter.tendsto.inv_tendsto_zero Filter.Tendsto.inv_tendsto_zero | ||
|
|
||
| /-- The function `x^(-n)` tends to `0` at `+∞` for any positive natural `n`. | ||
| A version for positive real powers exists as `tendsto_rpow_neg_atTop`. -/ | ||
| theorem tendsto_pow_neg_atTop {n : ℕ} (hn : n ≠ 0) : | ||
| Tendsto (fun x : 𝕜 => x ^ (-(n : ℤ))) atTop (𝓝 0) := by | ||
| simpa only [zpow_neg, zpow_ofNat] using (@tendsto_pow_atTop 𝕜 _ _ hn).inv_tendsto_atTop | ||
| #align tendsto_pow_neg_at_top tendsto_pow_neg_atTop | ||
|
|
||
| theorem tendsto_zpow_atTop_zero {n : ℤ} (hn : n < 0) : | ||
| Tendsto (fun x : 𝕜 => x ^ n) atTop (𝓝 0) := by | ||
| lift -n to ℕ using le_of_lt (neg_pos.mpr hn) with N h | ||
| rw [← neg_pos, ← h, Nat.cast_pos] at hn | ||
| simpa only [h, neg_neg] using tendsto_pow_neg_atTop hn.ne' | ||
| #align tendsto_zpow_at_top_zero tendsto_zpow_atTop_zero | ||
|
|
||
| theorem tendsto_const_mul_zpow_atTop_zero {n : ℤ} {c : 𝕜} (hn : n < 0) : | ||
| Tendsto (fun x => c * x ^ n) atTop (𝓝 0) := | ||
| mul_zero c ▸ Filter.Tendsto.const_mul c (tendsto_zpow_atTop_zero hn) | ||
| #align tendsto_const_mul_zpow_at_top_zero tendsto_const_mul_zpow_atTop_zero | ||
|
|
||
| theorem tendsto_const_mul_pow_nhds_iff' {n : ℕ} {c d : 𝕜} : | ||
| Tendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d := by | ||
| rcases eq_or_ne n 0 with (rfl | hn) | ||
| · simp [tendsto_const_nhds_iff] | ||
| rcases lt_trichotomy c 0 with (hc | rfl | hc) | ||
| · have := tendsto_const_mul_pow_atBot_iff.2 ⟨hn, hc⟩ | ||
| simp [not_tendsto_nhds_of_tendsto_atBot this, hc.ne, hn] | ||
| · simp [tendsto_const_nhds_iff] | ||
| · have := tendsto_const_mul_pow_atTop_iff.2 ⟨hn, hc⟩ | ||
| simp [not_tendsto_nhds_of_tendsto_atTop this, hc.ne', hn] | ||
| #align tendsto_const_mul_pow_nhds_iff' tendsto_const_mul_pow_nhds_iff' | ||
|
|
||
| theorem tendsto_const_mul_pow_nhds_iff {n : ℕ} {c d : 𝕜} (hc : c ≠ 0) : | ||
| Tendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d := by | ||
| simp [tendsto_const_mul_pow_nhds_iff', hc] | ||
| #align tendsto_const_mul_pow_nhds_iff tendsto_const_mul_pow_nhds_iff | ||
|
|
||
| theorem tendsto_const_mul_zpow_atTop_nhds_iff {n : ℤ} {c d : 𝕜} (hc : c ≠ 0) : | ||
| Tendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0 := by | ||
| refine' ⟨fun h => _, fun h => _⟩ | ||
| · cases n with -- porting note: Lean 3 proof used `by_cases`, then `lift` but `lift` failed | ||
| | ofNat n => | ||
| left | ||
| simpa [tendsto_const_mul_pow_nhds_iff hc] using h | ||
| | negSucc n => | ||
| have hn := Int.negSucc_lt_zero n | ||
| exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩ | ||
| · cases' h with h h | ||
| · simp only [h.left, h.right, zpow_zero, mul_one] | ||
| exact tendsto_const_nhds | ||
| · exact h.2.symm ▸ tendsto_const_mul_zpow_atTop_zero h.1 | ||
| #align tendsto_const_mul_zpow_at_top_nhds_iff tendsto_const_mul_zpow_atTop_nhds_iff | ||
|
|
||
| -- see Note [lower instance priority] | ||
| instance (priority := 100) LinearOrderedSemifield.toHasContinuousInv₀ {𝕜} | ||
| [LinearOrderedSemifield 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [ContinuousMul 𝕜] : | ||
| HasContinuousInv₀ 𝕜 := .of_nhds_one <| tendsto_order.2 <| by | ||
| refine ⟨fun x hx => ?_, fun x hx => ?_⟩ | ||
| · obtain ⟨x', h₀, hxx', h₁⟩ : ∃ x', 0 < x' ∧ x ≤ x' ∧ x' < 1 := | ||
| ⟨max x (1 / 2), one_half_pos.trans_le (le_max_right _ _), le_max_left _ _, | ||
| max_lt hx one_half_lt_one⟩ | ||
| filter_upwards [Ioo_mem_nhds one_pos (one_lt_inv h₀ h₁)] with y hy | ||
| exact hxx'.trans_lt <| inv_inv x' ▸ inv_lt_inv_of_lt hy.1 hy.2 | ||
| · filter_upwards [Ioi_mem_nhds (inv_lt_one hx)] with y hy | ||
| simpa only [inv_inv] using inv_lt_inv_of_lt (inv_pos.2 <| one_pos.trans hx) hy | ||
|
|
||
| instance (priority := 100) LinearOrderedField.toTopologicalDivisionRing : | ||
| TopologicalDivisionRing 𝕜 := ⟨⟩ | ||
| #align linear_ordered_field.to_topological_division_ring LinearOrderedField.toTopologicalDivisionRing | ||
|
|
||
| -- porting note: todo: generalize to a `GroupWithzero` | ||
| theorem nhdsWithin_pos_comap_mul_left {x : 𝕜} (hx : 0 < x) : | ||
| comap (x * ·) (𝓝[>] 0) = 𝓝[>] 0 := by | ||
| rw [nhdsWithin, comap_inf, comap_principal, preimage_const_mul_Ioi _ hx, zero_div] | ||
| congr 1 | ||
| refine ((Homeomorph.mulLeft₀ x hx.ne').comap_nhds_eq _).trans ?_ | ||
| simp | ||
| #align nhds_within_pos_comap_mul_left nhdsWithin_pos_comap_mul_left | ||
|
|
||
| theorem eventually_nhdsWithin_pos_mul_left {x : 𝕜} (hx : 0 < x) {p : 𝕜 → Prop} | ||
| (h : ∀ᶠ ε in 𝓝[>] 0, p ε) : ∀ᶠ ε in 𝓝[>] 0, p (x * ε) := by | ||
| rw [← nhdsWithin_pos_comap_mul_left hx] | ||
| exact h.comap fun ε => x * ε | ||
| #align eventually_nhds_within_pos_mul_left eventually_nhdsWithin_pos_mul_left |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters