A canonical, jointly continuous representative of the constructed common signed pressure.

Constructed compatible inviscid corrections at every finite Sobolev order.

noncomputable def EulerAllOrderCorrectionFamily.solution (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))

The actual finite-order correction chosen from the proved global nonlinear construction.

Equations

• EulerAllOrderCorrectionFamily.solution period hT A B q hq = Classical.choose ⋯

theorem EulerAllOrderCorrectionFamily.solution_initial (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : (solution period hT A B q hq) ⟨0, ⋯⟩ = 0

The constructed finite-order correction has zero initial trace.

theorem EulerAllOrderCorrectionFamily.solution_divergence (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((solution period hT A B q hq) t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction

The constructed finite-order correction satisfies the actual lifted divergence constraint.

theorem EulerAllOrderCorrectionFamily.solution_energy (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (P : ℕ) (hPN : P ≤ q - 4) (hP : P + 6 ≤ q + 1) (t : ↑(Set.Icc 0 T)) : EulerGevreyMetricEstimate.energyNorm period P hP (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period B.metric) t) ((solution period hT A B q hq) t) ≤ B.delta / 2

Every retained cutoff of the constructed correction has the proved common energy bound.

theorem EulerAllOrderCorrectionFamily.solution_hasDerivAt (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T ⋯ (solution period hT A B q hq) r)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq).apply ⟨t, ⋯⟩ ((solution period hT A B q hq) ⟨t, ⋯⟩))) t

The constructed correction satisfies the actual nonlinear projected-pressure equation at every interior time.

theorem EulerAllOrderCorrectionFamily.solution_compatible (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period (q + 1))) (solution period hT A B (q + 1) ⋯) = solution period hT A B q hq

The separately constructed solutions are genuinely the same correction after restriction; uniqueness is proved from their actual equations.

