Mathlib.Data.Real.Basic

Real structure

Full source

/-- The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. -/
structure Real where ofCauchy ::
  /-- The underlying Cauchy completion -/
  cauchy : CauSeq.Completion.Cauchy (abs : ℚ → ℚ)

Real numbers as Cauchy sequences

Informal description

The structure `ℝ` represents the type of real numbers, constructed as equivalence classes of Cauchy sequences of rational numbers. This approach is chosen due to the ease of proving that the real numbers form a commutative ring by lifting operations to the rational numbers. The properties of being an Archimedean floor ring and a conditionally complete linear order are not included in this structure but are addressed in separate files to simplify the imports.

termℝ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
notation "ℝ" => Real

Real numbers notation

Informal description

The notation `ℝ` represents the type of real numbers, defined as equivalence classes of Cauchy sequences of rational numbers.

CauSeq.Completion.ofRat_rat theorem

{abv : ℚ → ℚ} [IsAbsoluteValue abv] (q : ℚ) : ofRat (q : ℚ) = (q : Cauchy abv)

Full source

@[simp]
theorem ofRat_rat {abv : ℚ → ℚ} [IsAbsoluteValue abv] (q : ℚ) :
    ofRat (q : ℚ) = (q : Cauchy abv) :=
  rfl

Embedding of Rationals into Completion via Constant Cauchy Sequences

Informal description

For any absolute value function $abv: \mathbb{Q} \to \mathbb{Q}$ and any rational number $q \in \mathbb{Q}$, the canonical embedding of $q$ into the completion of $\mathbb{Q}$ with respect to $abv$ is equal to the equivalence class of the constant Cauchy sequence $(q, q, \dots)$.

Real.ext_cauchy_iff theorem

: ∀ {x y : Real}, x = y ↔ x.cauchy = y.cauchy

Full source

theorem ext_cauchy_iff : ∀ {x y : Real}, x = y ↔ x.cauchy = y.cauchy
  | ⟨a⟩, ⟨b⟩ => by rw [ofCauchy.injEq]

Equality of Real Numbers via Cauchy Sequences

Informal description

For any two real numbers $x$ and $y$, $x$ is equal to $y$ if and only if their underlying Cauchy sequences are equal, i.e., $x = y \leftrightarrow x.\text{cauchy} = y.\text{cauchy}$.

Real.ext_cauchy theorem

{x y : Real} : x.cauchy = y.cauchy → x = y

Full source

theorem ext_cauchy {x y : Real} : x.cauchy = y.cauchy → x = y :=
  ext_cauchy_iff.2

Equality of Real Numbers via Cauchy Sequences

Informal description

For any two real numbers $x$ and $y$, if their underlying Cauchy sequences are equal, then $x = y$.

Real.equivCauchy definition

: ℝ ≃ CauSeq.Completion.Cauchy (abs : ℚ → ℚ)

Full source

/-- The real numbers are isomorphic to the quotient of Cauchy sequences on the rationals. -/
def equivCauchy : ℝℝ ≃ CauSeq.Completion.Cauchy (abs : ℚ → ℚ) :=
  ⟨Real.cauchy, Real.ofCauchy, fun ⟨_⟩ => rfl, fun _ => rfl⟩

Real numbers as Cauchy sequence completion

Informal description

The real numbers $\mathbb{R}$ are isomorphic to the completion of the rational numbers $\mathbb{Q}$ under the standard absolute value, where the completion is constructed as equivalence classes of Cauchy sequences. More precisely, there exists a bijection between $\mathbb{R}$ and the space of Cauchy sequences of rational numbers modulo equivalence, where two sequences are equivalent if their difference tends to zero. This isomorphism preserves the algebraic and order structures of the real numbers.

Real.instZero instance

: Zero ℝ

Full source

instance : Zero ℝ :=
  ⟨zero⟩

Zero Element of Real Numbers

Informal description

The real numbers $\mathbb{R}$ have a zero element $0$.

Real.instOne instance

: One ℝ

Full source

instance : One ℝ :=
  ⟨one⟩

The Multiplicative Identity of Real Numbers

Informal description

The real numbers $\mathbb{R}$ have a canonical multiplicative identity element $1$.

Real.instAdd instance

: Add ℝ

Full source

instance : Add ℝ :=
  ⟨add⟩

Addition Operation on Real Numbers

Informal description

The real numbers $\mathbb{R}$ are equipped with a canonical addition operation.

Real.instNeg instance

: Neg ℝ

Full source

instance : Neg ℝ :=
  ⟨neg⟩

Negation Operation on Real Numbers

Informal description

The real numbers $\mathbb{R}$ have a negation operation.

Real.instMul instance

: Mul ℝ

Full source

instance : Mul ℝ :=
  ⟨mul⟩

Multiplication Operation on Real Numbers

Informal description

The real numbers $\mathbb{R}$ are equipped with a canonical multiplication operation.

Real.instSub instance

: Sub ℝ

Full source

instance : Sub ℝ :=
  ⟨fun a b => a + -b⟩

Subtraction Operation on Real Numbers

Informal description

The real numbers $\mathbb{R}$ are equipped with a canonical subtraction operation.

Real.instInv instance

: Inv ℝ

Full source

noncomputable instance : Inv ℝ :=
  ⟨inv'⟩

Inversion Operation on Real Numbers

Informal description

The real numbers $\mathbb{R}$ are equipped with a canonical inversion operation.

Real.ofCauchy_zero theorem

: (⟨0⟩ : ℝ) = 0

Full source

theorem ofCauchy_zero : (⟨0⟩ : ℝ) = 0 :=
  zero_def.symm

Zero Cauchy Sequence Yields Zero Real Number

Informal description

The real number constructed from the zero Cauchy sequence of rational numbers is equal to the zero element of the real numbers, i.e., $\langle 0 \rangle = 0$.

Real.ofCauchy_one theorem

: (⟨1⟩ : ℝ) = 1

Full source

theorem ofCauchy_one : (⟨1⟩ : ℝ) = 1 :=
  one_def.symm

Cauchy Construction Preserves Multiplicative Identity in Real Numbers

Informal description

The real number constructed from the Cauchy sequence representing the rational number $1$ is equal to the multiplicative identity $1$ in $\mathbb{R}$.

Real.ofCauchy_add theorem

(a b) : (⟨a + b⟩ : ℝ) = ⟨a⟩ + ⟨b⟩

Full source

theorem ofCauchy_add (a b) : (⟨a + b⟩ : ℝ) = ⟨a⟩ + ⟨b⟩ :=
  (add_def _ _).symm

Addition of Real Numbers via Cauchy Sequences

Informal description

For any two Cauchy sequences $a$ and $b$ of rational numbers, the real number constructed from their pointwise sum $\langle a + b \rangle$ is equal to the sum of the real numbers constructed from each sequence individually, i.e., $\langle a \rangle + \langle b \rangle$.

Real.ofCauchy_neg theorem

(a) : (⟨-a⟩ : ℝ) = -⟨a⟩

Full source

theorem ofCauchy_neg (a) : (⟨-a⟩ : ℝ) = -⟨a⟩ :=
  (neg_def _).symm

Negation Preserved Under Real Construction from Cauchy Sequences

Informal description

For any Cauchy sequence $a$ of rational numbers, the equivalence class of the negation of $a$ is equal to the negation of the equivalence class of $a$, i.e., $\langle -a \rangle = -\langle a \rangle$.

