The source forward estimates apply to the actual packet paths

The input bound below is on the literal forcing divided by g. The weighted Duhamel identities identify the result with the actual unweighted solution, and with its actual time derivative divided by g. No g derivative or profile extremum is introduced.

Actual forward coordinate and time-derivative bounds at one radius

The source propagator bound is used only on the support half-ball. The real physical time derivative, divided by g, obeys the same fixed-Hq external-word radius as the forcing and spends just the solve's one shift.

The bounded time-right-side estimate applies to the actual PDE time derivative divided by g.

theorem EulerSourceCylinderEquation.velocityDerivative_eq_physicalRhs (P : ℝ) [Fact (0 < P)] {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) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) : velocityDerivative P S hS T hT Q Q₁ c hc hQ f a₀ = EulerSourceCylinderTimeBounds.physicalRhs P S hS Q Q₁ c hc hQ f (coordinates P S hS T hT Q Q₁ c hc hQ f a₀)

noncomputable def EulerSourceCylinderEquation.normalizedVelocityDerivative (P : ℝ) [Fact (0 < P)] {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) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))

This is A_t/g, obtained from the actual equation rather than differentiating A/g.

Equations

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

theorem EulerSourceCylinderEquation.velocityDerivative_weight_eq (P : ℝ) [Fact (0 < P)] {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) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) : velocityDerivative P S hS T hT Q Q₁ c hc hQ ((EulerContinuousTimeWeight.weight g) f) a₀ = (EulerContinuousTimeWeight.weight g) (normalizedVelocityDerivative P S hS T hT Q Q₁ c hc hQ f a₀ g hg)

theorem EulerSourceCylinderEquation.normalized_full_velocityDerivative_eq (P : ℝ) [Fact (0 < P)] {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) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) : (EulerContinuousTimeWeight.normalize g hg) ((EulerLpCylinderPaths.includePath P S hS) (velocityDerivative P S hS T hT Q Q₁ c hc hQ ((EulerContinuousTimeWeight.weight g) f) a₀)) = (EulerLpCylinderPaths.includePath P S hS) (normalizedVelocityDerivative P S hS T hT Q Q₁ c hc hQ f a₀ g hg)

@[instance_reducible]

noncomputable def EulerSourceCylinderForwardSobolev.instSourceCylinderDerivativeBounds1 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedRing (U →L[ℝ] U)

Cache the standard NormedRing (U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerSourceCylinderForwardSobolev.instSourceCylinderDerivativeBounds1 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceCylinderForwardSobolev.instSourceCylinderDerivativeBounds2 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedRing (BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] U))

Cache the standard NormedRing (Space →ᵇ U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerSourceCylinderForwardSobolev.instSourceCylinderDerivativeBounds2 = inferInstance

theorem EulerSourceCylinderForwardSobolev.normalizedCoordinates_contDiff (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (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 P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hSc : IsCompact S) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) (normalizedCoordinates P T hT S hS Q Q₁ c hc hQ g hg f a₀))

theorem EulerSourceCylinderForwardSobolev.coordinate_forward_block_bound (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (T : ℝ) (hT : 0 ≤ T) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (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 P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hSc : IsCompact S) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hg₀ : g ⟨0, ⋯⟩ = 1) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (C A D Rc C₀ C₁ Ri R : ℝ) (hC : 0 ≤ C) (hA : 0 ≤ A) (hD : 0 ≤ D) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hbQ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hRforcing : EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) ≤ R) (hR : 2 * EulerLinearDuhamel.forwardSobolevCost ι q T C A (forcingCost ι q Ri C₀ * D) (18 * Ri * C₀ * C₁) (4 * Ri) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) + 1) ≤ R) (hH3 : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ∀ (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖((EulerLinearFundamentalExistence.fundamentalPath T hT (EulerSourceForwardCoefficient.sourceGenerator Q Q₁ c hc hQ)).forward t) x ∘SL ((EulerLinearFundamentalExistence.fundamentalPath T hT (EulerSourceForwardCoefficient.sourceGenerator Q Q₁ c hc hQ)).backward s) x‖ ≤ C * g t / g s) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) n 0 ≤ D * EulerGevrey.majorant R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) n 0 ≤ A * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) (normalizedCoordinates P T hT S hS Q Q₁ c hc hQ g hg f a₀))) n 0 ≤ EulerGevrey.majorant R (d + 1) n

theorem EulerSourceCylinderForwardSobolev.derivative_forward_block_bound (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (T : ℝ) (hT : 0 ≤ T) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (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 P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hSc : IsCompact S) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hg₀ : g ⟨0, ⋯⟩ = 1) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (C A D Rc C₀ C₁ Ri R : ℝ) (hC : 0 ≤ C) (hA : 0 ≤ A) (hD : 0 ≤ D) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hbQ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hRforcing : EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) ≤ R) (hR : 2 * EulerLinearDuhamel.forwardSobolevCost ι q T C A (forcingCost ι q Ri C₀ * D) (18 * Ri * C₀ * C₁) (4 * Ri) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) + 1) ≤ R) (hH3 : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ∀ (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖((EulerLinearFundamentalExistence.fundamentalPath T hT (EulerSourceForwardCoefficient.sourceGenerator Q Q₁ c hc hQ)).forward t) x ∘SL ((EulerLinearFundamentalExistence.fundamentalPath T hT (EulerSourceForwardCoefficient.sourceGenerator Q Q₁ c hc hQ)).backward s) x‖ ≤ C * g t / g s) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) n 0 ≤ D * EulerGevrey.majorant R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) n 0 ≤ A * EulerGevrey.majorant R d n) (hRone : 1 ≤ R) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) (EulerSourceCylinderEquation.normalizedVelocityDerivative P S hS T hT Q Q₁ c hc hQ f a₀ g hg))) n 0 ≤ EulerSourceCylinderTimeBounds.physicalCost ι q Ri C₀ C₁ D 1 * EulerGevrey.majorant R (d + 1) n