theorem EulerAllOrderCorrectionFamily.solution_value_succ (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((solution period hT A B (q + 1) ⋯) t) = EulerCylinderSobolevSpace.value period ((solution period hT A B q hq) t)

Adjacent finite-order solutions have exactly the same underlying L² field.

The actual nonlinear source and signed coercive pressure agree across the constructed Sobolev solutions.

noncomputable def EulerAllOrderPressureCoherence.rawSourcePath (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

The actual continuous nonlinear raw source at a finite Sobolev order.

Equations

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

noncomputable def EulerAllOrderPressureCoherence.signedPressurePath (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

The actual continuous signed coercive pressure at a finite Sobolev order.

Equations

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

theorem EulerAllOrderPressureCoherence.rawSourcePath_truncate (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : (EulerCylinderSobolevSpace.truncateOperator period q) ((rawSourcePath period hT A B (q + 1) ⋯) t) = (rawSourcePath period hT A B q hq) t

The genuine raw sources of the constructed solutions restrict exactly across adjacent orders.

theorem EulerAllOrderPressureCoherence.rawSourcePath_value_succ (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((rawSourcePath period hT A B (q + 1) ⋯) t) = EulerCylinderSobolevSpace.value period ((rawSourcePath period hT A B q hq) t)

Adjacent genuine raw sources represent the same actual L² field.

theorem EulerAllOrderPressureCoherence.signedPressurePath_value_succ (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((signedPressurePath period hT A B (q + 1) ⋯) t) = EulerCylinderSobolevSpace.value period ((signedPressurePath period hT A B q hq) t)

The actual signed coercive pressures represent the same L² field at adjacent Sobolev orders.

theorem EulerAllOrderPressureCoherence.signedPressurePath_value_base (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((signedPressurePath period hT A B q hq) t) = EulerCylinderSobolevSpace.value period ((signedPressurePath period hT A B 6 ⋯) t)

Every finite-order signed pressure represents the same actual base pressure.

noncomputable def EulerAllOrderPressureCoherence.commonPressure (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))

The common actual signed pressure is a continuous L² path.

Equations

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

theorem EulerAllOrderPressureCoherence.signedPressurePath_value_common (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((signedPressurePath period hT A B q hq) t) = (commonPressure period hT A B) t

Every finite-order pressure realizes the common pressure field.

theorem EulerAllOrderPressureCoherence.commonPressure_gradient (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (t : ↑(Set.Icc 0 T)) : (commonPressure period hT A B) t ∈ EulerLiftedGradientSpace.gradientSpace period A.κ A.direction

The common actual correction pressure belongs to the closed lifted gradient subspace.

Smooth actual pressure and graph potentials of the constructed common inviscid correction.

A common actual lifted inviscid correction with genuine jets of every order and smooth spatial representatives.

theorem EulerAllOrderLiftedCorrection.solution_value_base (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((EulerAllOrderCorrectionFamily.solution period hT A B q hq) t) = EulerCylinderSobolevSpace.value period ((EulerAllOrderCorrectionFamily.solution period hT A B 6 ⋯) t)

The independently constructed finite-order corrections all represent the same actual L² field.

noncomputable def EulerAllOrderLiftedCorrection.commonPath (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))

The common continuous L² path constructed from the genuine finite-order nonlinear solves.

Equations

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

theorem EulerAllOrderLiftedCorrection.solution_value_common (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((EulerAllOrderCorrectionFamily.solution period hT A B q hq) t) = (commonPath period hT A B) t

Every finite-order constructed path realizes the common actual L² path.

theorem EulerAllOrderLiftedCorrection.commonPath_initial (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) : (commonPath period hT A B) ⟨0, ⋯⟩ = 0

The common constructed correction has zero initial trace.

theorem EulerAllOrderLiftedCorrection.commonPath_divergence (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (t : ↑(Set.Icc 0 T)) : (commonPath period hT A B) t ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction

The common path belongs to the genuine closed lifted divergence-free subspace.

noncomputable def EulerAllOrderLiftedCorrection.commonJet (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (n : ℕ) (t : ↑(Set.Icc 0 T)) : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection n ((commonPath period hT A B) t)

An actual strong derivative jet of any prescribed order for the common nonlinear solution.

Equations

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

theorem EulerAllOrderLiftedCorrection.commonPath_energy (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (P : ℕ) (t : ↑(Set.Icc 0 T)) : EulerGevreyMetricEstimate.energyNorm period P ⋯ (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period B.metric) t) ((EulerAllOrderCorrectionFamily.solution period hT A B (P + 6) ⋯) t) ≤ B.delta / 2

Every external cutoff of the common solution retains the actual uniform Gevrey metric bound.

theorem EulerAllOrderLiftedCorrection.commonPath_hasDerivAt (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ (commonPath period hT A B)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A 6) ⋯).apply ⟨t, ⋯⟩ ((EulerAllOrderCorrectionFamily.solution period hT A B 6 ⋯) ⟨t, ⋯⟩))) t

The common L² path satisfies the actual nonlinear inviscid correction equation.

theorem EulerAllOrderLiftedCorrection.exists_smooth_lifted_correction (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) : ∃ (U : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))) (g : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), U ⟨0, ⋯⟩ = 0 ∧ (∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), Nonempty (EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection n (U t))) ∧ (∀ (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period ((EulerAllOrderCorrectionFamily.solution period hT A B q hq) t) = U t) ∧ (∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (g t) x)) ∧ (∀ (t : ↑(Set.Icc 0 T)), ↑↑(U t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g t) ∧ (∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period), ∑ i : Fin 3, (EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection A.κ A.direction i) (g t) x).ofLp i = 0) ∧ ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ U) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A 6) ⋯).apply ⟨t, ⋯⟩ ((EulerAllOrderCorrectionFamily.solution period hT A B 6 ⋯) ⟨t, ⋯⟩))) t

Actual coherent all-order data and their concrete budgets construct a common inviscid correction with genuine jets at every order and spatially smooth, pointwise divergence-free representatives. No correction solution, energy estimate, convergence, or all-order compatibility is assumed.

