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 dDifferentiableAt Time.val td:f₀: EuclideanSpace (Fin d)c:x:Space ds:Direction dh':Differentiable f₀t:Timei:Fin dDifferentiableAt f₀ (x, s.unit⟫_ - c * t.val)d:f₀: EuclideanSpace (Fin d)c:x:Space ds:Direction dh':Differentiable f₀t:Timei:Fin dDifferentiableAt (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 dDifferentiableAt Time.val td:f₀: EuclideanSpace (Fin d)c:x:Space ds:Direction dh':Differentiable f₀t:Timei:Fin dDifferentiableAt f₀ (x, s.unit⟫_ - c * t.val)d:f₀: EuclideanSpace (Fin d)c:x:Space ds:Direction dh':Differentiable f₀t:Timei:Fin dDifferentiableAt (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 dDifferentiableAt Time.val td:f₀: EuclideanSpace (Fin d)c:x:Space ds:Direction dh':Differentiable f₀t:Timei:Fin dDifferentiableAt f₀ (x, s.unit⟫_ - c * t.val)d:f₀: EuclideanSpace (Fin d)c:x:Space ds:Direction dh':Differentiable f₀t:Timei:Fin dDifferentiableAt (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 dDifferentiableAt Time.val td:f₀: EuclideanSpace (Fin d)c:x:Space ds:Direction dh':Differentiable f₀t:Timei:Fin dDifferentiableAt f₀ (x, s.unit⟫_ - c * t.val)d:f₀: EuclideanSpace (Fin d)c:x:Space ds:Direction dh':Differentiable f₀t:Timei:Fin dDifferentiableAt (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 dDifferentiableAt Time.val td:f₀: EuclideanSpace (Fin d)c:x:Space ds:Direction dh':Differentiable f₀t:Timei:Fin dDifferentiableAt f₀ (x, s.unit⟫_ - c * t.val)d:f₀: EuclideanSpace (Fin d)c:x:Space ds:Direction dh':Differentiable f₀t:Timei:Fin dDifferentiableAt (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 x => _root_.deriv f₀ x) x) = fun x => iteratedDeriv 2 f₀ x d:f₀: EuclideanSpace (Fin d)c:x✝:Space ds:Direction dh':ContDiff 2 f₀t:Timei:Fin dx:_root_.deriv (fun x => _root_.deriv f₀ x) x = iteratedDeriv 2 f₀ x erw [d:f₀: EuclideanSpace (Fin d)c:x✝:Space ds:Direction dh':ContDiff 2 f₀t:Timei:Fin dx:_root_.deriv (fun x => _root_.deriv f₀ x) x = _root_.deriv (iteratedDeriv 1 f₀) xd:f₀: EuclideanSpace (Fin d)c:x✝:Space ds:Direction dh':ContDiff 2 f₀t:Timei:Fin dx:_root_.deriv (fun x => _root_.deriv f₀ x) x = _root_.deriv (iteratedDeriv 1 f₀) x 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 dDifferentiableAt (fun x => x) xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':Differentiable f₀i:Fin dx:Space dj:Fin dDifferentiableAt (fun x => s.unit) xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':Differentiable f₀i:Fin dx:Space dj:Fin dDifferentiableAt 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 dDifferentiableAt (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 dDifferentiableAt (fun x => x) xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':Differentiable f₀i:Fin dx:Space dj:Fin dDifferentiableAt (fun x => s.unit) xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':Differentiable f₀i:Fin dx:Space dj:Fin dDifferentiableAt 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 dDifferentiableAt (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 dDifferentiableAt (fun x => x) xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':Differentiable f₀i:Fin dx:Space dj:Fin dDifferentiableAt (fun x => s.unit) xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':Differentiable f₀i:Fin dx:Space dj:Fin dDifferentiableAt 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 dDifferentiableAt (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 dDifferentiableAt (fun x => x) xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':Differentiable f₀i:Fin dx:Space dj:Fin dDifferentiableAt (fun x => s.unit) xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':Differentiable f₀i:Fin dx:Space dj:Fin dDifferentiableAt 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 dDifferentiableAt (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 dDifferentiable f₀t:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':Differentiable f₀i:Fin dj:Fin dx:Space dDifferentiableAt (⇑(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 dDifferentiableAt (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 dDifferentiable f₀t:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':Differentiable f₀i:Fin dj:Fin dx:Space dDifferentiableAt (⇑(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 dDifferentiableAt (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 dDifferentiable f₀ All goals completed! 🐙 t:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':Differentiable f₀i:Fin dj:Fin dx:Space dDifferentiableAt (⇑(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 dDifferentiableAt (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 dDifferentiable 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 dDifferentiableAt (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 x => _root_.deriv f₀ x) x) = fun x => iteratedDeriv 2 f₀ xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i:Fin dj:Fin dx:Space dDifferentiable fun x => _root_.deriv f₀ xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i:Fin dj:Fin dx:Space dDifferentiableAt (fun x => (planeWave (fun x => (fderiv f₀ x) 1) c s t x).ofLp j) x t:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i✝:Fin dj:Fin dx✝:Space dx:i:Fin d(_root_.deriv (fun x => _root_.deriv f₀ x) x).ofLp i = (iteratedDeriv 2 f₀ x).ofLp it:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i:Fin dj:Fin dx:Space dDifferentiable fun x => _root_.deriv f₀ xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i:Fin dj:Fin dx:Space dDifferentiableAt (fun x => (planeWave (fun x => (fderiv f₀ x) 1) c s t x).ofLp j) x erw [t:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i✝:Fin dj:Fin dx✝:Space dx:i:Fin d(_root_.deriv (fun x => _root_.deriv f₀ x) x).ofLp i = (iteratedDeriv 1 (_root_.deriv f₀) x).ofLp it:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i:Fin dj:Fin dx:Space dDifferentiable fun x => _root_.deriv f₀ xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i:Fin dj:Fin dx:Space dDifferentiableAt (fun x => (planeWave (fun x => (fderiv f₀ x) 1) c s t x).ofLp j) xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i✝:Fin dj:Fin dx✝:Space dx:i:Fin d(_root_.deriv (fun x => _root_.deriv f₀ x) x).ofLp i = (iteratedDeriv 1 (_root_.deriv f₀) x).ofLp it:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i:Fin dj:Fin dx:Space dDifferentiable fun x => _root_.deriv f₀ xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i:Fin dj:Fin dx:Space dDifferentiableAt (fun x => (planeWave (fun x => (fderiv f₀ x) 1) c s t x).ofLp j) x t:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i:Fin dj:Fin dx:Space dDifferentiable fun x => _root_.deriv f₀ xt:Timed:f₀: EuclideanSpace (Fin d)c:s:Direction dh':ContDiff 2 f₀i:Fin dj:Fin dx:Space dDifferentiableAt (fun x => (planeWave (fun x => (fderiv f₀ x) 1) c s t x).ofLp j) x repeat 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 dc ^ 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 dDifferentiableAt (fun x => x, s.unit⟫_ - c * t) x d:t:s:Direction dc:x:Space dDifferentiableAt (fun x => x, s.unit⟫_) xd:t:s:Direction dc:x:Space dDifferentiableAt (fun x => c * t) x d:t:s:Direction dc:x:Space dDifferentiableAt (fun x => x) xd:t:s:Direction dc:x:Space dDifferentiableAt (fun x => s.unit) xd:t:s:Direction dc:x:Space dDifferentiableAt (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) xDifferentiableAt (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) xDifferentiableAt (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) xDifferentiableAt (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) xDifferentiableAt (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) xDifferentiableAt ((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) xDifferentiableAt (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) xDifferentiableAt (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) xDifferentiableAt (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) xDifferentiableAt (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) xDifferentiableAt (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) xDifferentiableAt (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) xDifferentiableAt (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.

lemma space_fderiv_of_inner_product_wave_eq_space_fderiv {t : Time} {f₀ : EuclideanSpace (Fin d)} {s : Direction d} {u v : Fin d} (h' : Differentiable f₀) : c * ((fun x' => (fderiv (fun x => inner (f₀ (inner x s.unit - c * t)) (EuclideanSpace.single v 1)) x') ((Space.basis u))) x) = - s.unit u * ∂ₜ (fun t => f₀ (inner x s.unit - c * t)) t v := d:c:x:Space dt:Timef₀: EuclideanSpace (Fin d)s:Direction du:Fin dv:Fin dh':Differentiable f₀c * (fun x' => (fderiv (fun x => f₀ (x, s.unit⟫_ - c * t.val), EuclideanSpace.single v 1⟫_) x') (Space.basis u)) x = -s.unit.val u * (∂ₜ (fun t => f₀ (x, s.unit⟫_ - c * t.val)) t).ofLp v d:c:x:Space dt:Timef₀: EuclideanSpace (Fin d)s:Direction du:Fin dv:Fin dh':Differentiable f₀c * (fderiv (fun x => (f₀ (x, s.unit⟫_ - c * t.val)).ofLp v) x) (Space.basis u) = -(s.unit.val u * (∂ₜ (fun t => f₀ (x, s.unit⟫_ - c * t.val)) t).ofLp v) d:c:x:Space dt:Timef₀: EuclideanSpace (Fin d)s:Direction du:Fin dv:Fin dh':Differentiable f₀c * (fderiv (fun x => (f₀ (x, s.unit⟫_ - c * t.val)).ofLp v) x) (Space.basis u) = c * (fderiv (fun x => (f₀ (x, s.unit⟫_ - c * t.val)).ofLp v) x) (Space.basis u)d:c:x:Space dt:Timef₀: EuclideanSpace (Fin d)s:Direction du:Fin dv:Fin dh':Differentiable f₀c * (fderiv (fun x => (f₀ (x, s.unit⟫_ - c * t.val)).ofLp v) x) (Space.basis u) = -(s.unit.val u * (∂ₜ (fun t => f₀ (x, s.unit⟫_ - c * t.val)) t).ofLp v) d:c:x:Space dt:Timef₀: EuclideanSpace (Fin d)s:Direction du:Fin dv:Fin dh':Differentiable f₀c * (fderiv (fun x => (f₀ (x, s.unit⟫_ - c * t.val)).ofLp v) x) (Space.basis u) = c * (fderiv (fun x => (f₀ (x, s.unit⟫_ - c * t.val)).ofLp v) x) (Space.basis u) All goals completed! 🐙 erw [d:c:x:Space dt:Timef₀: EuclideanSpace (Fin d)s:Direction du:Fin dv:Fin dh':Differentiable f₀c * Space.deriv u (fun x => (f₀ (x, s.unit⟫_ - c * t.val)).ofLp v) x = -(s.unit.val u * (∂ₜ (fun t => f₀ (x, s.unit⟫_ - c * t.val)) 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 fun x => (planeWave (fun x => (fderiv f₀ x) 1) c s t x).ofLp v) x = -(s.unit.val u * (∂ₜ (fun t => f₀ (x, s.unit⟫_ - c * t.val)) 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 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 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 sDifferentiable 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 sDifferentiable 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 sDifferentiableAt (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 sDifferentiableAt (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 3Differentiable 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 sDifferentiable 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 sDifferentiable 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 sDifferentiable 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 sDifferentiable 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 sDifferentiable 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 sDifferentiable 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 sDifferentiable 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 sDifferentiable 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 3Differentiable fun x => (WithLp.toLp 2 x).ofLp i u:s:Directionf₀: EuclideanSpace (Fin 3)h':Differentiable f₀i:Fin 3Differentiable 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 3Differentiable 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 ds.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 dDifferentiableAt (fun x => x, s.unit⟫_) xd:c:t:f₀: EuclideanSpace (Fin d)s:Direction di:Fin dh':Differentiable f₀x:Space dy:Space dDifferentiableAt (fun x => c * t) xd:c:t:f₀: EuclideanSpace (Fin d)s:Direction di:Fin dh':Differentiable f₀x:Space dy:Space dDifferentiableAt f₀ (x, s.unit⟫_ - c * t)d:c:t:f₀: EuclideanSpace (Fin d)s:Direction di:Fin dh':Differentiable f₀x:Space dy:Space dDifferentiableAt (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 dDifferentiableAt (⇑(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 dDifferentiableAt (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 dDifferentiableAt (fun x => x, s.unit⟫_) xd:c:t:f₀: EuclideanSpace (Fin d)s:Direction di:Fin dh':Differentiable f₀x:Space dy:Space dDifferentiableAt (fun x => c * t) xd:c:t:f₀: EuclideanSpace (Fin d)s:Direction di:Fin dh':Differentiable f₀x:Space dy:Space dDifferentiableAt f₀ (x, s.unit⟫_ - c * t)d:c:t:f₀: EuclideanSpace (Fin d)s:Direction di:Fin dh':Differentiable f₀x:Space dy:Space dDifferentiableAt (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 dDifferentiableAt (⇑(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 dDifferentiableAt (fun x => f₀ (x, s.unit⟫_ - c * t)) x repeat All goals completed! 🐙