Real.ofCauchy_sub theorem

(a b) : (⟨a - b⟩ : ℝ) = ⟨a⟩ - ⟨b⟩

Full source

theorem ofCauchy_sub (a b) : (⟨a - b⟩ : ℝ) = ⟨a⟩ - ⟨b⟩ := by
  rw [sub_eq_add_neg, ofCauchy_add, ofCauchy_neg]
  rfl

Subtraction of Real Numbers via Cauchy Sequences

Informal description

For any two Cauchy sequences $a$ and $b$ of rational numbers, the real number constructed from their pointwise difference $\langle a - b \rangle$ is equal to the difference of the real numbers constructed from each sequence individually, i.e., $\langle a \rangle - \langle b \rangle$.

Real.ofCauchy_mul theorem

(a b) : (⟨a * b⟩ : ℝ) = ⟨a⟩ * ⟨b⟩

Full source

theorem ofCauchy_mul (a b) : (⟨a * b⟩ : ℝ) = ⟨a⟩ * ⟨b⟩ :=
  (mul_def _ _).symm

Multiplication of Real Numbers via Cauchy Sequences

Informal description

For any two Cauchy sequences $a$ and $b$ of rational numbers, the equivalence class of their pointwise product $a * b$ is equal to the product of their equivalence classes in the real numbers, i.e., $\langle a * b \rangle = \langle a \rangle \cdot \langle b \rangle$.

Real.ofCauchy_inv theorem

{f} : (⟨f⁻¹⟩ : ℝ) = ⟨f⟩⁻¹

Full source

theorem ofCauchy_inv {f} : (⟨f⁻¹⟩ : ℝ) = ⟨f⟩⟨f⟩⁻¹ :=
  show _ = inv' _ by rw [inv']

Inversion Commutes with Real Number Construction from Cauchy Sequences

Informal description

For any Cauchy sequence $f$ of rational numbers, the real number constructed from the pointwise inverse sequence $f^{-1}$ is equal to the multiplicative inverse of the real number constructed from $f$. In other words, the canonical map from Cauchy sequences to real numbers commutes with the inversion operation.

Real.cauchy_zero theorem

: (0 : ℝ).cauchy = 0

Full source

theorem cauchy_zero : (0 : ℝ).cauchy = 0 :=
  show zero.cauchy = 0 by rw [zero_def]

Cauchy Sequence Representation of Zero in Real Numbers

Informal description

The Cauchy sequence representing the real number $0$ is equal to the zero sequence of rational numbers, i.e., $(0 : \mathbb{R}).\text{cauchy} = 0$.

Real.cauchy_one theorem

: (1 : ℝ).cauchy = 1

Full source

theorem cauchy_one : (1 : ℝ).cauchy = 1 :=
  show one.cauchy = 1 by rw [one_def]

Cauchy Sequence Representation of One in Real Numbers

Informal description

The Cauchy sequence representing the real number $1$ is equal to the constant sequence of rational numbers with value $1$.

Real.cauchy_add theorem

: ∀ a b, (a + b : ℝ).cauchy = a.cauchy + b.cauchy

Full source

theorem cauchy_add : ∀ a b, (a + b : ℝ).cauchy = a.cauchy + b.cauchy
  | ⟨a⟩, ⟨b⟩ => show (add _ _).cauchy = _ by rw [add_def]

Cauchy Sequence Representation of Real Addition

Informal description

For any real numbers $a$ and $b$, the Cauchy sequence representing their sum $(a + b)$ is equal to the sum of their respective Cauchy sequences, i.e., $(a + b).\text{cauchy} = a.\text{cauchy} + b.\text{cauchy}$.

Real.cauchy_neg theorem

: ∀ a, (-a : ℝ).cauchy = -a.cauchy

Full source

theorem cauchy_neg : ∀ a, (-a : ℝ).cauchy = -a.cauchy
  | ⟨a⟩ => show (neg _).cauchy = _ by rw [neg_def]

Negation Preserves Cauchy Sequences in Real Numbers

Informal description

For any real number $a$, the Cauchy sequence representing $-a$ is equal to the negation of the Cauchy sequence representing $a$.

Real.cauchy_mul theorem

: ∀ a b, (a * b : ℝ).cauchy = a.cauchy * b.cauchy

Full source

theorem cauchy_mul : ∀ a b, (a * b : ℝ).cauchy = a.cauchy * b.cauchy
  | ⟨a⟩, ⟨b⟩ => show (mul _ _).cauchy = _ by rw [mul_def]

Multiplication Preserves Cauchy Sequences in Real Numbers

Informal description

For any two real numbers $a$ and $b$, the Cauchy sequence representing their product $a \cdot b$ is equal to the product of the Cauchy sequences representing $a$ and $b$.

Real.cauchy_sub theorem

: ∀ a b, (a - b : ℝ).cauchy = a.cauchy - b.cauchy

Full source

theorem cauchy_sub : ∀ a b, (a - b : ℝ).cauchy = a.cauchy - b.cauchy
  | ⟨a⟩, ⟨b⟩ => by
    rw [sub_eq_add_neg, ← cauchy_neg, ← cauchy_add]
    rfl

Subtraction Preserves Cauchy Sequences in Real Numbers

Informal description

For any real numbers $a$ and $b$, the Cauchy sequence representing their difference $a - b$ is equal to the difference of their respective Cauchy sequences, i.e., $(a - b).\text{cauchy} = a.\text{cauchy} - b.\text{cauchy}$.

Real.cauchy_inv theorem

: ∀ f, (f⁻¹ : ℝ).cauchy = f.cauchy⁻¹

Full source

theorem cauchy_inv : ∀ f, (f⁻¹ : ℝ).cauchy = f.cauchy⁻¹
  | ⟨f⟩ => show (inv' _).cauchy = _ by rw [inv']

Inversion Preserves Cauchy Sequences in Real Numbers

Informal description

For any real number $f$, the Cauchy sequence representing its multiplicative inverse $f^{-1}$ is equal to the multiplicative inverse of the Cauchy sequence representing $f$.

Real.instNatCast instance

: NatCast ℝ

Full source

instance instNatCast : NatCast ℝ where natCast n := ⟨n⟩

Natural Number Cast Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ have a canonical structure of a natural number cast, where natural numbers are embedded into $\mathbb{R}$ via the standard inclusion.

Real.instIntCast instance

: IntCast ℝ

Full source

instance instIntCast : IntCast ℝ where intCast z := ⟨z⟩

Integer Casting for Real Numbers

Informal description

The real numbers $\mathbb{R}$ have a canonical integer casting operation, which maps any integer to its corresponding real number.

Real.instNNRatCast instance

: NNRatCast ℝ

Full source

instance instNNRatCast : NNRatCast ℝ where nnratCast q := ⟨q⟩

Nonnegative Rational Cast Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ have a canonical structure of a nonnegative rational cast, which embeds the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ into $\mathbb{R}$.

Real.instRatCast instance

: RatCast ℝ

Full source

instance instRatCast : RatCast ℝ where ratCast q := ⟨q⟩

Rational Number Casting for Real Numbers

Informal description

The real numbers $\mathbb{R}$ have a canonical casting operation from the rational numbers $\mathbb{Q}$.

Real.ofCauchy_natCast theorem

(n : ℕ) : (⟨n⟩ : ℝ) = n

Full source

