Heat regularization of bounded uniformly continuous data

Restricting the bounded continuous heat operator from TauCeti.Analysis.PDE.HeatKernel.BoundedContinuous to the closed subspace of bounded uniformly continuous functions gives TauCeti.heatCauchyPotentialBUC.

On that subspace the regularizations converge in supremum norm to the initial datum. In particular, smooth functions with bounded derivatives of every order are dense there, with no increase of the supremum norm. Such approximants allow comparison estimates for smooth-data parabolic problems to pass to uniformly continuous initial traces. This file asserts neither solvability for variable coefficients nor a uniform bound on derivatives as time tends to zero.

The analytic inputs are the derivative bounds for heat convolutions in TauCeti.Analysis.PDE.HeatKernel.HeatEquation and the uniform approximate-identity theorem TauCeti.tendstoUniformly_heatKernel_convolution.

References

• A. Lunardi, Linear and nonlinear diffusion problems, Cortona lecture notes (2004), Chapter 4.
• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Chapter II, 2.12 (diffusion on bounded uniformly continuous functions).

theorem TauCeti.uniformContinuous_heatCauchyPotentialBCF {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (t : ℝ) (g : BoundedContinuousFunction E F) (hg : UniformContinuous ⇑g) : UniformContinuous ⇑((heatCauchyPotentialBCF t) g)

The heat regularization preserves uniform continuity, including at nonpositive times.

noncomputable def TauCeti.heatCauchyPotentialBUC {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (t : ℝ) : ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F) →L[ℝ] ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)

Heat regularization on the closed subspace of bounded uniformly continuous functions.

@[simp]

theorem TauCeti.coe_heatCauchyPotentialBUC {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (t : ℝ) (g : ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)) : ↑((heatCauchyPotentialBUC t) g) = (heatCauchyPotentialBCF t) ↑g

The bounded continuous function underlying heat regularization on the uniformly continuous subspace is the usual bounded heat regularization.

@[simp]

theorem TauCeti.heatCauchyPotentialBUC_of_nonpos {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {t : ℝ} (ht : t ≤ 0) : heatCauchyPotentialBUC t = ContinuousLinearMap.id ℝ ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)

At nonpositive times heat regularization on bounded uniformly continuous functions is the identity. In particular, this gives the time-zero initial value.

theorem TauCeti.norm_heatCauchyPotentialBUC_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (t : ℝ) : ‖heatCauchyPotentialBUC t‖ ≤ 1

The heat operator on bounded uniformly continuous functions is a contraction.

theorem TauCeti.tendsto_heatCauchyPotentialBUC {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (g : ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)) : Filter.Tendsto (fun (t : ℝ) => (heatCauchyPotentialBUC t) g) (nhdsWithin 0 (Set.Ioi 0)) (nhds g)

Uniform attainment of the initial trace. Heat regularizations of bounded uniformly continuous data converge in the inherited supremum norm as t → 0⁺.

theorem TauCeti.exists_contDiff_bounded_derivatives_approximation {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (g : ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)) {ε : ℝ} (hε : 0 < ε) : ∃ (f : ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)), ContDiff ℝ ↑⊤ ⇑↑f ∧ ‖f - g‖ < ε ∧ ‖f‖ ≤ ‖g‖ ∧ ∀ (m : ℕ), ∃ (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ m (⇑↑f) x‖ ≤ C

Smooth approximation of bounded uniformly continuous data. For every positive tolerance there is a bounded uniformly continuous, smooth approximant with bounded derivatives of every order. Its supremum norm does not exceed that of the datum.