Mathlib.Analysis.Normed.Field.Lemmas

DilationEquiv.mulLeft definition

(a : α) (ha : a ≠ 0) : α ≃ᵈ α

Full source

/-- Multiplication by a nonzero element `a` on the left
as a `DilationEquiv` of a normed division ring. -/
@[simps!]
def DilationEquiv.mulLeft (a : α) (ha : a ≠ 0) : α ≃ᵈ α where
  __ := Dilation.mulLeft a ha
  toEquiv := Equiv.mulLeft₀ a ha

Left multiplication as a dilation equivalence in a normed division ring

Informal description

For a nonzero element $a$ in a normed division ring $\alpha$, the left multiplication map $x \mapsto a \cdot x$ is a dilation equivalence. This means it is a bijective dilation that preserves the multiplicative structure and scales distances by the norm of $a$, i.e., $\text{dist}(a \cdot x, a \cdot y) = \|a\| \cdot \text{dist}(x, y)$ for all $x, y \in \alpha$.

DilationEquiv.mulRight definition

(a : α) (ha : a ≠ 0) : α ≃ᵈ α

Full source

/-- Multiplication by a nonzero element `a` on the right
as a `DilationEquiv` of a normed division ring. -/
@[simps!]
def DilationEquiv.mulRight (a : α) (ha : a ≠ 0) : α ≃ᵈ α where
  __ := Dilation.mulRight a ha
  toEquiv := Equiv.mulRight₀ a ha

Right multiplication as a dilation equivalence in a normed division ring

Informal description

For a nonzero element $a$ in a normed division ring $\alpha$, the right multiplication map $x \mapsto x \cdot a$ is a dilation equivalence. Specifically, it is a bijective dilation that scales distances by the norm of $a$, i.e., $\text{dist}(x \cdot a, y \cdot a) = \|a\| \cdot \text{dist}(x, y)$ for all $x, y \in \alpha$.

Filter.map_mul_left_cobounded theorem

{a : α} (ha : a ≠ 0) : map (a * ·) (cobounded α) = cobounded α

Full source

@[simp]
lemma map_mul_left_cobounded {a : α} (ha : a ≠ 0) :
    map (a * ·) (cobounded α) = cobounded α :=
  DilationEquiv.map_cobounded (DilationEquiv.mulLeft a ha)

Left Multiplication Preserves the Cobounded Filter in a Normed Division Ring

Informal description

For any nonzero element $a$ in a normed division ring $\alpha$, the image of the cobounded filter under left multiplication by $a$ is equal to the cobounded filter itself. That is, the map $x \mapsto a \cdot x$ preserves the cobounded filter.

Filter.map_mul_right_cobounded theorem

{a : α} (ha : a ≠ 0) : map (· * a) (cobounded α) = cobounded α

Full source

@[simp]
lemma map_mul_right_cobounded {a : α} (ha : a ≠ 0) :
    map (· * a) (cobounded α) = cobounded α :=
  DilationEquiv.map_cobounded (DilationEquiv.mulRight a ha)

Right Multiplication Preserves Cobounded Filter in Normed Division Rings

Informal description

For any nonzero element $a$ in a normed division ring $\alpha$, the map $x \mapsto x \cdot a$ preserves the cobounded filter, i.e., the image of the cobounded filter under right multiplication by $a$ is equal to the cobounded filter itself.

Filter.tendsto_mul_left_cobounded theorem

{a : α} (ha : a ≠ 0) : Tendsto (a * ·) (cobounded α) (cobounded α)

Full source

/-- Multiplication on the left by a nonzero element of a normed division ring tends to infinity at
infinity. -/
theorem tendsto_mul_left_cobounded {a : α} (ha : a ≠ 0) :
    Tendsto (a * ·) (cobounded α) (cobounded α) :=
  (map_mul_left_cobounded ha).le

Left Multiplication by Nonzero Element Tends to Infinity at Infinity in Normed Division Rings

Informal description

For any nonzero element $a$ in a normed division ring $\alpha$, the function $x \mapsto a \cdot x$ tends to infinity as $x$ tends to infinity. That is, left multiplication by $a$ preserves the property of tending to infinity.

Filter.tendsto_mul_right_cobounded theorem

{a : α} (ha : a ≠ 0) : Tendsto (· * a) (cobounded α) (cobounded α)