lemma ofCauchy_natCast (n : ℕ) : (⟨n⟩ : ℝ) = n := rfl

Natural Number Embedding in Real Numbers via Cauchy Sequences Preserves Equality

Informal description

For any natural number $n$, the real number obtained by embedding $n$ via the Cauchy sequence construction is equal to $n$ itself, i.e., $\langle n \rangle = n$.

Real.ofCauchy_intCast theorem

(z : ℤ) : (⟨z⟩ : ℝ) = z

Full source

lemma ofCauchy_intCast (z : ℤ) : (⟨z⟩ : ℝ) = z := rfl

Integer Casting Preserves Value in Real Numbers

Informal description

For any integer $z \in \mathbb{Z}$, the real number obtained by casting $z$ to $\mathbb{R}$ via the Cauchy sequence construction is equal to $z$ itself, i.e., $\langle z \rangle = z$.

Real.ofCauchy_nnratCast theorem

(q : ℚ≥0) : (⟨q⟩ : ℝ) = q

Full source

lemma ofCauchy_nnratCast (q : ℚ≥0) : (⟨q⟩ : ℝ) = q := rfl

Embedding of Nonnegative Rationals into Reals Preserves Equality

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the real number obtained by embedding $q$ into $\mathbb{R}$ via the Cauchy sequence construction is equal to $q$ itself, i.e., $\langle q \rangle = q$.

Real.ofCauchy_ratCast theorem

(q : ℚ) : (⟨q⟩ : ℝ) = q

Full source

lemma ofCauchy_ratCast (q : ℚ) : (⟨q⟩ : ℝ) = q := rfl

Embedding of Rational Numbers into Real Numbers Preserves Equality

Informal description

For any rational number $q \in \mathbb{Q}$, the real number obtained by embedding $q$ into $\mathbb{R}$ via the Cauchy sequence construction is equal to $q$ itself, i.e., $\langle q \rangle = q$.

Real.cauchy_natCast theorem

(n : ℕ) : (n : ℝ).cauchy = n

Full source

lemma cauchy_natCast (n : ℕ) : (n : ℝ).cauchy = n := rfl

Natural Number Embedding into Reals Preserves Value

Informal description

For any natural number $n$, the Cauchy sequence representation of $n$ as a real number is equal to the natural number $n$ itself.

Real.cauchy_intCast theorem

(z : ℤ) : (z : ℝ).cauchy = z

Full source

lemma cauchy_intCast (z : ℤ) : (z : ℝ).cauchy = z := rfl

Integer Casting Preserves Cauchy Sequence Representation

Informal description

For any integer $z \in \mathbb{Z}$, the Cauchy sequence representation of the real number obtained by casting $z$ to $\mathbb{R}$ is equal to the constant sequence with value $z$.

Real.cauchy_nnratCast theorem

(q : ℚ≥0) : (q : ℝ).cauchy = q

Full source

lemma cauchy_nnratCast (q : ℚ≥0) : (q : ℝ).cauchy = q := rfl

Nonnegative Rational Cast Preserves Cauchy Sequence Representation

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the Cauchy sequence representation of $q$ as a real number is equal to $q$ itself.

Real.cauchy_ratCast theorem

(q : ℚ) : (q : ℝ).cauchy = q

Full source

lemma cauchy_ratCast (q : ℚ) : (q : ℝ).cauchy = q := rfl

Rational Casting Preserves Cauchy Sequence Representation

Informal description

For any rational number $q \in \mathbb{Q}$, the Cauchy sequence representation of the real number obtained by casting $q$ to $\mathbb{R}$ is equal to the constant sequence with value $q$.

Real.commRing instance

: CommRing ℝ

Full source

instance commRing : CommRing ℝ where
  natCast n := ⟨n⟩
  intCast z := ⟨z⟩
  zero := (0 : ℝ)
  one := (1 : ℝ)
  mul := (· * ·)
  add := (· + ·)
  neg := @Neg.neg ℝ _
  sub := @Sub.sub ℝ _
  npow := @npowRec ℝ ⟨1⟩ ⟨(· * ·)⟩
  nsmul := @nsmulRec ℝ ⟨0⟩ ⟨(· + ·)⟩
  zsmul := @zsmulRec ℝ ⟨0⟩ ⟨(· + ·)⟩ ⟨@Neg.neg ℝ _⟩ (@nsmulRec ℝ ⟨0⟩ ⟨(· + ·)⟩)
  add_zero a := by apply ext_cauchy; simp [cauchy_add, cauchy_zero]
  zero_add a := by apply ext_cauchy; simp [cauchy_add, cauchy_zero]
  add_comm a b := by apply ext_cauchy; simp only [cauchy_add, add_comm]
  add_assoc a b c := by apply ext_cauchy; simp only [cauchy_add, add_assoc]
  mul_zero a := by apply ext_cauchy; simp [cauchy_mul, cauchy_zero]
  zero_mul a := by apply ext_cauchy; simp [cauchy_mul, cauchy_zero]
  mul_one a := by apply ext_cauchy; simp [cauchy_mul, cauchy_one]
  one_mul a := by apply ext_cauchy; simp [cauchy_mul, cauchy_one]
  mul_comm a b := by apply ext_cauchy; simp only [cauchy_mul, mul_comm]
  mul_assoc a b c := by apply ext_cauchy; simp only [cauchy_mul, mul_assoc]
  left_distrib a b c := by apply ext_cauchy; simp only [cauchy_add, cauchy_mul, mul_add]
  right_distrib a b c := by apply ext_cauchy; simp only [cauchy_add, cauchy_mul, add_mul]
  neg_add_cancel a := by apply ext_cauchy; simp [cauchy_add, cauchy_neg, cauchy_zero]
  natCast_zero := by apply ext_cauchy; simp [cauchy_zero]
  natCast_succ n := by apply ext_cauchy; simp [cauchy_one, cauchy_add]
  intCast_negSucc z := by apply ext_cauchy; simp [cauchy_neg, cauchy_natCast]

The Commutative Ring Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a commutative ring.

Real.ringEquivCauchy definition

: ℝ ≃+* CauSeq.Completion.Cauchy (abs : ℚ → ℚ)

Full source

