Research proof index

The gradient of a distribution (Space d) →d[ℝ] ℝ as a distribution (Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d)). -/ noncomputable def distGrad {d} : ((Space d) →d[ℝ] ℝ) →ₗ[ℝ] (Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d)) where toFun f := basis.repr.toContinuousLinearMap ∘L ((InnerProductSpace.toDual ℝ (Space d)).symm.toContinuousLinearMap).comp (fderivD ℝ...

A power series which is differentiable everywhere, and in the limit as n → ∞ tends to ‖x‖. -/ def normPowerSeries {d} : ℕ → Space d → ℝ := fun n x => √(‖x‖ ^ 2 + 1/(n + 1)) lemma normPowerSeries_eq (n : ℕ) : normPowerSeries (d := d) n = fun x => √(‖x‖ ^ 2 + 1/(n + 1)) := rfl lemma normPowerSeries_eq_rpow {d} (n : ℕ) : normPowerSeries (d := d) n = fun...

The distributional Laplacian of ‖x‖ ^ (2 - d) is (2 - d) * d * volume (Metric.ball 0 1) times the Dirac delta at the origin. For d ≥ 3 this ‖x‖ ^ (2 - d) is the (singular) fundamental solution of the Laplacian, and for d = 1 it is ‖x‖. When d = 2 the exponent vanishes, so the identity collapses to the trivial Δᵈ 1 = 0; the genuine two-dime...

The space derivative of a distribution dependent on time and space. -/ noncomputable def distSpaceDeriv {M d} [NormedAddCommGroup M] [NormedSpace ℝ M] (i : Fin d) : ((Time × Space d) →d[ℝ] M) →ₗ[ℝ] (Time × Space d) →d[ℝ] M where toFun f := let ev : (Time × Space d →L[ℝ] M) →L[ℝ] M := { toFun v := v (0, basis i) map_add' v1 v2 := by simp only [root.add_a...

The space derivative of a distribution dependent on time and space. -/ noncomputable def distSpaceDeriv {M d} [NormedAddCommGroup M] [NormedSpace ℝ M] (i : Fin d) : ((Time × Space d) →d[ℝ] M) →ₗ[ℝ] (Time × Space d) →d[ℝ] M where toFun f := let ev : (Time × Space d →L[ℝ] M) →L[ℝ] M := { toFun v := v (0, basis i) map_add' v1 v2 := by simp only [root.add_a...

Second derivatives distribute coordinate-wise over subtraction (two components for curl). -/ lemma deriv_coord_2nd_sub (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 f) : ∂[u] (fun x => ∂[v] (fun x => f x w) x - ∂[w] (fun x => f x v) x) = (∂[u] (∂[v] (fun x => f x w))) - (∂[u] (∂[w] (fun x => f x v))) := by repeat rw [deriv_eq_fderiv_fun] ext x...