Physlib.SpaceAndTime.Space.Slice — Physlib

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.SpaceAndTime.Space.Module

Slices of space

i. Overview

In this module we will define the equivalence between Space d.succ and ℝ × Space d which extracts the ith coordinate on Space d.succ.

ii. Key results

slice : The continuous linear equivalence between Space d.succ and ℝ × Space d extracting the ith coordinate.

iii. Table of contents

A. Slicing spaces

A.1. Basic applications of the slicing map

A.2. Slice as a measurable embedding

A.3. The norm of the slice map

A.4. Derivative of the slice map

A.5. Basis in terms of slices

iv. References

https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/API.20around.20.60Space.20.28d1.20.2B.20d2.29.60.20to.20.60Space.20d1.20x.20Space.20d2.60/with/556754634

@[expose] public section

A. Slicing spaces

The linear equivalence between Space d.succ and ℝ × Space d extracting the ith coordinate.

def slice {d} (i : Fin d.succ) : Space d.succ ≃L[ℝ] ℝ × Space d where
  toFun x := ⟨x i, ⟨fun j => x (Fin.succAbove i j)⟩⟩
  invFun p := ⟨fun j => Fin.insertNthEquiv (fun _ => ℝ) i (p.fst, p.snd) j⟩
  map_add' x y := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succx:Space d.succy:Space d.succ⊢ ((x + y).val i, { val := fun j => (x + y).val (i.succAbove j) }) =
  (x.val i, { val := fun j => x.val (i.succAbove j) }) + (y.val i, { val := fun j => y.val (i.succAbove j) })
    simp only [Nat.succ_eq_add_one, Prod.mk_add_mk, Prod.mk.injEq]𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succx:Space d.succy:Space d.succ⊢ (x + y).val i = x.val i + y.val i ∧
  { val := fun j => (x + y).val (i.succAbove j) } =
    { val := fun j => x.val (i.succAbove j) } + { val := fun j => y.val (i.succAbove j) }
    apply And.introleft𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succx:Space d.succy:Space d.succ⊢ (x + y).val i = x.val i + y.val iright𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succx:Space d.succy:Space d.succ⊢ { val := fun j => (x + y).val (i.succAbove j) } =
  { val := fun j => x.val (i.succAbove j) } + { val := fun j => y.val (i.succAbove j) }
    ·left𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succx:Space d.succy:Space d.succ⊢ (x + y).val i = x.val i + y.val i simpAll goals completed! 🐙
    ·right𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succx:Space d.succy:Space d.succ⊢ { val := fun j => (x + y).val (i.succAbove j) } =
  { val := fun j => x.val (i.succAbove j) } + { val := fun j => y.val (i.succAbove j) } ext jright𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succx:Space d.succy:Space d.succj:Fin d⊢ { val := fun j => (x + y).val (i.succAbove j) }.val j =
  ({ val := fun j => x.val (i.succAbove j) } + { val := fun j => y.val (i.succAbove j) }).val j
      simpAll goals completed! 🐙
  map_smul' c x := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succc:ℝx:Space d.succ⊢ ((c • x).val i, { val := fun j => (c • x).val (i.succAbove j) }) =
  (RingHom.id ℝ) c • (x.val i, { val := fun j => x.val (i.succAbove j) })
    simp only [Nat.succ_eq_add_one, smul_eq_mul, RingHom.id_apply, Prod.smul_mk,
      Prod.mk.injEq]𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succc:ℝx:Space d.succ⊢ (c • x).val i = c * x.val i ∧
  { val := fun j => (c • x).val (i.succAbove j) } = c • { val := fun j => x.val (i.succAbove j) }
    apply And.introleft𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succc:ℝx:Space d.succ⊢ (c • x).val i = c * x.val iright𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succc:ℝx:Space d.succ⊢ { val := fun j => (c • x).val (i.succAbove j) } = c • { val := fun j => x.val (i.succAbove j) }
    ·left𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succc:ℝx:Space d.succ⊢ (c • x).val i = c * x.val i simpAll goals completed! 🐙
    ·right𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succc:ℝx:Space d.succ⊢ { val := fun j => (c • x).val (i.succAbove j) } = c • { val := fun j => x.val (i.succAbove j) } ext jright𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succc:ℝx:Space d.succj:Fin d⊢ { val := fun j => (c • x).val (i.succAbove j) }.val j = (c • { val := fun j => x.val (i.succAbove j) }).val j
      simpAll goals completed! 🐙
  left_inv p := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succp:Space d.succ⊢ (fun p => { val := fun j => (Fin.insertNthEquiv (fun x => ℝ) i) (p.1, p.2.val) j })
    ((fun x => (x.val i, { val := fun j => x.val (i.succAbove j) })) p) =
  p
    simp only [Nat.succ_eq_add_one, Fin.insertNthEquiv_apply]𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succp:Space d.succ⊢ { val := fun j => i.insertNth (p.val i) (fun j => p.val (i.succAbove j)) j } = p
    ext j𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succp:Space d.succj:Fin (d + 1)⊢ { val := fun j => i.insertNth (p.val i) (fun j => p.val (i.succAbove j)) j }.val j = p.val j
    rcases Fin.eq_self_or_eq_succAbove i j with rfl | ⟨k, rfl⟩inl𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕp:Space d.succj:Fin (d + 1)⊢ { val := fun j_1 => j.insertNth (p.val j) (fun j_2 => p.val (j.succAbove j_2)) j_1 }.val j = p.val jinr𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succp:Space d.succk:Fin d⊢ { val := fun j => i.insertNth (p.val i) (fun j => p.val (i.succAbove j)) j }.val (i.succAbove k) = p.val (i.succAbove k)
    ·inl𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕp:Space d.succj:Fin (d + 1)⊢ { val := fun j_1 => j.insertNth (p.val j) (fun j_2 => p.val (j.succAbove j_2)) j_1 }.val j = p.val j simpAll goals completed! 🐙
    ·inr𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succp:Space d.succk:Fin d⊢ { val := fun j => i.insertNth (p.val i) (fun j => p.val (i.succAbove j)) j }.val (i.succAbove k) = p.val (i.succAbove k) simp only [Fin.insertNth_apply_succAbove]All goals completed! 🐙
  right_inv p := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succp:ℝ × Space d⊢ (fun x => (x.val i, { val := fun j => x.val (i.succAbove j) }))
    ((fun p => { val := fun j => (Fin.insertNthEquiv (fun x => ℝ) i) (p.1, p.2.val) j }) p) =
  p
    match p with
    | (p1, p2) =>𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succp:ℝ × Space dp1:ℝp2:Space d⊢ (fun x => (x.val i, { val := fun j => x.val (i.succAbove j) }))
    ((fun p => { val := fun j => (Fin.insertNthEquiv (fun x => ℝ) i) (p.1, p.2.val) j }) (p1, p2)) =
  (p1, p2)
    simpAll goals completed! 🐙
  continuous_toFun := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succ⊢ Continuous fun x => (x.val i, { val := fun j => x.val (i.succAbove j) }) fun_propAll goals completed! 🐙
  continuous_invFun := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succ⊢ Continuous fun p => { val := fun j => (Fin.insertNthEquiv (fun x => ℝ) i) (p.1, p.2.val) j }
    apply Continuous.comphg𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succ⊢ Continuous mkhf𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succ⊢ Continuous fun p j => (Fin.insertNthEquiv (fun x => ℝ) i) (p.1, p.2.val) j
    ·hg𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succ⊢ Continuous mk fun_propAll goals completed! 🐙
    apply continuous_pihf𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succ⊢ ∀ (i_1 : Fin d.succ), Continuous fun a => (Fin.insertNthEquiv (fun x => ℝ) i) (a.1, a.2.val) i_1
    intro jhf𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succj:Fin d.succ⊢ Continuous fun a => (Fin.insertNthEquiv (fun x => ℝ) i) (a.1, a.2.val) j
    rcases Fin.eq_self_or_eq_succAbove i j with rfl | ⟨k, rfl⟩hf.inl𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕj:Fin d.succ⊢ Continuous fun a => (Fin.insertNthEquiv (fun x => ℝ) j) (a.1, a.2.val) jhf.inr𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succk:Fin d⊢ Continuous fun a => (Fin.insertNthEquiv (fun x => ℝ) i) (a.1, a.2.val) (i.succAbove k)
    ·hf.inl𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕj:Fin d.succ⊢ Continuous fun a => (Fin.insertNthEquiv (fun x => ℝ) j) (a.1, a.2.val) j simphf.inl𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕj:Fin d.succ⊢ Continuous fun a => a.1
      fun_propAll goals completed! 🐙
    ·hf.inr𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succk:Fin d⊢ Continuous fun a => (Fin.insertNthEquiv (fun x => ℝ) i) (a.1, a.2.val) (i.succAbove k) simphf.inr𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succk:Fin d⊢ Continuous fun a => a.2.val k
      fun_propAll goals completed! 🐙

