The heat estimates specialized to genuine ordinary smooth L² fields.

The same Gaussian average as a continuous dilation of a fixed kernel.

theorem EulerWholeSpaceGaussian.normalization_sq {c : ℝ} (hc : 0 < c) : normalization (c ^ 2) = (c ^ 3)⁻¹ * normalization 1

theorem EulerWholeSpaceGaussian.kernel_sq_smul {c : ℝ} (hc : 0 < c) (y : EulerSmoothLimit.Space) : kernel (c ^ 2) (c • y) = (c ^ 3)⁻¹ * kernel 1 y

theorem EulerWholeSpaceGaussian.norm_mul_kernel_integrable {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (fun (y : EulerSmoothLimit.Space) => ‖y‖ * kernel t y) MeasureTheory.volume

noncomputable def EulerWholeSpaceGaussian.scaledAverage {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (t : ℝ) (f : EulerSmoothLimit.Space → V) (x : EulerSmoothLimit.Space) : V

This formula continues the actual heat average to t=0 by dilation.

Equations

• EulerWholeSpaceGaussian.scaledAverage t f x = ∫ (y : EulerSmoothLimit.Space), EulerWholeSpaceGaussian.kernel 1 y • f (x + √t • y)

theorem EulerWholeSpaceGaussian.scaledAverage_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : ℝ} (ht : 0 < t) (f : EulerSmoothLimit.Space → V) (x : EulerSmoothLimit.Space) : scaledAverage t f x = average t f x

theorem EulerWholeSpaceGaussian.scaledAverage_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (f : EulerSmoothLimit.Space → V) (x : EulerSmoothLimit.Space) : scaledAverage 0 f x = f x

theorem EulerWholeSpaceGaussian.scaledAverage_continuous {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : Continuous f) (C : ℝ) (hb : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C) (x : EulerSmoothLimit.Space) : Continuous fun (t : ℝ) => scaledAverage t f x

theorem EulerWholeSpaceGaussian.average_tendsto_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (f : EulerSmoothLimit.Space → V) (hf : Continuous f) (C : ℝ) (hb : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C) (x : EulerSmoothLimit.Space) : Filter.Tendsto (fun (t : ℝ) => average t f x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))

theorem EulerWholeSpaceGaussian.average_integrable_of_memLp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : ℝ} (ht : 0 < t) (f : EulerSmoothLimit.Space → V) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (x : EulerSmoothLimit.Space) : MeasureTheory.Integrable (fun (y : EulerSmoothLimit.Space) => kernel t y • f (x + y)) MeasureTheory.volume

theorem EulerWholeSpaceGaussian.average_sub {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : ℝ} (ht : 0 < t) (f g : EulerSmoothLimit.Space → V) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (x : EulerSmoothLimit.Space) : average t (fun (y : EulerSmoothLimit.Space) => f y - g y) x = average t f x - average t g x

theorem EulerWholeSpaceGaussian.average_sum {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : ℝ} (ht : 0 < t) (f : Fin 3 → EulerSmoothLimit.Space → V) (hf : ∀ (i : Fin 3), MeasureTheory.MemLp (f i) 2 MeasureTheory.volume) (x : EulerSmoothLimit.Space) : average t (fun (y : EulerSmoothLimit.Space) => ∑ i : Fin 3, f i y) x = ∑ i : Fin 3, average t (f i) x

theorem EulerWholeSpaceGaussian.secondAverage_directional_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : ℝ} (ht : 0 < t) (A : EulerLpTranslation.SmoothL2Field V) (j : Fin 3) (x : EulerSmoothLimit.Space) : ‖secondAverage t (A.directionalField (EulerOrdinarySobolev.axis j)).field x‖ ≤ 3 * t ^ (-3 / 4) * ‖A.jetLp 3‖

theorem EulerWholeSpaceGaussian.field_sup_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (A : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : ‖A.field x‖ ≤ ‖EulerMeanSobolevBoundedField.finiteField A‖

theorem EulerWholeSpaceGaussian.average_field_hasDerivAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {t : ℝ} (ht : 0 < t) (A : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : HasDerivAt (fun (s : ℝ) => average s A.field x) ((1 / 4) • secondAverage t A.field x) t

theorem EulerWholeSpaceGaussian.scaledAverage_field_hasDerivAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {t : ℝ} (ht : 0 < t) (A : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : HasDerivAt (fun (s : ℝ) => scaledAverage s A.field x) ((1 / 4) • secondAverage t A.field x) t

theorem EulerWholeSpaceGaussian.average_field_first_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (A : EulerLpTranslation.SmoothL2Field V) (a x : EulerSmoothLimit.Space) : ‖average 1 (fun (y : EulerSmoothLimit.Space) => (fderiv ℝ A.field y) a) x‖ ≤ lowCost * ‖a‖ * ‖A.toLp‖

theorem EulerWholeSpaceGaussian.average_field_second_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {t : ℝ} (ht : 0 < t) (A : EulerLpTranslation.SmoothL2Field V) (W : ℝ) (hW : ∀ (x : EulerSmoothLimit.Space), ‖A.field x‖ ≤ W) (a b x : EulerSmoothLimit.Space) : ‖average t (fun (z : EulerSmoothLimit.Space) => (fderiv ℝ (fun (y : EulerSmoothLimit.Space) => (fderiv ℝ A.field y) b) z) a) x‖ ≤ 10 * 2 ^ (3 / 2) * t⁻¹ * ‖a‖ * ‖b‖ * W

theorem EulerWholeSpaceGaussian.secondAverage_eq_laplacian {t : ℝ} (ht : 0 < t) (A : EulerLpTranslation.SmoothL2Field ℝ) (x : EulerSmoothLimit.Space) : secondAverage t A.field x = average t (Laplacian.laplacian A.field) x