Actual all-order correction data from the source deformation and two prescribed packet fields. No correction solution or energy budget is assumed.

Positivity and the literal inverse identity for the pressure metric. Both follow from the prescribed deformation and its two-sided inverse.

theorem EulerPacketCorrectionCoefficients.norm_sq_lower_of_inverse {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A B : E →L[ℝ] E) (b : ℝ) (hb : 0 < b) (hBA : ∀ (v : E), B (A v) = v) (hB : ‖B‖ ≤ b) (v : E) : b⁻¹ ^ 2 * ‖v‖ ^ 2 ≤ ‖A v‖ ^ 2

theorem EulerPacketCorrectionCoefficients.frame_adjoint_inverse {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x v : EulerSmoothLimit.Space) : (ContinuousLinearMap.adjoint ((D.F.field t) x)) ((ContinuousLinearMap.adjoint ((D.FInv.field t) x)) v) = v

theorem EulerPacketCorrectionCoefficients.inverse_adjoint_frame {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x v : EulerSmoothLimit.Space) : (ContinuousLinearMap.adjoint ((D.FInv.field t) x)) ((ContinuousLinearMap.adjoint ((D.F.field t) x)) v) = v

theorem EulerPacketCorrectionCoefficients.metric_inner {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x v w : EulerSmoothLimit.Space) : inner ℝ ((((metricCoefficient D).path t) x) v) w = inner ℝ ((ContinuousLinearMap.adjoint ((D.FInv.field t) x)) v) ((ContinuousLinearMap.adjoint ((D.FInv.field t) x)) w)

theorem EulerPacketCorrectionCoefficients.inverseMetric_inner {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x v w : EulerSmoothLimit.Space) : inner ℝ ((((inverseMetricCoefficient D).path t) x) v) w = inner ℝ (((D.F.field t) x) v) (((D.F.field t) x) w)

theorem EulerPacketCorrectionCoefficients.metric_coercive {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x v : EulerSmoothLimit.Space) : D.normalLower * ‖v‖ ^ 2 ≤ inner ℝ ((((metricCoefficient D).path t) x) v) v

theorem EulerPacketCorrectionCoefficients.inverseMetric_coercive {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x v : EulerSmoothLimit.Space) : D.frameLower * ‖v‖ ^ 2 ≤ inner ℝ ((((inverseMetricCoefficient D).path t) x) v) v

theorem EulerPacketCorrectionCoefficients.inverseMetric_inverse {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x v : EulerSmoothLimit.Space) : (((inverseMetricCoefficient D).path t) x) ((((metricCoefficient D).path t) x) v) = v

theorem EulerPacketCorrectionCoefficients.metric_inverseMetric {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x v : EulerSmoothLimit.Space) : (((metricCoefficient D).path t) x) ((((inverseMetricCoefficient D).path t) x) v) = v

theorem EulerPacketCorrectionCoefficients.metric_symmetric {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x v w : EulerSmoothLimit.Space) : inner ℝ ((((metricCoefficient D).path t) x) v) w = inner ℝ v ((((metricCoefficient D).path t) x) w)

theorem EulerPacketCorrectionCoefficients.inverseMetric_symmetric {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x v w : EulerSmoothLimit.Space) : inner ℝ ((((inverseMetricCoefficient D).path t) x) v) w = inner ℝ v ((((inverseMetricCoefficient D).path t) x) w)

theorem EulerPacketCorrectionCoefficients.metricTower_coercive {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) (v : EulerSmoothLimit.Space) : D.normalLower * ‖v‖ ^ 2 ≤ inner ℝ ((((metricTower D P).coefficient t).coefficient x) v) v

theorem EulerPacketCorrectionCoefficients.inverseMetricTower_inverse {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) (v : EulerSmoothLimit.Space) : (((inverseMetricTower D P).coefficient t).coefficient x) ((((metricTower D P).coefficient t).coefficient x) v) = v

noncomputable def EulerPacketCorrectionCoefficients.correctionData {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (hκ : |κ| ≤ 1) (approximation residual : EulerAllOrderCorrectionData.FieldTower P D.T) : EulerAllOrderCorrectionData.Data P D.T

Correction data, bundling κ, direction, scale_bound, direction_bound and the required compatibility proofs.

Equations

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

noncomputable def EulerPacketCorrectionCoefficients.correctionDataOfFields {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (hκ : |κ| ≤ 1) {z r : EulerPacketProfileRecursion.VectorField} (Z : EulerPacketCylinderField.Field P D.T z) (G : EulerPacketCylinderField.Field P D.T r) : EulerAllOrderCorrectionData.Data P D.T

Correction data of fields, given by correctionData D P κ hκ Z.toFieldTower G.toFieldTower.

Equations

• EulerPacketCorrectionCoefficients.correctionDataOfFields D P κ hκ Z G = EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z.toFieldTower G.toFieldTower

@[simp]

theorem EulerPacketCorrectionCoefficients.correctionDataOfFields_approximation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (hκ : |κ| ≤ 1) {z r : EulerPacketProfileRecursion.VectorField} (Z : EulerPacketCylinderField.Field P D.T z) (G : EulerPacketCylinderField.Field P D.T r) : (correctionDataOfFields D P κ hκ Z G).approximation.field = Z.path

@[simp]

theorem EulerPacketCorrectionCoefficients.correctionDataOfFields_residual {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (hκ : |κ| ≤ 1) {z r : EulerPacketProfileRecursion.VectorField} (Z : EulerPacketCylinderField.Field P D.T z) (G : EulerPacketCylinderField.Field P D.T r) : (correctionDataOfFields D P κ hκ Z G).residual.field = G.path

@[simp]

theorem EulerPacketCorrectionCoefficients.correctionData_metric {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (hκ : |κ| ≤ 1) (Z G : EulerAllOrderCorrectionData.FieldTower P D.T) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) : ((correctionData D P κ hκ Z G).metric.coefficient t).coefficient x = (D.FInv.field t) x.1 ∘SL ContinuousLinearMap.adjoint ((D.FInv.field t) x.1)

@[simp]

theorem EulerPacketCorrectionCoefficients.correctionData_linear {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (hκ : |κ| ≤ 1) (Z G : EulerAllOrderCorrectionData.FieldTower P D.T) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) : ((correctionData D P κ hκ Z G).linear.coefficient t).coefficient x = 2 • (D.FInv.field t) x.1 ∘SL (D.F₁.field t) x.1

theorem EulerPacketCorrectionCoefficients.correctionData_quadratic {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (hκ : |κ| ≤ 1) (Z G : EulerAllOrderCorrectionData.FieldTower P D.T) (i : Fin 3) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) : (((correctionData D P κ hκ Z G).quadratic i).coefficient t).coefficient x = κ • (D.FInv.field t) x.1 ∘SL (fderiv ℝ (⇑(D.F.field t)) x.1) (EuclideanSpace.single i 1)