Coherent prescribed cylinder data at every finite Sobolev order.

structure EulerAllOrderCorrectionData.CoefficientTower (period : ℝ) [Fact (0 < period)] (T : ℝ) : Type

A single actual coefficient field with genuine derivative jets and continuous multiplier action at every finite order.

• coefficient : ↑(Set.Icc 0 T) → EulerSpatialSobolevInverse.SmoothCoefficient period

  The actual smooth bounded coefficient at each time.

• jet (q : ℕ) (t : ↑(Set.Icc 0 T)) : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (self.coefficient t)

  Genuine strong derivative jets of this same coefficient.

• continuous (q : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (self.jet q t)

  Actual multiplier continuity at every finite Sobolev order.

structure EulerAllOrderCorrectionData.FieldTower (period : ℝ) [Fact (0 < period)] (T : ℝ) : Type

A single prescribed L² path realized by actual continuous Sobolev paths at every order.

• field : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))

  The common actual L² field path.

• realization (q : ℕ) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

  Actual finite-order Sobolev realizations of that field.

• value_eq (q : ℕ) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((self.realization q) t) = self.field t

  Each realization represents exactly the prescribed field.

theorem EulerAllOrderCorrectionData.FieldTower.truncate (period : ℝ) [Fact (0 < period)] {T : ℝ} (f : FieldTower period T) (q : ℕ) : (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period q)) (f.realization (q + 1)) = f.realization q

Coherence of prescribed Sobolev realizations follows from genuine derivative uniqueness.

structure EulerAllOrderCorrectionData.Data (period : ℝ) [Fact (0 < period)] (T : ℝ) : Type

Actual all-order prescribed coefficient, approximation and residual data; no correction solution or energy estimate is contained here.

• κ : ℝ

  The fixed spatial scale in the lifted derivative.

• direction : EulerLiftedGradientSpace.Vector3

  The fixed angular direction.

• scale_bound : |self.κ| ≤ 1

  The actual scale bound used by transport.

• direction_bound : ‖self.direction‖ ≤ 1

  The actual direction bound used by transport.

• metric : CoefficientTower period T

  The actual pressure coefficient and all its derivative jets.

• metric_continuous : Continuous fun (t : ↑(Set.Icc 0 T)) => (self.metric.coefficient t).operator

  The coefficient is continuous as an actual L² multiplier.

• coercivity : ℝ

  The actual positive coercivity constant.

• coercivity_pos : 0 < self.coercivity

  Strict positivity of that constant.

• metric_pos (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3) : self.coercivity * ‖v‖ ^ 2 ≤ inner ℝ (((self.metric.coefficient t).coefficient x) v) v

  Pointwise coercivity of the actual coefficient.

• linear : CoefficientTower period T

  The actual order-zero linear coefficient.

• quadratic : Fin 3 → CoefficientTower period T

  The three actual order-zero quadratic coefficients.

• approximation : FieldTower period T

  The prescribed approximate solution, with all actual Sobolev realizations.

• residual : FieldTower period T

  The prescribed residual, with all actual Sobolev realizations.

def EulerAllOrderCorrectionData.Data.atOrder (period : ℝ) [Fact (0 < period)] {T : ℝ} (A : Data period T) (q : ℕ) : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)

The literal finite-order correction data extracted from a coherent prescribed tower.

Equations

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

theorem EulerAllOrderCorrectionData.Data.lower_atOrder (period : ℝ) [Fact (0 < period)] {T : ℝ} (A : Data period T) (q : ℕ) : EulerCorrectionLowerData.lowerData period (atOrder period A (q + 1)) (A.metric.jet q) (A.linear.jet q) (fun (i : Fin 3) => (A.quadratic i).jet q) ⋯ ⋯ ⋯ = atOrder period A q

Lowering the actual prescribed data gives exactly the next member of the same tower.

def EulerAllOrderCorrectionData.Data.metricBudget (period : ℝ) [Fact (0 < period)] {T : ℝ} (A : Data period T) (hT : 0 ≤ T) (K : EulerCorrectionEnergyData.MetricBudget period T hT (atOrder period A 1)) (q : ℕ) : EulerCorrectionEnergyData.MetricBudget period T hT (atOrder period A (q + 1))

A single actual inverse-metric budget applies to every finite realization of the same coefficient field.

Equations

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