A.1. Basic applications of the slicing map

              lemma slice_symm_apply {d : ℕ} (i : Fin d.succ) (r : ℝ) (x : Space d) :
    (slice i).symm (r, x) = fun j =>
      Fin.insertNthEquiv (fun _ => ℝ) i (r, x) j := byd:ℕi:Fin d.succr:ℝx:Space d⊢ ((slice i).symm (r, x)).val = fun j => (Fin.insertNthEquiv (fun x => ℝ) i) (r, x.val) j rflAll goals completed! 🐙@[simp]
lemma slice_symm_apply_self {d : ℕ} (i : Fin d.succ) (r : ℝ) (x : Space d) :
    (slice i).symm (r, x) i = r := byd:ℕi:Fin d.succr:ℝx:Space d⊢ ((slice i).symm (r, x)).val i = r
  simp [slice_symm_apply]All goals completed! 🐙@[simp]
lemma slice_symm_apply_succAbove {d : ℕ} (i : Fin d.succ) (r : ℝ) (x : Space d) (j : Fin d) :
    (slice i).symm (r, x) (Fin.succAbove i j) = x j := byd:ℕi:Fin d.succr:ℝx:Space dj:Fin d⊢ ((slice i).symm (r, x)).val (i.succAbove j) = x.val j
  simp [slice_symm_apply]All goals completed! 🐙