The bounded field is the actual time derivative divided by g, by normalized_full_velocityDerivative_eq. No profile derivative appears.

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Forcing.instTransversePacketForwardBounds1 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedRing (U →L[ℝ] U)

Cache the standard NormedRing (U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Forcing.instTransversePacketForwardBounds1 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Forcing.instTransversePacketForwardBounds2 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedRing (BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] U))

Cache the standard NormedRing (Space →ᵇ U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Forcing.instTransversePacketForwardBounds2 = inferInstance

theorem EulerTransversePacketProvider.Forcing.source_velocity_normalized_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (g : C(↑(Set.Icc 0 D.T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) {ι : Type u_2} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : D.support ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hg0 : g ⟨0, ⋯⟩ = 1) (C A Cf Rc C₀ C₁ Ri R : ℝ) (hC : 0 ≤ C) (hA : 0 ≤ A) (hCf : 0 ≤ Cf) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hRi : 2 * EulerTimeLpGramGevrey.gramCost D.frameLower C₀ 1 * (Rc + 1) ≤ Ri) (hbF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbF₁ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hRforcing : EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) ≤ R) (hR : 2 * EulerLinearDuhamel.forwardSobolevCost ι q D.T C A (EulerSourceCylinderForwardSobolev.forcingCost ι q Ri C₀ * Cf) (18 * Ri * C₀ * C₁) (4 * Ri) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) + 1) ≤ R) (hH3 : ∀ (t s : ↑(Set.Icc 0 D.T)), s ≤ t → ∀ (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖((EulerLinearFundamentalExistence.fundamentalPath D.T ⋯ (EulerSourceForwardCoefficient.sourceGenerator D.frame D.frameDerivative D.frameLower ⋯ ⋯)).forward t) x ∘SL ((EulerLinearFundamentalExistence.fundamentalPath D.T ⋯ (EulerSourceForwardCoefficient.sourceGenerator D.frame D.frameDerivative D.frameLower ⋯ ⋯)).backward s) x‖ ≤ C * g t / g s) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) ((EulerLpCylinderPaths.includePath P D.support ⋯) G.path))) n 0 ≤ Cf * EulerGevrey.majorant R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant R d n) (hRframe : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) ((EulerLpCylinderPaths.includePath P D.support ⋯) (G.velocityPath I)))) n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C₀ * EulerGevrey.majorant R (d + 1) n

The literal forward packet velocity divided by g, at the input radius.

theorem EulerTransversePacketProvider.Forcing.source_derivative_normalized_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (g : C(↑(Set.Icc 0 D.T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) {ι : Type u_2} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : D.support ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hg0 : g ⟨0, ⋯⟩ = 1) (C A Cf Rc C₀ C₁ Ri R : ℝ) (hC : 0 ≤ C) (hA : 0 ≤ A) (hCf : 0 ≤ Cf) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hRi : 2 * EulerTimeLpGramGevrey.gramCost D.frameLower C₀ 1 * (Rc + 1) ≤ Ri) (hbF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbF₁ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hRforcing : EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) ≤ R) (hR : 2 * EulerLinearDuhamel.forwardSobolevCost ι q D.T C A (EulerSourceCylinderForwardSobolev.forcingCost ι q Ri C₀ * Cf) (18 * Ri * C₀ * C₁) (4 * Ri) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) + 1) ≤ R) (hH3 : ∀ (t s : ↑(Set.Icc 0 D.T)), s ≤ t → ∀ (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖((EulerLinearFundamentalExistence.fundamentalPath D.T ⋯ (EulerSourceForwardCoefficient.sourceGenerator D.frame D.frameDerivative D.frameLower ⋯ ⋯)).forward t) x ∘SL ((EulerLinearFundamentalExistence.fundamentalPath D.T ⋯ (EulerSourceForwardCoefficient.sourceGenerator D.frame D.frameDerivative D.frameLower ⋯ ⋯)).backward s) x‖ ≤ C * g t / g s) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) ((EulerLpCylinderPaths.includePath P D.support ⋯) G.path))) n 0 ≤ Cf * EulerGevrey.majorant R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant R d n) (hRone : 1 ≤ R) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) ((EulerLpCylinderPaths.includePath P D.support ⋯) (G.derivativePath I)))) n 0 ≤ EulerSourceCylinderTimeBounds.physicalCost ι q Ri C₀ C₁ Cf 1 * EulerGevrey.majorant R (d + 1) n

This is A_t/g for the actual raw solution, not a derivative of A/g.