Gaussian averaging genuinely gains one strong derivative for every cylinder L² datum.

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

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

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

The bounded moment operator used to close the derivative graph.

Equations

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

@[simp]

theorem EulerGaussianCylinderHeat.lineHeatDerivativeOperator_apply (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (v : NNReal) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (lineHeatDerivativeOperator period a v) f = lineHeatDerivative period a v f

theorem EulerGaussianCylinderHeat.mollify_lineOrbit_differentiable (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (n : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : Differentiable ℝ (lineOrbit period a (EulerCylinderMollifier.mollify period n f))

Genuine cylinder mollifications are differentiable along every one-parameter translation orbit.

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

For positive variance the Gaussian average of every L² field has the stated strong derivative.

theorem EulerGaussianCylinderHeat.lineHeat_one_derivative (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) {v : NNReal} (hv : 0 < v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (lineOrbit period a (lineHeat period a v f)) g 0 ∧ ‖g‖ ≤ gaussianAbsMoment 1 / √↑v * ‖f‖

Actual one-derivative smoothing, with both the derivative witness and its parabolic bound.

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

The derivative of the heat average commutes with every cylinder translation.