theorem GlobalTheorem.hull_scalar_prodGlobalTheorem.hull_scalar_prod {n : ℕ} (V : Finset (GlobalTheorem.E✝ n)) (Vne : V.Nonempty) (S : GlobalTheorem.E✝ n)
  (hs : S ∈ (convexHull ℝ) ↑V) (w : GlobalTheorem.E✝ n) : inner ℝ w S ≤ (Finset.image (fun x ↦ inner ℝ w x) V).max' ⋯ {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.
}
  (VFinset (GlobalTheorem.E✝ n) : FinsetFinset.{u_4} (α : Type u_4) : Type u_4`Finset α` is the type of finite sets of elements of `α`. It is implemented
as a multiset (a list up to permutation) which has no duplicate elements.  (GlobalTheorem.E✝GlobalTheorem.E✝ (n : ℕ) : Type nℕ))
  (VneV.Nonempty : VFinset (GlobalTheorem.E✝ n).NonemptyFinset.Nonempty.{u_1} {α : Type u_1} (s : Finset α) : PropThe property `s.Nonempty` expresses the fact that the finset `s` is not empty. It should be used
in theorem assumptions instead of `∃ x, x ∈ s` or `s ≠ ∅` as it gives access to a nice API thanks
to the dot notation. )
  (SGlobalTheorem.E✝ n : GlobalTheorem.E✝GlobalTheorem.E✝ (n : ℕ) : Type nℕ)
  (hsS ∈ (convexHull ℝ) ↑V : SGlobalTheorem.E✝ n ∈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`. (convexHullconvexHull.{u_1, u_2} (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] :
  ClosureOperator (Set E)The convex hull of a set `s` is the minimal convex set that includes `s`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) ↑VFinset (GlobalTheorem.E✝ n))
  (wGlobalTheorem.E✝ n : GlobalTheorem.E✝GlobalTheorem.E✝ (n : ℕ) : Type nℕ) :
  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.  wGlobalTheorem.E✝ n SGlobalTheorem.E✝ n ≤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`.
    (Finset.imageFinset.image.{u_1, u_2} {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Finset α) : Finset β`image f s` is the forward image of `s` under `f`.  (fun xGlobalTheorem.E✝ n ↦ 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.  wGlobalTheorem.E✝ n xGlobalTheorem.E✝ n)
          VFinset (GlobalTheorem.E✝ n)).max'Finset.max'.{u_2} {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : αGiven a nonempty finset `s` in a linear order `α`, then `s.max' H` is its maximum, as an
element of `α`, where `H` is a proof of nonemptiness. Without this assumption, use instead `s.max`,
taking values in `WithBot α`. 
      ⋯

theorem GlobalTheorem.rotation_partials_boundedGlobalTheorem.rotation_partials_bounded (S : Euc(3)) {w : Euc(2)} (w_unit : ‖w‖ = 1) :
  GlobalTheorem.mixed_partials_bounded (GlobalTheorem.rotproj_inner_unit S w)
  (SEuc(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. ) {wEuc(2) : 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. 2)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. }
  (w_unit‖w‖ = 1 : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. wEuc(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) :
  GlobalTheorem.mixed_partials_boundedGlobalTheorem.mixed_partials_bounded {n : ℕ} (f : E n → ℝ) : Prop
    (GlobalTheorem.rotproj_inner_unitGlobalTheorem.rotproj_inner_unit (S : Euc(3)) (w : Euc(2)) (x : Euc(3)) : ℝ SEuc(3) wEuc(2))

theorem GlobalTheorem.bounded_partials_control_differenceGlobalTheorem.bounded_partials_control_difference {n : ℕ} (f : GlobalTheorem.E✝ n → ℝ) (fc : ContDiff ℝ 2 f)
  (x y : GlobalTheorem.E✝ n) (ε : ℝ) (hε : 0 ≤ ε) (hdiff : ∀ (i : Fin n), |x.ofLp i - y.ofLp i| ≤ ε)
  (mpb : GlobalTheorem.mixed_partials_bounded f) :
  |f x - f y| ≤ ε * ∑ i, |GlobalTheorem.nth_partial i f x| + ↑n ^ 2 / 2 * ε ^ 2
  {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.
} (fGlobalTheorem.E✝ n → ℝ : GlobalTheorem.E✝GlobalTheorem.E✝ (n : ℕ) : Type nℕ → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (fcContDiff ℝ 2 f : ContDiffContDiff.{u, uE, uF} (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : WithTop ℕ∞) (f : E → F) : PropA function is continuously differentiable up to `n` if it admits derivatives up to
order `n`, which are continuous. Contrary to the case of definitions in domains (where derivatives
might not be unique) we do not need to localize the definition in space or time.
The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
number, `∞`, or `ω`.

For `n = ω`, we require the function to be analytic. The precise
definition we give (all the derivatives should be analytic) is more involved to work around issues
when the space is not complete, but it is equivalent when the space is complete.
 ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  2 fGlobalTheorem.E✝ n → ℝ)
  (xGlobalTheorem.E✝ n yGlobalTheorem.E✝ n : GlobalTheorem.E✝GlobalTheorem.E✝ (n : ℕ) : Type nℕ) (εℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (hε0 ≤ ε : 0 ≤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`. εℝ)
  (hdiff∀ (i : Fin n), |x.ofLp i - y.ofLp i| ≤ ε :
    ∀ (iFin 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` xGlobalTheorem.E✝ n.ofLpWithLp.ofLp.{u_1} {p : ENNReal} {V : Type u_1} (self : WithLp p V) : VConverts an element of `WithLp p V` to an element of `V`.  iFin 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). yGlobalTheorem.E✝ n.ofLpWithLp.ofLp.{u_1} {p : ENNReal} {V : Type u_1} (self : WithLp p V) : VConverts an element of `WithLp p V` to an element of `V`.  iFin 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`. εℝ)
  (mpbGlobalTheorem.mixed_partials_bounded f :
    GlobalTheorem.mixed_partials_boundedGlobalTheorem.mixed_partials_bounded {n : ℕ} (f : E n → ℝ) : Prop
      fGlobalTheorem.E✝ n → ℝ) :
  |abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a` fGlobalTheorem.E✝ n → ℝ xGlobalTheorem.E✝ 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). fGlobalTheorem.E✝ n → ℝ yGlobalTheorem.E✝ 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`.
    εℝ *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`.
        ∑ iFin n,
          |abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a` GlobalTheorem.nth_partialGlobalTheorem.nth_partial {n : ℕ} (i : Fin n) (f : E n → ℝ) (x : E n) : ℝ iFin n fGlobalTheorem.E✝ n → ℝ
              xGlobalTheorem.E✝ n|abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α`abs a`, denoted `|a|`, is the absolute value of `a`  +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`.
      ↑nℕ ^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`. 2 /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`. 2 *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`. εℝ ^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`. 2

theorem GlobalTheorem.rotation_partials_existGlobalTheorem.rotation_partials_exist {S : Euc(3)} (S_nonzero : ‖S‖ > 0) {w : Euc(2)} :
  ContDiff ℝ 2 (GlobalTheorem.rotproj_inner_unit S w)
  {SEuc(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. } (S_nonzero‖S‖ > 0 : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. SEuc(3)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  >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)
  {wEuc(2) : 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. 2)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. } :
  ContDiffContDiff.{u, uE, uF} (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : WithTop ℕ∞) (f : E → F) : PropA function is continuously differentiable up to `n` if it admits derivatives up to
order `n`, which are continuous. Contrary to the case of definitions in domains (where derivatives
might not be unique) we do not need to localize the definition in space or time.
The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
number, `∞`, or `ω`.

For `n = ω`, we require the function to be analytic. The precise
definition we give (all the derivatives should be analytic) is more involved to work around issues
when the space is not complete, but it is equivalent when the space is complete.
 ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  2
    (GlobalTheorem.rotproj_inner_unitGlobalTheorem.rotproj_inner_unit (S : Euc(3)) (w : Euc(2)) (x : Euc(3)) : ℝ SEuc(3) wEuc(2))

theorem GlobalTheorem.rotation_partials_exist_outerGlobalTheorem.rotation_partials_exist_outer {S : Euc(3)} (S_nonzero : ‖S‖ > 0) {w : Euc(2)} :
  ContDiff ℝ 2 (GlobalTheorem.rotproj_outer_unit S w)
  {SEuc(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. } (S_nonzero‖S‖ > 0 : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. SEuc(3)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  >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)
  {wEuc(2) : 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. 2)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. } :
  ContDiffContDiff.{u, uE, uF} (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : WithTop ℕ∞) (f : E → F) : PropA function is continuously differentiable up to `n` if it admits derivatives up to
order `n`, which are continuous. Contrary to the case of definitions in domains (where derivatives
might not be unique) we do not need to localize the definition in space or time.
The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
number, `∞`, or `ω`.

For `n = ω`, we require the function to be analytic. The precise
definition we give (all the derivatives should be analytic) is more involved to work around issues
when the space is not complete, but it is equivalent when the space is complete.
 ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  2
    (GlobalTheorem.rotproj_outer_unitGlobalTheorem.rotproj_outer_unit (S : Euc(3)) (w x : Euc(2)) : ℝ SEuc(3) wEuc(2))

theorem GlobalTheorem.partials_helper0GlobalTheorem.partials_helper0 {pbar : Pose ℝ} {ε : ℝ} {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι}
  (pc : GlobalTheorem.GlobalTheoremPrecondition poly pbar ε) :
  ‖pc.S‖ * GlobalTheorem.nth_partial 0 pc.fu pbar.innerParams = inner ℝ (pbar.rotR' (pbar.rotM₁ pc.S)) pc.w
  {pbarPose ℝ : PosePose (R : Type) : Type ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {εℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {ιType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  ιType] [NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 ιType]
  {polyGoodPoly ι : GoodPolyGoodPoly (ι : Type) [Fintype ι] [Nonempty ι] : Type ιType}
  (pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε :
    GlobalTheorem.GlobalTheoremPreconditionGlobalTheorem.GlobalTheoremPrecondition {ι : Type} [Fintype ι] [Nonempty ι] (poly : GoodPoly ι) (p : Pose ℝ) (ε : ℝ) :
  TypeA compact way of saying "the pose satisfies the global theorem precondition at width ε".
We require the existence of some inner-shadow vertex S from the polyhedron, and a covector w meant to express
the direction we're projecting ℝ² → ℝ to find that S "sticks out too far" compared to all the
other outer-shadow vertices P (which the calculation of H iterates over) in the polygon that lies in ℝ².

      polyGoodPoly ι pbarPose ℝ εℝ) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.SGlobalTheorem.GlobalTheoremPrecondition.S {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι} {p : Pose ℝ} {ε : ℝ}
  (self : GlobalTheorem.GlobalTheoremPrecondition poly p ε) : Euc(3)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  *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`.
      GlobalTheorem.nth_partialGlobalTheorem.nth_partial {n : ℕ} (i : Fin n) (f : E n → ℝ) (x : E n) : ℝ 0 pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.fuGlobalTheorem.GlobalTheoremPrecondition.fu {pbar : Pose ℝ} {ε : ℝ} {ι : Type} [Fintype ι] [Nonempty ι]
  {poly : GoodPoly ι} (pc : GlobalTheorem.GlobalTheoremPrecondition poly pbar ε) : Euc(3) → ℝThis is the function that Theorem 17's proof calls `f`.
It always returns a unit vector.

        pbarPose ℝ.innerParamsPose.innerParams (p : Pose ℝ) : Euc(3) =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`.
    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.  (pbarPose ℝ.rotR'Pose.rotR' (p : Pose ℝ) : Euc(2) →L[ℝ] Euc(2) (pbarPose ℝ.rotM₁Pose.rotM₁ (p : Pose ℝ) : Euc(3) →L[ℝ] Euc(2) pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.SGlobalTheorem.GlobalTheoremPrecondition.S {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι} {p : Pose ℝ} {ε : ℝ}
  (self : GlobalTheorem.GlobalTheoremPrecondition poly p ε) : Euc(3)))
      pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.wGlobalTheorem.GlobalTheoremPrecondition.w {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι} {p : Pose ℝ} {ε : ℝ}
  (self : GlobalTheorem.GlobalTheoremPrecondition poly p ε) : Euc(2)

theorem GlobalTheorem.partials_helper1GlobalTheorem.partials_helper1 {pbar : Pose ℝ} {ε : ℝ} {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι}
  (pc : GlobalTheorem.GlobalTheoremPrecondition poly pbar ε) :
  ‖pc.S‖ * GlobalTheorem.nth_partial 1 pc.fu pbar.innerParams = inner ℝ (pbar.rotR (pbar.rotM₁θ pc.S)) pc.w
  {pbarPose ℝ : PosePose (R : Type) : Type ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {εℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {ιType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  ιType] [NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 ιType]
  {polyGoodPoly ι : GoodPolyGoodPoly (ι : Type) [Fintype ι] [Nonempty ι] : Type ιType}
  (pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε :
    GlobalTheorem.GlobalTheoremPreconditionGlobalTheorem.GlobalTheoremPrecondition {ι : Type} [Fintype ι] [Nonempty ι] (poly : GoodPoly ι) (p : Pose ℝ) (ε : ℝ) :
  TypeA compact way of saying "the pose satisfies the global theorem precondition at width ε".
We require the existence of some inner-shadow vertex S from the polyhedron, and a covector w meant to express
the direction we're projecting ℝ² → ℝ to find that S "sticks out too far" compared to all the
other outer-shadow vertices P (which the calculation of H iterates over) in the polygon that lies in ℝ².

      polyGoodPoly ι pbarPose ℝ εℝ) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.SGlobalTheorem.GlobalTheoremPrecondition.S {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι} {p : Pose ℝ} {ε : ℝ}
  (self : GlobalTheorem.GlobalTheoremPrecondition poly p ε) : Euc(3)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  *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`.
      GlobalTheorem.nth_partialGlobalTheorem.nth_partial {n : ℕ} (i : Fin n) (f : E n → ℝ) (x : E n) : ℝ 1 pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.fuGlobalTheorem.GlobalTheoremPrecondition.fu {pbar : Pose ℝ} {ε : ℝ} {ι : Type} [Fintype ι] [Nonempty ι]
  {poly : GoodPoly ι} (pc : GlobalTheorem.GlobalTheoremPrecondition poly pbar ε) : Euc(3) → ℝThis is the function that Theorem 17's proof calls `f`.
It always returns a unit vector.

        pbarPose ℝ.innerParamsPose.innerParams (p : Pose ℝ) : Euc(3) =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`.
    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.  (pbarPose ℝ.rotRPose.rotR (p : Pose ℝ) : Euc(2) →L[ℝ] Euc(2) (pbarPose ℝ.rotM₁θPose.rotM₁θ (p : Pose ℝ) : Euc(3) →L[ℝ] Euc(2) pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.SGlobalTheorem.GlobalTheoremPrecondition.S {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι} {p : Pose ℝ} {ε : ℝ}
  (self : GlobalTheorem.GlobalTheoremPrecondition poly p ε) : Euc(3)))
      pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.wGlobalTheorem.GlobalTheoremPrecondition.w {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι} {p : Pose ℝ} {ε : ℝ}
  (self : GlobalTheorem.GlobalTheoremPrecondition poly p ε) : Euc(2)

theorem GlobalTheorem.partials_helper2GlobalTheorem.partials_helper2 {pbar : Pose ℝ} {ε : ℝ} {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι}
  (pc : GlobalTheorem.GlobalTheoremPrecondition poly pbar ε) :
  ‖pc.S‖ * GlobalTheorem.nth_partial 2 pc.fu pbar.innerParams = inner ℝ (pbar.rotR (pbar.rotM₁φ pc.S)) pc.w
  {pbarPose ℝ : PosePose (R : Type) : Type ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {εℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {ιType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  ιType] [NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 ιType]
  {polyGoodPoly ι : GoodPolyGoodPoly (ι : Type) [Fintype ι] [Nonempty ι] : Type ιType}
  (pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε :
    GlobalTheorem.GlobalTheoremPreconditionGlobalTheorem.GlobalTheoremPrecondition {ι : Type} [Fintype ι] [Nonempty ι] (poly : GoodPoly ι) (p : Pose ℝ) (ε : ℝ) :
  TypeA compact way of saying "the pose satisfies the global theorem precondition at width ε".
We require the existence of some inner-shadow vertex S from the polyhedron, and a covector w meant to express
the direction we're projecting ℝ² → ℝ to find that S "sticks out too far" compared to all the
other outer-shadow vertices P (which the calculation of H iterates over) in the polygon that lies in ℝ².

      polyGoodPoly ι pbarPose ℝ εℝ) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.SGlobalTheorem.GlobalTheoremPrecondition.S {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι} {p : Pose ℝ} {ε : ℝ}
  (self : GlobalTheorem.GlobalTheoremPrecondition poly p ε) : Euc(3)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  *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`.
      GlobalTheorem.nth_partialGlobalTheorem.nth_partial {n : ℕ} (i : Fin n) (f : E n → ℝ) (x : E n) : ℝ 2 pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.fuGlobalTheorem.GlobalTheoremPrecondition.fu {pbar : Pose ℝ} {ε : ℝ} {ι : Type} [Fintype ι] [Nonempty ι]
  {poly : GoodPoly ι} (pc : GlobalTheorem.GlobalTheoremPrecondition poly pbar ε) : Euc(3) → ℝThis is the function that Theorem 17's proof calls `f`.
It always returns a unit vector.

        pbarPose ℝ.innerParamsPose.innerParams (p : Pose ℝ) : Euc(3) =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`.
    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.  (pbarPose ℝ.rotRPose.rotR (p : Pose ℝ) : Euc(2) →L[ℝ] Euc(2) (pbarPose ℝ.rotM₁φPose.rotM₁φ (p : Pose ℝ) : Euc(3) →L[ℝ] Euc(2) pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.SGlobalTheorem.GlobalTheoremPrecondition.S {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι} {p : Pose ℝ} {ε : ℝ}
  (self : GlobalTheorem.GlobalTheoremPrecondition poly p ε) : Euc(3)))
      pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.wGlobalTheorem.GlobalTheoremPrecondition.w {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι} {p : Pose ℝ} {ε : ℝ}
  (self : GlobalTheorem.GlobalTheoremPrecondition poly p ε) : Euc(2)

theorem GlobalTheorem.partials_helper3GlobalTheorem.partials_helper3 {pbar : Pose ℝ} {ε : ℝ} {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι}
  (pc : GlobalTheorem.GlobalTheoremPrecondition poly pbar ε) (P : Euc(3)) :
  ‖P‖ * GlobalTheorem.nth_partial 0 (GlobalTheorem.GlobalTheoremPrecondition.fu_outer P pc) pbar.outerParams =
    inner ℝ (pbar.rotM₂θ P) pc.w
  {pbarPose ℝ : PosePose (R : Type) : Type ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {εℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {ιType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  ιType] [NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 ιType]
  {polyGoodPoly ι : GoodPolyGoodPoly (ι : Type) [Fintype ι] [Nonempty ι] : Type ιType}
  (pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε :
    GlobalTheorem.GlobalTheoremPreconditionGlobalTheorem.GlobalTheoremPrecondition {ι : Type} [Fintype ι] [Nonempty ι] (poly : GoodPoly ι) (p : Pose ℝ) (ε : ℝ) :
  TypeA compact way of saying "the pose satisfies the global theorem precondition at width ε".
We require the existence of some inner-shadow vertex S from the polyhedron, and a covector w meant to express
the direction we're projecting ℝ² → ℝ to find that S "sticks out too far" compared to all the
other outer-shadow vertices P (which the calculation of H iterates over) in the polygon that lies in ℝ².

      polyGoodPoly ι pbarPose ℝ εℝ)
  (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. ) :
  ‖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.  *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`.
      GlobalTheorem.nth_partialGlobalTheorem.nth_partial {n : ℕ} (i : Fin n) (f : E n → ℝ) (x : E n) : ℝ 0
        (GlobalTheorem.GlobalTheoremPrecondition.fu_outerGlobalTheorem.GlobalTheoremPrecondition.fu_outer {pbar : Pose ℝ} {ε : ℝ} {ι : Type} [Fintype ι] [Nonempty ι]
  {poly : GoodPoly ι} (P : Euc(3)) (pc : GlobalTheorem.GlobalTheoremPrecondition poly pbar ε) : Euc(2) → ℝThis is an outer-shadow analog of `fu`

          PEuc(3) pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε)
        pbarPose ℝ.outerParamsPose.outerParams (p : Pose ℝ) : Euc(2) =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`.
    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.  (pbarPose ℝ.rotM₂θPose.rotM₂θ (p : Pose ℝ) : Euc(3) →L[ℝ] Euc(2) PEuc(3)) pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.wGlobalTheorem.GlobalTheoremPrecondition.w {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι} {p : Pose ℝ} {ε : ℝ}
  (self : GlobalTheorem.GlobalTheoremPrecondition poly p ε) : Euc(2)

theorem GlobalTheorem.partials_helper4GlobalTheorem.partials_helper4 {pbar : Pose ℝ} {ε : ℝ} {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι}
  (pc : GlobalTheorem.GlobalTheoremPrecondition poly pbar ε) (P : Euc(3)) :
  ‖P‖ * GlobalTheorem.nth_partial 1 (GlobalTheorem.GlobalTheoremPrecondition.fu_outer P pc) pbar.outerParams =
    inner ℝ (pbar.rotM₂φ P) pc.w
  {pbarPose ℝ : PosePose (R : Type) : Type ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {εℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } {ιType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  ιType] [NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 ιType]
  {polyGoodPoly ι : GoodPolyGoodPoly (ι : Type) [Fintype ι] [Nonempty ι] : Type ιType}
  (pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε :
    GlobalTheorem.GlobalTheoremPreconditionGlobalTheorem.GlobalTheoremPrecondition {ι : Type} [Fintype ι] [Nonempty ι] (poly : GoodPoly ι) (p : Pose ℝ) (ε : ℝ) :
  TypeA compact way of saying "the pose satisfies the global theorem precondition at width ε".
We require the existence of some inner-shadow vertex S from the polyhedron, and a covector w meant to express
the direction we're projecting ℝ² → ℝ to find that S "sticks out too far" compared to all the
other outer-shadow vertices P (which the calculation of H iterates over) in the polygon that lies in ℝ².

      polyGoodPoly ι pbarPose ℝ εℝ)
  (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. ) :
  ‖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.  *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`.
      GlobalTheorem.nth_partialGlobalTheorem.nth_partial {n : ℕ} (i : Fin n) (f : E n → ℝ) (x : E n) : ℝ 1
        (GlobalTheorem.GlobalTheoremPrecondition.fu_outerGlobalTheorem.GlobalTheoremPrecondition.fu_outer {pbar : Pose ℝ} {ε : ℝ} {ι : Type} [Fintype ι] [Nonempty ι]
  {poly : GoodPoly ι} (P : Euc(3)) (pc : GlobalTheorem.GlobalTheoremPrecondition poly pbar ε) : Euc(2) → ℝThis is an outer-shadow analog of `fu`

          PEuc(3) pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε)
        pbarPose ℝ.outerParamsPose.outerParams (p : Pose ℝ) : Euc(2) =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`.
    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.  (pbarPose ℝ.rotM₂φPose.rotM₂φ (p : Pose ℝ) : Euc(3) →L[ℝ] Euc(2) PEuc(3)) pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε.wGlobalTheorem.GlobalTheoremPrecondition.w {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι} {p : Pose ℝ} {ε : ℝ}
  (self : GlobalTheorem.GlobalTheoremPrecondition poly p ε) : Euc(2)

theorem GlobalTheorem.global_theoremGlobalTheorem.global_theorem {ι : Type} [Fintype ι] [Nonempty ι] (pbar : Pose ℝ) (ε : ℝ) (hε : 0 ≤ ε)
  (poly : GoodPoly ι) (pc : GlobalTheorem.GlobalTheoremPrecondition poly pbar ε) :
  ¬∃ p ∈ Metric.closedBall pbar ε, RupertPose p poly.hullThe Global Theorem, [SY25] Theorem 17
 {ιType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  ιType] [NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 ιType] (pbarPose ℝ : PosePose (R : Type) : Type ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (εℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (hε0 ≤ ε : 0 ≤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`. εℝ) (polyGoodPoly ι : GoodPolyGoodPoly (ι : Type) [Fintype ι] [Nonempty ι] : Type ιType)
  (pcGlobalTheorem.GlobalTheoremPrecondition poly pbar ε :
    GlobalTheorem.GlobalTheoremPreconditionGlobalTheorem.GlobalTheoremPrecondition {ι : Type} [Fintype ι] [Nonempty ι] (poly : GoodPoly ι) (p : Pose ℝ) (ε : ℝ) :
  TypeA compact way of saying "the pose satisfies the global theorem precondition at width ε".
We require the existence of some inner-shadow vertex S from the polyhedron, and a covector w meant to express
the direction we're projecting ℝ² → ℝ to find that S "sticks out too far" compared to all the
other outer-shadow vertices P (which the calculation of H iterates over) in the polygon that lies in ℝ².

      polyGoodPoly ι pbarPose ℝ εℝ) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ pPose ℝ ∈ Metric.closedBallMetric.closedBall.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`closedBall x ε` is the set of all points `y` with `dist y x ≤ ε`  pbarPose ℝ εℝ,
      RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 pPose ℝ polyGoodPoly ι.hullGoodPoly.hull {ι : Type} [Fintype ι] [Nonempty ι] (poly : GoodPoly ι) : Set Euc(3)