Related estimates used together by the same construction modules.

The true heat-time evolution of Gaussian averaging on ordinary space.

The literal time derivative of the Gaussian density and local domination.

noncomputable def EulerWholeSpaceGaussian.timeKernel (t : ℝ) (y : EulerSmoothLimit.Space) : ℝ

Time kernel, given by (t⁻¹^2*‖y‖^2-(3/2:ℝ)*t⁻¹)*kernel t y.

Equations

• EulerWholeSpaceGaussian.timeKernel t y = (t⁻¹ ^ 2 * ‖y‖ ^ 2 - 3 / 2 * t⁻¹) * EulerWholeSpaceGaussian.kernel t y

theorem EulerWholeSpaceGaussian.normalization_hasDerivAt {t : ℝ} (ht : 0 < t) : HasDerivAt normalization (-(3 / 2) * t⁻¹ * normalization t) t

theorem EulerWholeSpaceGaussian.kernel_hasDerivAt {t : ℝ} (ht : 0 < t) (y : EulerSmoothLimit.Space) : HasDerivAt (fun (s : ℝ) => kernel s y) (timeKernel t y) t

theorem EulerWholeSpaceGaussian.timeKernel_continuous (t : ℝ) : Continuous (timeKernel t)

theorem EulerWholeSpaceGaussian.timeKernel_second_sum (t : ℝ) (y : EulerSmoothLimit.Space) : timeKernel t y = 1 / 4 * ∑ i : Fin 3, secondKernel t (EuclideanSpace.single i 1) (EuclideanSpace.single i 1) y

theorem EulerWholeSpaceGaussian.timeKernel_bound {t : ℝ} (ht : 0 < t) (y : EulerSmoothLimit.Space) : ‖timeKernel t y‖ ≤ 15 / 2 * t⁻¹ * wideKernel t y

theorem EulerWholeSpaceGaussian.timeKernel_integrable {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (timeKernel t) MeasureTheory.volume

noncomputable def EulerWholeSpaceGaussian.timeEnvelope (t : ℝ) (y : EulerSmoothLimit.Space) : ℝ

Time envelope, given by (15*t⁻¹*normalization (t/2))*Real.exp (-(4*t)⁻¹*‖y‖^2).

Equations

• EulerWholeSpaceGaussian.timeEnvelope t y = 15 * t⁻¹ * EulerWholeSpaceGaussian.normalization (t / 2) * Real.exp (-(4 * t)⁻¹ * ‖y‖ ^ 2)

theorem EulerWholeSpaceGaussian.timeEnvelope_integrable {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (timeEnvelope t) MeasureTheory.volume

theorem EulerWholeSpaceGaussian.normalization_antitone {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) : normalization t ≤ normalization s

theorem EulerWholeSpaceGaussian.timeKernel_local_bound {t : ℝ} (ht : 0 < t) (s : ℝ) (hs : s ∈ Set.Ioo (t / 2) (2 * t)) (y : EulerSmoothLimit.Space) : ‖timeKernel s y‖ ≤ timeEnvelope t y

theorem EulerWholeSpaceGaussian.average_hasDerivAt_kernel {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : ℝ} (ht : 0 < t) (f : EulerSmoothLimit.Space → V) (hf : Continuous f) (C₀ : ℝ) (h₀ : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C₀) (x : EulerSmoothLimit.Space) : HasDerivAt (fun (s : ℝ) => average s f x) (∫ (y : EulerSmoothLimit.Space), timeKernel t y • f (x + y)) t

Differentiating the explicit kernel under its ordinary Bochner integral.

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

Second average, given by ∑ i : Fin 3, average t (fun z => fderiv ℝ (fun y => fderiv ℝ f y (EuclideanSpace.single i 1)) z (EuclideanSpace.single i 1)) x.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerWholeSpaceGaussian.timeIntegral_eq_secondAverage {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : ℝ} (ht : 0 < t) (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (C₀ C₁ C₂ : ℝ) (h₀ : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C₀) (h₁ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ f x‖ ≤ C₁) (h₂ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ f) x‖ ≤ C₂) (x : EulerSmoothLimit.Space) : ∫ (y : EulerSmoothLimit.Space), timeKernel t y • f (x + y) = (1 / 4) • secondAverage t f x

The explicit time-kernel integral equals one quarter of the sum of the actual second spatial derivatives averaged against the same Gaussian.

theorem EulerWholeSpaceGaussian.average_hasDerivAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : ℝ} (ht : 0 < t) (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (C₀ C₁ C₂ : ℝ) (h₀ : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C₀) (h₁ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ f x‖ ≤ C₁) (h₂ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ f) x‖ ≤ C₂) (x : EulerSmoothLimit.Space) : HasDerivAt (fun (s : ℝ) => average s f x) ((1 / 4) • secondAverage t f x) t

The low-frequency derivative of the true Gaussian average is controlled by the ordinary L² norm of the original field.

theorem EulerWholeSpaceGaussian.firstKernel_sq_bound {t : ℝ} (ht : 0 < t) (a y : EulerSmoothLimit.Space) : ‖firstKernel t a y‖ ^ 2 ≤ 8 * t⁻¹ * normalization t * ‖a‖ ^ 2 * wideKernel t y

theorem EulerWholeSpaceGaussian.firstKernel_memLp {t : ℝ} (ht : 0 < t) (a : EulerSmoothLimit.Space) : MeasureTheory.MemLp (firstKernel t a) 2 MeasureTheory.volume

theorem EulerWholeSpaceGaussian.integral_firstKernel_sq_bound {t : ℝ} (ht : 0 < t) (a : EulerSmoothLimit.Space) : ∫ (y : EulerSmoothLimit.Space), ‖firstKernel t a y‖ ^ 2 ≤ 8 * normalization t * 2 ^ (3 / 2) * t⁻¹ * ‖a‖ ^ 2

noncomputable def EulerWholeSpaceGaussian.lowCost : ℝ

Low cost, given by Real.sqrt (8*normalization 1*(2:ℝ)^((3:ℝ)/2)).

Equations

• EulerWholeSpaceGaussian.lowCost = √(8 * EulerWholeSpaceGaussian.normalization 1 * 2 ^ (3 / 2))

theorem EulerWholeSpaceGaussian.lowCost_nonneg : 0 ≤ lowCost

theorem EulerWholeSpaceGaussian.firstKernel_one_L2_bound (a : EulerSmoothLimit.Space) : √(∫ (y : EulerSmoothLimit.Space), ‖firstKernel 1 a y‖ ^ 2) ≤ lowCost * ‖a‖

theorem EulerWholeSpaceGaussian.average_first_L2_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (hLp : MeasureTheory.MemLp f 2 MeasureTheory.volume) (C₀ C₁ : ℝ) (h₀ : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C₀) (h₁ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ f x‖ ≤ C₁) (a x : EulerSmoothLimit.Space) : ‖average 1 (fun (y : EulerSmoothLimit.Space) => (fderiv ℝ f y) a) x‖ ≤ lowCost * ‖a‖ * (MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal