Imports
/- Copyright (c) 2025 Zhi Kai Pong. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Zhi Kai Pong -/ module public import Physlib.SpaceAndTime.Space.CrossProduct public import Physlib.SpaceAndTime.Space.Derivatives.Laplacian

Wave equation

i. Overview

In this module we define the wave equation in d-dimensional Euclidean space, and prove that plane waves are solutions to the wave equation. By a plne wave we mean a function of the form f(t, x) = f₀(⟪x, s⟫_ℝ - c * t) where s is a direction vector and c is the propagation speed.

ii. Key results

    WaveEquation: The general form of the wave equation where c is the propagation speed.

    planeWave: A vector-valued plane wave travelling in the direction of s with propagation speed c.

    planeWave_waveEquation: The plane wave satisfies the wave equation.

iii. Table of contents

    A. The wave equation

    B. Plane wave solutions

      B.1. Definition of a plane wave

      B.2. Differentiablity conditions

      B.3. Time derivatives of plane waves

      B.4. Space derivatives of plane waves

      B.5. Laplacian of plane waves

      B.6. Plane waves satisfy the wave equation

    C. Old lemmas used throughout files

iv. References

@[expose] public section

A. The wave equation

The general form of the wave equation where c is the propagation speed.

def WaveEquation {d} (f : Time → Space d → EuclideanSpace ℝ (Fin d)) (t : Time) (x : Space d) (c : ℝ) : Prop := c^2 • Δᵥ (f t) x - ∂ₜ (fun t => (∂ₜ (fun t => f t x) t)) t = 0

B. Plane wave solutions

B.1. Definition of a plane wave

lemma planeWave_eq {d f₀ c x} {s : Direction d} : planeWave f₀ c s t x = f₀ (⟪x, s.unit⟫_ℝ - c * t) := rfl

B.2. Differentiablity conditions

@[fun_prop] lemma planeWave_differentiable_time {d f₀ c x} {s : Direction d} (h' : Differentiable ℝ f₀) : Differentiable ℝ (fun t => planeWave f₀ c s t x) := d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun t => planeWave f₀ c s t x d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun t => f₀ (⟪x, s.unit⟫_ℝ - c * t.val) d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ f₀d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun t => ⟪x, s.unit⟫_ℝ - c * t.val d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ f₀d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun t => ⟪x, s.unit⟫_ℝ - c * t.val All goals completed! 🐙@[fun_prop] lemma planeWave_differentiable_space {d f₀ c t} {s : Direction d} (h' : Differentiable ℝ f₀) : Differentiable ℝ (fun x => planeWave f₀ c s t x) := d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => planeWave f₀ c s t x d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => f₀ (⟪x, s.unit⟫_ℝ - c * t.val) d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ f₀d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ⟪x, s.unit⟫_ℝ - c * t.val d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ f₀ All goals completed! 🐙 d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ⟪x, s.unit⟫_ℝ - c * t.val d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ⟪x, s.unit⟫_ℝd:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => c * t.val d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ⟪x, s.unit⟫_ℝ d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => xd:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => s.unit d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => x All goals completed! 🐙 d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => s.unit All goals completed! 🐙 d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝt:Times:Direction dh':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => c * t.val All goals completed! 🐙@[fun_prop] lemma planeWave_differentiable {s : Direction d} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} (h' : Differentiable ℝ f₀) : Differentiable ℝ ↿(planeWave f₀ c s) := d:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ ↿(planeWave f₀ c s) d:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ ↿fun t x => f₀ (⟪x, s.unit⟫_ℝ - c * t.val) d:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ (f₀ ∘ fun x => match x with | (t, x) => ⟪x, s.unit⟫_ℝ - c * t.val) d:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ f₀d:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => match x with | (t, x) => ⟪x, s.unit⟫_ℝ - c * t.val d:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ f₀ All goals completed! 🐙 d:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => match x with | (t, x) => ⟪x, s.unit⟫_ℝ - c * t.val d:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ⟪x.2, s.unit⟫_ℝd:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => c * x.1.val d:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ⟪x.2, s.unit⟫_ℝ d:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ Prod.sndd:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => s.unit repeat All goals completed! 🐙 d:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => c * x.1.val All goals completed! 🐙

