The profile estimate belongs to the actual unnormalized PDE solution

The weighted construction is exactly division of the genuine solution with physical forcing g f by g. This is an algebraic identity of continuous paths; it does not differentiate g or introduce its extrema into any estimate.

theorem EulerSourceCylinderEquation.coordinates_weight_eq (period : ℝ) [Fact (0 < period)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) : coordinates period S hS T hT Q Q₁ c hc hQ ((EulerContinuousTimeWeight.weight g) f) a₀ = (EulerContinuousTimeWeight.weight g) (EulerSourceCylinderForwardSobolev.normalizedCoordinates period T hT S hS Q Q₁ c hc hQ g hg f a₀)

The normalized coordinate estimate is for this exact raw Duhamel solution.

theorem EulerSourceCylinderEquation.velocity_weight_eq (period : ℝ) [Fact (0 < period)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) : velocity period S hS T hT Q Q₁ c hc hQ ((EulerContinuousTimeWeight.weight g) f) a₀ = (EulerContinuousTimeWeight.weight g) (EulerSourceCylinderForwardSobolev.normalizedVelocity period T hT S hS Q Q₁ c hc hQ g hg f a₀)

The physical reconstruction has the same exact profile identity.

theorem EulerSourceCylinderEquation.normalized_full_velocity_eq (period : ℝ) [Fact (0 < period)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) : (EulerContinuousTimeWeight.normalize g hg) ((EulerLpCylinderPaths.includePath period S hS) (velocity period S hS T hT Q Q₁ c hc hQ ((EulerContinuousTimeWeight.weight g) f) a₀)) = (EulerLpCylinderPaths.includePath period S hS) (EulerSourceCylinderForwardSobolev.normalizedVelocity period T hT S hS Q Q₁ c hc hQ g hg f a₀)

Therefore the proved fixed-radius bound is literally the normalized full-cylinder orbit of the actual physical solution.