A.2. Slice as a measurable embedding

lemma slice_symm_measurableEmbedding {d : ℕ} (i : Fin d.succ) :
    MeasurableEmbedding (slice i).symm := byd:ℕi:Fin d.succ⊢ MeasurableEmbedding ⇑(slice i).symm
  change MeasurableEmbedding (fun (p : ℝ × Space d) => (Space.equivPi d.succ).symm
    ((MeasurableEquiv.piFinSuccAbove (fun _ => ℝ) i).symm (p.fst, p.snd)))d:ℕi:Fin d.succ⊢ MeasurableEmbedding fun p => (equivPi d.succ).symm ((MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm (p.1, p.2.val))
  apply MeasurableEmbedding.comphgd:ℕi:Fin d.succ⊢ MeasurableEmbedding ⇑(equivPi d.succ).symmhfd:ℕi:Fin d.succ⊢ MeasurableEmbedding fun p => (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm (p.1, p.2.val)
  ·hgd:ℕi:Fin d.succ⊢ MeasurableEmbedding ⇑(equivPi d.succ).symm apply Measurable.measurableEmbeddinghg.f_measd:ℕi:Fin d.succ⊢ Measurable ⇑(equivPi d.succ).symmhg.f_injd:ℕi:Fin d.succ⊢ Function.Injective ⇑(equivPi d.succ).symm
    ·hg.f_measd:ℕi:Fin d.succ⊢ Measurable ⇑(equivPi d.succ).symm fun_propAll goals completed! 🐙
    ·hg.f_injd:ℕi:Fin d.succ⊢ Function.Injective ⇑(equivPi d.succ).symm exact ContinuousLinearEquiv.injective (equivPi d.succ).symmAll goals completed! 🐙
  apply MeasurableEmbedding.comphf.hgd:ℕi:Fin d.succ⊢ MeasurableEmbedding ⇑(MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symmhf.hfd:ℕi:Fin d.succ⊢ MeasurableEmbedding fun p => (p.1, p.2.val)
  ·hf.hgd:ℕi:Fin d.succ⊢ MeasurableEmbedding ⇑(MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm exact MeasurableEquiv.measurableEmbedding (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symmAll goals completed! 🐙
  ·hf.hfd:ℕi:Fin d.succ⊢ MeasurableEmbedding fun p => (p.1, p.2.val) apply Measurable.measurableEmbeddinghf.hf.f_measd:ℕi:Fin d.succ⊢ Measurable fun p => (p.1, p.2.val)hf.hf.f_injd:ℕi:Fin d.succ⊢ Function.Injective fun p => (p.1, p.2.val)
    ·hf.hf.f_measd:ℕi:Fin d.succ⊢ Measurable fun p => (p.1, p.2.val) fun_propAll goals completed! 🐙
    ·hf.hf.f_injd:ℕi:Fin d.succ⊢ Function.Injective fun p => (p.1, p.2.val) intro a b hhf.hf.f_injd:ℕi:Fin d.succa:ℝ × Space db:ℝ × Space dh:(fun p => (p.1, p.2.val)) a = (fun p => (p.1, p.2.val)) b⊢ a = b
      match a, b with
      | (r1, x1), (r2, x2) =>d:ℕi:Fin d.succa:ℝ × Space db:ℝ × Space dr1:ℝx1:Space dr2:ℝx2:Space dh:(fun p => (p.1, p.2.val)) (r1, x1) = (fun p => (p.1, p.2.val)) (r2, x2)⊢ (r1, x1) = (r2, x2)
      simp_allAll goals completed! 🐙

A.3. The norm of the slice map

              

lemma norm_slice_symm_eq {d : ℕ} (i : Fin d.succ) (r : ℝ) (x : Space d) :
    ‖(slice i).symm (r, x)‖ = √(‖r‖ ^ 2 + ‖x‖ ^ 2) := byd:ℕi:Fin d.succr:ℝx:Space d⊢ ‖(slice i).symm (r, x)‖ = √(‖r‖ ^ 2 + ‖x‖ ^ 2)
  simp [Nat.succ_eq_add_one, norm_eq]d:ℕi:Fin d.succr:ℝx:Space d⊢ √(∑ i_1, ((slice i).symm (r, x)).val i_1 ^ 2) = √(r ^ 2 + √(∑ i, x.val i ^ 2) ^ 2)
  congrd:ℕi:Fin d.succr:ℝx:Space d⊢ ∑ i_1, ((slice i).symm (r, x)).val i_1 ^ 2 = r ^ 2 + √(∑ i, x.val i ^ 2) ^ 2
  rw [Fin.sum_univ_succAbove _ id:ℕi:Fin d.succr:ℝx:Space d⊢ ((slice i).symm (r, x)).val i ^ 2 + ∑ i_1, ((slice i).symm (r, x)).val (i.succAbove i_1) ^ 2 =
  r ^ 2 + √(∑ i, x.val i ^ 2) ^ 2d:ℕi:Fin d.succr:ℝx:Space d⊢ ((slice i).symm (r, x)).val i ^ 2 + ∑ i_1, ((slice i).symm (r, x)).val (i.succAbove i_1) ^ 2 =
  r ^ 2 + √(∑ i, x.val i ^ 2) ^ 2]d:ℕi:Fin d.succr:ℝx:Space d⊢ ((slice i).symm (r, x)).val i ^ 2 + ∑ i_1, ((slice i).symm (r, x)).val (i.succAbove i_1) ^ 2 =
  r ^ 2 + √(∑ i, x.val i ^ 2) ^ 2
  simp [slice_symm_apply_succAbove]d:ℕi:Fin d.succr:ℝx:Space d⊢ ∑ x_1, x.val x_1 ^ 2 = √(∑ x_1, x.val x_1 ^ 2) ^ 2
  refine Eq.symm (Real.sq_sqrt ?_)d:ℕi:Fin d.succr:ℝx:Space d⊢ 0 ≤ ∑ x_1, x.val x_1 ^ 2
  positivityAll goals completed! 🐙

lemma abs_right_le_norm_slice_symm {d : ℕ} (i : Fin d.succ) (r : ℝ) (x : Space d) :
    |r| ≤ ‖(slice i).symm (r, x)‖ := byd:ℕi:Fin d.succr:ℝx:Space d⊢ |r| ≤ ‖(slice i).symm (r, x)‖
  rw [norm_slice_symm_eqd:ℕi:Fin d.succr:ℝx:Space d⊢ |r| ≤ √(‖r‖ ^ 2 + ‖x‖ ^ 2)d:ℕi:Fin d.succr:ℝx:Space d⊢ |r| ≤ √(‖r‖ ^ 2 + ‖x‖ ^ 2)]d:ℕi:Fin d.succr:ℝx:Space d⊢ |r| ≤ √(‖r‖ ^ 2 + ‖x‖ ^ 2)
  refine (le_sqrt (byd:ℕi:Fin d.succr:ℝx:Space d⊢ 0 ≤ |r| positivityAll goals completed! 🐙) (byd:ℕi:Fin d.succr:ℝx:Space d⊢ 0 ≤ ‖r‖ ^ 2 + ‖x‖ ^ 2 positivityAll goals completed! 🐙)).mpr ?_
  simpAll goals completed! 🐙

@[simp]
lemma norm_left_le_norm_slice_symm {d : ℕ} (i : Fin d.succ) (r : ℝ) (x : Space d) :
    ‖x‖ ≤ ‖(slice i).symm (r, x)‖ := byd:ℕi:Fin d.succr:ℝx:Space d⊢ ‖x‖ ≤ ‖(slice i).symm (r, x)‖
  rw [norm_slice_symm_eqd:ℕi:Fin d.succr:ℝx:Space d⊢ ‖x‖ ≤ √(‖r‖ ^ 2 + ‖x‖ ^ 2)d:ℕi:Fin d.succr:ℝx:Space d⊢ ‖x‖ ≤ √(‖r‖ ^ 2 + ‖x‖ ^ 2)]d:ℕi:Fin d.succr:ℝx:Space d⊢ ‖x‖ ≤ √(‖r‖ ^ 2 + ‖x‖ ^ 2)
  refine (le_sqrt (byd:ℕi:Fin d.succr:ℝx:Space d⊢ 0 ≤ ‖x‖ positivityAll goals completed! 🐙) (byd:ℕi:Fin d.succr:ℝx:Space d⊢ 0 ≤ ‖r‖ ^ 2 + ‖x‖ ^ 2 positivityAll goals completed! 🐙)).mpr ?_
  simp only [norm_eq_abs, sq_abs, le_add_iff_nonneg_left]d:ℕi:Fin d.succr:ℝx:Space d⊢ 0 ≤ r ^ 2
  positivityAll goals completed! 🐙

A.4. Derivative of the slice map

              

@[simp]
lemma fderiv_slice_symm {d : ℕ} (i : Fin d.succ) (p1 : ℝ × Space d) :
    fderiv ℝ (slice i).symm p1 = (slice i).symm := byd:ℕi:Fin d.succp1:ℝ × Space d⊢ fderiv ℝ (⇑(slice i).symm) p1 = ↑(slice i).symm
  rw [ContinuousLinearEquiv.fderivd:ℕi:Fin d.succp1:ℝ × Space d⊢ ↑(slice i).symm = ↑(slice i).symmAll goals completed! 🐙]All goals completed! 🐙

lemma fderiv_slice_symm_left_apply {d : ℕ} (i : Fin d.succ) (x : Space d) (r1 r2 : ℝ) :
    (fderiv ℝ (fun r => (slice i).symm (r, x))) r1 r2 = (slice i).symm (r2, 0) := byd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ (fderiv ℝ (fun r => (slice i).symm (r, x)) r1) r2 = (slice i).symm (r2, 0)
  rw [fderiv_fun_comp,d:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ (fderiv ℝ ⇑(slice i).symm (r1, x) ∘SL fderiv ℝ (fun r => (r, x)) r1) r2 = (slice i).symm (r2, 0)hgd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ ⇑(slice i).symm (r1, x)hfd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ (fun r => (r, x)) r1d:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ (fderiv ℝ ⇑(slice i).symm (r1, x) ∘SL (fderiv ℝ (fun r => r) r1).prod (fderiv ℝ (fun r => x) r1)) r2 =
  (slice i).symm (r2, 0)d:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ (fun r => x) r1hgd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ ⇑(slice i).symm (r1, x)hfd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ (fun r => (r, x)) r1 DifferentiableAt.fderiv_prodMk (byd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ (fun r => r) r1d:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ (fderiv ℝ ⇑(slice i).symm (r1, x) ∘SL (fderiv ℝ (fun r => r) r1).prod (fderiv ℝ (fun r => x) r1)) r2 =
  (slice i).symm (r2, 0)d:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ (fun r => x) r1hgd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ ⇑(slice i).symm (r1, x)hfd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ (fun r => (r, x)) r1 fun_propAll goals completed! 🐙d:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ (fderiv ℝ ⇑(slice i).symm (r1, x) ∘SL (fderiv ℝ (fun r => r) r1).prod (fderiv ℝ (fun r => x) r1)) r2 =
  (slice i).symm (r2, 0)d:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ (fun r => x) r1hgd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ ⇑(slice i).symm (r1, x)hfd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ (fun r => (r, x)) r1)]d:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ (fderiv ℝ ⇑(slice i).symm (r1, x) ∘SL (fderiv ℝ (fun r => r) r1).prod (fderiv ℝ (fun r => x) r1)) r2 =
  (slice i).symm (r2, 0)d:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ (fun r => x) r1hgd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ ⇑(slice i).symm (r1, x)hfd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ (fun r => (r, x)) r1
  simp only [Nat.succ_eq_add_one, fderiv_slice_symm, fderiv_fun_id, fderiv_fun_const, Pi.zero_apply,
    ContinuousLinearMap.coe_comp, ContinuousLinearEquiv.coe_coe, Function.comp_apply,
    ContinuousLinearMap.prod_apply, ContinuousLinearMap.coe_id', id_eq,
    _root_.zero_apply]d:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ (fun r => x) r1hgd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ ⇑(slice i).symm (r1, x)hfd:ℕi:Fin d.succx:Space dr1:ℝr2:ℝ⊢ DifferentiableAt ℝ (fun r => (r, x)) r1
  repeat' fun_propAll goals completed! 🐙

@[simp]
lemma fderiv_slice_symm_right_apply {d : ℕ} (i : Fin d.succ) (r : ℝ)
    (x1 x2 : Space d) :
    (fderiv ℝ (fun x => (slice i).symm (r, x))) x1 x2 = (slice i).symm (0, x2) := byd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ (fderiv ℝ (fun x => (slice i).symm (r, x)) x1) x2 = (slice i).symm (0, x2)
  rw [fderiv_fun_comp,d:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ (fderiv ℝ ⇑(slice i).symm (r, x1) ∘SL fderiv ℝ (Prod.mk r) x1) x2 = (slice i).symm (0, x2)hgd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ ⇑(slice i).symm (r, x1)hfd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ (Prod.mk r) x1d:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ (fderiv ℝ ⇑(slice i).symm (r, x1) ∘SL (fderiv ℝ (fun x => r) x1).prod (fderiv ℝ (fun x => x) x1)) x2 =
  (slice i).symm (0, x2)d:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ (fun x => x) x1hgd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ ⇑(slice i).symm (r, x1)hfd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ (Prod.mk r) x1 DifferentiableAt.fderiv_prodMk (byd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ (fun x => r) x1d:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ (fderiv ℝ ⇑(slice i).symm (r, x1) ∘SL (fderiv ℝ (fun x => r) x1).prod (fderiv ℝ (fun x => x) x1)) x2 =
  (slice i).symm (0, x2)d:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ (fun x => x) x1hgd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ ⇑(slice i).symm (r, x1)hfd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ (Prod.mk r) x1 fun_propAll goals completed! 🐙d:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ (fderiv ℝ ⇑(slice i).symm (r, x1) ∘SL (fderiv ℝ (fun x => r) x1).prod (fderiv ℝ (fun x => x) x1)) x2 =
  (slice i).symm (0, x2)d:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ (fun x => x) x1hgd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ ⇑(slice i).symm (r, x1)hfd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ (Prod.mk r) x1)]d:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ (fderiv ℝ ⇑(slice i).symm (r, x1) ∘SL (fderiv ℝ (fun x => r) x1).prod (fderiv ℝ (fun x => x) x1)) x2 =
  (slice i).symm (0, x2)d:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ (fun x => x) x1hgd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ ⇑(slice i).symm (r, x1)hfd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ (Prod.mk r) x1
  simp only [Nat.succ_eq_add_one, fderiv_slice_symm, fderiv_fun_const, Pi.zero_apply, fderiv_fun_id,
    ContinuousLinearMap.coe_comp, ContinuousLinearEquiv.coe_coe, Function.comp_apply,
    ContinuousLinearMap.prod_apply, _root_.zero_apply, ContinuousLinearMap.coe_id',
    id_eq]d:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ (fun x => x) x1hgd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ ⇑(slice i).symm (r, x1)hfd:ℕi:Fin d.succr:ℝx1:Space dx2:Space d⊢ DifferentiableAt ℝ (Prod.mk r) x1
  repeat' fun_propAll goals completed! 🐙

lemma fderiv_fun_slice_symm_right_apply {d : ℕ} (i : Fin d.succ) (r : ℝ)
    (x1 x2 : Space d) (f : Space d.succ → F) (hf : DifferentiableAt ℝ f ((slice i).symm (r, x1))) :
    (fderiv ℝ (fun x => f ((slice i).symm (r, x)))) x1 x2 =
    fderiv ℝ f ((slice i).symm (r, x1)) ((slice i).symm (0, x2)) := byF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr:ℝx1:Space dx2:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r, x1))⊢ (fderiv ℝ (fun x => f ((slice i).symm (r, x))) x1) x2 = (fderiv ℝ f ((slice i).symm (r, x1))) ((slice i).symm (0, x2))
  rw [fderiv_fun_comp _ _ (byF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr:ℝx1:Space dx2:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r, x1))⊢ DifferentiableAt ℝ (fun x => (slice i).symm (r, x)) x1F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr:ℝx1:Space dx2:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r, x1))⊢ (fderiv ℝ f ((slice i).symm (r, x1)) ∘SL fderiv ℝ (fun x => (slice i).symm (r, x)) x1) x2 =
  (fderiv ℝ f ((slice i).symm (r, x1))) ((slice i).symm (0, x2))F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr:ℝx1:Space dx2:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r, x1))⊢ DifferentiableAt ℝ f ((slice i).symm (r, x1)) fun_propAll goals completed! 🐙F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr:ℝx1:Space dx2:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r, x1))⊢ (fderiv ℝ f ((slice i).symm (r, x1)) ∘SL fderiv ℝ (fun x => (slice i).symm (r, x)) x1) x2 =
  (fderiv ℝ f ((slice i).symm (r, x1))) ((slice i).symm (0, x2))F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr:ℝx1:Space dx2:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r, x1))⊢ DifferentiableAt ℝ f ((slice i).symm (r, x1)))]F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr:ℝx1:Space dx2:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r, x1))⊢ (fderiv ℝ f ((slice i).symm (r, x1)) ∘SL fderiv ℝ (fun x => (slice i).symm (r, x)) x1) x2 =
  (fderiv ℝ f ((slice i).symm (r, x1))) ((slice i).symm (0, x2))F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr:ℝx1:Space dx2:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r, x1))⊢ DifferentiableAt ℝ f ((slice i).symm (r, x1))
  simp only [Nat.succ_eq_add_one, ContinuousLinearMap.coe_comp, Function.comp_apply,
    fderiv_slice_symm_right_apply]F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr:ℝx1:Space dx2:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r, x1))⊢ DifferentiableAt ℝ f ((slice i).symm (r, x1))
  fun_propAll goals completed! 🐙

