Source coefficient bounds for the actual pressure path

The normal inverse is constructed from m, and the angular primitive is the actual bounded scalar cylinder operator. The resulting fixed-Hq estimate uses one fixed external radius and adds no shift to its supplied inputs.

Actual normal pressure residuals preserve the fixed-Sobolev mixed-word radius.

noncomputable def EulerLpCylinderRectangular.normalResidualPath (period : ℝ) [Fact (0 < period)] {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (N : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] ℝ))) (M : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] E))) (f v : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))) : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ))

The actual scalar coefficient of the normal residual, as a cylinder L² path.

Equations

• EulerLpCylinderRectangular.normalResidualPath period N M f v = ((EulerLpCylinderRectangular.fullMultiplierMap period) N) (f - 2 • ((EulerLpCylinderRectangular.fullMultiplierMap period) M) v)

theorem EulerLpCylinderRectangular.normalResidualPath_contDiff (period : ℝ) [Fact (0 < period)] {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (N : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] ℝ))) (M : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] E))) (f v : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))) (hN : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath N)) (hM : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath M)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) f) (hv : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) v) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) (normalResidualPath period N M f v)

theorem EulerLpCylinderRectangular.normalResidualPath_block_bound (period : ℝ) [Fact (0 < period)] {K : Type u_1} {E : Type u_2} {ι : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (N : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] ℝ))) (M : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] E))) (f v : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (hN : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath N)) (hM : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath M)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) f) (hv : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) v) (Rc CN CM R Df Dv : ℝ) (hRc : 0 ≤ Rc) (hCN : 0 ≤ CN) (hCM : 0 ≤ CM) (hDf : 0 ≤ Df) (hDv : 0 ≤ Dv) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hbN : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath N) a‖ ≤ CN * EulerGevrey.majorant Rc 0 n) (hbM : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath M) a‖ ≤ CM * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbf : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) f) n 0 ≤ Df * EulerGevrey.majorant R d n) (hbv : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) v) n 0 ≤ Dv * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) (normalResidualPath period N M f v)) n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CN * (Df + 6 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CM * Dv) * EulerGevrey.majorant R d n

Both multiplications and the subtraction preserve exactly the input external radius.

noncomputable def EulerSourceNormalResidualBounds.sourceResidual (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (M : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (f v : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P EulerSmoothLimit.Space))) : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))

Source residual, given by normalResidualPath P (normalFunctional m cm hcm hm) M.field f v.

Equations

• EulerSourceNormalResidualBounds.sourceResidual P M m cm hcm hm f v = EulerLpCylinderRectangular.normalResidualPath P (EulerSourceNormalCoefficient.normalFunctional m cm hcm hm) M.field f v

noncomputable def EulerSourceNormalResidualBounds.sourcePressure (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (M : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (f v : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P EulerSmoothLimit.Space))) : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))

Source pressure, given by pathPrimitive P (sourceResidual P M m cm hcm hm f v).

Equations

• EulerSourceNormalResidualBounds.sourcePressure P M m cm hcm hm f v = (EulerCylinderScalarPrimitive.pathPrimitive P) (EulerSourceNormalResidualBounds.sourceResidual P M m cm hcm hm f v)

theorem EulerSourceNormalResidualBounds.sourceResidual_contDiff (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (M : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (f v : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P EulerSmoothLimit.Space))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) (hv : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) v) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (sourceResidual P M m cm hcm hm f v)

theorem EulerSourceNormalResidualBounds.sourcePressure_contDiff (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (M : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (f v : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P EulerSmoothLimit.Space))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) (hv : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) v) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (sourcePressure P M m cm hcm hm f v)

def EulerSourceNormalResidualBounds.pressureCost (ι : Type u_3) [Fintype ι] (q : ℕ) (Ri Cm CM Df Dv : ℝ) : ℝ

An explicit fixed-order coefficient polynomial for the pressure source.

Equations

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

theorem EulerSourceNormalResidualBounds.sourceResidual_block_bound (P : ℝ) [Fact (0 < P)] {K : Type u_1} {ι : Type u_2} [TopologicalSpace K] [CompactSpace K] [Fintype ι] (M : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (f v : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P EulerSmoothLimit.Space))) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) (hv : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) v) (Rc Cm CM Ri R Df Dv : ℝ) (hRc : 0 ≤ Rc) (hCm : 0 ≤ Cm) (hCM : 0 ≤ CM) (hDf : 0 ≤ Df) (hDv : 0 ≤ Dv) (hRi : 2 * EulerTimeLpGramGevrey.gramCost cm Cm 1 * (Rc + 1) ≤ Ri) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) ≤ R) (hbm : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(m.field t)) x‖ ≤ Cm * EulerGevrey.majorant Rc 0 n) (hbM : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(M.field t)) x‖ ≤ CM * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbf : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) n 0 ≤ Df * EulerGevrey.majorant R d n) (hbv : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) v) n 0 ≤ Dv * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (sourceResidual P M m cm hcm hm f v)) n 0 ≤ pressureCost ι q Ri Cm CM Df Dv * EulerGevrey.majorant R d n

theorem EulerSourceNormalResidualBounds.sourcePressure_block_bound (P : ℝ) [Fact (0 < P)] {K : Type u_1} {ι : Type u_2} [TopologicalSpace K] [CompactSpace K] [Fintype ι] (M : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (f v : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P EulerSmoothLimit.Space))) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) (hv : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) v) (Rc Cm CM Ri R Df Dv : ℝ) (hRc : 0 ≤ Rc) (hCm : 0 ≤ Cm) (hCM : 0 ≤ CM) (hDf : 0 ≤ Df) (hDv : 0 ≤ Dv) (hRi : 2 * EulerTimeLpGramGevrey.gramCost cm Cm 1 * (Rc + 1) ≤ Ri) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) ≤ R) (hbm : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(m.field t)) x‖ ≤ Cm * EulerGevrey.majorant Rc 0 n) (hbM : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(M.field t)) x‖ ≤ CM * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbf : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) n 0 ≤ Df * EulerGevrey.majorant R d n) (hbv : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) v) n 0 ≤ Dv * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (sourcePressure P M m cm hcm hm f v)) n 0 ≤ P * pressureCost ι q Ri Cm CM Df Dv * EulerGevrey.majorant R d n

The actual normalized angular pressure costs only the period, and preserves the supplied fixed-order block, external radius, and shift.