Full source

/-- Multiplication on the right by a nonzero element of a normed division ring tends to infinity at
infinity. -/
theorem tendsto_mul_right_cobounded {a : α} (ha : a ≠ 0) :
    Tendsto (· * a) (cobounded α) (cobounded α) :=
  (map_mul_right_cobounded ha).le

Right multiplication by a nonzero element tends to infinity at infinity in a normed division ring

Informal description

For any nonzero element $a$ in a normed division ring $\alpha$, the function $x \mapsto x \cdot a$ tends to infinity at infinity, i.e., it maps sequences diverging to infinity to sequences diverging to infinity.

Filter.inv_cobounded₀ theorem

: (cobounded α)⁻¹ = 𝓝[≠] 0

Full source

@[simp]
lemma inv_cobounded₀ : (cobounded α)⁻¹ = 𝓝[≠] 0 := by
  rw [← comap_norm_atTop, ← Filter.comap_inv, ← comap_norm_nhdsGT_zero, ← inv_atTop₀,
    ← Filter.comap_inv]
  simp only [comap_comap, Function.comp_def, norm_inv]

Inverse of Filter at Infinity Equals Punctured Neighborhood of Zero in Normed Division Rings

Informal description

In a normed division ring $\alpha$, the inverse of the filter at infinity (cobounded $\alpha$) is equal to the neighborhood filter of zero excluding zero itself, i.e., $(\text{cobounded }\alpha)^{-1} = \mathcal{N}_{\neq 0}(0)$.

Filter.inv_nhdsWithin_ne_zero theorem

: (𝓝[≠] (0 : α))⁻¹ = cobounded α

Full source

@[simp]
lemma inv_nhdsWithin_ne_zero : (𝓝[≠] (0 : α))⁻¹ = cobounded α := by
  rw [← inv_cobounded₀, inv_inv]

Inverse of Punctured Neighborhood of Zero Equals Filter at Infinity in Normed Division Rings

Informal description

In a normed division ring $\alpha$, the inverse of the punctured neighborhood filter of zero is equal to the filter at infinity, i.e., $(\mathcal{N}_{\neq 0}(0))^{-1} = \text{cobounded }\alpha$.

Filter.tendsto_inv₀_cobounded' theorem

: Tendsto Inv.inv (cobounded α) (𝓝[≠] 0)

Full source

lemma tendsto_inv₀_cobounded' : Tendsto Inv.inv (cobounded α) (𝓝[≠] 0) :=
  inv_cobounded₀.le

Inversion Tends to Punctured Zero Neighborhood at Infinity in Normed Division Rings

Informal description

In a normed division ring $\alpha$, the inversion function $x \mapsto x^{-1}$ tends to the punctured neighborhood of zero as $x$ tends to infinity (i.e., as $\|x\|$ tends to infinity).

Filter.tendsto_inv₀_cobounded theorem

: Tendsto Inv.inv (cobounded α) (𝓝 0)

Full source

theorem tendsto_inv₀_cobounded : Tendsto Inv.inv (cobounded α) (𝓝 0) :=
  tendsto_inv₀_cobounded'.mono_right inf_le_left

Inversion Tends to Zero at Infinity in Normed Division Rings

Informal description

In a normed division ring $\alpha$, the inversion function $x \mapsto x^{-1}$ tends to zero as $x$ tends to infinity (i.e., as $\|x\|$ tends to infinity).

Filter.tendsto_inv₀_nhdsWithin_ne_zero theorem

: Tendsto Inv.inv (𝓝[≠] 0) (cobounded α)

Full source

lemma tendsto_inv₀_nhdsWithin_ne_zero : Tendsto Inv.inv (𝓝[≠] 0) (cobounded α) :=
  inv_nhdsWithin_ne_zero.le

Inversion Tends to Infinity Near Zero in Normed Division Rings

Informal description

In a normed division ring $\alpha$, the inversion function $x \mapsto x^{-1}$ tends to infinity (i.e., the filter of cobounded sets) as $x$ tends to zero within the punctured neighborhood of zero.

NormedDivisionRing.to_hasContinuousInv₀ instance

: HasContinuousInv₀ α

Full source

