Spatial regularity of the actual source mean operator

All coefficient families here are formed from literal bounded smooth matrix fields and smooth compact cutoffs. Their operator regularity is proved by those constructions and then passed through the genuine fixed mean inverse.

@[instance_reducible]

noncomputable def EulerMeanSourceOperatorRegularity.instMeanSourceOperatorRegularity1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanSourceOperatorRegularity.instMeanSourceOperatorRegularity1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanSourceOperatorRegularity.instMeanSourceOperatorRegularity2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanSourceOperatorRegularity.instMeanSourceOperatorRegularity2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanSourceOperatorRegularity.instMeanSourceOperatorRegularity3 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanSourceOperatorRegularity.instMeanSourceOperatorRegularity3 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanSourceOperatorRegularity.instMeanSourceOperatorRegularity4 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard InnerProductSpace ℝ (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanSourceOperatorRegularity.instMeanSourceOperatorRegularity4 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanSourceOperatorRegularity.instMeanSourceOperatorRegularity5 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard NormedAddCommGroup (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanSourceOperatorRegularity.instMeanSourceOperatorRegularity5 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanSourceOperatorRegularity.instMeanSourceOperatorRegularity6 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard InnerProductSpace ℝ (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanSourceOperatorRegularity.instMeanSourceOperatorRegularity6 T = inferInstance

theorem EulerMeanSourceOperatorRegularity.translatedSourceOperator_contDiff (T : ℝ) (hT : 0 ≤ T) (F F₁ H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (χ : EulerMeanBoundary.Cutoff) (L : ℝ) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanFixedTranslation.translatedMeanOperator T hT a (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) (EulerMeanCoefficients.operatorPath T H.field) (EulerMeanCoefficients.multiplier M0.field) (EulerMeanBoundary.boundaryOperator χ) L

The entire translated source mean operator is genuinely smooth in the spatial shift.

theorem EulerMeanSourceOperatorRegularity.translatedSourcePrimitive_contDiff (T : ℝ) (hT : 0 ≤ T) (F F₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanFixedTranslation.translatedMeanPrimitive T hT a (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field)

The translated primitive in the forcing term is a genuinely smooth operator family.

theorem EulerMeanSourceOperatorRegularity.sourceSolution_translation_contDiff (T : ℝ) (hT : 0 ≤ T) (F F₁ H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (χ : EulerMeanBoundary.Cutoff) (L c : ℝ) (hc : 0 < c) (hcoercive : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), c * ‖v‖ ^ 2 ≤ inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) (EulerMeanCoefficients.operatorPath T H.field) (EulerMeanCoefficients.multiplier M0.field) (EulerMeanBoundary.boundaryOperator χ) L) v) v) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) ((EulerCoerciveProjection.coerciveInverse (EulerMeanFixedSpaceInverse.fixedMeanOperator T hT (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) (EulerMeanCoefficients.operatorPath T H.field) (EulerMeanCoefficients.multiplier M0.field) (EulerMeanBoundary.boundaryOperator χ) L) c hc hcoercive) (-(ContinuousLinearMap.adjoint (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field))) f))

The actual source inverse has a smooth spatial orbit when the given forcing does. The coercivity certificate is supplied by the already proved source boundary estimate.