Canonical smooth pressure reconstruction for the generic finite-solution assembly.

noncomputable def EulerCorrectionAssembly.FiniteFamily.pointPressure (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.Vector3

Bounded evaluation of the actual finite pressure fixes a canonical common pressure representative.

Equations

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

theorem EulerCorrectionAssembly.FiniteFamily.pointPressure_ae (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (t : ↑(Set.Icc 0 T)) : ↑↑((commonPressure period F) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] pointPressure period F t

The canonical pressure represents the actual common signed L² pressure.

theorem EulerCorrectionAssembly.FiniteFamily.pointPressure_joint_continuous (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) : Continuous (Function.uncurry (pointPressure period F))

The canonical pressure is jointly continuous in time and the cylinder point.

theorem EulerCorrectionAssembly.FiniteFamily.pointPressure_smooth (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (pointPressure period F t) x)

Proved pressure coherence supplies spatial smoothness of the canonical pressure representative.

noncomputable def EulerCorrectionAssembly.FiniteFamily.graphPressure (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (k : ℝ) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.Vector3

The genuine signed pressure-gradient vector field on the oscillatory physical graph.

Equations

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

theorem EulerCorrectionAssembly.FiniteFamily.graphPressure_joint_continuous (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (k : ℝ) : Continuous (Function.uncurry (graphPressure period F k))

The actual graph pressure-gradient field is jointly continuous.

theorem EulerCorrectionAssembly.FiniteFamily.graphPressure_has_potential (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 T)) : ∃ (q : EulerLiftedGradientSpace.Vector3 → ℝ), ContDiff ℝ (↑⊤) q ∧ ∀ (x : EulerLiftedGradientSpace.Vector3), gradient q x = graphPressure period F k t x

The actual common pressure has a genuine smooth scalar potential on each reciprocal-frequency graph.

noncomputable def EulerCorrectionAssembly.FiniteFamily.normalizedGraphPotential (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (k : ℝ) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : ℝ

The actual graph pressure reconstructed by a canonical radial integral based at the origin.

Equations

• EulerCorrectionAssembly.FiniteFamily.normalizedGraphPotential period F k t x = EulerCanonicalGraphPotential.radialPotential (EulerCorrectionAssembly.FiniteFamily.graphPressure period F k t) x

theorem EulerCorrectionAssembly.FiniteFamily.normalizedGraphPotential_zero (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (k : ℝ) (t : ↑(Set.Icc 0 T)) : normalizedGraphPotential period F k t 0 = 0

The reconstructed scalar pressure has zero value at the origin at every time.

theorem EulerCorrectionAssembly.FiniteFamily.normalizedGraphPotential_joint_continuous (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (k : ℝ) : Continuous (Function.uncurry (normalizedGraphPotential period F k))

The normalized scalar pressure is jointly continuous, including both endpoint time slices.

theorem EulerCorrectionAssembly.FiniteFamily.normalizedGraphPotential_smooth (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (normalizedGraphPotential period F k t)

The normalized scalar pressure is spatially smooth at every time.

theorem EulerCorrectionAssembly.FiniteFamily.normalizedGraphPotential_gradient (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : gradient (normalizedGraphPotential period F k t) x = A.κ • pointPressure period F t (EulerGraphPressurePotential.cylinderGraph period k A.direction x)

The canonical scalar pressure has the actual signed graph pressure as its gradient.