lemma fderiv_fun_slice_symm_left_apply {d : ℕ} (i : Fin d.succ) (r1 r2 : ℝ)
    (x : Space d) (f : Space d.succ → F) (hf : DifferentiableAt ℝ f ((slice i).symm (r1, x))) :
    (fderiv ℝ (fun r => f ((slice i).symm (r, x)))) r1 r2 =
    fderiv ℝ f ((slice i).symm (r1, x)) ((slice i).symm (r2, 0)) := byF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr1:ℝr2:ℝx:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r1, x))⊢ (fderiv ℝ (fun r => f ((slice i).symm (r, x))) r1) r2 = (fderiv ℝ f ((slice i).symm (r1, x))) ((slice i).symm (r2, 0))
  rw [fderiv_fun_comp _ _ (byF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr1:ℝr2:ℝx:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r1, x))⊢ DifferentiableAt ℝ (fun r => (slice i).symm (r, x)) r1F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr1:ℝr2:ℝx:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r1, x))⊢ (fderiv ℝ f ((slice i).symm (r1, x)) ∘SL fderiv ℝ (fun r => (slice i).symm (r, x)) r1) r2 =
  (fderiv ℝ f ((slice i).symm (r1, x))) ((slice i).symm (r2, 0))F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr1:ℝr2:ℝx:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r1, x))⊢ DifferentiableAt ℝ f ((slice i).symm (r1, x)) fun_propAll goals completed! 🐙F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr1:ℝr2:ℝx:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r1, x))⊢ (fderiv ℝ f ((slice i).symm (r1, x)) ∘SL fderiv ℝ (fun r => (slice i).symm (r, x)) r1) r2 =
  (fderiv ℝ f ((slice i).symm (r1, x))) ((slice i).symm (r2, 0))F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr1:ℝr2:ℝx:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r1, x))⊢ DifferentiableAt ℝ f ((slice i).symm (r1, x)))]F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr1:ℝr2:ℝx:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r1, x))⊢ (fderiv ℝ f ((slice i).symm (r1, x)) ∘SL fderiv ℝ (fun r => (slice i).symm (r, x)) r1) r2 =
  (fderiv ℝ f ((slice i).symm (r1, x))) ((slice i).symm (r2, 0))F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr1:ℝr2:ℝx:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r1, x))⊢ DifferentiableAt ℝ f ((slice i).symm (r1, x))
  simp only [Nat.succ_eq_add_one, ContinuousLinearMap.coe_comp, Function.comp_apply,
    fderiv_slice_symm_left_apply]F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕi:Fin d.succr1:ℝr2:ℝx:Space df:Space d.succ → Fhf:DifferentiableAt ℝ f ((slice i).symm (r1, x))⊢ DifferentiableAt ℝ f ((slice i).symm (r1, x))
  fun_propAll goals completed! 🐙