B.3. Time derivatives of plane waves

d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ ((fderiv ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t.val) ∘SL (-(c • fderiv ℝ Time.val t))) 1).ofLp i = ((-c • fun t => planeWave (fun x => (fderiv ℝ f₀ x) 1) c s t x) t).ofLp id:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ Time.val td:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t.val)d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ (fun t => ⟪x, s.unit⟫_ℝ - c * t.val) t d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ ((fderiv ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t.val) ∘SL fderiv ℝ Time.val t) 1).ofLp i = (planeWave (fun x => (fderiv ℝ f₀ x) 1) c s t x).ofLp i ∨ c = 0d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ Time.val td:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t.val)d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ (fun t => ⟪x, s.unit⟫_ℝ - c * t.val) t d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ ((fderiv ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t.val) ∘SL fderiv ℝ Time.val t) 1).ofLp i = (planeWave (fun x => (fderiv ℝ f₀ x) 1) c s t x).ofLp id:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ Time.val td:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t.val)d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ (fun t => ⟪x, s.unit⟫_ℝ - c * t.val) t d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ (_root_.deriv f₀ (⟪x, s.unit⟫_ℝ - c * t.val)).ofLp i = (planeWave (fun x => _root_.deriv f₀ x) c s t x).ofLp id:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ Time.val td:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t.val)d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ (fun t => ⟪x, s.unit⟫_ℝ - c * t.val) t d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ Time.val td:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t.val)d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':Differentiable ℝ f₀t:Timei:Fin d⊢ DifferentiableAt ℝ (fun t => ⟪x, s.unit⟫_ℝ - c * t.val) t repeat All goals completed! 🐙d:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝx:Space ds:Direction dh':ContDiff ℝ 2 f₀t:Timei:Fin d⊢ (fun x => _root_.deriv (fun y => _root_.deriv f₀ y) x) = iteratedDeriv 2 f₀ All goals completed! 🐙

B.4. Space derivatives of plane waves

