theorem RationalApprox.sinℚ_approxRationalApprox.sinℚ_approx (x : ℝ) : |Real.sin x - RationalApprox.sinℚ x| ≤ |x| ^ 27 / ↑(Nat.factorial 27) (xℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  |abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a` Real.sinReal.sin (x : ℝ) : ℝThe real sine function, defined as the real part of the complex sine  xℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). RationalApprox.sinℚRationalApprox.sinℚ {k : Type} [Field k] (x : k) : kSine partial sum $x - x^3/3! + x^5/5! - ⋯ + x^{25}/25!$
 xℝ|abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a`  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. |abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a` xℝ|abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a`  ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 27 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ↑(Nat.factorialNat.factorial : ℕ → ℕ`Nat.factorial n` is the factorial of `n`.  27)

theorem RationalApprox.cosℚ_approxRationalApprox.cosℚ_approx (x : ℝ) : |Real.cos x - RationalApprox.cosℚ x| ≤ |x| ^ 26 / ↑(Nat.factorial 26) (xℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  |abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a` Real.cosReal.cos (x : ℝ) : ℝThe real cosine function, defined as the real part of the complex cosine  xℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). RationalApprox.cosℚRationalApprox.cosℚ {k : Type} [Field k] (x : k) : kCosine partial sum $1 - x^2/2! + x^4/4! - ⋯ + x^{24}/24!$
 xℝ|abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a`  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. |abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a` xℝ|abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a`  ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 26 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ↑(Nat.factorialNat.factorial : ℕ → ℕ`Nat.factorial n` is the factorial of `n`.  26)

theorem RationalApprox.sinℚ_approx'RationalApprox.sinℚ_approx' (x : ℝ) (hx : x ∈ Set.Icc (-4) 4) :
  |Real.sin x - RationalApprox.sinℚ x| ≤ RationalApprox.κ / 7 (xℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (hxx ∈ Set.Icc (-4) 4 : xℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  |abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a` Real.sinReal.sin (x : ℝ) : ℝThe real sine function, defined as the real part of the complex sine  xℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). RationalApprox.sinℚRationalApprox.sinℚ {k : Type} [Field k] (x : k) : kSine partial sum $x - x^3/3! + x^5/5! - ⋯ + x^{25}/25!$
 xℝ|abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a`  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. RationalApprox.κRationalApprox.κ : ℝ /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. 7

theorem RationalApprox.cosℚ_approx'RationalApprox.cosℚ_approx' (x : ℝ) (hx : x ∈ Set.Icc (-4) 4) :
  |Real.cos x - RationalApprox.cosℚ x| ≤ RationalApprox.κ / 7 (xℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (hxx ∈ Set.Icc (-4) 4 : xℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  |abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a` Real.cosReal.cos (x : ℝ) : ℝThe real cosine function, defined as the real part of the complex cosine  xℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). RationalApprox.cosℚRationalApprox.cosℚ {k : Type} [Field k] (x : k) : kCosine partial sum $1 - x^2/2! + x^4/4! - ⋯ + x^{24}/24!$
 xℝ|abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a`  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. RationalApprox.κRationalApprox.κ : ℝ /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. 7

theorem RationalApprox.norm_le_delta_sqrt_dimsRationalApprox.norm_le_delta_sqrt_dims {m n : ℕ} {δ : ℝ} (A : Matrix (Fin m) (Fin n) ℝ) (hδ : 0 < δ)
  (hle : ∀ (i : Fin m) (j : Fin n), |A i j| ≤ δ) :
  ‖LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin A)‖ ≤ δ * √(↑m * ↑n)[SY25] Lemma 39  {mℕ nℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} {δℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. }
  (AMatrix (Fin m) (Fin n) ℝ : MatrixMatrix.{u, u', v} (m : Type u) (n : Type u') (α : Type v) : Type (max u u' v)`Matrix m n R` is the type of matrices with entries in `R`, whose rows are indexed by `m`
and whose columns are indexed by `n`.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 mℕ) (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ) ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (hδ0 < δ : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. δℝ)
  (hle∀ (i : Fin m) (j : Fin n), |A i j| ≤ δ : ∀ (iFin m : FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 mℕ) (jFin n : FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ), |abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a` AMatrix (Fin m) (Fin n) ℝ iFin m jFin n|abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a`  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. δℝ) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. LinearMap.toContinuousLinearMapLinearMap.toContinuousLinearMap.{u, v, x} {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E]
  [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type x} [AddCommGroup F']
  [Module 𝕜 F'] [TopologicalSpace F'] [IsTopologicalAddGroup F'] [ContinuousSMul 𝕜 F'] [CompleteSpace 𝕜] [T2Space E]
  [FiniteDimensional 𝕜 E] : (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F'The continuous linear map induced by a linear map on a finite-dimensional space  (Matrix.toEuclideanLinMatrix.toEuclideanLin.{u_3, u_7, u_8} {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n]
  [DecidableEq n] : Matrix m n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 mA shorthand for `Matrix.toLpLin 2 2`.  AMatrix (Fin m) (Fin n) ℝ)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.
    δℝ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. √Real.sqrt (x : ℝ) : ℝThe square root of a real number. This returns 0 for negative inputs.

This has notation `√x`. Note that `√x⁻¹` is parsed as `√(x⁻¹)`. (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.↑mℕ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. ↑nℕ)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.

theorem RationalApprox.norm_matrix_actual_approx_le_kappaRationalApprox.norm_matrix_actual_approx_le_kappa {m n : ↥(Finset.Icc 1 3)}
  (A : Matrix (Fin ↑m) (Fin ↑n) RationalApprox.DistLeKappaEntry) (x y : ↑(Set.Icc (-4) 4)) :
  ‖RationalApprox.clinActual A ↑x ↑y - RationalApprox.clinApprox A ↑x ↑y‖ ≤ RationalApprox.κ[SY25] Lemma 40 
  {m↥(Finset.Icc 1 3) n↥(Finset.Icc 1 3) : ↥(Finset.IccFinset.Icc.{u_1} {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset αThe finset $[a, b]$ of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `Set.Icc a b` as a
finset.  1 3)}
  (AMatrix (Fin ↑m) (Fin ↑n) RationalApprox.DistLeKappaEntry : MatrixMatrix.{u, u', v} (m : Type u) (n : Type u') (α : Type v) : Type (max u u' v)`Matrix m n R` is the type of matrices with entries in `R`, whose rows are indexed by `m`
and whose columns are indexed by `n`.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 ↑m↥(Finset.Icc 1 3)) (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 ↑n↥(Finset.Icc 1 3)) RationalApprox.DistLeKappaEntryRationalApprox.DistLeKappaEntry : Type)
  (x↑(Set.Icc (-4) 4) y↑(Set.Icc (-4) 4) : ↑(Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4)) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. RationalApprox.clinActualRationalApprox.clinActual {m n : ℕ} (A : Matrix (Fin m) (Fin n) RationalApprox.DistLeKappaEntry) (x y : ℝ) :
  E n →L[ℝ] E m AMatrix (Fin ↑m) (Fin ↑n) RationalApprox.DistLeKappaEntry ↑x↑(Set.Icc (-4) 4) ↑y↑(Set.Icc (-4) 4) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).
        RationalApprox.clinApproxRationalApprox.clinApprox {m n : ℕ} (A : Matrix (Fin m) (Fin n) RationalApprox.DistLeKappaEntry) (x y : ℝ) :
  E n →L[ℝ] E m AMatrix (Fin ↑m) (Fin ↑n) RationalApprox.DistLeKappaEntry ↑x↑(Set.Icc (-4) 4) ↑y↑(Set.Icc (-4) 4)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.
    RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.R_difference_norm_boundedRationalApprox.R_difference_norm_bounded (α : ℝ) (hα : α ∈ Set.Icc (-4) 4) :
  ‖rotR α - RationalApprox.rotRℚℝ α‖ ≤ RationalApprox.κProof of [SY25] Corollary 41  (αℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (hαα ∈ Set.Icc (-4) 4 : αℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. rotRrotR : AddChar ℝ (Euc(2) →L[ℝ] Euc(2)) αℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). RationalApprox.rotRℚℝRationalApprox.rotRℚℝ (α : ℝ) : Euc(2) →L[ℝ] Euc(2) αℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.R'_difference_norm_boundedRationalApprox.R'_difference_norm_bounded (α : ℝ) (hα : α ∈ Set.Icc (-4) 4) :
  ‖rotR' α - RationalApprox.rotR'ℚℝ α‖ ≤ RationalApprox.κ (αℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (hαα ∈ Set.Icc (-4) 4 : αℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. rotR'rotR' (α : ℝ) : Euc(2) →L[ℝ] Euc(2) αℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). RationalApprox.rotR'ℚℝRationalApprox.rotR'ℚℝ (α : ℝ) : Euc(2) →L[ℝ] Euc(2) αℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.M_difference_norm_boundedRationalApprox.M_difference_norm_bounded (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotM θ φ - RationalApprox.rotMℚℝ θ φ‖ ≤ RationalApprox.κ (θℝ φℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (hθθ ∈ Set.Icc (-4) 4 : θℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) (hφφ ∈ Set.Icc (-4) 4 : φℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. rotMrotM (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). RationalApprox.rotMℚℝRationalApprox.rotMℚℝ (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.Mθ_difference_norm_boundedRationalApprox.Mθ_difference_norm_bounded (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMθ θ φ - RationalApprox.rotMθℚℝ θ φ‖ ≤ RationalApprox.κ (θℝ φℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (hθθ ∈ Set.Icc (-4) 4 : θℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) (hφφ ∈ Set.Icc (-4) 4 : φℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. rotMθrotMθ (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). RationalApprox.rotMθℚℝRationalApprox.rotMθℚℝ (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.Mφ_difference_norm_boundedRationalApprox.Mφ_difference_norm_bounded (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMφ θ φ - RationalApprox.rotMφℚℝ θ φ‖ ≤ RationalApprox.κ (θℝ φℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (hθθ ∈ Set.Icc (-4) 4 : θℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) (hφφ ∈ Set.Icc (-4) 4 : φℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. rotMφrotMφ (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). RationalApprox.rotMφℚℝRationalApprox.rotMφℚℝ (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.X_difference_norm_boundedRationalApprox.X_difference_norm_bounded (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖vecXL θ φ - RationalApprox.vecXLℚℝ θ φ‖ ≤ RationalApprox.κ (θℝ φℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (hθθ ∈ Set.Icc (-4) 4 : θℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) (hφφ ∈ Set.Icc (-4) 4 : φℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. vecXLvecXL (θ φ : ℝ) : Euc(1) →L[ℝ] Euc(3) θℝ φℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). RationalApprox.vecXLℚℝRationalApprox.vecXLℚℝ (θ φ : ℝ) : Euc(1) →L[ℝ] Euc(3) θℝ φℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.Rℚ_norm_boundedRationalApprox.Rℚ_norm_bounded (α : ℝ) (hα : α ∈ Set.Icc (-4) 4) : ‖RationalApprox.rotRℚℝ α‖ ≤ 1 + RationalApprox.κ (αℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (hαα ∈ Set.Icc (-4) 4 : αℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. RationalApprox.rotRℚℝRationalApprox.rotRℚℝ (α : ℝ) : Euc(2) →L[ℝ] Euc(2) αℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.Mℚ_norm_boundedRationalApprox.Mℚ_norm_bounded {θ φ : ℝ} (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMℚℝ θ φ‖ ≤ 1 + RationalApprox.κ {θℝ φℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } (hθθ ∈ Set.Icc (-4) 4 : θℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4)
  (hφφ ∈ Set.Icc (-4) 4 : φℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. RationalApprox.rotMℚℝRationalApprox.rotMℚℝ (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.R'ℚ_norm_boundedRationalApprox.R'ℚ_norm_bounded (α : ℝ) (hα : α ∈ Set.Icc (-4) 4) : ‖RationalApprox.rotR'ℚℝ α‖ ≤ 1 + RationalApprox.κ (αℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (hαα ∈ Set.Icc (-4) 4 : αℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. RationalApprox.rotR'ℚℝRationalApprox.rotR'ℚℝ (α : ℝ) : Euc(2) →L[ℝ] Euc(2) αℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.Mθℚ_norm_boundedRationalApprox.Mθℚ_norm_bounded {θ φ : ℝ} (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMθℚℝ θ φ‖ ≤ 1 + RationalApprox.κ {θℝ φℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } (hθθ ∈ Set.Icc (-4) 4 : θℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4)
  (hφφ ∈ Set.Icc (-4) 4 : φℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. RationalApprox.rotMθℚℝRationalApprox.rotMθℚℝ (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.Mφℚ_norm_boundedRationalApprox.Mφℚ_norm_bounded {θ φ : ℝ} (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMφℚℝ θ φ‖ ≤ 1 + RationalApprox.κ {θℝ φℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } (hθθ ∈ Set.Icc (-4) 4 : θℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4)
  (hφφ ∈ Set.Icc (-4) 4 : φℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. RationalApprox.rotMφℚℝRationalApprox.rotMφℚℝ (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.norm_sub_le_prodRationalApprox.norm_sub_le_prod {n m : ℕ} (mv : RationalApprox.MatVec n m) (κ : ℝ) (κ_pos : κ > 0)
  (hκ : mv.DiffBoundedBy κ) : ‖mv.compA - mv.compB‖ ≤ ↑mv.size * κ * mv.maxNormList.prod[SY25] Lemma 42  {nℕ mℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  (mvRationalApprox.MatVec n m : RationalApprox.MatVecRationalApprox.MatVec (n m : ℕ) : TypeTwo sequences of matrices A₁,...,Aₖ and B₁,...,Bₖ with sizes that make
the products A₁...Aₖ and B₁...Bₖ well-defined, as in [SY25] Lemma 42.
 nℕ mℕ) (κℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (κ_posκ > 0 : κℝ >GT.gt.{u} {α : Type u} [LT α] (a b : α) : Prop`a > b` is an abbreviation for `b < a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `>` in identifiers is `gt`. 0)
  (hκmv.DiffBoundedBy κ : mvRationalApprox.MatVec n m.DiffBoundedByRationalApprox.MatVec.DiffBoundedBy {n m : ℕ} (mv : RationalApprox.MatVec n m) (κ : ℝ) : Prop κℝ) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. mvRationalApprox.MatVec n m.compARationalApprox.MatVec.compA {n m : ℕ} (mv : RationalApprox.MatVec n m) : Euc(m) →L[ℝ] Euc(n) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). mvRationalApprox.MatVec n m.compBRationalApprox.MatVec.compB {n m : ℕ} (mv : RationalApprox.MatVec n m) : Euc(m) →L[ℝ] Euc(n)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. ↑mvRationalApprox.MatVec n m.sizeRationalApprox.MatVec.size {n m : ℕ} (mv : RationalApprox.MatVec n m) : ℕ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. κℝ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. mvRationalApprox.MatVec n m.maxNormListRationalApprox.MatVec.maxNormList {n m : ℕ} (mv : RationalApprox.MatVec n m) : List ℝ.prodList.prod.{u_1} {α : Type u_1} [Mul α] [One α] (xs : List α) : αComputes the product of the elements of a list.

Examples:

[a, b, c].prod = a * (b * (c * 1))
[2, 3, 5].prod = 30

theorem RationalApprox.bounds_kappa_MRationalApprox.bounds_kappa_M {P : Euc(3)} {P_ : Fin 3 → ℚ} {θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotM ↑↑θ ↑↑φ) P) (toR2 w) - ↑((RationalApprox.rotMℚ ↑θ ↑φ) P_ ⬝ᵥ w)‖ ≤ 3 * RationalApprox.κ {PEuc(3) : Euc(EuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation. 3)EuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation. } {P_Fin 3 → ℚ : FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 3 → ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
}
  {θ↑(Set.Icc (-4) 4) φ↑(Set.Icc (-4) 4) : ↑(Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4)} {wFin 2 → ℚ : FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 2 → ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
} (hP‖P‖ ≤ 1 : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. PEuc(3)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1)
  (approx‖P - toR3 P_‖ ≤ RationalApprox.κ : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. PEuc(3) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). toR3toR3 (v : Fin 3 → ℚ) : Euc(3)Cast a `Fin 3 → ℚ` to an `ℝ³` point.  P_Fin 3 → ℚ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. RationalApprox.κRationalApprox.κ : ℝ) (hw‖toR2 w‖ = 1 : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. toR2toR2 (v : Fin 2 → ℚ) : Euc(2)Cast a `Fin 2 → ℚ` to an `ℝ²` point.  wFin 2 → ℚ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. innerInner.inner.{u_4, u_5} (𝕜 : Type u_4) {E : Type u_5} [self : Inner 𝕜 E] : E → E → 𝕜The inner product function.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  ((rotMrotM (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) ↑↑θ↑(Set.Icc (-4) 4) ↑↑φ↑(Set.Icc (-4) 4)) PEuc(3)) (toR2toR2 (v : Fin 2 → ℚ) : Euc(2)Cast a `Fin 2 → ℚ` to an `ℝ²` point.  wFin 2 → ℚ) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).
        ↑(dotProduct.{v, u_2} {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α`dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`. (RationalApprox.rotMℚRationalApprox.rotMℚ (θ φ : ℚ) : (Fin 3 → ℚ) →ₗ[ℚ] Fin 2 → ℚ ↑θ↑(Set.Icc (-4) 4) ↑φ↑(Set.Icc (-4) 4)) P_Fin 3 → ℚ ⬝ᵥdotProduct.{v, u_2} {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α`dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`.  wFin 2 → ℚ)dotProduct.{v, u_2} {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α`dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`. ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.
    3 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.bounds_kappa_MθRationalApprox.bounds_kappa_Mθ {P : Euc(3)} {P_ : Fin 3 → ℚ} {θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMθ ↑↑θ ↑↑φ) P) (toR2 w) - ↑((RationalApprox.rotMθℚ ↑θ ↑φ) P_ ⬝ᵥ w)‖ ≤ 3 * RationalApprox.κ {PEuc(3) : Euc(EuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation. 3)EuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation. } {P_Fin 3 → ℚ : FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 3 → ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
}
  {θ↑(Set.Icc (-4) 4) φ↑(Set.Icc (-4) 4) : ↑(Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4)} {wFin 2 → ℚ : FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 2 → ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
} (hP‖P‖ ≤ 1 : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. PEuc(3)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1)
  (approx‖P - toR3 P_‖ ≤ RationalApprox.κ : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. PEuc(3) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). toR3toR3 (v : Fin 3 → ℚ) : Euc(3)Cast a `Fin 3 → ℚ` to an `ℝ³` point.  P_Fin 3 → ℚ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. RationalApprox.κRationalApprox.κ : ℝ) (hw‖toR2 w‖ = 1 : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. toR2toR2 (v : Fin 2 → ℚ) : Euc(2)Cast a `Fin 2 → ℚ` to an `ℝ²` point.  wFin 2 → ℚ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. innerInner.inner.{u_4, u_5} (𝕜 : Type u_4) {E : Type u_5} [self : Inner 𝕜 E] : E → E → 𝕜The inner product function.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  ((rotMθrotMθ (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) ↑↑θ↑(Set.Icc (-4) 4) ↑↑φ↑(Set.Icc (-4) 4)) PEuc(3)) (toR2toR2 (v : Fin 2 → ℚ) : Euc(2)Cast a `Fin 2 → ℚ` to an `ℝ²` point.  wFin 2 → ℚ) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).
        ↑(dotProduct.{v, u_2} {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α`dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`. (RationalApprox.rotMθℚRationalApprox.rotMθℚ (θ φ : ℚ) : (Fin 3 → ℚ) →ₗ[ℚ] Fin 2 → ℚ ↑θ↑(Set.Icc (-4) 4) ↑φ↑(Set.Icc (-4) 4)) P_Fin 3 → ℚ ⬝ᵥdotProduct.{v, u_2} {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α`dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`.  wFin 2 → ℚ)dotProduct.{v, u_2} {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α`dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`. ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.
    3 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.bounds_kappa_MφRationalApprox.bounds_kappa_Mφ {P : Euc(3)} {P_ : Fin 3 → ℚ} {θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMφ ↑↑θ ↑↑φ) P) (toR2 w) - ↑((RationalApprox.rotMφℚ ↑θ ↑φ) P_ ⬝ᵥ w)‖ ≤ 3 * RationalApprox.κ {PEuc(3) : Euc(EuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation. 3)EuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation. } {P_Fin 3 → ℚ : FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 3 → ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
}
  {θ↑(Set.Icc (-4) 4) φ↑(Set.Icc (-4) 4) : ↑(Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4)} {wFin 2 → ℚ : FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 2 → ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
} (hP‖P‖ ≤ 1 : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. PEuc(3)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1)
  (approx‖P - toR3 P_‖ ≤ RationalApprox.κ : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. PEuc(3) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). toR3toR3 (v : Fin 3 → ℚ) : Euc(3)Cast a `Fin 3 → ℚ` to an `ℝ³` point.  P_Fin 3 → ℚ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. RationalApprox.κRationalApprox.κ : ℝ) (hw‖toR2 w‖ = 1 : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. toR2toR2 (v : Fin 2 → ℚ) : Euc(2)Cast a `Fin 2 → ℚ` to an `ℝ²` point.  wFin 2 → ℚ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. innerInner.inner.{u_4, u_5} (𝕜 : Type u_4) {E : Type u_5} [self : Inner 𝕜 E] : E → E → 𝕜The inner product function.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  ((rotMφrotMφ (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) ↑↑θ↑(Set.Icc (-4) 4) ↑↑φ↑(Set.Icc (-4) 4)) PEuc(3)) (toR2toR2 (v : Fin 2 → ℚ) : Euc(2)Cast a `Fin 2 → ℚ` to an `ℝ²` point.  wFin 2 → ℚ) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).
        ↑(dotProduct.{v, u_2} {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α`dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`. (RationalApprox.rotMφℚRationalApprox.rotMφℚ (θ φ : ℚ) : (Fin 3 → ℚ) →ₗ[ℚ] Fin 2 → ℚ ↑θ↑(Set.Icc (-4) 4) ↑φ↑(Set.Icc (-4) 4)) P_Fin 3 → ℚ ⬝ᵥdotProduct.{v, u_2} {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α`dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`.  wFin 2 → ℚ)dotProduct.{v, u_2} {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α`dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`. ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.
    3 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. RationalApprox.κRationalApprox.κ : ℝ

theorem RationalApprox.bounds_kappa_RMRationalApprox.bounds_kappa_RM {P : Euc(3)} {P_ : Fin 3 → ℚ} {α θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotR ↑↑α) ((rotM ↑↑θ ↑↑φ) P)) (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α) ((RationalApprox.rotMℚ ↑θ ↑φ) P_) ⬝ᵥ w)‖ ≤
    4 * RationalApprox.κ {PEuc(3) : Euc(EuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation. 3)EuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation. } {P_Fin 3 → ℚ : FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 3 → ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
}
  {α↑(Set.Icc (-4) 4) θ↑(Set.Icc (-4) 4) φ↑(Set.Icc (-4) 4) : ↑(Set.IccSet.Icc.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Icc a b` is the left-closed right-closed interval $[a, b]$.  (-4) 4)} {wFin 2 → ℚ : FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 2 → ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
} (hP‖P‖ ≤ 1 : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. PEuc(3)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1)
  (approx‖P - toR3 P_‖ ≤ RationalApprox.κ : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. PEuc(3) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). toR3toR3 (v : Fin 3 → ℚ) : Euc(3)Cast a `Fin 3 → ℚ` to an `ℝ³` point.  P_Fin 3 → ℚ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. RationalApprox.κRationalApprox.κ : ℝ) (hw‖toR2 w‖ = 1 : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. toR2toR2 (v : Fin 2 → ℚ) : Euc(2)Cast a `Fin 2 → ℚ` to an `ℝ²` point.  wFin 2 → ℚ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. innerInner.inner.{u_4, u_5} (𝕜 : Type u_4) {E : Type u_5} [self : Inner 𝕜 E] : E → E → 𝕜The inner product function.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  ((rotRrotR : AddChar ℝ (Euc(2) →L[ℝ] Euc(2)) ↑↑α↑(Set.Icc (-4) 4)) ((rotMrotM (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) ↑↑θ↑(Set.Icc (-4) 4) ↑↑φ↑(Set.Icc (-4) 4)) PEuc(3))) (toR2toR2 (v : Fin 2 → ℚ) : Euc(2)Cast a `Fin 2 → ℚ` to an `ℝ²` point.  wFin 2 → ℚ) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).
        ↑(dotProduct.{v, u_2} {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α`dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`. (RationalApprox.rotRℚRationalApprox.rotRℚ (α : ℚ) : (Fin 2 → ℚ) →ₗ[ℚ] Fin 2 → ℚ ↑α↑(Set.Icc (-4) 4)) ((RationalApprox.rotMℚRationalApprox.rotMℚ (θ φ : ℚ) : (Fin 3 → ℚ) →ₗ[ℚ] Fin 2 → ℚ ↑θ↑(Set.Icc (-4) 4) ↑φ↑(Set.Icc (-4) 4)) P_Fin 3 → ℚ) ⬝ᵥdotProduct.{v, u_2} {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α`dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`. 
            wFin 2 → ℚ)dotProduct.{v, u_2} {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α`dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`. ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.
    4 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. RationalApprox.κRationalApprox.κ : ℝ