Dissipation of the genuine cylinder Laplacian in a variable positive metric.

noncomputable def EulerMetricHeatEnergy.directionalCoefficientOperator (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (a : EulerLiftedGradientSpace.LiftTangent) : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual multiplier by a directional derivative of a smooth metric coefficient.

Equations

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

theorem EulerMetricHeatEnergy.directionalCoefficientOperator_bound (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ‖(directionalCoefficientOperator period K a) f‖ ≤ ↑K.firstBound * ‖a‖ * ‖f‖

The directional coefficient multiplier has the expected first-derivative norm bound.

theorem EulerMetricHeatEnergy.metric_product_hasDerivAt (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (a : EulerLiftedGradientSpace.LiftTangent) (f f' : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hf : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) f) f' 0) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) (K.operator f)) (K.operator f' + (directionalCoefficientOperator period K a) f) 0

Strong translation differentiation of an actual coefficient product.

theorem EulerMetricHeatEnergy.metric_second_derivative_identity (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (a : EulerLiftedGradientSpace.LiftTangent) (f f' f'' : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hf : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) f) f' 0) (hf' : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) f') f'' 0) : inner ℝ (K.operator f) f'' = -inner ℝ (K.operator f') f' - inner ℝ ((directionalCoefficientOperator period K a) f) f'

Exact metric integration by parts for one genuine second translation derivative.

theorem EulerMetricHeatEnergy.metric_cross_young (c D x y : ℝ) (hc : 0 < c) : D * x * y ≤ c ^ 2 / 2 * y ^ 2 + D ^ 2 / (2 * c ^ 2) * x ^ 2

The scalar Young inequality with the precise coercivity constant used in heat energy.

theorem EulerMetricHeatEnergy.metric_second_derivative_bound (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (a : EulerLiftedGradientSpace.LiftTangent) (f f' f'' : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hf : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) f) f' 0) (hf' : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) f') f'' 0) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ ((K.coefficient x) v) v) : inner ℝ (K.operator f) f'' ≤ -(c ^ 2 / 2) * ‖f'‖ ^ 2 + (↑K.firstBound * ‖a‖) ^ 2 / (2 * c ^ 2) * ‖f‖ ^ 2

A positive metric absorbs half of the second-derivative dissipation, leaving an explicit L² error.

theorem EulerMetricHeatEnergy.standardDirection_norm (i : Fin 4) : ‖EulerCylinderSobolev.standardDirection i‖ = 1

Every standard angular or spatial cylinder coordinate vector has norm one.

noncomputable def EulerMetricHeatEnergy.jetLaplacian (period : ℝ) [Fact (0 < period)] {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 2 f) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual cylinder Laplacian assembled from strong second coordinate derivatives.

Equations

• EulerMetricHeatEnergy.jetLaplacian period J = ∑ i : Fin 4, J.word fun (x : Fin 2) => i

theorem EulerMetricHeatEnergy.metric_heat_bound (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 2 f) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ ((K.coefficient x) v) v) : inner ℝ (K.operator f) (jetLaplacian period J) ≤ -(c ^ 2 / 2) * ∑ i : Fin 4, ‖J.word fun (x : Fin 1) => i‖ ^ 2 + 2 * ↑K.firstBound ^ 2 / c ^ 2 * ‖f‖ ^ 2

The L² metric heat estimate for an actual second-order cylinder jet.

noncomputable def EulerMetricHeatEnergy.classicalLaplacian (period : ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3

The sum of the four actual classical second coordinate derivatives on the cylinder.

Equations

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

theorem EulerMetricHeatEnergy.jetLaplacian_ae (period : ℝ) [Fact (0 < period)] {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 2 f) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑f =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : ↑↑(jetLaplacian period J) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] classicalLaplacian period g

The jet Laplacian is represented by the actual classical Laplacian of every smooth representative.

theorem EulerMetricHeatEnergy.classical_metric_heat_bound (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 2 f) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑f =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ ((K.coefficient x) v) v) : ∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ ((K.coefficient x) (g x)) (classicalLaplacian period g x) ∂EulerLiftedGradientSpace.liftMeasure period ≤ -(c ^ 2 / 2) * ∑ i : Fin 4, ‖J.word fun (x : Fin 1) => i‖ ^ 2 + 2 * ↑K.firstBound ^ 2 / c ^ 2 * ‖f‖ ^ 2

The metric heat bound is an actual integral estimate for a smooth cylinder representative.