t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ (⟪x, (fderiv ℝ (fun x => s.unit) x) (Space.basis i)⟫_ℝ + ⟪(fderiv ℝ (fun x => x) x) (Space.basis i), s.unit⟫_ℝ) * (_root_.deriv f₀ (⟪x, s.unit⟫_ℝ - c * t.val)).ofLp j = s.unit.val i * (planeWave (fun x => _root_.deriv f₀ x) c s t x).ofLp jt:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ (fun x => x) xt:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ (fun x => s.unit) xt:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t.val)t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ (fun x => ⟪x, s.unit⟫_ℝ - c * t.val) x t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ (_root_.deriv f₀ (⟪x, s.unit⟫_ℝ - c * t.val)).ofLp j = (planeWave (fun x => _root_.deriv f₀ x) c s t x).ofLp j ∨ s.unit.val i = 0t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ (fun x => x) xt:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ (fun x => s.unit) xt:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t.val)t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ (fun x => ⟪x, s.unit⟫_ℝ - c * t.val) x t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ (_root_.deriv f₀ (⟪x, s.unit⟫_ℝ - c * t.val)).ofLp j = (planeWave (fun x => _root_.deriv f₀ x) c s t x).ofLp jt:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ (fun x => x) xt:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ (fun x => s.unit) xt:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t.val)t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ (fun x => ⟪x, s.unit⟫_ℝ - c * t.val) x t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ (fun x => x) xt:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ (fun x => s.unit) xt:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t.val)t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dx:Space dj:Fin d⊢ DifferentiableAt ℝ (fun x => ⟪x, s.unit⟫_ℝ - c * t.val) x repeat All goals completed! 🐙t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dj:Fin dx:Space d⊢ ((s.unit.val i • fun x => planeWave (fun x => (fderiv ℝ f₀ x) 1) c s t x) x).ofLp j = s.unit.val i * (planeWave (fun x => _root_.deriv f₀ x) c s t x).ofLp jt:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dj:Fin dx:Space d⊢ Differentiable ℝ f₀t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dj:Fin dx:Space d⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj j)) (planeWave f₀ c s t x)t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dj:Fin dx:Space d⊢ DifferentiableAt ℝ (fun x => planeWave f₀ c s t x) x t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dj:Fin dx:Space d⊢ Differentiable ℝ f₀t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dj:Fin dx:Space d⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj j)) (planeWave f₀ c s t x)t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dj:Fin dx:Space d⊢ DifferentiableAt ℝ (fun x => planeWave f₀ c s t x) x t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dj:Fin dx:Space d⊢ Differentiable ℝ f₀ All goals completed! 🐙 t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dj:Fin dx:Space d⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj j)) (planeWave f₀ c s t x) All goals completed! 🐙 t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':Differentiable ℝ f₀i:Fin dj:Fin dx:Space d⊢ DifferentiableAt ℝ (fun x => planeWave f₀ c s t x) x All goals completed! 🐙t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':ContDiff ℝ 2 f₀i:Fin dx✝:Space dx:ℝ⊢ _root_.deriv (fun x => _root_.deriv f₀ x) x = _root_.deriv (iteratedDeriv 1 f₀) x All goals completed! 🐙 t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':ContDiff ℝ 2 f₀i:Fin dx:Space d⊢ Differentiable ℝ fun x => _root_.deriv f₀ x All goals completed! 🐙 t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':ContDiff ℝ 2 f₀i:Fin dx:Space d⊢ DifferentiableAt ℝ (fun x => planeWave (fun x => (fderiv ℝ f₀ x) 1) c s t x) x All goals completed! 🐙t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':ContDiff ℝ 2 f₀i:Fin dj:Fin dx:Space d⊢ (fun x => _root_.deriv (fun y => _root_.deriv f₀ y) x) = iteratedDeriv 2 f₀ All goals completed! 🐙 all_goals All goals completed! 🐙 t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':ContDiff ℝ 2 f₀i:Fin dj:Fin dx:Space d⊢ DifferentiableAt ℝ (fun x => (planeWave (fun x => (fderiv ℝ f₀ x) 1) c s t x).ofLp j) x All goals completed! 🐙

B.5. Laplacian of plane waves

t:Timed:ℕf₀:ℝ → EuclideanSpace ℝ (Fin d)c:ℝs:Direction dh':ContDiff ℝ 2 f₀x:Space dj:Fin d⊢ (∑ i, s.unit.val i ^ 2) * (planeWave (fun x => iteratedDeriv 2 f₀ x) c s t x).ofLp j = (planeWave (fun x => iteratedDeriv 2 f₀ x) c s t x).ofLp j All goals completed! 🐙

B.6. Plane waves satisfy the wave equation

The plane wave satisfies the wave equation.

d:ℕc:ℝs:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)hf₀:ContDiff ℝ 2 f₀t:Timex:Space d⊢ c ^ 2 • (fun x => planeWave (fun x => iteratedDeriv 2 f₀ x) c s t x) x - (c ^ 2 • fun t => planeWave (iteratedDeriv 2 f₀) c s t x) t = 0 All goals completed! 🐙

C. Old lemmas used throughout files

These lemmas will eventually be moved, renamed and/or replaced.

