Mathlib.Topology.Algebra.Order.Group

LinearOrderedCommGroup.toIsTopologicalGroup instance

: IsTopologicalGroup G

Full source

@[to_additive]
instance (priority := 100) LinearOrderedCommGroup.toIsTopologicalGroup :
    IsTopologicalGroup G where
  continuous_mul := by
    simp only [continuous_iff_continuousAt, Prod.forall, ContinuousAt,
      LinearOrderedCommGroup.tendsto_nhds]
    intro a b ε hε
    rcases dense_or_discrete 1 ε with ⟨δ, hδ₁, hδε⟩ | ⟨-, hε_min⟩
    · filter_upwards [(eventually_mabs_div_lt _ hδ₁).prod_nhds
        (eventually_mabs_div_lt _ (one_lt_div'.mpr hδε))]
      rintro ⟨c, d⟩ ⟨hc, hd⟩
      calc
        |c * d / (a * b)|ₘ = |(c / a) * (d / b)|ₘ := by rw [div_mul_div_comm]
        _ ≤ |c / a|ₘ * |d / b|ₘ := mabs_mul ..
        _ < δ * (ε / δ) := mul_lt_mul_of_lt_of_lt hc hd
        _ = ε := mul_div_cancel ..
    · have (x : G) : ∀ᶠ y in 𝓝 x, y = x :=
        (eventually_mabs_div_lt _ hε).mono fun y hy ↦ mabs_div_le_one.mp <| hε_min _ hy
      filter_upwards [(this _).prod_nhds (this _)]
      simp [hε]
  continuous_inv := continuous_iff_continuousAt.2 fun a ↦
    LinearOrderedCommGroup.tendsto_nhds.2 fun ε ε0 ↦
      (eventually_mabs_div_lt a ε0).mono fun x hx ↦ by rwa [inv_div_inv, mabs_div_comm]

Topological Group Structure on Linear Ordered Commutative Groups

Informal description

Every linear ordered commutative group $G$ with the order topology is a topological group.

continuous_mabs theorem

: Continuous (mabs : G → G)

Full source

@[to_additive (attr := continuity)]
theorem continuous_mabs : Continuous (mabs : G → G) :=
  continuous_id.max continuous_inv

Continuity of Absolute Value in Ordered Commutative Groups

Informal description

The absolute value function $|\cdot| : G \to G$ on a linearly ordered commutative group $G$ is continuous with respect to the order topology.

Filter.Tendsto.mabs theorem

{a : G} (h : Tendsto f l (𝓝 a)) : Tendsto (fun x => |f x|ₘ) l (𝓝 |a|ₘ)

Full source

@[to_additive]
protected theorem Filter.Tendsto.mabs {a : G} (h : Tendsto f l (𝓝 a)) :
    Tendsto (fun x => |f x|ₘ) l (𝓝 |a|ₘ) :=
  (continuous_mabs.tendsto _).comp h

Absolute Value Preserves Limits in Ordered Commutative Groups

Informal description

Let $G$ be a linearly ordered commutative group with the order topology, and let $f$ be a function from some type $\alpha$ to $G$. If $f$ tends to an element $a \in G$ as $x$ approaches a limit point $l$ (i.e., $\lim_{x \to l} f(x) = a$), then the absolute value of $f$ tends to the absolute value of $a$ as $x$ approaches $l$ (i.e., $\lim_{x \to l} |f(x)| = |a|$).

comap_mabs_nhds_one theorem

: comap mabs (𝓝 (1 : G)) = 𝓝 1

Full source

@[to_additive (attr := simp)]
theorem comap_mabs_nhds_one : comap mabs (𝓝 (1 : G)) = 𝓝 1 := by
  simp [nhds_eq_iInf_mabs_div]

Preimage of Neighborhood Filter under Absolute Value at Identity

Informal description

The preimage of the neighborhood filter at the identity element $1$ under the absolute value function $|\cdot|$ on a linearly ordered commutative group $G$ is equal to the neighborhood filter at $1$ itself, i.e., $\text{comap}\, |\cdot|\, (\mathcal{N}(1)) = \mathcal{N}(1)$.

tendsto_one_iff_mabs_tendsto_one theorem

(f : α → G) : Tendsto f l (𝓝 1) ↔ Tendsto (mabs ∘ f) l (𝓝 1)

Full source

@[to_additive]
theorem tendsto_one_iff_mabs_tendsto_one (f : α → G) :
    TendstoTendsto f l (𝓝 1) ↔ Tendsto (mabs ∘ f) l (𝓝 1) := by
  rw [← tendsto_comap_iff, comap_mabs_nhds_one]

Limit of Function Equals Identity if and only if Limit of Absolute Value Equals Identity

Informal description

For a function $f \colon \alpha \to G$ with values in a linearly ordered commutative group $G$, the limit of $f$ at a point is the identity element $1$ if and only if the limit of the absolute value of $f$ at that point is $1$. In other words, $\lim_{x \to a} f(x) = 1 \leftrightarrow \lim_{x \to a} |f(x)| = 1$.

Continuous.mabs theorem

(h : Continuous f) : Continuous fun x => |f x|ₘ

Full source

@[to_additive (attr := fun_prop)]
protected theorem Continuous.mabs (h : Continuous f) : Continuous fun x => |f x|ₘ :=
  continuous_mabs.comp h

Continuity of Absolute Value of Continuous Functions in Ordered Groups

Informal description

If $f \colon X \to G$ is a continuous function from a topological space $X$ to a linearly ordered commutative group $G$ with the order topology, then the function $x \mapsto |f(x)|$ is also continuous.

ContinuousAt.mabs theorem

(h : ContinuousAt f x) : ContinuousAt (fun x => |f x|ₘ) x

Full source

@[to_additive (attr := fun_prop)]
protected theorem ContinuousAt.mabs (h : ContinuousAt f x) : ContinuousAt (fun x => |f x|ₘ) x :=
  Filter.Tendsto.mabs h

Absolute Value Preserves Continuity at a Point in Ordered Groups

Informal description

Let $G$ be a linearly ordered commutative group with the order topology, and let $f \colon X \to G$ be a function from a topological space $X$ to $G$. If $f$ is continuous at a point $x \in X$, then the function $x \mapsto |f(x)|$ is also continuous at $x$.

ContinuousWithinAt.mabs theorem

(h : ContinuousWithinAt f s x) : ContinuousWithinAt (fun x => |f x|ₘ) s x

Full source

@[to_additive]
protected theorem ContinuousWithinAt.mabs (h : ContinuousWithinAt f s x) :
    ContinuousWithinAt (fun x => |f x|ₘ) s x :=
  Filter.Tendsto.mabs h

Absolute Value Preserves Continuity Within a Subset at a Point in Ordered Groups

Informal description

Let $G$ be a linearly ordered commutative group with the order topology, and let $f \colon X \to G$ be a function from a topological space $X$ to $G$. If $f$ is continuous at a point $x \in X$ within a subset $s \subseteq X$, then the function $x \mapsto |f(x)|$ is also continuous at $x$ within $s$.

ContinuousOn.mabs theorem

(h : ContinuousOn f s) : ContinuousOn (fun x => |f x|ₘ) s

Full source

@[to_additive (attr := fun_prop)]
protected theorem ContinuousOn.mabs (h : ContinuousOn f s) : ContinuousOn (fun x => |f x|ₘ) s :=
  fun x hx => (h x hx).mabs

Absolute Value Preserves Continuity on a Subset in Ordered Groups

Informal description

Let $G$ be a linearly ordered commutative group with the order topology, and let $f \colon X \to G$ be a function from a topological space $X$ to $G$. If $f$ is continuous on a subset $s \subseteq X$, then the function $x \mapsto |f(x)|$ is also continuous on $s$.

tendsto_mabs_nhdsNE_one theorem

: Tendsto (mabs : G → G) (𝓝[≠] 1) (𝓝[>] 1)

Full source

@[to_additive]
theorem tendsto_mabs_nhdsNE_one : Tendsto (mabs : G → G) (𝓝[≠] 1) (𝓝[>] 1) :=
  (continuous_mabs.tendsto' (1 : G) 1 mabs_one).inf <|
    tendsto_principal_principal.2 fun _x => one_lt_mabs.2

Limit Behavior of Absolute Value Near Identity in Ordered Commutative Groups

Informal description

The absolute value function $|\cdot| : G \to G$ on a linearly ordered commutative group $G$ satisfies the limit property that as $x$ approaches 1 (but not equal to 1), $|x|$ approaches 1 from above.

denseRange_zpow_iff_surjective theorem

{a : G} : DenseRange (a ^ · : ℤ → G) ↔ Surjective (a ^ · : ℤ → G)

Full source

/-- In a linearly ordered multiplicative group, the integer powers of an element are dense
iff they are the whole group. -/
@[to_additive "In a linearly ordered additive group, the integer multiples of an element are dense
iff they are the whole group."]
theorem denseRange_zpow_iff_surjective {a : G} :
    DenseRangeDenseRange (a ^ · : ℤ → G) ↔ Surjective (a ^ · : ℤ → G) := by
  refine ⟨fun h ↦ ?_, fun h ↦ h.denseRange⟩
  wlog ha₀ : 1 < a generalizing a
  · simp only [← range_eq_univ, DenseRange] at *
    rcases (not_lt.1 ha₀).eq_or_lt with rfl | hlt
    · simpa only [one_zpow, range_const, dense_iff_closure_eq, closure_singleton] using h
    · have H : range (a⁻¹ ^ · : ℤ → G) = range (a ^ · : ℤ → G) := by
        simpa only [← inv_zpow, zpow_neg, comp_def] using neg_surjective.range_comp (a ^ · : ℤ → G)
      rw [← H]
      apply this <;> simpa only [H, one_lt_inv']
  intro b
  obtain ⟨m, hm, hm'⟩ : ∃ m : ℤ, a ^ m ∈ Ioo b (b * a * a) := by
    have hne : (Ioo b (b * a * a)).Nonempty := ⟨b * a, by simpa⟩
    simpa using h.exists_mem_open isOpen_Ioo hne
  rcases eq_or_ne b (a ^ (m - 1)) with rfl | hne; · simp
  suffices (Ioo (a ^ m) (a ^ (m + 1))).Nonempty by
    rcases h.exists_mem_open isOpen_Ioo this with ⟨l, hl⟩
    have : m < l ∧ l < m + 1 := by simpa [zpow_lt_zpow_iff_right ha₀] using hl
    omega
  rcases hne.lt_or_lt with hlt | hlt
  · refine ⟨b * a * a, hm', ?_⟩
    simpa only [zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv, lt_div_iff_mul_lt,
      mul_lt_mul_iff_right] using hlt
  · use b * a
    simp only [mem_Ioo, zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv,
      mul_lt_mul_iff_right] at hlt ⊢
    exact ⟨div_lt_iff_lt_mul.1 hlt, hm⟩

Density of Integer Powers in Linearly Ordered Commutative Group is Equivalent to Surjectivity of Power Map

Informal description

For any element $a$ in a linearly ordered commutative group $G$, the set of integer powers $\{a^n \mid n \in \mathbb{Z}\}$ is dense in $G$ if and only if the power map $n \mapsto a^n$ is surjective onto $G$.

not_denseRange_zpow theorem

[Nontrivial G] [DenselyOrdered G] {a : G} : ¬DenseRange (a ^ · : ℤ → G)

Full source

/-- In a nontrivial densely linearly ordered commutative group,
the integer powers of an element can't be dense. -/
@[to_additive "In a nontrivial densely linearly ordered additive group,
the integer multiples of an element can't be dense."]
theorem not_denseRange_zpow [Nontrivial G] [DenselyOrdered G] {a : G} :
    ¬DenseRange (a ^ · : ℤ → G) :=
  denseRange_zpow_iff_surjective.not.mpr fun h ↦
    not_isCyclic_of_denselyOrdered G ⟨⟨a, h⟩⟩

Non-Density of Integer Powers in Densely Ordered Commutative Group

Informal description

In a nontrivial densely linearly ordered commutative group $G$, for any element $a \in G$, the set of integer powers $\{a^n \mid n \in \mathbb{Z}\}$ is not dense in $G$.