instance (priority := 100) NormedDivisionRing.to_hasContinuousInv₀ : HasContinuousInv₀ α := by
  refine ⟨fun r r0 => tendsto_iff_norm_sub_tendsto_zero.2 ?_⟩
  have r0' : 0 < ‖r‖ := norm_pos_iff.2 r0
  rcases exists_between r0' with ⟨ε, ε0, εr⟩
  have : ∀ᶠ e in 𝓝 r, ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε := by
    filter_upwards [(isOpen_lt continuous_const continuous_norm).eventually_mem εr] with e he
    have e0 : e ≠ 0 := norm_pos_iff.1 (ε0.trans he)
    calc
      ‖e⁻¹ - r⁻¹‖ = ‖r‖‖r‖⁻¹ * ‖r - e‖ * ‖e‖‖e‖⁻¹ := by
        rw [← norm_inv, ← norm_inv, ← norm_mul, ← norm_mul, mul_sub, sub_mul,
          mul_assoc _ e, inv_mul_cancel₀ r0, mul_inv_cancel₀ e0, one_mul, mul_one]
      _ = ‖r - e‖ / ‖r‖ / ‖e‖ := by field_simp [mul_comm]
      _ ≤ ‖r - e‖ / ‖r‖ / ε := by gcongr
  refine squeeze_zero' (Eventually.of_forall fun _ => norm_nonneg _) this ?_
  refine (((continuous_const.sub continuous_id).norm.div_const _).div_const _).tendsto' _ _ ?_
  simp

Continuity of Inversion in Normed Division Rings

Informal description

Every normed division ring $\alpha$ has a continuous inversion operation at all nonzero points. That is, the function $x \mapsto x^{-1}$ is continuous on $\alpha \setminus \{0\}$.

NormedDivisionRing.to_isTopologicalDivisionRing instance

: IsTopologicalDivisionRing α

Full source

/-- A normed division ring is a topological division ring. -/
instance (priority := 100) NormedDivisionRing.to_isTopologicalDivisionRing :
    IsTopologicalDivisionRing α where

Normed Division Rings are Topological Division Rings

Informal description

Every normed division ring $\alpha$ is a topological division ring. That is, the ring operations (addition and multiplication) are continuous, and the inversion operation $x \mapsto x^{-1}$ is continuous at every nonzero element $x \in \alpha$.

NormedField.tendsto_norm_inv_nhdsNE_zero_atTop theorem

: Tendsto (fun x : α ↦ ‖x⁻¹‖) (𝓝[≠] 0) atTop

Full source

lemma NormedField.tendsto_norm_inv_nhdsNE_zero_atTop : Tendsto (fun x : α ↦ ‖x⁻¹‖) (𝓝[≠] 0) atTop :=
  (tendsto_inv_nhdsGT_zero.comp tendsto_norm_nhdsNE_zero).congr fun x ↦ (norm_inv x).symm

Limit of Norm of Inverse at Zero in Normed Fields: $\lim_{x \to 0^*} \|x^{-1}\| = \infty$

Informal description

In a normed field $\alpha$, the function $x \mapsto \|x^{-1}\|$ tends to infinity as $x$ approaches zero (excluding zero itself).

NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop theorem

{m : ℤ} (hm : m < 0) : Tendsto (fun x : α ↦ ‖x ^ m‖) (𝓝[≠] 0) atTop

Full source