lemma wave_differentiable {s : Direction d} {c : ℝ} {x : Space d} : DifferentiableAt ℝ (fun x => inner ℝ x s.unit - c * t) x := d:ℕt:ℝs:Direction dc:ℝx:Space d⊢ DifferentiableAt ℝ (fun x => ⟪x, s.unit⟫_ℝ - c * t) x d:ℕt:ℝs:Direction dc:ℝx:Space d⊢ DifferentiableAt ℝ (fun x => ⟪x, s.unit⟫_ℝ) xd:ℕt:ℝs:Direction dc:ℝx:Space d⊢ DifferentiableAt ℝ (fun x => c * t) x d:ℕt:ℝs:Direction dc:ℝx:Space d⊢ DifferentiableAt ℝ (fun x => x) xd:ℕt:ℝs:Direction dc:ℝx:Space d⊢ DifferentiableAt ℝ (fun x => s.unit) xd:ℕt:ℝs:Direction dc:ℝx:Space d⊢ DifferentiableAt ℝ (fun x => c * t) x repeat All goals completed! 🐙d:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) xhdi':(fderiv ℝ (fun x' => (f₀' (⟪x', s.unit⟫_ℝ - c * t)) (s.unit.val u)) x) (Space.basis u) = s.unit.val u ^ 2 • (f₀'' (⟪x, s.unit⟫_ℝ - c * t)) 1⊢ ⟪(f₀' (⟪x, s.unit⟫_ℝ - c * t)) (s.unit.val u), (fderiv ℝ (fun x' => EuclideanSpace.single v 1) x) (Space.basis u)⟫_ℝ + ⟪s.unit.val u ^ 2 • (f₀'' (⟪x, s.unit⟫_ℝ - c * t)) 1, EuclideanSpace.single v 1⟫_ℝ = ⟪s.unit.val u ^ 2 • (f₀'' (⟪x, s.unit⟫_ℝ - c * t)) 1, EuclideanSpace.single v 1⟫_ℝd:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) x⊢ DifferentiableAt ℝ (fun x' => (f₀' (⟪x', s.unit⟫_ℝ - c * t)) (s.unit.val u)) xd:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) x⊢ DifferentiableAt ℝ (fun x' => EuclideanSpace.single v 1) x d:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) x⊢ DifferentiableAt ℝ (fun x' => (f₀' (⟪x', s.unit⟫_ℝ - c * t)) (s.unit.val u)) xd:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) x⊢ DifferentiableAt ℝ (fun x' => EuclideanSpace.single v 1) x d:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) x⊢ DifferentiableAt ℝ ((fun x' => (f₀' x') (s.unit.val u)) ∘ fun x => ⟪x, s.unit⟫_ℝ - c * t) xd:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) x⊢ DifferentiableAt ℝ (fun x' => EuclideanSpace.single v 1) x d:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) x⊢ DifferentiableAt ℝ (fun x' => (f₀' x') (s.unit.val u)) (⟪x, s.unit⟫_ℝ - c * t)d:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) x⊢ DifferentiableAt ℝ (fun x' => ⟪x', s.unit⟫_ℝ - c * t) xd:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) x⊢ DifferentiableAt ℝ (fun x' => EuclideanSpace.single v 1) x d:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) x⊢ DifferentiableAt ℝ (fun x' => (f₀' x') (s.unit.val u)) (⟪x, s.unit⟫_ℝ - c * t) conv_lhs => d:ℕc:ℝt:ℝx✝:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) xx:ℝ| (f₀' x) (s.unit.val u) d:ℕc:ℝt:ℝx✝:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) xx:ℝ| s.unit.val u • (f₀' x) 1 All goals completed! 🐙 d:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) x⊢ DifferentiableAt ℝ (fun x' => ⟪x', s.unit⟫_ℝ - c * t) x All goals completed! 🐙 d:ℕc:ℝt:ℝx:Space du:Fin dv:Fin ds:Direction df₀':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)f₀'':ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)h'':∀ (x : ℝ), HasFDerivAt (fun x' => (f₀' x') 1) (f₀'' x) x⊢ DifferentiableAt ℝ (fun x' => EuclideanSpace.single v 1) x All goals completed! 🐙

If f₀ is a function of (inner ℝ x s - c * t), the fderiv of its components with respect to spatial coordinates is equal to the corresponding component of the propagation direction s times time derivative.

