A genuine inverse-metric budget for the source correction data. Its time derivative, symmetry, coercivity and inverse identity are proved from the prescribed deformation; the bounds are finite norms of actual coefficient paths and their actual first translation derivative.

The time derivative of the actual inverse pressure metric, first as a bounded matrix field and then as its cylinder L² multiplier.

@[instance_reducible]

noncomputable def EulerPacketCorrectionCoefficients.instPacketCorrectionMetricTime1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCorrectionCoefficients.instPacketCorrectionMetricTime1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCorrectionCoefficients.instPacketCorrectionMetricTime2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCorrectionCoefficients.instPacketCorrectionMetricTime2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCorrectionCoefficients.instPacketCorrectionMetricTime3 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCorrectionCoefficients.instPacketCorrectionMetricTime3 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCorrectionCoefficients.instPacketCorrectionMetricTime4 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCorrectionCoefficients.instPacketCorrectionMetricTime4 = inferInstance

noncomputable def EulerPacketCorrectionCoefficients.rawInverseMetricTime {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (z : EulerPacketPointJets.Domain) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Raw inverse metric time, given by (rawFrameTime D z).adjoint.comp (rawFrame D z) + (rawFrame D z).adjoint.comp (rawFrameTime D z).

Equations

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

noncomputable def EulerPacketCorrectionCoefficients.inverseMetricTimeCoefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : EulerPacketCylinderField.MatrixCoefficient D.T (rawInverseMetricTime D)

Inverse metric time coefficient, given by ((frameTimeCoefficient D).adjoint.comp (frameCoefficient D)).add ((frameCoefficient D).adjoint.comp (frameTimeCoefficient D)).

Equations

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

@[simp]

theorem EulerPacketCorrectionCoefficients.inverseMetricTimeCoefficient_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ((inverseMetricTimeCoefficient D).path t) x = ContinuousLinearMap.adjoint ((D.F₁.field t) x) ∘SL (D.F.field t) x + ContinuousLinearMap.adjoint ((D.F.field t) x) ∘SL (D.F₁.field t) x

theorem EulerPacketCorrectionCoefficients.inverseMetric_field_hasDerivWithinAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ℝ) (ht : t ∈ Set.Icc 0 D.T) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath D.T ⋯ (inverseMetricCoefficient D).path s) x) ((EulerVolterraConvolution.extendPath D.T ⋯ (inverseMetricTimeCoefficient D).path t) x) (Set.Icc 0 D.T) t

noncomputable def EulerPacketCorrectionCoefficients.inverseMetricDerivativePath {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 P))

Inverse metric derivative path, given by fullPathMap P (inverseMetricTimeCoefficient D).path.

Equations

• EulerPacketCorrectionCoefficients.inverseMetricDerivativePath D P = (EulerLpCylinderRectangular.fullPathMap P) (EulerPacketCorrectionCoefficients.inverseMetricTimeCoefficient D).path

theorem EulerPacketCorrectionCoefficients.inverseMetric_operator_hasDerivWithinAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (t : ↑(Set.Icc 0 D.T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ ((EulerLpCylinderRectangular.fullPathMap P) (inverseMetricCoefficient D).path)) ((inverseMetricDerivativePath D P) t) (Set.Icc 0 D.T) ↑t

theorem EulerPacketCorrectionCoefficients.inverseMetricDerivativePath_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (t : ↑(Set.Icc 0 D.T)) : ‖(inverseMetricDerivativePath D P) t‖ ≤ ‖(inverseMetricTimeCoefficient D).path‖

@[instance_reducible]

noncomputable def EulerPacketCorrectionCoefficients.instPacketCorrectionMetricBudget1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCorrectionCoefficients.instPacketCorrectionMetricBudget1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCorrectionCoefficients.instPacketCorrectionMetricBudget2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCorrectionCoefficients.instPacketCorrectionMetricBudget2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCorrectionCoefficients.instPacketCorrectionMetricBudget3 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCorrectionCoefficients.instPacketCorrectionMetricBudget3 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCorrectionCoefficients.instPacketCorrectionMetricBudget4 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCorrectionCoefficients.instPacketCorrectionMetricBudget4 = inferInstance

theorem EulerPacketCorrectionCoefficients.inverseMetric_operatorPath_eq {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] : EulerRegularizedMetricPaths.metricOperatorPath P D.T (inverseMetricTower D P).coefficient ⋯ = (EulerLpCylinderRectangular.fullPathMap P) (inverseMetricCoefficient D).path

theorem EulerPacketCorrectionCoefficients.inverseMetric_operator_hasDerivAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (t : ℝ) (ht : t ∈ Set.Ioo 0 D.T) : HasDerivAt (EulerVolterraConvolution.extendPath D.T ⋯ (EulerRegularizedMetricPaths.metricOperatorPath P D.T (inverseMetricTower D P).coefficient ⋯)) (EulerVolterraConvolution.extendPath D.T ⋯ (inverseMetricDerivativePath D P) t) t

noncomputable def EulerPacketCorrectionCoefficients.inverseMetricBound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : ℝ

Inverse metric bound, given by ‖(inverseMetricCoefficient D).path‖.

Equations

• EulerPacketCorrectionCoefficients.inverseMetricBound D = ‖(EulerPacketCorrectionCoefficients.inverseMetricCoefficient D).path‖

noncomputable def EulerPacketCorrectionCoefficients.inverseMetricFirstBound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : ℝ

Inverse metric first bound, given by ‖iteratedFDeriv ℝ 1 (translateCoefficientPath (inverseMetricCoefficient D).path) 0‖.

Equations

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

noncomputable def EulerPacketCorrectionCoefficients.inverseMetricTimeBound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : ℝ

Inverse metric time bound, given by ‖(inverseMetricTimeCoefficient D).path‖.

Equations

• EulerPacketCorrectionCoefficients.inverseMetricTimeBound D = ‖(EulerPacketCorrectionCoefficients.inverseMetricTimeCoefficient D).path‖

theorem EulerPacketCorrectionCoefficients.inverseMetricBound_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : inverseMetricBound D ≤ ‖D.F.field‖ ^ 2

theorem EulerPacketCorrectionCoefficients.inverseMetricTimeBound_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : inverseMetricTimeBound D ≤ 2 * ‖D.F.field‖ * ‖D.F₁.field‖

noncomputable def EulerPacketCorrectionCoefficients.sourceMetricBudget {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) (q : ℕ) : EulerCorrectionEnergyData.MetricBudget P D.T ⋯ (EulerAllOrderCorrectionData.Data.atOrder P (correctionData D P κ hκ Z G) (q + 1))

The actual source inverse metric supplies every field of the metric budget at every finite Sobolev order.

Equations

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

noncomputable def EulerPacketCorrectionCoefficients.sourceMetricBudgetOfFields {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) (q : ℕ) : EulerCorrectionEnergyData.MetricBudget P D.T ⋯ (EulerAllOrderCorrectionData.Data.atOrder P (correctionDataOfFields D P κ hκ Z G) (q + 1))

Source metric budget of fields, given by sourceMetricBudget D P κ hκ Z.toFieldTower G.toFieldTower q.

Equations

• EulerPacketCorrectionCoefficients.sourceMetricBudgetOfFields D P κ hκ Z G q = EulerPacketCorrectionCoefficients.sourceMetricBudget D P κ hκ Z.toFieldTower G.toFieldTower q

@[simp]

theorem EulerPacketCorrectionCoefficients.sourceMetricBudget_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) (q : ℕ) : (sourceMetricBudget D P κ hκ Z G q).metric = (inverseMetricTower D P).coefficient

@[simp]

theorem EulerPacketCorrectionCoefficients.sourceMetricBudget_derivative {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) (q : ℕ) : (sourceMetricBudget D P κ hκ Z G q).derivative = inverseMetricDerivativePath D P

@[simp]

theorem EulerPacketCorrectionCoefficients.sourceMetricBudget_c {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) (q : ℕ) : (sourceMetricBudget D P κ hκ Z G q).c = D.inverseBound⁻¹

theorem EulerPacketCorrectionCoefficients.sourceMetricBudget_bound_le {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) (q : ℕ) : (sourceMetricBudget D P κ hκ Z G q).bound ≤ ‖D.F.field‖ ^ 2

theorem EulerPacketCorrectionCoefficients.sourceMetricBudget_time_le {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) (q : ℕ) : (sourceMetricBudget D P κ hκ Z G q).time ≤ 2 * ‖D.F.field‖ * ‖D.F₁.field‖