Derivative Adjoint

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.pressure_coord_fderiv_eq_deriv_update {f : Foundation.Parabolic.Vec3 → ℝ} {x : Foundation.Parabolic.Vec3} (hf : DifferentiableAt ℝ f x) (i : Fin 3) : (fderiv ℝ f x) (basisVec i) = deriv (fun (s : ℝ) => f (Function.update x i s)) (x i)

theorem CKN.pressure_newtonian_derivative_adjoint {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (i : Fin 3) (y : Foundation.Parabolic.Vec3) : ∫ (x : Foundation.Parabolic.Vec3), spatialDeriv Foundation.Heat.newtonianKernel i (x - y) * spatialLaplacian ψ x = spatialDeriv ψ i y

theorem CKN.pressureNewtonianDerivativePotential_distributional_pairing_smooth {i : Fin 3} {g ψ : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hgc : HasCompactSupport g) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i g x * spatialLaplacian ψ x = ∫ (y : Foundation.Parabolic.Vec3), g y * spatialDeriv ψ i y