d:ℕc:ℝx:Space dt:Timef₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction du:Fin dv:Fin dh':Differentiable ℝ f₀⊢ c * (s.unit.val u • fun x => (planeWave (fun x => (fderiv ℝ f₀ x) 1) c s t x).ofLp v) x = -(s.unit.val u * ((-c • fun t => planeWave (fun x => (fderiv ℝ f₀ x) 1) c s t x) t).ofLp v) d:ℕc:ℝx:Space dt:Timef₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction du:Fin dv:Fin dh':Differentiable ℝ f₀⊢ c * (s.unit.val u * (planeWave (fun x => _root_.deriv f₀ x) c s t x).ofLp v) = s.unit.val u * (c * (planeWave (fun x => _root_.deriv f₀ x) c s t x).ofLp v) All goals completed! 🐙
d:ℕc:ℝx:Space ds:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)f:Time → Space d → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ Differentiable ℝ fun t => planeWave f₀ c s t x d:ℕc:ℝx:Space ds:Direction df₀:ℝ → EuclideanSpace ℝ (Fin d)f:Time → Space d → EuclideanSpace ℝ (Fin d)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ Differentiable ℝ fun t => f₀ (⟪x, s.unit⟫_ℝ - c * t.val) All goals completed! 🐙c:ℝx:Spacet:Times:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)f:Time → Space → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ DifferentiableAt ℝ (fun t => (fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (planeWave f₀ c s t x)) t c:ℝx:Spacet:Times:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)f:Time → Space → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ DifferentiableAt ℝ (fun t => (fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (f₀ (⟪x, s.unit 3⟫_ℝ - c * t.val))) t c:ℝx:Spacet:Times:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)f:Time → Space → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ ∀ (i : Fin 3), Differentiable ℝ fun t => ((fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (f₀ (⟪x, s.unit 3⟫_ℝ - c * t.val))).ofLp i c:ℝx:Spacet:Times:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)f:Time → Space → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀hf:f = planeWave f₀ c si:Fin 3⊢ Differentiable ℝ fun t => ((fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (f₀ (⟪x, s.unit 3⟫_ℝ - c * t.val))).ofLp i c:ℝx:Spacet:Times:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)f:Time → Space → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ Differentiable ℝ fun t => ((fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (f₀ (⟪x, s.unit 3⟫_ℝ - c * t.val))).ofLp ((fun i => i) ⟨0, ⋯⟩)c:ℝx:Spacet:Times:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)f:Time → Space → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ Differentiable ℝ fun t => ((fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (f₀ (⟪x, s.unit 3⟫_ℝ - c * t.val))).ofLp ((fun i => i) ⟨1, ⋯⟩)c:ℝx:Spacet:Times:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)f:Time → Space → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ Differentiable ℝ fun t => ((fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (f₀ (⟪x, s.unit 3⟫_ℝ - c * t.val))).ofLp ((fun i => i) ⟨2, ⋯⟩) c:ℝx:Spacet:Times:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)f:Time → Space → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ Differentiable ℝ fun t => ((fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (f₀ (⟪x, s.unit 3⟫_ℝ - c * t.val))).ofLp ((fun i => i) ⟨0, ⋯⟩)c:ℝx:Spacet:Times:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)f:Time → Space → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ Differentiable ℝ fun t => ((fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (f₀ (⟪x, s.unit 3⟫_ℝ - c * t.val))).ofLp ((fun i => i) ⟨1, ⋯⟩)c:ℝx:Spacet:Times:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)f:Time → Space → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ Differentiable ℝ fun t => ((fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (f₀ (⟪x, s.unit 3⟫_ℝ - c * t.val))).ofLp ((fun i => i) ⟨2, ⋯⟩) c:ℝx:Spacet:Times:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)f:Time → Space → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ Differentiable ℝ fun t => ((fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm (((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (f₀ (⟪x, s.unit 3⟫_ℝ - c * t.val))).ofLp ((fun i => i) ⟨2, ⋯⟩) c:ℝx:Spacet:Times:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)f:Time → Space → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀hf:f = planeWave f₀ c s⊢ Differentiable ℝ fun t => (Space.basis.repr (s.unit 3)).ofLp 0 * (f₀ (⟪x, s.unit 3⟫_ℝ - c * t.val)).ofLp 1 - (Space.basis.repr (s.unit 3)).ofLp 1 * (f₀ (⟪x, s.unit 3⟫_ℝ - c * t.val)).ofLp 0 All goals completed! 🐙u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀⊢ ∀ (i : Fin 3), Differentiable ℝ fun x => (WithLp.toLp 2 x).ofLp i u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀i:Fin 3⊢ Differentiable ℝ fun x => (WithLp.toLp 2 x).ofLp i u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀i:Fin 3⊢ Differentiable ℝ fun x => x i All goals completed! 🐙 u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀⊢ ∀ (i : Fin 3), Differentiable ℝ fun x => ((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) (Space.basis.repr (s.unit 3)))) ((WithLp.equiv 2 (Fin 3 → ℝ)) (f₀ x)) i u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀i:Fin 3⊢ Differentiable ℝ fun x => ((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) (Space.basis.repr (s.unit 3)))) ((WithLp.equiv 2 (Fin 3 → ℝ)) (f₀ x)) i u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) (Space.basis.repr (s.unit 3)))) ((WithLp.equiv 2 (Fin 3 → ℝ)) (f₀ x)) ((fun i => i) ⟨0, ⋯⟩)u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) (Space.basis.repr (s.unit 3)))) ((WithLp.equiv 2 (Fin 3 → ℝ)) (f₀ x)) ((fun i => i) ⟨1, ⋯⟩)u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) (Space.basis.repr (s.unit 3)))) ((WithLp.equiv 2 (Fin 3 → ℝ)) (f₀ x)) ((fun i => i) ⟨2, ⋯⟩) u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) (Space.basis.repr (s.unit 3)))) ((WithLp.equiv 2 (Fin 3 → ℝ)) (f₀ x)) ((fun i => i) ⟨0, ⋯⟩)u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) (Space.basis.repr (s.unit 3)))) ((WithLp.equiv 2 (Fin 3 → ℝ)) (f₀ x)) ((fun i => i) ⟨1, ⋯⟩)u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) (Space.basis.repr (s.unit 3)))) ((WithLp.equiv 2 (Fin 3 → ℝ)) (f₀ x)) ((fun i => i) ⟨2, ⋯⟩) u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => ((LinearMap.mk₂ ℝ (fun a b => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯) ((WithLp.equiv 2 (Fin 3 → ℝ)) (Space.basis.repr (s.unit 3)))) ((WithLp.equiv 2 (Fin 3 → ℝ)) (f₀ x)) ((fun i => i) ⟨2, ⋯⟩) u:ℝs:Directionf₀:ℝ → EuclideanSpace ℝ (Fin 3)h':Differentiable ℝ f₀⊢ Differentiable ℝ fun x => (Space.basis.repr (s.unit 3)).ofLp 0 * (f₀ x).ofLp 1 - (Space.basis.repr (s.unit 3)).ofLp 1 * (f₀ x).ofLp 0 All goals completed! 🐙d:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ s.unit.val i • 1 * (⟪y, s.unit⟫_ℝ • 1 * (_root_.deriv f₀ (⟪x, s.unit⟫_ℝ - c * t)).ofLp i) = ⟪y, s.unit⟫_ℝ • 1 * (s.unit.val i • 1 * (_root_.deriv f₀ (⟪x, s.unit⟫_ℝ - c * t)).ofLp i)d:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ DifferentiableAt ℝ (fun x => ⟪x, s.unit⟫_ℝ) xd:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ DifferentiableAt ℝ (fun x => c * t) xd:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ DifferentiableAt ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t)d:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ DifferentiableAt ℝ (fun x => ⟪x, s.unit⟫_ℝ - c * t) xd:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj i)) (f₀ (⟪x, s.unit⟫_ℝ - c * t))d:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ DifferentiableAt ℝ (fun x => f₀ (⟪x, s.unit⟫_ℝ - c * t)) x d:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ DifferentiableAt ℝ (fun x => ⟪x, s.unit⟫_ℝ) xd:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ DifferentiableAt ℝ (fun x => c * t) xd:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ DifferentiableAt ℝ f₀ (⟪x, s.unit⟫_ℝ - c * t)d:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ DifferentiableAt ℝ (fun x => ⟪x, s.unit⟫_ℝ - c * t) xd:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj i)) (f₀ (⟪x, s.unit⟫_ℝ - c * t))d:ℕc:ℝt:ℝf₀:ℝ → EuclideanSpace ℝ (Fin d)s:Direction di:Fin dh':Differentiable ℝ f₀x:Space dy:Space d⊢ DifferentiableAt ℝ (fun x => f₀ (⟪x, s.unit⟫_ℝ - c * t)) x repeat All goals completed! 🐙