noncomputable def EulerAllOrderSmoothPressure.pressureJet (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (n : ℕ) (t : ↑(Set.Icc 0 T)) : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection n ((EulerAllOrderPressureCoherence.commonPressure period hT A B) t)

Every strong derivative order of the common actual signed pressure is supplied by a constructed finite Sobolev realization.

Equations

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

theorem EulerAllOrderSmoothPressure.commonPath_pressure_equation (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ (EulerAllOrderLiftedCorrection.commonPath period hT A B)) (-EulerCylinderSobolevSpace.value period ((EulerAllOrderPressureCoherence.rawSourcePath period hT A B 6 ⋯) ⟨t, ⋯⟩) - (A.metric.coefficient ⟨t, ⋯⟩).operator ((EulerAllOrderPressureCoherence.commonPressure period hT A B) ⟨t, ⋯⟩)) t

The common nonlinear correction satisfies its actual signed-pressure equation in L².

theorem EulerAllOrderSmoothPressure.exists_smooth_signed_pressure (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) : ∃ (p : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), (∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (p t) x)) ∧ ∀ (t : ↑(Set.Icc 0 T)), ↑↑((EulerAllOrderPressureCoherence.commonPressure period hT A B) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] p t

The constructed signed pressure has a genuine smooth spatial representative at every time.

theorem EulerAllOrderSmoothPressure.exists_smooth_pressure_graph (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (k : ℝ) (hk : k * A.κ = 1) : ∃ (p : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (Q : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.Vector3 → ℝ), (∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (p t) x)) ∧ (∀ (t : ↑(Set.Icc 0 T)), ↑↑((EulerAllOrderPressureCoherence.commonPressure period hT A B) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] p t) ∧ (∀ (t : ↑(Set.Icc 0 T)), ContDiff ℝ (↑⊤) (Q t)) ∧ ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3), gradient (Q t) x = A.κ • p t (EulerGraphPressurePotential.cylinderGraph period k A.direction x)

The actual signed correction pressure yields a smooth scalar potential on every reciprocal-frequency graph. The common pressure, all its strong jets, its smooth representative and its closed-gradient property are constructed internally.

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

The canonical pointwise pressure, obtained by bounded evaluation of its actual continuous H3 realization.

Equations

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

theorem EulerCommonPressureRepresentative.pointPressure_ae (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (t : ↑(Set.Icc 0 T)) : ↑↑((EulerAllOrderPressureCoherence.commonPressure period hT A B) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] pointPressure period hT A B t

The canonical pointwise pressure represents the constructed common L² pressure.

theorem EulerCommonPressureRepresentative.pointPressure_joint_continuous (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) : Continuous fun (p : ↑(Set.Icc 0 T) × EulerLiftedGradientSpace.LiftDomain period) => pointPressure period hT A B p.1 p.2

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

theorem EulerCommonPressureRepresentative.pointPressure_continuous (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (t : ↑(Set.Icc 0 T)) : Continuous (pointPressure period hT A B t)

The canonical pressure is continuous on each spatial slice.

theorem EulerCommonPressureRepresentative.pointPressure_smooth (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (pointPressure period hT A B t) x)

These same canonical representatives are smooth in every spatial coordinate.

theorem EulerCommonPressureRepresentative.cylinderGraph_continuous (period k : ℝ) (m : EulerLiftedGradientSpace.Vector3) : Continuous (EulerGraphPressurePotential.cylinderGraph period k m)

The physical phase graph is a continuous map into the periodic cylinder.

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

The genuine signed graph pressure-gradient vector field.

Equations

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

theorem EulerCommonPressureRepresentative.graphPressure_joint_continuous (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget period hT A) (k : ℝ) : Continuous (Function.uncurry (graphPressure period hT A B k))

The actual graph pressure-gradient field is jointly continuous in time and space.

theorem EulerCommonPressureRepresentative.graphPressure_has_potential (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : EulerAllOrderCorrectionBudget.Budget 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 hT A B k t x

Each actual canonical graph field has a genuine smooth potential by the proved lifted gradient-space reconstruction.