A genuine one-derivative Gaussian smoothing estimate for cylinder L² fields.

Gaussian heat averaging in the genuine cylinder L² translation representation.

noncomputable def EulerGaussianCylinderHeat.lineOrbit (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (x : ℝ) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual one-parameter cylinder translation orbit.

Equations

• EulerGaussianCylinderHeat.lineOrbit period a f x = (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a x)) f

theorem EulerGaussianCylinderHeat.lineOrbit_continuous (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : Continuous (lineOrbit period a f)

@[simp]

theorem EulerGaussianCylinderHeat.lineOrbit_norm (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (x : ℝ) : ‖lineOrbit period a f x‖ = ‖f‖

@[simp]

theorem EulerGaussianCylinderHeat.lineOrbit_zero (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : lineOrbit period a f 0 = f

theorem EulerGaussianCylinderHeat.lineOrbit_integrable (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable (lineOrbit period a f) μ

noncomputable def EulerGaussianCylinderHeat.lineHeat (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

Gaussian averaging with variance v along a cylinder direction.

Equations

• EulerGaussianCylinderHeat.lineHeat period a v f = ∫ (x : ℝ), EulerGaussianCylinderHeat.lineOrbit period a f x ∂EulerGaussianCylinderHeat.gaussianMeasure 0 v

@[simp]

theorem EulerGaussianCylinderHeat.lineHeat_zero (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : lineHeat period a 0 f = f

theorem EulerGaussianCylinderHeat.lineHeat_norm_le (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ‖lineHeat period a v f‖ ≤ ‖f‖

Gaussian averaging is contractive, including variance zero.

theorem EulerGaussianCylinderHeat.lineHeat_add (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) : lineHeat period a v (f + g) = lineHeat period a v f + lineHeat period a v g

theorem EulerGaussianCylinderHeat.lineHeat_smul (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (c : ℝ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : lineHeat period a v (c • f) = c • lineHeat period a v f

noncomputable def EulerGaussianCylinderHeat.lineHeatOperator (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual bounded Gaussian averaging operator.

Equations

• EulerGaussianCylinderHeat.lineHeatOperator period a v = { toFun := EulerGaussianCylinderHeat.lineHeat period a v, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem EulerGaussianCylinderHeat.lineHeatOperator_apply (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (lineHeatOperator period a v) f = lineHeat period a v f

theorem EulerGaussianCylinderHeat.lineHeatOperator_norm_le (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) : ‖lineHeatOperator period a v‖ ≤ 1

theorem EulerGaussianCylinderHeat.lineHeat_translation (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (b : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (EulerLiftedGradientSpace.translation period b) (lineHeat period a v f) = lineHeat period a v ((EulerLiftedGradientSpace.translation period b) f)

The heat average commutes with every cylinder translation.

theorem EulerGaussianCylinderHeat.jointOrbit_integrable (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (μ ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => lineOrbit period a f (p.1 + p.2)) (μ.prod ν)

A joint translation orbit is integrable against the product of two finite measures.

theorem EulerGaussianCylinderHeat.lineHeat_semigroup (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v w : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : lineHeat period a v (lineHeat period a w f) = lineHeat period a (v + w) f

Addition of Gaussian variances gives the semigroup law on actual cylinder L² fields.

theorem EulerGaussianCylinderHeat.lineHeat_commute (period : ℝ) [Fact (0 < period)] (a b : EulerLiftedGradientSpace.LiftTangent) (v w : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : lineHeat period a v (lineHeat period b w f) = lineHeat period b w (lineHeat period a v f)

Different coordinate heat averages commute, since all cylinder translations commute.

theorem EulerGaussianCylinderHeat.lineHeat_eq_standardGaussian (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : lineHeat period a v f = ∫ (x : ℝ), lineOrbit period a f (√↑v * x) ∂gaussianMeasure 0 1

Fixed standard-Gaussian representation of every nonnegative-variance average.

theorem EulerGaussianCylinderHeat.lineHeat_continuous (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : Continuous fun (v : NNReal) => lineHeat period a v f

The Gaussian operators are strongly continuous in their nonnegative variance parameter.

theorem EulerGaussianCylinderHeat.kernelOrbit_integrable (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (k : ℝ → ℝ) (hk : MeasureTheory.Integrable k MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : ℝ) => k x • lineOrbit period a f x) MeasureTheory.volume

Multiplying the isometric orbit by an L¹ scalar kernel gives a Bochner integrable field.

theorem EulerGaussianCylinderHeat.gaussianPDF_hasDerivAt (v : NNReal) (x : ℝ) : HasDerivAt (gaussianDensity 0 v) (-(x / ↑v) * gaussianDensity 0 v x) x

The actual derivative of the real Gaussian density.

theorem EulerGaussianCylinderHeat.gaussianMomentKernel_integrable (v : NNReal) : MeasureTheory.Integrable (fun (x : ℝ) => x / ↑v * gaussianDensity 0 v x) MeasureTheory.volume

The Gaussian first-moment kernel is integrable against Lebesgue measure.

noncomputable def EulerGaussianCylinderHeat.gaussianAbsMoment (v : NNReal) : ℝ

The first absolute moment of a centered Gaussian.

Equations

• EulerGaussianCylinderHeat.gaussianAbsMoment v = ∫ (x : ℝ), |x| ∂EulerGaussianCylinderHeat.gaussianMeasure 0 v

theorem EulerGaussianCylinderHeat.gaussianAbsMoment_nonneg (v : NNReal) : 0 ≤ gaussianAbsMoment v

theorem EulerGaussianCylinderHeat.gaussianId_integrable (v : NNReal) : MeasureTheory.Integrable (fun (x : ℝ) => x) (gaussianMeasure 0 v)

theorem EulerGaussianCylinderHeat.gaussianAbsMoment_scale (v : NNReal) : gaussianAbsMoment v = √↑v * gaussianAbsMoment 1

Absolute Gaussian moments scale by the standard deviation.

theorem EulerGaussianCylinderHeat.gaussianMomentOrbit_integrable (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : MeasureTheory.Integrable (fun (x : ℝ) => x • lineOrbit period a f x) (gaussianMeasure 0 v)

noncomputable def EulerGaussianCylinderHeat.lineHeatDerivative (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The bounded candidate generator after Gaussian smoothing.

Equations

• EulerGaussianCylinderHeat.lineHeatDerivative period a v f = (↑v)⁻¹ • ∫ (x : ℝ), x • EulerGaussianCylinderHeat.lineOrbit period a f x ∂EulerGaussianCylinderHeat.gaussianMeasure 0 v

theorem EulerGaussianCylinderHeat.lineHeatDerivative_norm_le (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ‖lineHeatDerivative period a v f‖ ≤ (↑v)⁻¹ * gaussianAbsMoment v * ‖f‖

theorem EulerGaussianCylinderHeat.lineHeatDerivative_smoothing_bound (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) {v : NNReal} (hv : 0 < v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ‖lineHeatDerivative period a v f‖ ≤ gaussianAbsMoment 1 / √↑v * ‖f‖

The true parabolic one-derivative bound, with inverse square root of variance.

theorem EulerGaussianCylinderHeat.lineHeat_strongDerivative (period : ℝ) [Fact (0 < period)] (a b : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hD : HasDerivAt (lineOrbit period b f) g 0) : HasDerivAt (lineOrbit period b (lineHeat period a v f)) (lineHeat period a v g) 0

Strong derivatives commute with Gaussian averaging.

theorem EulerGaussianCylinderHeat.lineHeat_derivative_identity (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) {v : NNReal} (hv : v ≠ 0) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hD : HasDerivAt (lineOrbit period a f) g 0) : lineHeat period a v g = lineHeatDerivative period a v f

Gaussian integration by parts identifies the averaged strong derivative with the bounded moment operator.

Real exponential-moment identities complement the Gaussian averaging API.

theorem NavierStokesAndEuler.ExponentialMoments.hasDerivAt_integral {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ∈ interior {s : ℝ | MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X ω)) μ}) (n : ℕ) : HasDerivAt (fun (s : ℝ) => ∫ (ω : Ω), X ω ^ n * Real.exp (s * X ω) ∂μ) (∫ (ω : Ω), X ω ^ (n + 1) * Real.exp (t * X ω) ∂μ) t

Differentiating a real exponential moment raises its power by one.

theorem NavierStokesAndEuler.ExponentialMoments.analyticAt_integral {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ∈ interior {s : ℝ | MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X ω)) μ}) (n : ℕ) : AnalyticAt ℝ (fun (s : ℝ) => ∫ (ω : Ω), X ω ^ n * Real.exp (s * X ω) ∂μ) t

Real exponential moments are analytic inside their integrability interval.