PhysLean Documentation

PhysLean.SpaceAndTime.Space.Slice

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 #

iii. Table of contents #

iv. References #

A. Slicing spaces #

source
def Space.slice {d : ℕ} (i : Fin d.succ) :
Space d.succ ≃L[ℝ] ℝ × Space d

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    A.1. Basic applications of the slicing map #

    source
    theorem Space.slice_symm_apply {d : ℕ} (i : Fin d.succ) (r : ℝ) (x : Space d) :
    ((slice i).symm (r, x)).val = fun (j : Fin (d + 1)) => (Fin.insertNthEquiv (fun (x : Fin (d + 1)) => ℝ) i) (r, x.val) j
    source
    @[simp]
    theorem Space.slice_symm_apply_self {d : ℕ} (i : Fin d.succ) (r : ℝ) (x : Space d) :
    ((slice i).symm (r, x)).val i = r
    source
    @[simp]
    theorem Space.slice_symm_apply_succAbove {d : ℕ} (i : Fin d.succ) (r : ℝ) (x : Space d) (j : Fin d) :
    ((slice i).symm (r, x)).val (i.succAbove j) = x.val j

    A.2. Slice as a measurable embedding #

    source
    theorem Space.slice_symm_measurableEmbedding {d : ℕ} (i : Fin d.succ) :
    MeasurableEmbedding ⇑(slice i).symm

    A.3. The norm of the slice map #

    source
    theorem Space.norm_slice_symm_eq {d : ℕ} (i : Fin d.succ) (r : ℝ) (x : Space d) :
    ‖(slice i).symm (r, x)‖ = √(‖r‖ ^ 2 + ‖x‖ ^ 2)
    source
    theorem Space.abs_right_le_norm_slice_symm {d : ℕ} (i : Fin d.succ) (r : ℝ) (x : Space d) :
    |r| ≤ ‖(slice i).symm (r, x)‖
    source
    @[simp]
    theorem Space.norm_left_le_norm_slice_symm {d : ℕ} (i : Fin d.succ) (r : ℝ) (x : Space d) :
    ‖x‖ ≤ ‖(slice i).symm (r, x)‖

    A.4. Derivative of the slice map #

    source
    @[simp]
    theorem Space.fderiv_slice_symm {d : ℕ} (i : Fin d.succ) (p1 : ℝ × Space d) :
    fderiv ℝ (⇑(slice i).symm) p1 = ↑(slice i).symm
    source
    theorem Space.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)
    source
    @[simp]
    theorem Space.fderiv_slice_symm_right_apply {d : ℕ} (i : Fin d.succ) (r : ℝ) (x1 x2 : Space d) :
    (fderiv ℝ (fun (x : Space d) => (slice i).symm (r, x)) x1) x2 = (slice i).symm (0, x2)
    source
    theorem Space.fderiv_fun_slice_symm_right_apply {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {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 : Space d) => f ((slice i).symm (r, x))) x1) x2 = (fderiv ℝ f ((slice i).symm (r, x1))) ((slice i).symm (0, x2))
    source
    theorem Space.fderiv_fun_slice_symm_left_apply {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {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))

    A.5. Basis in terms of slices #

    source
    theorem Space.basis_self_eq_slice {d : ℕ} (i : Fin d.succ) :
    basis i = (slice i).symm (1, 0)
    source
    theorem Space.basis_succAbove_eq_slice {d : ℕ} (i : Fin d.succ) (j : Fin d) :
    basis (i.succAbove j) = (slice i).symm (0, basis j)