A.5. Basis in terms of slices

lemma basis_self_eq_slice {d : ℕ} (i : Fin d.succ) :
    basis i = (slice i).symm (1, 0) := byd:ℕi:Fin d.succ⊢ basis i = (slice i).symm (1, 0)
  ext jd:ℕi:Fin d.succj:Fin d.succ⊢ (basis i).val j = ((slice i).symm (1, 0)).val j
  rcases Fin.eq_self_or_eq_succAbove i j with rfl | ⟨k, rfl⟩inld:ℕj:Fin d.succ⊢ (basis j).val j = ((slice j).symm (1, 0)).val jinrd:ℕi:Fin d.succk:Fin d⊢ (basis i).val (i.succAbove k) = ((slice i).symm (1, 0)).val (i.succAbove k)
  ·inld:ℕj:Fin d.succ⊢ (basis j).val j = ((slice j).symm (1, 0)).val j simp [slice_symm_apply_self]All goals completed! 🐙
  ·inrd:ℕi:Fin d.succk:Fin d⊢ (basis i).val (i.succAbove k) = ((slice i).symm (1, 0)).val (i.succAbove k) simp [basis_apply]All goals completed! 🐙

lemma basis_succAbove_eq_slice {d : ℕ} (i : Fin d.succ) (j : Fin d) :
    basis (Fin.succAbove i j) = (slice i).symm (0, basis j) := byd:ℕi:Fin d.succj:Fin d⊢ basis (i.succAbove j) = (slice i).symm (0, basis j)
  ext kd:ℕi:Fin d.succj:Fin dk:Fin (d + 1)⊢ (basis (i.succAbove j)).val k = ((slice i).symm (0, basis j)).val k
  rcases Fin.eq_self_or_eq_succAbove i k with rfl | ⟨l, rfl⟩inld:ℕj:Fin dk:Fin (d + 1)⊢ (basis (k.succAbove j)).val k = ((slice k).symm (0, basis j)).val kinrd:ℕi:Fin d.succj:Fin dl:Fin d⊢ (basis (i.succAbove j)).val (i.succAbove l) = ((slice i).symm (0, basis j)).val (i.succAbove l)
  ·inld:ℕj:Fin dk:Fin (d + 1)⊢ (basis (k.succAbove j)).val k = ((slice k).symm (0, basis j)).val k simp [basis_apply, slice_symm_apply_self]All goals completed! 🐙
  ·inrd:ℕi:Fin d.succj:Fin dl:Fin d⊢ (basis (i.succAbove j)).val (i.succAbove l) = ((slice i).symm (0, basis j)).val (i.succAbove l) simp [basis_apply, slice_symm_apply_succAbove]All goals completed! 🐙