LeanPool.NavierStokesAndEuler.Euler.GaussianHeatTotal

The genuine four-coordinate cylinder heat semigroup and simultaneous derivative gain.

def EulerGaussianCylinderHeat.heatList (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

↥(EulerLiftedGradientSpace.LiftL2 period)

A finite product of commuting directional Gaussian averages.

Equations

EulerGaussianCylinderHeat.heatList period [] v f = f
EulerGaussianCylinderHeat.heatList period (a :: tail) v f = EulerGaussianCylinderHeat.lineHeat period a v (EulerGaussianCylinderHeat.heatList period tail v f)

Instances For

source

theorem EulerGaussianCylinderHeat.heatList_norm_le (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

‖heatList period directions v f‖ ≤ ‖f‖

source

theorem EulerGaussianCylinderHeat.heatList_add (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

heatList period directions v (f + g) = heatList period directions v f + heatList period directions v g

source

theorem EulerGaussianCylinderHeat.heatList_smul (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (c : ℝ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

heatList period directions v (c • f) = c • heatList period directions v f

source

noncomputable def EulerGaussianCylinderHeat.heatListOperator (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (v : NNReal) :

↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Heat list operator, constructed using LinearMap.mkContinuous.

Equations

EulerGaussianCylinderHeat.heatListOperator period directions v = { toFun := EulerGaussianCylinderHeat.heatList period directions v, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

Instances For

source

@[simp]

theorem EulerGaussianCylinderHeat.heatListOperator_apply (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

(heatListOperator period directions v) f = heatList period directions v f

source

theorem EulerGaussianCylinderHeat.heatList_translation (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (b : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

(EulerLiftedGradientSpace.translation period b) (heatList period directions v f) = heatList period directions v ((EulerLiftedGradientSpace.translation period b) f)

source

theorem EulerGaussianCylinderHeat.heatList_lineHeat_commute (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (a : EulerLiftedGradientSpace.LiftTangent) (v w : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

heatList period directions v (lineHeat period a w f) = lineHeat period a w (heatList period directions v f)

Every finite heat product commutes with every directional average.

source

@[simp]

theorem EulerGaussianCylinderHeat.heatList_zero (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

heatList period directions 0 f = f

source

theorem EulerGaussianCylinderHeat.heatList_semigroup (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (v w : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

heatList period directions v (heatList period directions w f) = heatList period directions (v + w) f

The finite product is itself a semigroup with additive variance.

source

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

dist (lineHeat period a v f) (lineHeat period a v g) ≤ dist f g

A Lipschitz estimate for the Gaussian operator in its input field.

source

theorem EulerGaussianCylinderHeat.lineHeat_joint_continuous (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) :

Continuous fun (p : NNReal × ↥(EulerLiftedGradientSpace.LiftL2 period)) => lineHeat period a p.1 p.2

Joint continuity follows from contraction in the field and strong continuity in variance.

source

theorem EulerGaussianCylinderHeat.heatList_continuous (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

Continuous fun (v : NNReal) => heatList period directions v f

source

theorem EulerGaussianCylinderHeat.heatList_one_derivative (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (a : EulerLiftedGradientSpace.LiftTangent) (ha : a ∈ directions) {v : NNReal} (hv : 0 < v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (lineOrbit period a (heatList period directions v f)) g 0 ∧ ‖g‖ ≤ gaussianAbsMoment 1 / √↑v * ‖f‖

A finite heat product gains a derivative in each direction included in the product.

source

noncomputable def EulerGaussianCylinderHeat.cylinderDirections :

List EulerLiftedGradientSpace.LiftTangent

The four actual commuting standard coordinate directions on R³×T.

Equations

EulerGaussianCylinderHeat.cylinderDirections = List.ofFn EulerCylinderSobolev.standardDirection

Instances For

source

noncomputable def EulerGaussianCylinderHeat.cylinderHeat (period : ℝ) [Fact (0 < period)] (v : NNReal) :

↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ ] ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual cylinder heat semigroup, parameterized by Gaussian variance.

Equations

EulerGaussianCylinderHeat.cylinderHeat period v = EulerGaussianCylinderHeat.heatListOperator period EulerGaussianCylinderHeat.cylinderDirections v

Instances For

source

theorem EulerGaussianCylinderHeat.cylinderHeat_norm_le (period : ℝ) [Fact (0 < period)] (v : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

‖(cylinderHeat period v) f‖ ≤ ‖f‖

source

@[simp]

theorem EulerGaussianCylinderHeat.cylinderHeat_zero (period : ℝ) [Fact (0 < period)] (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

(cylinderHeat period 0) f = f

source

theorem EulerGaussianCylinderHeat.cylinderHeat_semigroup (period : ℝ) [Fact (0 < period)] (v w : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

(cylinderHeat period v) ((cylinderHeat period w) f) = (cylinderHeat period (v + w)) f

source

theorem EulerGaussianCylinderHeat.cylinderHeat_continuous (period : ℝ) [Fact (0 < period)] (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

Continuous fun (v : NNReal) => (cylinderHeat period v) f

source

theorem EulerGaussianCylinderHeat.cylinderHeat_translation (period : ℝ) [Fact (0 < period)] (v : NNReal) (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) :

(cylinderHeat period v) ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) ((cylinderHeat period v) f)

source

theorem EulerGaussianCylinderHeat.cylinderHeat_one_derivative (period : ℝ) [Fact (0 < period)] {v : NNReal} (hv : 0 < v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (i : Fin 4) :

∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (lineOrbit period (EulerCylinderSobolev.standardDirection i) ((cylinderHeat period v) f)) g 0 ∧ ‖g‖ ≤ gaussianAbsMoment 1 / √↑v * ‖f‖

The actual heat average gains all four first derivatives with a uniform parabolic bound.