Atlas.DifferentialAnalysis.code.LaplacianExistence

source

theorem DifferentialOperators.laplacian_convolution_iteratedFDeriv_zpow_bound {n : ℕ} (hn : 3 ≤ n) (E : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hE : IsTemperedFundamentalSolution n laplacianPoly E) (f : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (m : ℕ) :

∃ (M : ℝ), 0 < M ∧ ∀ (x : EuclideanSpace ℝ (Fin n)), ‖iteratedFDeriv ℝ m (temperedConvolution E f) x‖ ≤ M * (1 + ‖x‖) ^ (2 - ↑n - ↑m)

For n ≥ 3, the convolution E ∗ f of a tempered fundamental solution of the Laplacian with a Schwartz function has iterated derivatives of order m bounded by M (1 + ‖x‖)^{2 - n - m}.

source

theorem DifferentialOperators.laplacian_convolution_pointwise_decay_bound {n : ℕ} (hn : 3 ≤ n) (E : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hE : IsTemperedFundamentalSolution n laplacianPoly E) (f : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (m : ℕ) :

∃ (C : ℝ), 0 < C ∧ ∀ (x : EuclideanSpace ℝ (Fin n)), ‖iteratedFDeriv ℝ m (temperedConvolution E f) x‖ ≤ C / (1 + ‖x‖)

For n ≥ 3, every iterated derivative of the convolution E ∗ f is pointwise bounded by C / (1 + ‖x‖), since the exponent 2 - n - m ≤ -1.

source

theorem DifferentialOperators.laplacian_fundamental_convolution_vanishes_at_infty {n : ℕ} (hn : 3 ≤ n) (E : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hE : IsTemperedFundamentalSolution n laplacianPoly E) (f : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (m : ℕ) :

Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ‖iteratedFDeriv ℝ m (temperedConvolution E f) x‖) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

For n ≥ 3, every iterated derivative of E ∗ f vanishes at infinity (tends to zero along the cocompact filter).

source

theorem DifferentialOperators.tempered_convolution_fourier_multiplier_exchange {n : ℕ} (E : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (f φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (m : EuclideanSpace ℝ (Fin n) → ℂ) (hm : Function.HasTemperateGrowth m) :

∫ (x : EuclideanSpace ℝ (Fin n)), (FourierTransform.fourier ((SchwartzMap.smulLeftCLM ℂ m) (FourierTransformInv.fourierInv φ))) x • temperedConvolution E f x = ∫ (x : EuclideanSpace ℝ (Fin n)), φ x • temperedConvolution ((TemperedDistribution.fourierMultiplierCLM ℂ m) E) f x

Exchange identity: pairing the Fourier-side multiplication by m against E ∗ f agrees with pairing φ against the convolution of f with the Fourier multiplier m · E.

source

theorem DifferentialOperators.fourier_multiplier_convolution_integral_eq {n : ℕ} (E : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hE : IsTemperedFundamentalSolution n laplacianPoly E) (f φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) :

∫ (x : EuclideanSpace ℝ (Fin n)), (FourierTransform.fourier ((SchwartzMap.smulLeftCLM ℂ (polySymbol n laplacianPoly)) (FourierTransformInv.fourierInv φ))) x • temperedConvolution E f x = ∫ (x : EuclideanSpace ℝ (Fin n)), φ x • f x

Pairing identity used in the Laplacian existence proof: integration of the Fourier-side symbol against E ∗ f reduces to ∫ φ • f thanks to the fundamental-solution property of E.

source

theorem DifferentialOperators.laplacian_fundamental_convolution_distributional_eq {n : ℕ} (hn : 3 ≤ n) (E : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hE : IsTemperedFundamentalSolution n laplacianPoly E) (f : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (u_td : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu_td : ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), u_td φ = ∫ (x : EuclideanSpace ℝ (Fin n)), φ x • temperedConvolution E f x) :

laplacianOp u_td = (SchwartzMap.toTemperedDistributionCLM (EuclideanSpace ℝ (Fin n)) ℂ MeasureTheory.volume) f

If u_td is the tempered distribution given by integration against E ∗ f, then Δ u_td = f as tempered distributions.

source

theorem DifferentialOperators.tempered_distribution_of_polynomial_growth {n : ℕ} (g : EuclideanSpace ℝ (Fin n) → ℂ) (hsmooth : ContDiff ℝ (↑⊤) g) (hgrowth : ∃ (C : ℝ) (k : ℕ), 0 < C ∧ ∀ (x : EuclideanSpace ℝ (Fin n)), ‖g x‖ ≤ C * (1 + ‖x‖ ^ 2) ^ (↑k / 2)) :

∃ (u_td : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ), ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), u_td φ = ∫ (x : EuclideanSpace ℝ (Fin n)), φ x • g x

A smooth function g of polynomial growth defines a tempered distribution via integration: there is a continuous linear functional on Schwartz space whose value at φ is ∫ φ • g.

source

theorem DifferentialOperators.fundamental_solution_convolution_gives_C0infty_solution {n : ℕ} (hn : 3 ≤ n) (E : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hE : IsTemperedFundamentalSolution n laplacianPoly E) (f : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) :

∃ (u : SmoothZeroAtInfty n) (u_td : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ), (∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), u_td φ = ∫ (x : EuclideanSpace ℝ (Fin n)), φ x • u x) ∧ laplacianOp u_td = (SchwartzMap.toTemperedDistributionCLM (EuclideanSpace ℝ (Fin n)) ℂ MeasureTheory.volume) f

Convolving a tempered fundamental solution of the Laplacian with a Schwartz datum f produces a smooth solution u vanishing at infinity together with all its derivatives, together with the corresponding tempered distribution u_td satisfying Δ u_td = f.

source

theorem DifferentialOperators.laplacian_schwartz_existence_C0infty {n : ℕ} (hn : 3 ≤ n) (f : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) :

Melrose Theorem 11.17 (Laplacian existence): for n ≥ 3 and a Schwartz datum f on ℝⁿ, the equation Δ u = f admits a smooth solution vanishing at infinity (with all derivatives), and any two such solutions agree.