The pressure estimate is for the actual normalized PDE pressure

All identities are algebraic identities of genuine continuous L² paths. They use no derivative, extremum, or reciprocal bound for the time profile.

theorem EulerSourceNormalResidualBounds.sourceResidual_weight (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) (g : C(K, ℝ)) (f v : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P EulerSmoothLimit.Space))) : sourceResidual P M m cm hcm hm ((EulerContinuousTimeWeight.weight g) f) ((EulerContinuousTimeWeight.weight g) v) = (EulerContinuousTimeWeight.weight g) (sourceResidual P M m cm hcm hm f v)

theorem EulerSourceNormalResidualBounds.sourcePressure_weight (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) (g : C(K, ℝ)) (f v : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P EulerSmoothLimit.Space))) : sourcePressure P M m cm hcm hm ((EulerContinuousTimeWeight.weight g) f) ((EulerContinuousTimeWeight.weight g) v) = (EulerContinuousTimeWeight.weight g) (sourcePressure P M m cm hcm hm f v)

theorem EulerSourceCylinderEquation.pressurePath_eq_sourcePressure (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (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 EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) : pressurePath P S hS T hT Q Q₁ c hc hQ f a₀ M m cm hcm hm = EulerSourceNormalResidualBounds.sourcePressure P M m cm hcm hm ((EulerLpCylinderPaths.includePath P S hS) f) ((EulerLpCylinderPaths.includePath P S hS) (velocity P S hS T hT Q Q₁ c hc hQ f a₀))

The bounded pressure used in the coefficient estimate is exactly the PDE pressure.

noncomputable def EulerSourceCylinderEquation.normalizedPressure (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (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 EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))

The actual pressure path divided by g, written in terms of the normalized physical forcing and the already constructed normalized physical velocity.

Equations

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

theorem EulerSourceCylinderEquation.pressurePath_weight_eq (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (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 EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) : pressurePath P S hS T hT Q Q₁ c hc hQ ((EulerContinuousTimeWeight.weight g) f) a₀ M m cm hcm hm = (EulerContinuousTimeWeight.weight g) (normalizedPressure P S hS T hT Q Q₁ c hc hQ f a₀ M m cm hcm hm g hg)

theorem EulerSourceCylinderEquation.normalized_full_pressure_eq (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (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 EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) : (EulerContinuousTimeWeight.normalize g hg) (pressurePath P S hS T hT Q Q₁ c hc hQ ((EulerContinuousTimeWeight.weight g) f) a₀ M m cm hcm hm) = normalizedPressure P S hS T hT Q Q₁ c hc hQ f a₀ M m cm hcm hm g hg