@[reducible, inline]

abbrev WaveEquation3D.E3 : Type

Shorthand for $3$-dimensional Euclidean space $\mathbb{R}^3$ used as the spatial domain for the wave equation.

structure WaveEquation3D.IsWaveSolution3D (u : ℝ → E3 → ℝ) : Prop

Predicate stating that $u : \mathbb{R} \times \mathbb{R}^3 \to \mathbb{R}$ is a $C^2$ solution of the $3$-dimensional wave equation $-\partial_t^2 u + \Delta u = 0$.

• smooth : ContDiff ℝ 2 fun (p : ℝ × E3) => u p.1 p.2
• wave_eq (t : ℝ) (x : E3) : (fderiv ℝ (fun (s : ℝ) => (fderiv ℝ (fun (s' : ℝ) => u s' x) s) 1) t) 1 = ∑ i : Fin 3, (fderiv ℝ (fun (y : E3) => (fderiv ℝ (fun (y' : E3) => u t y') y) (EuclideanSpace.single i 1)) x) (EuclideanSpace.single i 1)

structure WaveEquation3D.CauchyData3D : Type

Cauchy data for the $3$D wave equation: an initial position $f \in C^3(\mathbb{R}^3)$ and an initial velocity $g \in C^2(\mathbb{R}^3)$.

• f : E3 → ℝ
• g : E3 → ℝ
• f_smooth : ContDiff ℝ 3 self.f
• g_smooth : ContDiff ℝ 2 self.g

noncomputable def WaveEquation3D.sphericalToCart (θ φ : ℝ) : E3

Conversion from spherical coordinates $(\theta, \varphi)$ on the unit sphere $S^2 \subset \mathbb{R}^3$ to Cartesian coordinates $(\sin\theta\cos\varphi, \sin\theta\sin\varphi, \cos\theta)$.

@[irreducible]

noncomputable def WaveEquation3D.SphericalMean (h : E3 → ℝ) (x : E3) (r : ℝ) : ℝ

The spherical mean of $h : \mathbb{R}^3 \to \mathbb{R}$ over the sphere $\partial B_r(x)$ of radius $r$ centred at $x$, defined via the spherical parametrization $\frac{1}{4\pi}\int_0^\pi\!\!\int_0^{2\pi} h(x + r\,\omega(\theta,\varphi))\sin\theta\,d\varphi\,d\theta$.

theorem WaveEquation3D.integral_sin_eq_two : ∫ (θ : ℝ) in 0..Real.pi, Real.sin θ = 2

Elementary computation: $\int_0^\pi \sin\theta\, d\theta = 2$.

theorem WaveEquation3D.sphericalMean_at_zero (h : E3 → ℝ) (x : E3) : SphericalMean h x 0 = h x

The spherical mean over a sphere of radius zero equals the value at the centre: $\mathrm{SphericalMean}\,h\,x\,0 = h(x)$.

theorem WaveEquation3D.sphericalToCart_continuous : Continuous fun (p : (ℝ × ℝ) × ℝ) => (EuclideanSpace.equiv (Fin 3) ℝ).symm ![Real.sin p.1.2 * Real.cos p.2, Real.sin p.1.2 * Real.sin p.2, Real.cos p.1.2]

The spherical-to-Cartesian map (viewed as a function of an outer parameter and the angles $(\theta, \varphi)$) is continuous.

theorem WaveEquation3D.sphericalMean_continuous (h : E3 → ℝ) (hh : Continuous h) (x : E3) : Continuous fun (r : ℝ) => SphericalMean h x r

If $h$ is continuous, then $r \mapsto \mathrm{SphericalMean}\,h\,x\,r$ is continuous in the radius $r$.

theorem WaveEquation3D.SphericalMean_eq (h : E3 → ℝ) (x : E3) (r : ℝ) : SphericalMean h x r = 1 / (4 * Real.pi) * ∫ (θ : ℝ) in 0..Real.pi, ∫ (φ : ℝ) in 0..2 * Real.pi, h (x + r • sphericalToCart θ φ) * Real.sin θ

Definitional unfolding of SphericalMean as a parametric integral in spherical coordinates. Used to expose the integral form after the definition is marked irreducible.

noncomputable def WaveEquation3D.SphereIntegral (h : E3 → ℝ) (x : E3) (r : ℝ) : ℝ

The surface integral $\int_{\partial B_r(x)} h\,d\sigma = 4\pi r^2 \cdot \mathrm{SphericalMean}\,h\,x\,r$ on the sphere of radius $r$ around $x$.

noncomputable def WaveEquation3D.SphereIntegralNormalDeriv (h : E3 → ℝ) (x : E3) (r : ℝ) : ℝ

The integral over $\partial B_r(x)$ of the radial (outward normal) derivative of $h$, expressed as $4\pi r^2$ times the radial derivative of the spherical mean.

theorem WaveEquation3D.leibniz_sphericalCoord_iteratedDeriv2 (u : ℝ → E3 → ℝ) (s r : ℝ) (x : E3) (hsmooth : ContDiff ℝ 2 fun (p : ℝ × E3) => u p.1 p.2) : iteratedDeriv 2 (fun (s' : ℝ) => ∫ (θ : ℝ) in 0..Real.pi, ∫ (φ : ℝ) in 0..2 * Real.pi, u s' (x + r • sphericalToCart θ φ) * Real.sin θ) s = ∫ (θ : ℝ) in 0..Real.pi, ∫ (φ : ℝ) in 0..2 * Real.pi, iteratedDeriv 2 (fun (s' : ℝ) => u s' (x + r • sphericalToCart θ φ)) s * Real.sin θ

Leibniz / differentiation-under-the-integral for the second time derivative: the iterated derivative of order $2$ commutes with the spherical integral.

theorem WaveEquation3D.contDiffAt_sphericalCoord_integral (u : ℝ → E3 → ℝ) (s r : ℝ) (x : E3) (hsmooth : ContDiff ℝ 2 fun (p : ℝ × E3) => u p.1 p.2) : ContDiffAt ℝ 2 (fun (s' : ℝ) => ∫ (θ : ℝ) in 0..Real.pi, ∫ (φ : ℝ) in 0..2 * Real.pi, u s' (x + r • sphericalToCart θ φ) * Real.sin θ) s

Smoothness of the spherical-coordinate integral in the time parameter $s'$: the map $s' \mapsto \int_{S^2} u(s', x + r\omega)\,d\sigma(\omega)$ is $C^2$.

theorem WaveEquation3D.sphericalMean_leibniz_deriv2 (u : ℝ → E3 → ℝ) (s r : ℝ) (x : E3) (hu : IsWaveSolution3D u) : iteratedDeriv 2 (fun (s' : ℝ) => SphericalMean (u s') x r) s = SphericalMean (fun (y : E3) => iteratedDeriv 2 (fun (s' : ℝ) => u s' y) s) x r

The second time derivative passes inside the spherical mean: $\partial_t^2 \mathrm{SphericalMean}(u(t,\cdot))(x, r) = \mathrm{SphericalMean}(\partial_t^2 u(t,\cdot))(x, r)$.

theorem WaveEquation3D.sphericalMean_differentiable_time (u : ℝ → E3 → ℝ) (r : ℝ) (x : E3) (hu : IsWaveSolution3D u) (s : ℝ) : DifferentiableAt ℝ (fun (s' : ℝ) => SphericalMean (u s') x r) s

For a wave solution $u$, the spherical mean $s' \mapsto \mathrm{SphericalMean}(u(s',\cdot))(x,r)$ is differentiable at every time $s$.

theorem WaveEquation3D.sphericalMean_deriv_differentiable_time (u : ℝ → E3 → ℝ) (r : ℝ) (x : E3) (hu : IsWaveSolution3D u) (s : ℝ) : DifferentiableAt ℝ (fun (s' : ℝ) => deriv (fun (s'' : ℝ) => SphericalMean (u s'') x r) s') s

The first time derivative of the spherical mean is itself differentiable in time when $u$ is a $C^2$ wave solution.

theorem WaveEquation3D.leibniz_sphericalCoord_deriv1 (u : ℝ → E3 → ℝ) (s r : ℝ) (x : E3) (hsmooth : ContDiff ℝ 2 fun (p : ℝ × E3) => u p.1 p.2) : deriv (fun (s' : ℝ) => ∫ (θ : ℝ) in 0..Real.pi, ∫ (φ : ℝ) in 0..2 * Real.pi, u s' (x + r • sphericalToCart θ φ) * Real.sin θ) s = ∫ (θ : ℝ) in 0..Real.pi, ∫ (φ : ℝ) in 0..2 * Real.pi, deriv (fun (s' : ℝ) => u s' (x + r • sphericalToCart θ φ)) s * Real.sin θ

Leibniz / differentiation-under-the-integral for the first time derivative of the parametric spherical integral.

theorem WaveEquation3D.sphericalMean_leibniz_deriv1 (u : ℝ → E3 → ℝ) (s r : ℝ) (x : E3) (hu : IsWaveSolution3D u) : fderiv ℝ (fun (s' : ℝ) => SphericalMean (u s') x r) s = ContinuousLinearMap.smulRight 1 (SphericalMean (fun (y : E3) => (fderiv ℝ (fun (s' : ℝ) => u s' y) s) 1) x r)

Fréchet-derivative form of differentiation under the spherical mean in time: $\partial_t \mathrm{SphericalMean}(u(t,\cdot))(x,r) = \mathrm{SphericalMean}(\partial_t u(t,\cdot))(x,r)$.

theorem WaveEquation3D.sphericalMean_radius_hasDerivAt (f : E3 → ℝ) (x : E3) (r : ℝ) (_hr : 0 < r) (hf : ContDiff ℝ 2 f) : HasDerivAt (fun (ρ : ℝ) => SphericalMean f x ρ) (deriv (fun (ρ : ℝ) => SphericalMean f x ρ) r) r

For a $C^2$ function $f$, the spherical mean $\rho \mapsto \mathrm{SphericalMean}\,f\,x\,\rho$ has a derivative at every positive radius $r$.

theorem WaveEquation3D.leibniz_sphericalMean_tt (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (r : ℝ) (_hr : 0 ≤ r) (x : E3) : (∀ (s : ℝ), DifferentiableAt ℝ (fun (s' : ℝ) => SphericalMean (u s') x r) s) ∧ (∀ (s : ℝ), DifferentiableAt ℝ (fun (s' : ℝ) => (fderiv ℝ (fun (s'' : ℝ) => SphericalMean (u s'') x r) s') 1) s) ∧ ∀ (t : ℝ), (fderiv ℝ (fun (s : ℝ) => (fderiv ℝ (fun (s' : ℝ) => SphericalMean (u s') x r) s) 1) t) 1 = SphericalMean (fun (y : E3) => (fderiv ℝ (fun (s : ℝ) => (fderiv ℝ (fun (s' : ℝ) => u s' y) s) 1) t) 1) x r

Packaged Leibniz statement for second time derivatives of the spherical mean: $\mathrm{SphericalMean}(u(\cdot,\cdot))$ is twice differentiable in $t$ and the second derivative commutes with the spherical mean.

theorem WaveEquation3D.iteratedDeriv_two_mul_id (f : ℝ → ℝ) (hf : ContDiff ℝ 2 f) (x : ℝ) : iteratedDeriv 2 (fun (ρ : ℝ) => ρ * f ρ) x = x * iteratedDeriv 2 f x + 2 * deriv f x

Product-rule identity: for $f \in C^2$, $\frac{d^2}{d\rho^2}(\rho f(\rho))\big|_{\rho = x} = x f''(x) + 2 f'(x)$.

theorem WaveEquation3D.sphericalMean_contDiff_radius (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (t : ℝ) (x : E3) : ContDiff ℝ 2 (SphericalMean (u t) x)

For a wave solution $u$, the spherical mean $\rho \mapsto \mathrm{SphericalMean}(u(t,\cdot))(x, \rho)$ is $C^2$ as a function of the radius.

theorem WaveEquation3D.divergence_coarea_darboux_identity (f : E3 → ℝ) (x : E3) (r : ℝ) (hf : ContDiff ℝ 2 f) : r * SphericalMean (fun (y : E3) => ∑ i : Fin 3, (fderiv ℝ (fun (z : E3) => (fderiv ℝ f z) (EuclideanSpace.single i 1)) y) (EuclideanSpace.single i 1)) x r = r * iteratedDeriv 2 (SphericalMean f x) r + 2 * deriv (SphericalMean f x) r

Darboux-type identity (via divergence theorem and the coarea formula): $r \cdot \mathrm{SphericalMean}(\Delta f)(x, r) = r M_f''(r) + 2 M_f'(r)$, where $M_f(r) = \mathrm{SphericalMean}\,f\,x\,r$.

theorem WaveEquation3D.darboux_sphericalMean_expanded (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (t : ℝ) (x : E3) (r : ℝ) : r * SphericalMean (fun (y : E3) => ∑ i : Fin 3, (fderiv ℝ (fun (z : E3) => (fderiv ℝ (fun (z' : E3) => u t z') z) (EuclideanSpace.single i 1)) y) (EuclideanSpace.single i 1)) x r = r * iteratedDeriv 2 (SphericalMean (u t) x) r + 2 * deriv (SphericalMean (u t) x) r

Specialisation of the Darboux identity to a slice $u(t, \cdot)$ of a wave solution.

theorem WaveEquation3D.darboux_sphericalMean_core (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (t : ℝ) (x : E3) (r : ℝ) : r * SphericalMean (fun (y : E3) => ∑ i : Fin 3, (fderiv ℝ (fun (z : E3) => (fderiv ℝ (fun (z' : E3) => u t z') z) (EuclideanSpace.single i 1)) y) (EuclideanSpace.single i 1)) x r = iteratedDeriv 2 (fun (ρ : ℝ) => ρ * SphericalMean (u t) x ρ) r

Compact form of the Darboux identity, rewriting the right-hand side as $\partial_\rho^2(\rho \cdot \mathrm{SphericalMean}(u(t,\cdot))(x,\rho))$.

theorem WaveEquation3D.sphericalMean_laplacian_decomp (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (t : ℝ) (x : E3) (r : ℝ) : r * SphericalMean (fun (y : E3) => ∑ i : Fin 3, (fderiv ℝ (fun (z : E3) => (fderiv ℝ (fun (z' : E3) => u t z') z) (EuclideanSpace.single i 1)) y) (EuclideanSpace.single i 1)) x r = r * iteratedDeriv 2 (SphericalMean (u t) x) r + 2 * deriv (SphericalMean (u t) x) r

Decomposition relating the spherical mean of the Laplacian of $u(t,\cdot)$ to the radial second derivative of the spherical mean (expanded version).

theorem WaveEquation3D.darboux_sphericalMean_eq (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (t : ℝ) (x : E3) (r : ℝ) : r * SphericalMean (fun (y : E3) => ∑ i : Fin 3, (fderiv ℝ (fun (z : E3) => (fderiv ℝ (fun (z' : E3) => u t z') z) (EuclideanSpace.single i 1)) y) (EuclideanSpace.single i 1)) x r = iteratedDeriv 2 (fun (ρ : ℝ) => ρ * SphericalMean (u t) x ρ) r

Equivalent compact form of the Darboux identity for $u(t,\cdot)$.

theorem WaveEquation3D.divergence_darboux_sphericalMean (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (t r : ℝ) (_hr : 0 ≤ r) (x : E3) : r * SphericalMean (fun (y : E3) => ∑ i : Fin 3, (fderiv ℝ (fun (z : E3) => (fderiv ℝ (fun (z' : E3) => u t z') z) (EuclideanSpace.single i 1)) y) (EuclideanSpace.single i 1)) x r = (fderiv ℝ (fun (ρ : ℝ) => (fderiv ℝ (fun (ρ' : ℝ) => ρ' * SphericalMean (u t) x ρ') ρ) 1) r) 1

The Darboux identity rewritten with the second radial derivative expressed via fderiv: $r \cdot \mathrm{SphericalMean}(\Delta u(t,\cdot))(x,r) = \partial_\rho^2(\rho \cdot M(\rho))|_{\rho=r}$.

theorem WaveEquation3D.sphericalMean_commute_with_tt (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (t r : ℝ) (hr : 0 ≤ r) (x : E3) : (fderiv ℝ (fun (s : ℝ) => (fderiv ℝ (fun (s' : ℝ) => r * SphericalMean (u s') x r) s) 1) t) 1 = r * SphericalMean (fun (y : E3) => (fderiv ℝ (fun (s : ℝ) => (fderiv ℝ (fun (s' : ℝ) => u s' y) s) 1) t) 1) x r

The second time derivative commutes with multiplication by $r$ and with the spherical mean: $\partial_t^2 (r \cdot \mathrm{SphericalMean}(u(\cdot,\cdot))(x,r)) = r \cdot \mathrm{SphericalMean}(\partial_t^2 u(\cdot,\cdot))(x,r)$.

theorem WaveEquation3D.sphericalMean_laplacian_radial (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (t r : ℝ) (hr : 0 ≤ r) (x : E3) : r * SphericalMean (fun (y : E3) => ∑ i : Fin 3, (fderiv ℝ (fun (z : E3) => (fderiv ℝ (fun (z' : E3) => u t z') z) (EuclideanSpace.single i 1)) y) (EuclideanSpace.single i 1)) x r = (fderiv ℝ (fun (ρ : ℝ) => (fderiv ℝ (fun (ρ' : ℝ) => ρ' * SphericalMean (u t) x ρ') ρ) 1) r) 1

Restates the Darboux identity in fderiv notation, identifying the spherical mean of the Laplacian with a radial second-derivative expression.

theorem WaveEquation3D.sphericalMean_wave_reduction (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (t r : ℝ) (hr : 0 ≤ r) (x : E3) : (fderiv ℝ (fun (s : ℝ) => (fderiv ℝ (fun (s' : ℝ) => r * SphericalMean (u s') x r) s) 1) t) 1 = (fderiv ℝ (fun (ρ : ℝ) => (fderiv ℝ (fun (ρ' : ℝ) => ρ' * SphericalMean (u t) x ρ') ρ) 1) r) 1

Key reduction: $w(t,r) := r \cdot \mathrm{SphericalMean}(u(t,\cdot))(x,r)$ satisfies the $1+1$-dimensional wave equation $\partial_t^2 w = \partial_r^2 w$.

theorem WaveEquation3D.sphericalMean_time_deriv (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (r : ℝ) (_hr : 0 < r) (x : E3) : (fderiv ℝ (fun (t : ℝ) => r * SphericalMean (u t) x r) 0) 1 = r * SphericalMean (fun (y : E3) => (fderiv ℝ (fun (t : ℝ) => u t y) 0) 1) x r

Initial time derivative of $t \mapsto r \cdot \mathrm{SphericalMean}(u(t,\cdot))(x,r)$ at $t=0$ equals $r \cdot \mathrm{SphericalMean}(\partial_t u(0,\cdot))(x,r)$.

theorem WaveEquation3D.sphericalMean_limit_zero (h : E3 → ℝ) (hh : Continuous h) (x : E3) : Filter.Tendsto (fun (r : ℝ) => SphericalMean h x r) (nhdsWithin 0 (Set.Ioi 0)) (nhds (h x))

For a continuous $h$, the spherical mean tends to the centre value as the radius shrinks to $0^+$: $\lim_{r \to 0^+} \mathrm{SphericalMean}\,h\,x\,r = h(x)$.

theorem WaveEquation3D.dalembert_halfline_representation (w : ℝ → ℝ → ℝ) (F G : ℝ → ℝ) (hF : ContDiff ℝ 2 F) (hG : ContDiff ℝ 1 G) (hF0 : F 0 = 0) (hG0 : G 0 = 0) (hw_reg : ContDiff ℝ 2 fun (p : ℝ × ℝ) => w p.1 p.2) (hw_wave : ∀ (t r : ℝ), 0 ≤ r → deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => w t'' r) t') t = deriv (fun (r' : ℝ) => deriv (fun (r'' : ℝ) => w t r'') r') r) (hw_boundary : ∀ (t : ℝ), w t 0 = 0) (hw_initial_pos : ∀ (r : ℝ), 0 ≤ r → w 0 r = F r) (hw_initial_vel : ∀ (r : ℝ), 0 < r → HasDerivAt (fun (t : ℝ) => w t r) (G r) 0) (t r : ℝ) (ht : 0 ≤ t) (hr : 0 ≤ r) (hrt : r ≤ t) : w t r = 1 / 2 * (F (r + t) - F (t - r)) + 1 / 2 * ∫ (ρ : ℝ) in t - r..r + t, G ρ

D'Alembert-style formula for the wave equation on the half-line $\{r \ge 0\}$ with Dirichlet boundary $w(t,0) = 0$, vanishing odd-extended initial data $F, G$ with $F(0) = G(0) = 0$. For $r \le t$, $w(t, r) = \tfrac12(F(r+t) - F(t-r)) + \tfrac12 \int_{t-r}^{r+t} G(\rho)\,d\rho$.

noncomputable def WaveEquation3D.F_tilde (data : CauchyData3D) (r : ℝ) (x : E3) : ℝ

The "tilde" initial position: $\tilde F(r, x) := r \cdot \mathrm{SphericalMean}(f)(x, r)$, the spatial profile of the auxiliary $1+1$-dimensional wave problem associated with $u$.

noncomputable def WaveEquation3D.G_tilde (data : CauchyData3D) (r : ℝ) (x : E3) : ℝ

The "tilde" initial velocity: $\tilde G(r, x) := r \cdot \mathrm{SphericalMean}(g)(x, r)$.

theorem WaveEquation3D.sphere_integral_eq_area_times_mean (h : E3 → ℝ) (x : E3) (r : ℝ) : SphereIntegral h x r = 4 * Real.pi * r ^ 2 * SphericalMean h x r

The surface integral equals the area of the sphere times the spherical mean: $\int_{\partial B_r(x)} h\,d\sigma = 4\pi r^2 \cdot \mathrm{SphericalMean}\,h\,x\,r$.

theorem WaveEquation3D.sphericalMean_normal_deriv_relation (f : E3 → ℝ) (x : E3) (t : ℝ) (_ht : 0 < t) : SphereIntegralNormalDeriv f x t = 4 * Real.pi * t ^ 2 * deriv (fun (r : ℝ) => SphericalMean f x r) t

The integral of the outward normal derivative is $4\pi t^2$ times the radial derivative of the spherical mean.

theorem WaveEquation3D.F_tilde_hasDerivAt (f : E3 → ℝ) (x : E3) (t : ℝ) (ht : 0 < t) (hf : ContDiff ℝ 2 f) : HasDerivAt (fun (r : ℝ) => r * SphericalMean f x r) (SphericalMean f x t + t * deriv (fun (r : ℝ) => SphericalMean f x r) t) t

Product-rule derivative of $\tilde F$: at $t > 0$, $\frac{d}{dr}\big(r \cdot \mathrm{SphericalMean}\,f\,x\,r\big)\big|_{r=t} = \mathrm{SphericalMean}\,f\,x\,t + t \cdot \partial_r\mathrm{SphericalMean}\,f\,x\,t$.

theorem WaveEquation3D.symmetric_derivative_tendsto (f : ℝ → ℝ) (t d : ℝ) (hf : HasDerivAt f d t) : Filter.Tendsto (fun (h : ℝ) => (f (t + h) - f (t - h)) / (2 * h)) (nhdsWithin 0 (Set.Ioi 0)) (nhds d)

The symmetric difference quotient $(f(t+h) - f(t-h))/(2h)$ tends to the derivative $f'(t)$ as $h \to 0^+$, provided $f$ has a derivative $d$ at $t$.

theorem WaveEquation3D.integral_average_tendsto (g : ℝ → ℝ) (t : ℝ) (hg : Continuous g) : Filter.Tendsto (fun (h : ℝ) => (∫ (ρ : ℝ) in t - h..h + t, g ρ) / (2 * h)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (g t))

For a continuous $g$, the integral average over a shrinking symmetric interval $\frac{1}{2h}\int_{t-h}^{t+h} g(\rho)\,d\rho$ tends to $g(t)$ as $h \to 0^+$.

theorem WaveEquation3D.contDiff_sphericalToCart_pair : ContDiff ℝ ⊤ fun (p : ℝ × ℝ) => sphericalToCart p.1 p.2

The spherical-to-Cartesian map $(\theta, \varphi) \mapsto \omega(\theta, \varphi)$ is $C^\infty$ smooth.

theorem WaveEquation3D.contDiff_parametric_spherical_integral {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] (F : H → ℝ → ℝ → ℝ) {n : ℕ∞} (hF : ContDiff ℝ ↑n fun (p : H × ℝ × ℝ) => F p.1 p.2.1 p.2.2) : ContDiff ℝ ↑n fun (x : H) => ∫ (θ : ℝ) in 0..Real.pi, ∫ (φ : ℝ) in 0..2 * Real.pi, F x θ φ

If $F(x, \theta, \varphi)$ is jointly $C^n$ in all three arguments, then the parametric spherical integral $x \mapsto \int_0^\pi\!\!\int_0^{2\pi} F(x, \theta, \varphi)\,d\varphi\,d\theta$ is also $C^n$.

theorem WaveEquation3D.sphericalMean_contDiff_of_contDiff (h : E3 → ℝ) (x : E3) {n : ℕ∞} (hh : ContDiff ℝ (↑n) h) : ContDiff ℝ (↑n) (SphericalMean h x)

If $h$ is $C^n$, then $r \mapsto \mathrm{SphericalMean}\,h\,x\,r$ is $C^n$ in the radius.

theorem WaveEquation3D.sphericalMean_contDiff_pair (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (x : E3) : ContDiff ℝ 2 fun (p : ℝ × ℝ) => SphericalMean (u p.1) x p.2

Joint $C^2$ smoothness in $(t, r)$ of $(t, r) \mapsto \mathrm{SphericalMean}(u(t,\cdot))(x, r)$ when $u$ is a $C^2$ wave solution.

theorem WaveEquation3D.F_tilde_contDiff (data : CauchyData3D) (x : E3) : ContDiff ℝ 2 fun (r' : ℝ) => F_tilde data r' x

$\tilde F(\cdot, x)$ is $C^2$ in the radial variable, using $f \in C^3$.

theorem WaveEquation3D.G_tilde_contDiff (data : CauchyData3D) (x : E3) : ContDiff ℝ 1 fun (r' : ℝ) => G_tilde data r' x

$\tilde G(\cdot, x)$ is $C^1$ in the radial variable, using $g \in C^2$.

theorem WaveEquation3D.limit_sphericalMean_dalembert (data : CauchyData3D) (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (hf : ∀ (x : E3), u 0 x = data.f x) (hg : ∀ (x : E3), (fderiv ℝ (fun (t : ℝ) => u t x) 0) 1 = data.g x) (t : ℝ) (ht : 0 < t) (x : E3) : u t x = (fderiv ℝ (fun (r : ℝ) => F_tilde data r x) t) 1 + G_tilde data t x

Taking $r \to 0^+$ in the d'Alembert formula for the auxiliary $1+1$-dimensional problem recovers $u(t, x)$: $u(t, x) = \partial_r \tilde F(t, x) + \tilde G(t, x)$.

theorem WaveEquation3D.limit_gives_derivative_plus_G (data : CauchyData3D) (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (hf : ∀ (x : E3), u 0 x = data.f x) (hg : ∀ (x : E3), (fderiv ℝ (fun (t : ℝ) => u t x) 0) 1 = data.g x) (t : ℝ) (ht : 0 < t) (x : E3) : u t x = (fderiv ℝ (fun (r : ℝ) => F_tilde data r x) t) 1 + G_tilde data t x

Restatement of limit_sphericalMean_dalembert: $u(t, x) = \partial_r \tilde F(t, x) + \tilde G(t, x)$.

theorem WaveEquation3D.differentiation_under_integral_kirchhoff (data : CauchyData3D) (t : ℝ) (ht : 0 < t) (x : E3) : (fderiv ℝ (fun (r : ℝ) => F_tilde data r x) t) 1 = 1 / (4 * Real.pi * t ^ 2) * SphereIntegral data.f x t + 1 / (4 * Real.pi * t) * SphereIntegralNormalDeriv data.f x t

Differentiation under the integral sign yields the two surface-integral terms appearing in Kirchhoff's formula: $\partial_r \tilde F(t, x) = \frac{1}{4\pi t^2}\int_{\partial B_t(x)} f,d\sigma

• \frac{1}{4\pi t}\int_{\partial B_t(x)} \nabla_{\hat N} f,d\sigma$.

theorem WaveEquation3D.G_tilde_equals_sphere_integral (data : CauchyData3D) (t : ℝ) (ht : 0 < t) (x : E3) : G_tilde data t x = 1 / (4 * Real.pi * t) * SphereIntegral data.g x t

$\tilde G(t, x) = \frac{1}{4\pi t}\int_{\partial B_t(x)} g\,d\sigma$, the last term of Kirchhoff's formula.

theorem WaveEquation3D.kirchhoff_formula (data : CauchyData3D) (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (hf : ∀ (x : E3), u 0 x = data.f x) (hg : ∀ (x : E3), (fderiv ℝ (fun (t : ℝ) => u t x) 0) 1 = data.g x) (t : ℝ) (ht : 0 < t) (x : E3) : u t x = 1 / (4 * Real.pi * t ^ 2) * SphereIntegral data.f x t + 1 / (4 * Real.pi * t) * SphereIntegralNormalDeriv data.f x t + 1 / (4 * Real.pi * t) * SphereIntegral data.g x t

Kirchhoff's formula (Class Meeting #12, Theorem 1.1). The unique $C^2$ solution of the $3$-dimensional Cauchy problem $-\partial_t^2 u + \Delta u = 0$, $u(0,x) = f(x)$, $\partial_t u(0,x) = g(x)$ admits the representation $u(t, x) = \frac{1}{4\pi t^2}\int_{\partial B_t(x)} f,d\sigma

• \frac{1}{4\pi t}\int_{\partial B_t(x)} \nabla_{\hat N} f,d\sigma
• \frac{1}{4\pi t}\int_{\partial B_t(x)} g,d\sigma$ for $t > 0$.

noncomputable def WaveEquation3D.sphericalAverage (u : ℝ → E3 → ℝ) (t r : ℝ) (x : E3) : ℝ

The spherical average $\mathrm{SphericalMean}(u(t,\cdot))(x, r)$ of a wave solution $u$ at time $t$, centred at $x$ with radius $r$.

noncomputable def WaveEquation3D.sphericalAverage_tilde (u : ℝ → E3 → ℝ) (t r : ℝ) (x : E3) : ℝ

The radius-weighted spherical average $r \cdot \mathrm{SphericalMean}(u(t,\cdot))(x, r)$, which solves a $1+1$-dimensional half-line wave equation in $(t, r)$.

theorem WaveEquation3D.sphericalAverage_solves_1d_wave (data : CauchyData3D) (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (_hf : ∀ (x : E3), u 0 x = data.f x) (_hg : ∀ (x : E3), (fderiv ℝ (fun (t : ℝ) => u t x) 0) 1 = data.g x) (t r : ℝ) (hr : 0 ≤ r) (x : E3) : (fderiv ℝ (fun (s : ℝ) => (fderiv ℝ (fun (s' : ℝ) => sphericalAverage_tilde u s' r x) s) 1) t) 1 = (fderiv ℝ (fun (ρ : ℝ) => (fderiv ℝ (fun (ρ' : ℝ) => sphericalAverage_tilde u t ρ' x) ρ) 1) r) 1

The weighted spherical average $\tilde A(t, r) := r \cdot \mathrm{SphericalMean}(u(t,\cdot))(x, r)$ solves the $1+1$-dimensional wave equation $\partial_t^2 \tilde A = \partial_r^2 \tilde A$.

theorem WaveEquation3D.sphericalAverage_tilde_initial_position (data : CauchyData3D) (u : ℝ → E3 → ℝ) (_hu : IsWaveSolution3D u) (hf : ∀ (x : E3), u 0 x = data.f x) (_hg : ∀ (x : E3), (fderiv ℝ (fun (t : ℝ) => u t x) 0) 1 = data.g x) (r : ℝ) (_hr : 0 < r) (x : E3) : sphericalAverage_tilde u 0 r x = F_tilde data r x

Initial position of the weighted spherical average: $\tilde A(0, r, x) = \tilde F(r, x)$.

theorem WaveEquation3D.sphericalAverage_tilde_initial_velocity (data : CauchyData3D) (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (_hf : ∀ (x : E3), u 0 x = data.f x) (hg : ∀ (x : E3), (fderiv ℝ (fun (t : ℝ) => u t x) 0) 1 = data.g x) (r : ℝ) (hr : 0 < r) (x : E3) : (fderiv ℝ (fun (t : ℝ) => sphericalAverage_tilde u t r x) 0) 1 = G_tilde data r x

Initial velocity of the weighted spherical average: $\partial_t \tilde A(0, r, x) = \tilde G(r, x)$.

theorem WaveEquation3D.sphericalAverage_tilde_contDiff (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (x : E3) : ContDiff ℝ 2 fun (p : ℝ × ℝ) => sphericalAverage_tilde u p.1 p.2 x

The map $(t, r) \mapsto \tilde A(t, r, x) = r \cdot \mathrm{SphericalMean}(u(t,\cdot))(x, r)$ is $C^2$.

theorem WaveEquation3D.sphericalAverage_tilde_wave_deriv (data : CauchyData3D) (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (hf : ∀ (x : E3), u 0 x = data.f x) (hg : ∀ (x : E3), (fderiv ℝ (fun (t : ℝ) => u t x) 0) 1 = data.g x) (x : E3) (t r : ℝ) : 0 ≤ r → deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => sphericalAverage_tilde u t'' r x) t') t = deriv (fun (r' : ℝ) => deriv (fun (r'' : ℝ) => sphericalAverage_tilde u t r'' x) r') r

The weighted spherical average $\tilde A$ satisfies the $1+1$-dimensional wave equation $\partial_t^2 \tilde A = \partial_r^2 \tilde A$ (stated in deriv form).

theorem WaveEquation3D.sphericalAverage_tilde_hasDerivAt_initial (data : CauchyData3D) (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (hf : ∀ (x : E3), u 0 x = data.f x) (hg : ∀ (x : E3), (fderiv ℝ (fun (t : ℝ) => u t x) 0) 1 = data.g x) (x : E3) (r : ℝ) : 0 < r → HasDerivAt (fun (t : ℝ) => sphericalAverage_tilde u t r x) (G_tilde data r x) 0

At time $t = 0$, the weighted spherical average has time derivative equal to $\tilde G(r, x)$.

theorem WaveEquation3D.sphericalAverage_tilde_dalembert (data : CauchyData3D) (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (hf : ∀ (x : E3), u 0 x = data.f x) (hg : ∀ (x : E3), (fderiv ℝ (fun (t : ℝ) => u t x) 0) 1 = data.g x) (t r : ℝ) (ht : 0 ≤ t) (hr : 0 ≤ r) (hrt : r ≤ t) (x : E3) : sphericalAverage_tilde u t r x = 1 / 2 * (F_tilde data (r + t) x - F_tilde data (t - r) x) + 1 / 2 * ∫ (ρ : ℝ) in t - r..r + t, G_tilde data ρ x

D'Alembert representation for the weighted spherical average: for $0 \le r \le t$, $\tilde A(t, r, x) = \tfrac12(\tilde F(r+t, x) - \tilde F(t-r, x)) + \tfrac12 \int_{t-r}^{r+t} \tilde G(\rho, x)\,d\rho$.

theorem WaveEquation3D.corollary_1_0_2 (data : CauchyData3D) (u : ℝ → E3 → ℝ) (hu : IsWaveSolution3D u) (hf : ∀ (x : E3), u 0 x = data.f x) (hg : ∀ (x : E3), (fderiv ℝ (fun (t : ℝ) => u t x) 0) 1 = data.g x) (t r : ℝ) (ht : 0 ≤ t) (hr : 0 ≤ r) (hrt : r ≤ t) (x : E3) : sphericalAverage_tilde u t r x = 1 / 2 * (F_tilde data (r + t) x - F_tilde data (t - r) x) + 1 / 2 * ∫ (ρ : ℝ) in t - r..r + t, G_tilde data ρ x

Corollary 1.0.2: explicit d'Alembert representation for the weighted spherical average $\tilde A(t, r, x)$ in terms of the initial data $\tilde F$ and $\tilde G$.

def WaveEquation3D.minkowskiMetric (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

The Minkowski metric $m_{\mu\nu} = \mathrm{diag}(-1, 1, \dots, 1)$ on $\mathbb{R}^{1+n}$ as a matrix indexed by Fin (n + 1).

def WaveEquation3D.minkowskiInner (n : ℕ) (X Y : Fin (n + 1) → ℝ) : ℝ

The Minkowski inner product $m(X, Y) = X^\alpha m_{\alpha\beta} Y^\beta$ on $\mathbb{R}^{1+n}$.

theorem WaveEquation3D.minkowskiInner_comm (n : ℕ) (X Y : Fin (n + 1) → ℝ) : minkowskiInner n X Y = minkowskiInner n Y X

The Minkowski inner product is symmetric: $m(X, Y) = m(Y, X)$.

def WaveEquation3D.IsTimelike (n : ℕ) (X : Fin (n + 1) → ℝ) : Prop

A vector $X \in \mathbb{R}^{1+n}$ is timelike if $m(X, X) < 0$ (Definition 2.0.1, case (1)).

def WaveEquation3D.IsSpacelike (n : ℕ) (X : Fin (n + 1) → ℝ) : Prop

A vector $X \in \mathbb{R}^{1+n}$ is spacelike if $m(X, X) > 0$ (Definition 2.0.1, case (2)).

def WaveEquation3D.IsNull (n : ℕ) (X : Fin (n + 1) → ℝ) : Prop

A vector $X \in \mathbb{R}^{1+n}$ is null if $m(X, X) = 0$ (Definition 2.0.1, case (3)).

def WaveEquation3D.IsCausal (n : ℕ) (X : Fin (n + 1) → ℝ) : Prop

A vector $X \in \mathbb{R}^{1+n}$ is causal if it is timelike or null, equivalently $m(X, X) \le 0$ (Definition 2.0.1, case (4)).

def WaveEquation3D.IsFutureDirected (n : ℕ) (X : Fin (n + 1) → ℝ) : Prop

A vector $X \in \mathbb{R}^{1+n}$ is future-directed if its time component satisfies $X^0 > 0$ (Definition 2.0.2).

def WaveEquation3D.IsLorentzTransformation (n : ℕ) (Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ) : Prop

A matrix $\Lambda$ is a Lorentz transformation if it preserves the Minkowski metric: $\Lambda^T m \Lambda = m$ (Definition 2.1.1).

theorem WaveEquation3D.lorentz_preserves_inner {n : ℕ} {Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} (hΛ : IsLorentzTransformation n Λ) (X Y : Fin (n + 1) → ℝ) : minkowskiInner n (Λ.mulVec X) (Λ.mulVec Y) = minkowskiInner n X Y

A Lorentz transformation preserves the Minkowski inner product: $m(\Lambda X, \Lambda Y) = m(X, Y)$.

theorem WaveEquation3D.lorentz_preserves_timelike {n : ℕ} {Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} (hΛ : IsLorentzTransformation n Λ) {X : Fin (n + 1) → ℝ} (hX : IsTimelike n X) : IsTimelike n (Λ.mulVec X)

Corollary 2.1.1 (timelike case): Lorentz transformations preserve timelike vectors.

theorem WaveEquation3D.lorentz_preserves_spacelike {n : ℕ} {Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} (hΛ : IsLorentzTransformation n Λ) {X : Fin (n + 1) → ℝ} (hX : IsSpacelike n X) : IsSpacelike n (Λ.mulVec X)

Corollary 2.1.1 (spacelike case): Lorentz transformations preserve spacelike vectors.

theorem WaveEquation3D.lorentz_preserves_null {n : ℕ} {Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} (hΛ : IsLorentzTransformation n Λ) {X : Fin (n + 1) → ℝ} (hX : IsNull n X) : IsNull n (Λ.mulVec X)

Corollary 2.1.1 (null case): Lorentz transformations preserve null vectors.

theorem WaveEquation3D.lorentz_preserves_causal {n : ℕ} {Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} (hΛ : IsLorentzTransformation n Λ) {X : Fin (n + 1) → ℝ} (hX : IsCausal n X) : IsCausal n (Λ.mulVec X)

Corollary 2.1.1 (causal case): Lorentz transformations preserve causal vectors.

structure WaveEquation3D.NullFrame (n : ℕ) : Type

A null frame on $\mathbb{R}^{1+n}$ (Definition 2.2.1): a basis $\{L, \underline L, e_{(1)}, \dots, e_{(n-1)}\}$ where $L, \underline L$ are null with $m(L, \underline L) = -2$, and the $e_{(i)}$ are $m$-orthonormal vectors $m$-orthogonal to both $L$ and $\underline L$. The completeness field records the resulting expansion $X = -\tfrac12 m(\underline L, X) L - \tfrac12 m(L, X)\underline L + \sum_i m(e_{(i)}, X) e_{(i)}$.

• L : Fin (n + 1) → ℝ
• Lb : Fin (n + 1) → ℝ
• e : Fin (n - 1) → Fin (n + 1) → ℝ
• L_null : minkowskiInner n self.L self.L = 0
• Lb_null : minkowskiInner n self.Lb self.Lb = 0
• L_Lb_inner : minkowskiInner n self.L self.Lb = -2
• e_orthonormal (i j : Fin (n - 1)) : minkowskiInner n (self.e i) (self.e j) = if i = j then 1 else 0
• L_e_orthog (i : Fin (n - 1)) : minkowskiInner n self.L (self.e i) = 0
• Lb_e_orthog (i : Fin (n - 1)) : minkowskiInner n self.Lb (self.e i) = 0
• completeness (X : Fin (n + 1) → ℝ) : X = (-(1 / 2) * minkowskiInner n self.Lb X) • self.L + (-(1 / 2) * minkowskiInner n self.L X) • self.Lb + ∑ i : Fin (n - 1), minkowskiInner n (self.e i) X • self.e i

def WaveEquation3D.angularMetric (n : ℕ) (nf : NullFrame n) (X Y : Fin (n + 1) → ℝ) : ℝ

The angular metric $h(X, Y) := \sum_i m(e_{(i)}, X) m(e_{(i)}, Y)$ associated with a null frame; it is positive-definite on the $m$-orthogonal complement of $\mathrm{span}(L, \underline L)$ and vanishes on $\mathrm{span}(L, \underline L)$.

theorem WaveEquation3D.nullFrame_decomposition {n : ℕ} (nf : NullFrame n) (X Y : Fin (n + 1) → ℝ) : minkowskiInner n X Y = -(1 / 2) * minkowskiInner n nf.L X * minkowskiInner n nf.Lb Y - 1 / 2 * minkowskiInner n nf.Lb X * minkowskiInner n nf.L Y + angularMetric n nf X Y

Proposition 2.2.1 (null-frame decomposition of $m$): $m(X, Y) = -\tfrac12 m(L, X) m(\underline L, Y) - \tfrac12 m(\underline L, X) m(L, Y) + h(X, Y)$ where $h$ is the angular metric of the null frame.

theorem WaveEquation3D.angularMetric_vanish_L {n : ℕ} (nf : NullFrame n) (Y : Fin (n + 1) → ℝ) : angularMetric n nf nf.L Y = 0

The angular metric vanishes on $L$ in the first argument: $h(L, Y) = 0$.

theorem WaveEquation3D.angularMetric_vanish_Lb {n : ℕ} (nf : NullFrame n) (Y : Fin (n + 1) → ℝ) : angularMetric n nf nf.Lb Y = 0

The angular metric vanishes on $\underline L$ in the first argument: $h(\underline L, Y) = 0$.

theorem WaveEquation3D.angularMetric_comm {n : ℕ} (nf : NullFrame n) (X Y : Fin (n + 1) → ℝ) : angularMetric n nf X Y = angularMetric n nf Y X

The angular metric is symmetric: $h(X, Y) = h(Y, X)$.

theorem WaveEquation3D.angularMetric_vanish_L_right {n : ℕ} (nf : NullFrame n) (X : Fin (n + 1) → ℝ) : angularMetric n nf X nf.L = 0

The angular metric vanishes on $L$ in the second argument: $h(X, L) = 0$.

theorem WaveEquation3D.angularMetric_vanish_Lb_right {n : ℕ} (nf : NullFrame n) (X : Fin (n + 1) → ℝ) : angularMetric n nf X nf.Lb = 0

The angular metric vanishes on $\underline L$ in the second argument: $h(X, \underline L) = 0$.

theorem WaveEquation3D.angularMetric_on_e {n : ℕ} (nf : NullFrame n) (i j : Fin (n - 1)) : angularMetric n nf (nf.e i) (nf.e j) = if i = j then 1 else 0

Values of the angular metric on the angular basis: $h(e_{(i)}, e_{(j)}) = \delta_{ij}$.

theorem WaveEquation3D.angularMetric_nonneg {n : ℕ} (nf : NullFrame n) (X : Fin (n + 1) → ℝ) : 0 ≤ angularMetric n nf X X

The angular metric is positive semidefinite: $h(X, X) \ge 0$.

theorem WaveEquation3D.angularMetric_pos_def {n : ℕ} (nf : NullFrame n) (X : Fin (n + 1) → ℝ) (hL : minkowskiInner n nf.L X = 0) (hLb : minkowskiInner n nf.Lb X = 0) (hX : X ≠ 0) : 0 < angularMetric n nf X X

The angular metric is positive-definite on the $m$-orthogonal complement of $\mathrm{span}(L, \underline L)$: if $X \ne 0$ with $m(L, X) = m(\underline L, X) = 0$, then $h(X, X) > 0$.

theorem WaveEquation3D.minkowskiMetric_sq (n : ℕ) : minkowskiMetric n * minkowskiMetric n = 1

The Minkowski metric is an involution: $m \cdot m = I$.

theorem WaveEquation3D.minkowskiMetric_inv (n : ℕ) : (minkowskiMetric n)⁻¹ = minkowskiMetric n

The Minkowski metric is its own inverse: $m^{-1} = m$.

theorem WaveEquation3D.minkowskiInner_eta_cancel (n : ℕ) (V W : Fin (n + 1) → ℝ) : minkowskiInner n V ((minkowskiMetric n).mulVec W) = V ⬝ᵥ W

"Index-raising cancellation": $m(V, m \cdot W) = V \cdot W$ (Euclidean dot product).

theorem WaveEquation3D.nullFrame_inverse_decomposition {n : ℕ} (nf : NullFrame n) (μ ν : Fin (n + 1)) : (minkowskiMetric n)⁻¹ μ ν = -(1 / 2) * nf.L μ * nf.Lb ν - 1 / 2 * nf.Lb μ * nf.L ν + ∑ i : Fin (n - 1), nf.e i μ * nf.e i ν

Proposition 2.2.1 (raised-index version): the inverse Minkowski metric admits the null-frame decomposition $(m^{-1})^{\mu\nu} = -\tfrac12 L^\mu \underline L^\nu - \tfrac12 \underline L^\mu L^\nu + \sum_i e_{(i)}^\mu e_{(i)}^\nu$.