lemma NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop {m : ℤ} (hm : m < 0) :
    Tendsto (fun x : α ↦ ‖x ^ m‖) (𝓝[≠] 0) atTop := by
  obtain ⟨m, rfl⟩ := neg_surjective m
  rw [neg_lt_zero] at hm
  lift m to ℕ using hm.le
  rw [Int.natCast_pos] at hm
  simp only [norm_pow, zpow_neg, zpow_natCast, ← inv_pow]
  exact (tendsto_pow_atTop hm.ne').comp NormedField.tendsto_norm_inv_nhdsNE_zero_atTop

Limit of Norm of Negative Integer Power at Zero: $\lim_{x \to 0^*} \|x^m\| = \infty$ for $m < 0$

Informal description

For any negative integer $m < 0$ and any normed field $\alpha$, the function $x \mapsto \|x^m\|$ tends to infinity as $x$ approaches zero (excluding zero itself).

NormedField.discreteTopology_or_nontriviallyNormedField theorem

 (𝕜 : Type*) [h : NormedField 𝕜] :
  DiscreteTopology 𝕜 ∨ Nonempty ({ h' : NontriviallyNormedField 𝕜 // h'.toNormedField = h })

Full source

/-- A normed field is either nontrivially normed or has a discrete topology.
In the discrete topology case, all the norms are 1, by `norm_eq_one_iff_ne_zero_of_discrete`.
The nontrivially normed field instance is provided by a subtype with a proof that the
forgetful inheritance to the existing `NormedField` instance is definitionally true.
This allows one to have the new `NontriviallyNormedField` instance without data clashes. -/
lemma discreteTopology_or_nontriviallyNormedField (𝕜 : Type*) [h : NormedField 𝕜] :
    DiscreteTopologyDiscreteTopology 𝕜 ∨ Nonempty ({h' : NontriviallyNormedField 𝕜 // h'.toNormedField = h}) := by
  by_cases H : ∃ x : 𝕜, x ≠ 0 ∧ ‖x‖ ≠ 1
  · exact Or.inr ⟨(⟨NontriviallyNormedField.ofNormNeOne H, rfl⟩)⟩
  · simp_rw [discreteTopology_iff_isOpen_singleton_zero, Metric.isOpen_singleton_iff, dist_eq_norm,
             sub_zero]
    refine Or.inl ⟨1, zero_lt_one, ?_⟩
    contrapose! H
    refine H.imp ?_
    -- contextual to reuse the `a ≠ 0` hypothesis in the proof of `a ≠ 0 ∧ ‖a‖ ≠ 1`
    simp +contextual [add_comm, ne_of_lt]

Dichotomy for Normed Fields: Discrete Topology or Nontrivially Normed Structure

Informal description

For any normed field $\mathbb{K}$, either the topology on $\mathbb{K}$ is discrete, or there exists a nontrivially normed field structure on $\mathbb{K}$ that is definitionally equal to the original normed field structure.

NormedField.discreteTopology_of_bddAbove_range_norm theorem

{𝕜 : Type*} [NormedField 𝕜] (h : BddAbove (Set.range fun k : 𝕜 ↦ ‖k‖)) : DiscreteTopology 𝕜

Full source

lemma discreteTopology_of_bddAbove_range_norm {𝕜 : Type*} [NormedField 𝕜]
    (h : BddAbove (Set.range fun k : 𝕜 ↦ ‖k‖)) :
    DiscreteTopology 𝕜 := by
  refine (NormedField.discreteTopology_or_nontriviallyNormedField _).resolve_right ?_
  rintro ⟨_, rfl⟩
  obtain ⟨x, h⟩ := h
  obtain ⟨k, hk⟩ := NormedField.exists_lt_norm 𝕜 x
  exact hk.not_le (h (Set.mem_range_self k))

Discrete Topology from Bounded Norm Range in Normed Fields

Informal description

For any normed field $\mathbb{K}$, if the range of the norm function $\|\cdot\| : \mathbb{K} \to \mathbb{R}$ is bounded above, then the topology on $\mathbb{K}$ is discrete.

NormedField.denseRange_nnnorm theorem

: DenseRange (nnnorm : α → ℝ≥0)

Full source

theorem denseRange_nnnorm : DenseRange (nnnorm : α → ℝ≥0) :=
  dense_of_exists_between fun _ _ hr =>
    let ⟨x, h⟩ := exists_lt_nnnorm_lt α hr
    ⟨‖x‖₊, ⟨x, rfl⟩, h⟩

Density of Non-Negative Norm Range in a Normed Field

Informal description

For a normed field $\alpha$, the range of the non-negative norm function $\|\cdot\|_{\mathbb{R}_{\geq 0}} : \alpha \to \mathbb{R}_{\geq 0}$ is dense in $\mathbb{R}_{\geq 0}$.

NormedField.continuousAt_zpow theorem

: ContinuousAt (fun x ↦ x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n

Full source

@[simp]
protected lemma continuousAt_zpow : ContinuousAtContinuousAt (fun x ↦ x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n := by
  refine ⟨?_, continuousAt_zpow₀ _ _⟩
  contrapose!
  rintro ⟨rfl, hm⟩ hc
  exact not_tendsto_atTop_of_tendsto_nhds (hc.tendsto.mono_left nhdsWithin_le_nhds).norm
    (NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop hm)

Continuity of Integer Power Function in Normed Fields: $\text{ContinuousAt}(x \mapsto x^n, x) \leftrightarrow x \neq 0 \lor n \geq 0$

Informal description

For any element $x$ in a normed field $\alpha$ and any integer $n$, the function $x \mapsto x^n$ is continuous at $x$ if and only if either $x \neq 0$ or $n \geq 0$.

NormedField.continuousAt_inv theorem

: ContinuousAt Inv.inv x ↔ x ≠ 0

Full source

@[simp]
protected lemma continuousAt_inv : ContinuousAtContinuousAt Inv.inv x ↔ x ≠ 0 := by
  simpa using NormedField.continuousAt_zpow (n := -1) (x := x)

Continuity of Inversion in Normed Fields: $\text{ContinuousAt}(x \mapsto x^{-1}, x) \leftrightarrow x \neq 0$

Informal description

For any element $x$ in a normed field $\alpha$, the inversion function $x \mapsto x^{-1}$ is continuous at $x$ if and only if $x \neq 0$.

Rat.instNormedField instance

: NormedField ℚ

Full source

instance Rat.instNormedField : NormedField ℚ where
  __ := instField
  __ := instNormedAddCommGroup
  norm_mul a b := by simp only [norm, Rat.cast_mul, abs_mul]

The Normed Field Structure on Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ form a normed field, where the norm is compatible with the field structure and induces a metric space.

Rat.instDenselyNormedField instance

: DenselyNormedField ℚ

Full source

instance Rat.instDenselyNormedField : DenselyNormedField ℚ where
  lt_norm_lt r₁ r₂ h₀ hr :=
    let ⟨q, h⟩ := exists_rat_btwn hr
    ⟨q, by rwa [← Rat.norm_cast_real, Real.norm_eq_abs, abs_of_pos (h₀.trans_lt h.1)]⟩

The Densely Normed Field Structure on Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ form a densely normed field, where the image of the norm function is dense in the non-negative real numbers $\mathbb{R}_{\geq 0}$.

NormedField.completeSpace_iff_isComplete_closedBall theorem

{K : Type*} [NormedField K] : CompleteSpace K ↔ IsComplete (Metric.closedBall 0 1 : Set K)

Full source

lemma NormedField.completeSpace_iff_isComplete_closedBall {K : Type*} [NormedField K] :
    CompleteSpaceCompleteSpace K ↔ IsComplete (Metric.closedBall 0 1 : Set K) := by
  constructor <;> intro h
  · exact Metric.isClosed_closedBall.isComplete
  rcases NormedField.discreteTopology_or_nontriviallyNormedField K with _|⟨_, rfl⟩
  · rwa [completeSpace_iff_isComplete_univ,
         ← NormedDivisionRing.unitClosedBall_eq_univ_of_discrete]
  refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_
  obtain ⟨k, hk⟩ := hu.norm_bddAbove
  have kpos : 0 ≤ k := (_root_.norm_nonneg (u 0)).trans (hk (by simp))
  obtain ⟨x, hx⟩ := NormedField.exists_lt_norm K k
  have hu' : CauchySeq ((· / x) ∘ u) := (uniformContinuous_div_const' x).comp_cauchySeq hu
  have hb : ∀ n, ((· / x) ∘ u) n ∈ Metric.closedBall 0 1 := by
    intro
    simp only [Function.comp_apply, Metric.mem_closedBall, dist_zero_right, norm_div]
    rw [div_le_one (kpos.trans_lt hx)]
    exact hx.le.trans' (hk (by simp))
  obtain ⟨a, -, ha'⟩ := cauchySeq_tendsto_of_isComplete h hb hu'
  refine ⟨a * x, (((continuous_mul_right x).tendsto a).comp ha').congr ?_⟩
  have hx' : x ≠ 0 := by
    contrapose! hx
    simp [hx, kpos]
  simp [div_mul_cancel₀ _ hx']

Completeness of Normed Field Equivalent to Completeness of Closed Unit Ball

Informal description

A normed field $K$ is complete if and only if the closed unit ball $\overline{B}(0, 1) \subseteq K$ is a complete metric space.