/-- `Real.equivCauchy` as a ring equivalence. -/
@[simps]
def ringEquivCauchy : ℝℝ ≃+* CauSeq.Completion.Cauchy (abs : ℚ → ℚ) :=
  { equivCauchy with
    toFun := cauchy
    invFun := ofCauchy
    map_add' := cauchy_add
    map_mul' := cauchy_mul }

Ring Equivalence Between Real Numbers and Cauchy Completion of Rationals

Informal description

The ring equivalence between the real numbers $\mathbb{R}$ and the completion of the rational numbers $\mathbb{Q}$ under the standard absolute value, where the completion is constructed as equivalence classes of Cauchy sequences. This equivalence preserves both the additive and multiplicative structures, meaning that for any real numbers $a$ and $b$, the following hold: 1. The Cauchy sequence representing $a + b$ is equal to the sum of the Cauchy sequences representing $a$ and $b$. 2. The Cauchy sequence representing $a \cdot b$ is equal to the product of the Cauchy sequences representing $a$ and $b$. The equivalence is given by the bijection $\text{cauchy} : \mathbb{R} \to \text{Cauchy}(\mathbb{Q}, \text{abs})$ and its inverse $\text{ofCauchy} : \text{Cauchy}(\mathbb{Q}, \text{abs}) \to \mathbb{R}$.

Real.instRing instance

: Ring ℝ

Full source

instance instRing : Ring ℝ := by infer_instance

The Ring Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a ring.

Real.instCommSemiring instance

: CommSemiring ℝ

Full source

instance : CommSemiring ℝ := by infer_instance

The Commutative Semiring Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a commutative semiring.

Real.semiring instance

: Semiring ℝ

Full source

instance semiring : Semiring ℝ := by infer_instance

The Semiring Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a semiring.

Real.instCommMonoidWithZero instance

: CommMonoidWithZero ℝ

Full source

instance : CommMonoidWithZero ℝ := by infer_instance

The Commutative Monoid with Zero Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a commutative monoid with zero under multiplication.

Real.instMonoidWithZero instance

: MonoidWithZero ℝ

Full source

instance : MonoidWithZero ℝ := by infer_instance

The Monoid with Zero Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a monoid with zero under multiplication.

Real.instAddCommGroup instance

: AddCommGroup ℝ

Full source

instance : AddCommGroup ℝ := by infer_instance

The Additive Commutative Group Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form an additive commutative group.

Real.instAddGroup instance

: AddGroup ℝ

Full source

instance : AddGroup ℝ := by infer_instance

The Additive Group Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form an additive group.

Real.instAddCommMonoid instance

: AddCommMonoid ℝ

Full source

instance : AddCommMonoid ℝ := by infer_instance

Additive Commutative Monoid Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form an additive commutative monoid.

Real.instAddMonoid instance

: AddMonoid ℝ

Full source

instance : AddMonoid ℝ := by infer_instance

Additive Monoid Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form an additive monoid.

Real.instAddLeftCancelSemigroup instance

: AddLeftCancelSemigroup ℝ

Full source

instance : AddLeftCancelSemigroup ℝ := by infer_instance

Additive Left Cancellative Semigroup Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form an additive left cancellative semigroup.

Real.instAddRightCancelSemigroup instance

: AddRightCancelSemigroup ℝ

Full source

instance : AddRightCancelSemigroup ℝ := by infer_instance

Right Cancellation Property of Addition in Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a right-cancellative additive semigroup. That is, for any $a, b, c \in \mathbb{R}$, if $a + b = a + c$, then $b = c$.

Real.instAddCommSemigroup instance

: AddCommSemigroup ℝ

Full source

instance : AddCommSemigroup ℝ := by infer_instance

Additive Commutative Semigroup Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form an additive commutative semigroup.

Real.instAddSemigroup instance

: AddSemigroup ℝ

Full source

instance : AddSemigroup ℝ := by infer_instance

The Additive Semigroup Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form an additive semigroup.

Real.instCommMonoid instance

: CommMonoid ℝ

Full source

instance : CommMonoid ℝ := by infer_instance

The Commutative Monoid Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a commutative monoid.

Real.instMonoid instance

: Monoid ℝ

Full source

instance : Monoid ℝ := by infer_instance

The Monoid Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a monoid under multiplication.

Real.instCommSemigroup instance

: CommSemigroup ℝ

Full source

instance : CommSemigroup ℝ := by infer_instance

The Commutative Semigroup Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a commutative semigroup under multiplication.

Real.instSemigroup instance

: Semigroup ℝ

Full source

instance : Semigroup ℝ := by infer_instance

Semigroup Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a semigroup under multiplication.

Real.instInhabited instance

: Inhabited ℝ

Full source

instance : Inhabited ℝ :=
  ⟨0⟩

Real Numbers are Inhabited

Informal description

The real numbers $\mathbb{R}$ have a canonical inhabited instance, meaning there exists a default element in $\mathbb{R}$.

Real.mk definition

(x : CauSeq ℚ abs) : ℝ

Full source

/-- Make a real number from a Cauchy sequence of rationals (by taking the equivalence class). -/
def mk (x : CauSeq ℚ abs) : ℝ :=
  ⟨CauSeq.Completion.mk x⟩

Construction of real numbers from Cauchy sequences of rationals

Informal description

Given a Cauchy sequence $x$ of rational numbers (with respect to the absolute value metric), the function constructs a real number as the equivalence class of $x$ under the equivalence relation of being eventually equal.

Real.mk_eq theorem

{f g : CauSeq ℚ abs} : mk f = mk g ↔ f ≈ g

Full source

theorem mk_eq {f g : CauSeq ℚ abs} : mkmk f = mk g ↔ f ≈ g :=
  ext_cauchy_iff.trans CauSeq.Completion.mk_eq

Equality of Real Numbers via Cauchy Sequence Equivalence

Informal description

For any two Cauchy sequences $f$ and $g$ of rational numbers (with respect to the absolute value metric), the real numbers constructed from them are equal if and only if the sequences are eventually equal, i.e., $\text{mk}(f) = \text{mk}(g) \leftrightarrow f \approx g$.

Real.instLT instance

: LT ℝ

Full source

instance : LT ℝ :=
  ⟨lt⟩

The Linear Order Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ are equipped with a canonical linear order structure.

Real.lt_cauchy theorem

{f g} : (⟨⟦f⟧⟩ : ℝ) < ⟨⟦g⟧⟩ ↔ f < g

Full source

theorem lt_cauchy {f g} : (⟨⟦f⟧⟩ : ℝ) < ⟨⟦g⟧⟩ ↔ f < g :=
  show ltlt _ _ ↔ _ by rw [lt_def]; rfl

Order Correspondence Between Real Numbers and Their Cauchy Sequence Representatives

Informal description

For any two Cauchy sequences $f$ and $g$ of rational numbers, the real number represented by the equivalence class of $f$ is less than the real number represented by the equivalence class of $g$ if and only if $f$ is less than $g$ in the sense of Cauchy sequences.

Real.mk_lt theorem

{f g : CauSeq ℚ abs} : mk f < mk g ↔ f < g

Full source

@[simp]
theorem mk_lt {f g : CauSeq ℚ abs} : mkmk f < mk g ↔ f < g :=
  lt_cauchy

Order Correspondence Between Real Numbers and Their Cauchy Sequence Representatives

Informal description

For any two Cauchy sequences $f$ and $g$ of rational numbers (with respect to the absolute value metric), the real number constructed from $f$ is less than the real number constructed from $g$ if and only if $f$ is less than $g$ as Cauchy sequences.

Real.mk_zero theorem

: mk 0 = 0

Full source

theorem mk_zero : mk 0 = 0 := by rw [← ofCauchy_zero]; rfl

Zero Cauchy Sequence Yields Zero Real Number

Informal description

The real number constructed from the zero Cauchy sequence of rational numbers is equal to the zero element of the real numbers, i.e., $\langle 0 \rangle = 0$.

Real.mk_one theorem

: mk 1 = 1

Full source

theorem mk_one : mk 1 = 1 := by rw [← ofCauchy_one]; rfl

Cauchy Construction Preserves One: $\langle 1 \rangle = 1$

Informal description

The real number constructed from the constant Cauchy sequence of rational numbers equal to 1 is equal to the multiplicative identity $1$ in $\mathbb{R}$, i.e., $\langle 1 \rangle = 1$.

Real.mk_add theorem

{f g : CauSeq ℚ abs} : mk (f + g) = mk f + mk g

Full source

theorem mk_add {f g : CauSeq ℚ abs} : mk (f + g) = mk f + mk g := by simp [mk, ← ofCauchy_add]

Additivity of Real Number Construction from Cauchy Sequences

Informal description

For any two Cauchy sequences $f$ and $g$ of rational numbers (with respect to the absolute value metric), the real number constructed from their sum is equal to the sum of the real numbers constructed from each sequence individually. That is, $\langle f + g \rangle = \langle f \rangle + \langle g \rangle$.

Real.mk_mul theorem

{f g : CauSeq ℚ abs} : mk (f * g) = mk f * mk g

Full source

theorem mk_mul {f g : CauSeq ℚ abs} : mk (f * g) = mk f * mk g := by simp [mk, ← ofCauchy_mul]

Multiplicativity of Real Number Construction from Cauchy Sequences

Informal description

For any two Cauchy sequences $f$ and $g$ of rational numbers (with respect to the absolute value metric), the real number constructed from their product is equal to the product of the real numbers constructed from each sequence individually. That is, $\langle f \cdot g \rangle = \langle f \rangle \cdot \langle g \rangle$.

Real.mk_neg theorem

{f : CauSeq ℚ abs} : mk (-f) = -mk f

Full source

theorem mk_neg {f : CauSeq ℚ abs} : mk (-f) = -mk f := by simp [mk, ← ofCauchy_neg]

Negation Commutes with Real Number Construction from Cauchy Sequences

Informal description

For any Cauchy sequence $f$ of rational numbers (with respect to the absolute value metric), the real number constructed from the negation of $f$ is equal to the negation of the real number constructed from $f$. That is, $\langle -f \rangle = -\langle f \rangle$.

Real.mk_pos theorem

{f : CauSeq ℚ abs} : 0 < mk f ↔ Pos f

Full source

@[simp]
theorem mk_pos {f : CauSeq ℚ abs} : 0 < mk f ↔ Pos f := by
  rw [← mk_zero, mk_lt]
  exact iff_of_eq (congr_arg Pos (sub_zero f))

Positivity Correspondence Between Real Numbers and Their Cauchy Sequence Representatives

Informal description

For any Cauchy sequence $f$ of rational numbers (with respect to the absolute value metric), the real number constructed from $f$ is positive if and only if $f$ is eventually positive (i.e., there exists an index beyond which all terms of $f$ are positive). In other words, $0 < \langle f \rangle$ if and only if $f$ is a positive Cauchy sequence.

Real.mk_const theorem

{x : ℚ} : mk (const abs x) = x

Full source

lemma mk_const {x : ℚ} : mk (const abs x) = x := rfl

Real Construction from Constant Rational Sequence Preserves Value

Informal description

For any rational number $x$, the real number constructed from the constant Cauchy sequence (with value $x$) is equal to $x$ itself, i.e., $\langle x \rangle = x$.

Real.instLE instance

: LE ℝ

Full source

instance : LE ℝ :=
  ⟨le⟩

The Linear Order Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ are equipped with a canonical linear order structure $\leq$.

Real.mk_le theorem

{f g : CauSeq ℚ abs} : mk f ≤ mk g ↔ f ≤ g

Full source

@[simp]
theorem mk_le {f g : CauSeq ℚ abs} : mkmk f ≤ mk g ↔ f ≤ g := by
  simp only [le_def', mk_lt, mk_eq]; rfl

Order Comparison of Real Numbers via Cauchy Sequences

Informal description

For any two Cauchy sequences $f$ and $g$ of rational numbers (with respect to the absolute value metric), the real number constructed from $f$ is less than or equal to the real number constructed from $g$ if and only if $f$ is eventually less than or equal to $g$ pointwise.

Real.ind_mk theorem

{C : Real → Prop} (x : Real) (h : ∀ y, C (mk y)) : C x

Full source

@[elab_as_elim]
protected theorem ind_mk {C : Real → Prop} (x : Real) (h : ∀ y, C (mk y)) : C x := by
  obtain ⟨x⟩ := x
  induction x using Quot.induction_on
  exact h _

Induction Principle for Real Numbers via Cauchy Sequences

Informal description

Let $C$ be a predicate on real numbers. For any real number $x$ constructed from a Cauchy sequence of rationals, if $C$ holds for all real numbers constructed from any Cauchy sequence $y$, then $C$ holds for $x$.

Real.add_lt_add_iff_left theorem

{a b : ℝ} (c : ℝ) : c + a < c + b ↔ a < b

Full source

theorem add_lt_add_iff_left {a b : ℝ} (c : ℝ) : c + a < c + b ↔ a < b := by
  induction a using Real.ind_mk
  induction b using Real.ind_mk
  induction c using Real.ind_mk
  simp only [mk_lt, ← mk_add]
  show PosPos _ ↔ Pos _; rw [add_sub_add_left_eq_sub]

Left Addition Preserves Strict Inequality in Real Numbers

Informal description

For any real numbers $a$, $b$, and $c$, the inequality $c + a < c + b$ holds if and only if $a < b$.

Real.partialOrder instance

: PartialOrder ℝ

Full source

instance partialOrder : PartialOrder ℝ where
  le := (· ≤ ·)
  lt := (· < ·)
  lt_iff_le_not_le a b := by
    induction a using Real.ind_mk
    induction b using Real.ind_mk
    simpa using lt_iff_le_not_le
  le_refl a := by
    induction a using Real.ind_mk
    rw [mk_le]
  le_trans a b c := by
    induction a using Real.ind_mk
    induction b using Real.ind_mk
    induction c using Real.ind_mk
    simpa using le_trans
  le_antisymm a b := by
    induction a using Real.ind_mk
    induction b using Real.ind_mk
    simpa [mk_eq] using CauSeq.le_antisymm

The Partial Order Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ are equipped with a canonical partial order structure.

Real.instPreorder instance

: Preorder ℝ

Full source

instance : Preorder ℝ := by infer_instance

The Preorder Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ are equipped with a canonical preorder structure.

Real.ratCast_lt theorem

{x y : ℚ} : (x : ℝ) < (y : ℝ) ↔ x < y

Full source

theorem ratCast_lt {x y : ℚ} : (x : ℝ) < (y : ℝ) ↔ x < y := by
  rw [← mk_const, ← mk_const, mk_lt]
  exact const_lt

Preservation of Order under Rational-to-Real Casting: $(x : \mathbb{R}) < (y : \mathbb{R}) \leftrightarrow x < y$

Informal description

For any two rational numbers $x$ and $y$, the real number obtained by casting $x$ is less than the real number obtained by casting $y$ if and only if $x$ is less than $y$ in the rational numbers. In other words, the order relation is preserved when casting from $\mathbb{Q}$ to $\mathbb{R}$.

Real.zero_lt_one theorem

: (0 : ℝ) < 1

Full source

protected theorem zero_lt_one : (0 : ℝ) < 1 := by
  convert ratCast_lt.2 zero_lt_one <;> simp [← ofCauchy_ratCast, ofCauchy_one, ofCauchy_zero]

Strict inequality: $0 < 1$ in real numbers

Informal description

The real number $0$ is strictly less than the real number $1$, i.e., $0 < 1$.

Real.fact_zero_lt_one theorem

: Fact ((0 : ℝ) < 1)

Full source

protected theorem fact_zero_lt_one : Fact ((0 : ℝ) < 1) :=
  ⟨Real.zero_lt_one⟩

Fact: $0 < 1$ in Real Numbers

Informal description

The real number $0$ is strictly less than the real number $1$, i.e., $0 < 1$, and this fact is wrapped in the `Fact` structure for implicit use in type class resolution.

Real.instNontrivial instance

: Nontrivial ℝ

Full source

instance instNontrivial : Nontrivial ℝ where
  exists_pair_ne := ⟨0, 1, Real.zero_lt_one.ne⟩

Nontriviality of Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a nontrivial type, meaning they contain at least two distinct elements.

Real.instZeroLEOneClass instance

: ZeroLEOneClass ℝ

Full source

instance instZeroLEOneClass : ZeroLEOneClass ℝ where
  zero_le_one := le_of_lt Real.zero_lt_one

Nonnegativity of One in Real Numbers

Informal description

The real numbers $\mathbb{R}$ satisfy the inequality $0 \leq 1$ with respect to their canonical order and algebraic structure.

Real.instIsOrderedAddMonoid instance

: IsOrderedAddMonoid ℝ

Full source

instance instIsOrderedAddMonoid : IsOrderedAddMonoid ℝ where
  add_le_add_left := by
    simp only [le_iff_eq_or_lt]
    rintro a b ⟨rfl, h⟩
    · simp only [lt_self_iff_false, or_false, forall_const]
    · exact fun c => Or.inr ((add_lt_add_iff_left c).2 ‹_›)

Real Numbers as an Ordered Additive Monoid

Informal description

The real numbers $\mathbb{R}$ form an ordered additive monoid, meaning they are equipped with an addition operation that is commutative and associative, and a partial order such that addition is monotone with respect to the order. That is, for any real numbers $a, b, c$, if $a \leq b$ then $a + c \leq b + c$ and $c + a \leq c + b$.

Real.instIsStrictOrderedRing instance

: IsStrictOrderedRing ℝ

Full source

instance instIsStrictOrderedRing : IsStrictOrderedRing ℝ :=
  .of_mul_pos fun a b ↦ by
    induction' a using Real.ind_mk with a
    induction' b using Real.ind_mk with b
    simpa only [mk_lt, mk_pos, ← mk_mul] using CauSeq.mul_pos

The Strict Ordered Ring Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a strict ordered ring. That is, they satisfy: 1. Addition is strictly monotone: $a < b$ implies $a + c < b + c$ for all $c \in \mathbb{R}$ 2. Multiplication by positive elements is strictly monotone: if $0 < a$ and $b < c$ then $a \cdot b < a \cdot c$ 3. The inequality $0 \leq 1$ holds 4. The ring is nontrivial ($0 \neq 1$)

Real.instIsOrderedRing instance

: IsOrderedRing ℝ

Full source

instance instIsOrderedRing : IsOrderedRing ℝ :=
  inferInstance

The Ordered Ring Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form an ordered ring. That is, they satisfy: 1. Addition is monotone: $a \leq b$ implies $a + c \leq b + c$ for all $c \in \mathbb{R}$ 2. Multiplication by nonnegative elements is monotone: if $0 \leq a$ and $b \leq c$ then $a \cdot b \leq a \cdot c$ 3. The inequality $0 \leq 1$ holds

Real.instIsOrderedCancelAddMonoid instance

: IsOrderedCancelAddMonoid ℝ

Full source

instance instIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid ℝ :=
  inferInstance

Ordered Cancellative Additive Monoid Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form an ordered cancellative additive monoid. That is, the addition operation is cancellative (for any $a, b, c \in \mathbb{R}$, if $a + b = a + c$ then $b = c$) and monotone (for any $a, b, c \in \mathbb{R}$, if $a \leq b$ then $a + c \leq b + c$).

Real.instMax instance

: Max ℝ

Full source

instance : Max ℝ :=
  ⟨sup⟩

The Maximum Operation on Real Numbers

Informal description

The real numbers $\mathbb{R}$ have a canonical maximum operation $\max$ defined on them.

Real.ofCauchy_sup theorem

(a b) : (⟨⟦a ⊔ b⟧⟩ : ℝ) = ⟨⟦a⟧⟩ ⊔ ⟨⟦b⟧⟩

Full source

theorem ofCauchy_sup (a b) : (⟨⟦a ⊔ b⟧⟩ : ℝ) = ⟨⟦a⟧⟩⟨⟦a⟧⟩ ⊔ ⟨⟦b⟧⟩ :=
  show _ = sup _ _ by
    rw [sup_def]
    rfl

Supremum of Real Numbers Constructed from Cauchy Sequences

Informal description

For any two Cauchy sequences $a$ and $b$ of rational numbers, the real number constructed from the supremum of $a$ and $b$ is equal to the supremum of the real numbers constructed from $a$ and $b$ individually. That is, $\langle [a \sqcup b] \rangle = \langle [a] \rangle \sqcup \langle [b] \rangle$, where $\langle \cdot \rangle$ denotes the construction of a real number from an equivalence class of Cauchy sequences and $\sqcup$ denotes the supremum operation.

Real.mk_sup theorem

(a b) : (mk (a ⊔ b) : ℝ) = mk a ⊔ mk b

Full source

@[simp]
theorem mk_sup (a b) : (mk (a ⊔ b) : ℝ) = mkmk a ⊔ mk b :=
  ofCauchy_sup _ _

Supremum of Real Numbers Constructed from Cauchy Sequences

Informal description

For any two Cauchy sequences $a$ and $b$ of rational numbers, the real number constructed from the supremum of $a$ and $b$ is equal to the supremum of the real numbers constructed from $a$ and $b$ individually. That is, $\text{mk}(a \sqcup b) = \text{mk}(a) \sqcup \text{mk}(b)$, where $\text{mk}$ denotes the construction of a real number from a Cauchy sequence and $\sqcup$ denotes the supremum operation.

Real.instMin instance

: Min ℝ

Full source

instance : Min ℝ :=
  ⟨inf⟩

Minimum Operation on Real Numbers

Informal description

The real numbers $\mathbb{R}$ have a canonical minimum operation $\min$ defined on them.

Real.ofCauchy_inf theorem

(a b) : (⟨⟦a ⊓ b⟧⟩ : ℝ) = ⟨⟦a⟧⟩ ⊓ ⟨⟦b⟧⟩

Full source

theorem ofCauchy_inf (a b) : (⟨⟦a ⊓ b⟧⟩ : ℝ) = ⟨⟦a⟧⟩⟨⟦a⟧⟩ ⊓ ⟨⟦b⟧⟩ :=
  show _ = inf _ _ by
    rw [inf_def]
    rfl

Minimum Operation Preserved Under Real Construction from Cauchy Sequences

Informal description

For any two Cauchy sequences $a$ and $b$ of rational numbers, the real number constructed from the equivalence class of the pointwise minimum sequence $a \sqcap b$ is equal to the minimum of the real numbers constructed from the equivalence classes of $a$ and $b$ respectively. In other words, if $\mathbb{R}$ is constructed as equivalence classes of Cauchy sequences, then $\langle [a \sqcap b] \rangle = \langle [a] \rangle \sqcap \langle [b] \rangle$.

Real.mk_inf theorem

(a b) : (mk (a ⊓ b) : ℝ) = mk a ⊓ mk b

Full source

@[simp]
theorem mk_inf (a b) : (mk (a ⊓ b) : ℝ) = mkmk a ⊓ mk b :=
  ofCauchy_inf _ _

Minimum Operation Preserved Under Real Construction from Cauchy Sequences

Informal description

For any two Cauchy sequences $a$ and $b$ of rational numbers, the real number constructed from the pointwise minimum sequence $a \sqcap b$ is equal to the minimum of the real numbers constructed from $a$ and $b$ individually. That is, $\text{mk}(a \sqcap b) = \text{mk}(a) \sqcap \text{mk}(b)$.

Real.instDistribLattice instance

: DistribLattice ℝ

Full source

instance : DistribLattice ℝ :=
  { Real.partialOrder with
    sup := (· ⊔ ·)
    le := (· ≤ ·)
    le_sup_left := by
      intros a b
      induction a using Real.ind_mk
      induction b using Real.ind_mk
      dsimp only; rw [← mk_sup, mk_le]
      exact CauSeq.le_sup_left
    le_sup_right := by
      intros a b
      induction a using Real.ind_mk
      induction b using Real.ind_mk
      dsimp only; rw [← mk_sup, mk_le]
      exact CauSeq.le_sup_right
    sup_le := by
      intros a b c
      induction a using Real.ind_mk
      induction b using Real.ind_mk
      induction c using Real.ind_mk
      simp_rw [← mk_sup, mk_le]
      exact CauSeq.sup_le
    inf := (· ⊓ ·)
    inf_le_left := by
      intros a b
      induction a using Real.ind_mk
      induction b using Real.ind_mk
      dsimp only; rw [← mk_inf, mk_le]
      exact CauSeq.inf_le_left
    inf_le_right := by
      intros a b
      induction a using Real.ind_mk
      induction b using Real.ind_mk
      dsimp only; rw [← mk_inf, mk_le]
      exact CauSeq.inf_le_right
    le_inf := by
      intros a b c
      induction a using Real.ind_mk
      induction b using Real.ind_mk
      induction c using Real.ind_mk
      simp_rw [← mk_inf, mk_le]
      exact CauSeq.le_inf
    le_sup_inf := by
      intros a b c
      induction a using Real.ind_mk
      induction b using Real.ind_mk
      induction c using Real.ind_mk
      apply Eq.le
      simp only [← mk_sup, ← mk_inf]
      exact congr_arg mk (CauSeq.sup_inf_distrib_left ..).symm }

The Distributive Lattice Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a distributive lattice with respect to their canonical order structure, where the meet and join operations are given by the minimum and maximum functions respectively.

Real.lattice instance

: Lattice ℝ

Full source

instance lattice : Lattice ℝ :=
  inferInstance

The Lattice Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a lattice with respect to their canonical order structure, where the meet and join operations are given by the minimum and maximum functions respectively.

Real.instSemilatticeInf instance

: SemilatticeInf ℝ

Full source

instance : SemilatticeInf ℝ :=
  inferInstance

The Meet-Semilattice Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a meet-semilattice with respect to their canonical order structure, where the meet operation is given by the minimum function.

Real.instSemilatticeSup instance

: SemilatticeSup ℝ

Full source

instance : SemilatticeSup ℝ :=
  inferInstance

Join-Semilattice Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a join-semilattice with respect to their canonical order, where the join operation is given by the maximum function.

Real.leTotal_R instance

: IsTotal ℝ (· ≤ ·)

Full source

instance leTotal_R : IsTotal ℝ (· ≤ ·) :=
  ⟨by
    intros a b
    induction a using Real.ind_mk
    induction b using Real.ind_mk
    simpa using CauSeq.le_total ..⟩

Total Order on Real Numbers

Informal description

The real numbers $\mathbb{R}$ are totally ordered with respect to the canonical order relation $\leq$.

Real.linearOrder instance

: LinearOrder ℝ

Full source

noncomputable instance linearOrder : LinearOrder ℝ :=
  Lattice.toLinearOrder ℝ

Linear Order Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a linear order with respect to their canonical order relation $\leq$.

Real.instIsDomain instance

: IsDomain ℝ

Full source

instance : IsDomain ℝ := IsStrictOrderedRing.isDomain

Real Numbers as a Domain

Informal description

The real numbers $\mathbb{R}$ form a domain, meaning they are a nontrivial semiring with no zero divisors.

Real.instDivInvMonoid instance

: DivInvMonoid ℝ

Full source

noncomputable instance instDivInvMonoid : DivInvMonoid ℝ where

The Division Monoid Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a division monoid, meaning they are equipped with a division operation and an inversion operation that satisfy the axioms of a division monoid.

Real.ofCauchy_div theorem

(f g) : (⟨f / g⟩ : ℝ) = (⟨f⟩ : ℝ) / (⟨g⟩ : ℝ)

Full source

lemma ofCauchy_div (f g) : (⟨f / g⟩ : ℝ) = (⟨f⟩ : ℝ) / (⟨g⟩ : ℝ) := by
  simp_rw [div_eq_mul_inv, ofCauchy_mul, ofCauchy_inv]

Division of Real Numbers via Cauchy Sequences

Informal description

For any two Cauchy sequences $f$ and $g$ of rational numbers, the equivalence class of their pointwise quotient $f / g$ is equal to the quotient of their equivalence classes in the real numbers, i.e., $\langle f / g \rangle = \langle f \rangle / \langle g \rangle$.

Real.field instance

: Field ℝ

Full source

noncomputable instance field : Field ℝ where
  mul_inv_cancel := by
    rintro ⟨a⟩ h
    rw [mul_comm]
    simp only [← ofCauchy_inv, ← ofCauchy_mul, ← ofCauchy_one, ← ofCauchy_zero,
      Ne, ofCauchy.injEq] at *
    exact CauSeq.Completion.inv_mul_cancel h
  inv_zero := by simp [← ofCauchy_zero, ← ofCauchy_inv]
  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl
  qsmul := _
  qsmul_def := fun _ _ => rfl
  nnratCast_def q := by
    rw [← ofCauchy_nnratCast, NNRat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_natCast]
  ratCast_def q := by
    rw [← ofCauchy_ratCast, Rat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_intCast]

The Field Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a field.

Real.instDivisionRing instance

: DivisionRing ℝ

Full source

noncomputable instance : DivisionRing ℝ := by infer_instance

The Division Ring Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a division ring.

Real.decidableLT instance

(a b : ℝ) : Decidable (a < b)

Full source

noncomputable instance decidableLT (a b : ℝ) : Decidable (a < b) := by infer_instance

Decidability of Order on Real Numbers

Informal description

For any two real numbers $a$ and $b$, the proposition $a < b$ is decidable.

Real.decidableLE instance

(a b : ℝ) : Decidable (a ≤ b)

Full source

noncomputable instance decidableLE (a b : ℝ) : Decidable (a ≤ b) := by infer_instance

Decidability of the Order Relation on Real Numbers

Informal description

For any two real numbers $a$ and $b$, the inequality $a \leq b$ is decidable.

Real.decidableEq instance

(a b : ℝ) : Decidable (a = b)

Full source

noncomputable instance decidableEq (a b : ℝ) : Decidable (a = b) := by infer_instance

Decidability of Equality for Real Numbers

Informal description

For any two real numbers $a$ and $b$, the equality $a = b$ is decidable.

Real.instRepr instance

: Repr ℝ

Full source

/-- Show an underlying cauchy sequence for real numbers.

The representative chosen is the one passed in the VM to `Quot.mk`, so two cauchy sequences
converging to the same number may be printed differently.
-/
unsafe instance : Repr ℝ where
  reprPrec r p := Repr.addAppParen ("Real.ofCauchy " ++ repr r.cauchy) p

Representation of Real Numbers as Cauchy Sequences

Informal description

The real numbers $\mathbb{R}$ have a canonical representation as equivalence classes of Cauchy sequences of rational numbers.

Real.le_mk_of_forall_le theorem

{f : CauSeq ℚ abs} : (∃ i, ∀ j ≥ i, x ≤ f j) → x ≤ mk f

Full source

theorem le_mk_of_forall_le {f : CauSeq ℚ abs} : (∃ i, ∀ j ≥ i, x ≤ f j) → x ≤ mk f := by
  intro h
  induction x using Real.ind_mk
  apply le_of_not_lt
  rw [mk_lt]
  rintro ⟨K, K0, hK⟩
  obtain ⟨i, H⟩ := exists_forall_ge_and h (exists_forall_ge_and hK (f.cauchy₃ <| half_pos K0))
  apply not_lt_of_le (H _ le_rfl).1
  rw [← mk_const, mk_lt]
  refine ⟨_, half_pos K0, i, fun j ij => ?_⟩
  have := add_le_add (H _ ij).2.1 (le_of_lt (abs_lt.1 <| (H _ le_rfl).2.2 _ ij).1)
  rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this

Comparison of Real Number with Limit of Cauchy Sequence

Informal description

For any Cauchy sequence $f$ of rational numbers (with respect to the absolute value metric), if there exists an index $i$ such that for all $j \geq i$ the real number $x$ is less than or equal to $f(j)$, then $x$ is less than or equal to the real number constructed from $f$ (i.e., $x \leq \langle f \rangle$).

Real.mk_le_of_forall_le theorem

{f : CauSeq ℚ abs} {x : ℝ} (h : ∃ i, ∀ j ≥ i, (f j : ℝ) ≤ x) : mk f ≤ x

Full source

theorem mk_le_of_forall_le {f : CauSeq ℚ abs} {x : ℝ} (h : ∃ i, ∀ j ≥ i, (f j : ℝ) ≤ x) :
    mk f ≤ x := by
  obtain ⟨i, H⟩ := h
  rw [← neg_le_neg_iff, ← mk_neg]
  exact le_mk_of_forall_le ⟨i, fun j ij => by simp [H _ ij]⟩

Comparison of Cauchy Sequence Limit with Real Number

Informal description

For any Cauchy sequence $f$ of rational numbers (with respect to the absolute value metric) and any real number $x$, if there exists an index $i$ such that for all $j \geq i$ the rational number $f(j)$ (viewed as a real number) is less than or equal to $x$, then the real number constructed from $f$ is less than or equal to $x$. That is, $\langle f \rangle \leq x$.

Real.mk_near_of_forall_near theorem

{f : CauSeq ℚ abs} {x : ℝ} {ε : ℝ} (H : ∃ i, ∀ j ≥ i, |(f j : ℝ) - x| ≤ ε) : |mk f - x| ≤ ε

Full source

theorem mk_near_of_forall_near {f : CauSeq ℚ abs} {x : ℝ} {ε : ℝ}
    (H : ∃ i, ∀ j ≥ i, |(f j : ℝ) - x| ≤ ε) : |mk f - x| ≤ ε :=
  abs_sub_le_iff.2
    ⟨sub_le_iff_le_add'.2 <|
        mk_le_of_forall_le <|
          H.imp fun _ h j ij => sub_le_iff_le_add'.1 (abs_sub_le_iff.1 <| h j ij).1,
      sub_le_comm.1 <|
        le_mk_of_forall_le <| H.imp fun _ h j ij => sub_le_comm.1 (abs_sub_le_iff.1 <| h j ij).2⟩

Cauchy Sequence Limit Approximation: $|\langle f \rangle - x| \leq \varepsilon$ under Uniform Approximation Condition

Informal description

For any Cauchy sequence $f$ of rational numbers (with respect to the absolute value metric), any real number $x$, and any positive real number $\varepsilon$, if there exists an index $i$ such that for all $j \geq i$ the distance between $f(j)$ (viewed as a real number) and $x$ is at most $\varepsilon$, then the distance between the real number constructed from $f$ and $x$ is also at most $\varepsilon$. That is, $|\langle f \rangle - x| \leq \varepsilon$.

Real.mul_add_one_le_add_one_pow theorem

{a : ℝ} (ha : 0 ≤ a) (b : ℕ) : a * b + 1 ≤ (a + 1) ^ b

Full source

lemma mul_add_one_le_add_one_pow {a : ℝ} (ha : 0 ≤ a) (b : ℕ) : a * b + 1 ≤ (a + 1) ^ b := by
  rcases ha.eq_or_lt with rfl | ha'
  · simp
  clear ha
  induction b generalizing a with
  | zero => simp
  | succ b hb =>
    calc
      a * ↑(b + 1) + 1 = (0 + 1) ^ b * a + (a * b + 1) := by
        simp [mul_add, add_assoc, add_left_comm]
      _ ≤ (a + 1) ^ b * a + (a + 1) ^ b := by
        gcongr
        · norm_num
        · exact hb ha'
      _ = (a + 1) ^ (b + 1) := by simp [pow_succ, mul_add]

Inequality for Nonnegative Reals: $a \cdot b + 1 \leq (a + 1)^b$

Informal description

For any nonnegative real number $a \geq 0$ and any natural number $b$, the inequality $a \cdot b + 1 \leq (a + 1)^b$ holds.

IsPowMul definition

{R : Type*} [Pow R ℕ] (f : R → ℝ)

Full source

/-- A function `f : R → ℝ` is power-multiplicative if for all `r ∈ R` and all positive `n ∈ ℕ`,
`f (r ^ n) = (f r) ^ n`. -/
def IsPowMul {R : Type*} [Pow R ℕ] (f : R → ℝ) :=
  ∀ (a : R) {n : ℕ}, 1 ≤ n → f (a ^ n) = f a ^ n

Power-multiplicative function

Informal description

A function $f \colon R \to \mathbb{R}$ is called *power-multiplicative* if for every $a \in R$ and every positive integer $n \geq 1$, the equality $f(a^n) = (f(a))^n$ holds.

RingHom.IsBoundedWrt definition

{α : Type*} [Ring α] {β : Type*} [Ring β] (nα : α → ℝ) (nβ : β → ℝ) (f : α →+* β) : Prop

Full source

/-- A ring homomorphism `f : α →+* β` is bounded with respect to the functions `nα : α → ℝ` and
  `nβ : β → ℝ` if there exists a positive constant `C` such that for all `x` in `α`,
  `nβ (f x) ≤ C * nα x`. -/
def RingHom.IsBoundedWrt {α : Type*} [Ring α] {β : Type*} [Ring β] (nα : α → ℝ) (nβ : β → ℝ)
    (f : α →+* β) : Prop :=
  ∃ C : ℝ, 0 < C ∧ ∀ x : α, nβ (f x) ≤ C * nα x

Bounded ring homomorphism

Informal description

A ring homomorphism $f \colon \alpha \to \beta$ is said to be *bounded* with respect to the functions $n_\alpha \colon \alpha \to \mathbb{R}$ and $n_\beta \colon \beta \to \mathbb{R}$ if there exists a positive constant $C > 0$ such that for all $x \in \alpha$, the inequality $n_\beta(f(x)) \leq C \cdot n_\alpha(x)$ holds.