Same-radius bounds for the actual forward time right side

The coordinate and physical right sides are the literal bounded coefficient expressions in (12) and its physical reconstruction. They preserve the input external radius and shift. Scalar time weights commute with these expressions; in particular no derivative of the positive profile is used.

noncomputable def EulerSourceCylinderTimeBounds.coordinateRhs (P : ℝ) [Fact (0 < P)] {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(K, ↥(EulerLpCylinderPaths.Supported P E S hS))) (a : C(K, ↥(EulerLpCylinderPaths.Supported P U S hS))) : C(K, ↥(EulerLpCylinderPaths.Supported P U S hS))

Coordinate rhs, given by supportedMultiplierMap P S hS (sourceGenerator Q Q₁ c hc hQ) a + projectedForcing P S hS Q c hc hQ f.

Equations

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

noncomputable def EulerSourceCylinderTimeBounds.physicalRhs (P : ℝ) [Fact (0 < P)] {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(K, ↥(EulerLpCylinderPaths.Supported P E S hS))) (a : C(K, ↥(EulerLpCylinderPaths.Supported P U S hS))) : C(K, ↥(EulerLpCylinderPaths.Supported P E S hS))

Physical rhs, given by supportedMultiplierMap P S hS Q₁.field a + supportedMultiplierMap P S hS Q.field (coordinateRhs P S hS Q Q₁ c hc hQ f a).

Equations

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

theorem EulerSourceCylinderTimeBounds.coordinateRhs_contDiff (P : ℝ) [Fact (0 < P)] {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(K, ↥(EulerLpCylinderPaths.Supported P E S hS))) (a : C(K, ↥(EulerLpCylinderPaths.Supported P U S hS))) (hf : ContDiff ℝ ↑⊤ fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha : ContDiff ℝ ↑⊤ fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) a)) : ContDiff ℝ ↑⊤ fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) (coordinateRhs P S hS Q Q₁ c hc hQ f a))

theorem EulerSourceCylinderTimeBounds.physicalRhs_contDiff (P : ℝ) [Fact (0 < P)] {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(K, ↥(EulerLpCylinderPaths.Supported P E S hS))) (a : C(K, ↥(EulerLpCylinderPaths.Supported P U S hS))) (hf : ContDiff ℝ ↑⊤ fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha : ContDiff ℝ ↑⊤ fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) a)) : ContDiff ℝ ↑⊤ fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) (physicalRhs P S hS Q Q₁ c hc hQ f a))

def EulerSourceCylinderTimeBounds.coordinateCost (ι : Type u_5) [Fintype ι] (q : ℕ) (Ri C₀ C₁ Df Da : ℝ) : ℝ

Coordinate cost, given by 3*sobolevCoefficientAmplitude ι q (4*Ri) (18*Ri*C₀*C₁)*Da + 3*sobolevCoefficientAmplitude ι q (4*Ri) (3*Ri*C₀)*Df.

Equations

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

def EulerSourceCylinderTimeBounds.physicalCost (ι : Type u_5) [Fintype ι] (q : ℕ) (Ri C₀ C₁ Df Da : ℝ) : ℝ

Physical cost, given by 3*sobolevCoefficientAmplitude ι q (4*Ri) C₁*Da + 3*sobolevCoefficientAmplitude ι q (4*Ri) C₀*coordinateCost ι q Ri C₀ C₁ Df Da.

Equations

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

theorem EulerSourceCylinderTimeBounds.coordinateRhs_block_bound (P : ℝ) [Fact (0 < P)] {K : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(K, ↥(EulerLpCylinderPaths.Supported P E S hS))) (a : C(K, ↥(EulerLpCylinderPaths.Supported P U S hS))) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (hf : ContDiff ℝ ↑⊤ fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha : ContDiff ℝ ↑⊤ fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) a)) (Rc C₀ C₁ Ri R Df Da : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hDf : 0 ≤ Df) (hDa : 0 ≤ Da) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) ≤ R) (hbQ : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbf : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) f)) n 0 ≤ Df * EulerGevrey.majorant R d n) (hba : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) a)) n 0 ≤ Da * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) (coordinateRhs P S hS Q Q₁ c hc hQ f a))) n 0 ≤ coordinateCost ι q Ri C₀ C₁ Df Da * EulerGevrey.majorant R d n

theorem EulerSourceCylinderTimeBounds.physicalRhs_block_bound (P : ℝ) [Fact (0 < P)] {K : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(K, ↥(EulerLpCylinderPaths.Supported P E S hS))) (a : C(K, ↥(EulerLpCylinderPaths.Supported P U S hS))) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (hf : ContDiff ℝ ↑⊤ fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha : ContDiff ℝ ↑⊤ fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) a)) (Rc C₀ C₁ Ri R Df Da : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hDf : 0 ≤ Df) (hDa : 0 ≤ Da) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) ≤ R) (hbQ : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbf : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) f)) n 0 ≤ Df * EulerGevrey.majorant R d n) (hba : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) a)) n 0 ≤ Da * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerLpCylinderPaths.includePath P S hS) (physicalRhs P S hS Q Q₁ c hc hQ f a))) n 0 ≤ physicalCost ι q Ri C₀ C₁ Df Da * EulerGevrey.majorant R d n

theorem EulerSourceCylinderTimeBounds.coordinateRhs_weight (P : ℝ) [Fact (0 < P)] {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(K, ↥(EulerLpCylinderPaths.Supported P E S hS))) (a : C(K, ↥(EulerLpCylinderPaths.Supported P U S hS))) (g : C(K, ℝ)) : coordinateRhs P S hS Q Q₁ c hc hQ ((EulerContinuousTimeWeight.weight g) f) ((EulerContinuousTimeWeight.weight g) a) = (EulerContinuousTimeWeight.weight g) (coordinateRhs P S hS Q Q₁ c hc hQ f a)

theorem EulerSourceCylinderTimeBounds.physicalRhs_weight (P : ℝ) [Fact (0 < P)] {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(K, ↥(EulerLpCylinderPaths.Supported P E S hS))) (a : C(K, ↥(EulerLpCylinderPaths.Supported P U S hS))) (g : C(K, ℝ)) : physicalRhs P S hS Q Q₁ c hc hQ ((EulerContinuousTimeWeight.weight g) f) ((EulerContinuousTimeWeight.weight g) a) = (EulerContinuousTimeWeight.weight g) (physicalRhs P S hS Q Q₁ c hc hQ f a)