The initial induction state is completely constructed from the compact β-family. A single positive time and a single label constant work for the family, with actual low-order guards and pressure sign.

Actual constant coefficient towers for the ordinary Euler correction equation: identity pressure metric, zero lower-order coefficients, spatial scale one and angular direction zero. No solution is included in the data.

@[instance_reducible]

noncomputable def EulerConstantCorrection.instConstantCorrectionData1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerConstantCorrection.instConstantCorrectionData1 = inferInstance

@[instance_reducible]

noncomputable def EulerConstantCorrection.instConstantCorrectionData2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerConstantCorrection.instConstantCorrectionData2 = inferInstance

@[instance_reducible]

noncomputable def EulerConstantCorrection.instConstantCorrectionData3 : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerConstantCorrection.instConstantCorrectionData3 = inferInstance

@[instance_reducible]

noncomputable def EulerConstantCorrection.instConstantCorrectionData4 : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerConstantCorrection.instConstantCorrectionData4 = inferInstance

@[instance_reducible]

noncomputable def EulerConstantCorrection.instConstantCorrectionData5 : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerConstantCorrection.instConstantCorrectionData5 = inferInstance

@[instance_reducible]

noncomputable def EulerConstantCorrection.instConstantCorrectionData6 : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerConstantCorrection.instConstantCorrectionData6 = inferInstance

noncomputable def EulerConstantCorrection.coefficient (P : ℝ) (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerSpatialSobolevInverse.SmoothCoefficient P

Coefficient, bundling coefficient, smooth, bound, norm_bound and the required compatibility proofs.

Equations

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

def EulerConstantCorrection.jet (P : ℝ) (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (q : ℕ) : EulerSpatialSobolevInverse.CoefficientJet P EulerCylinderSobolev.standardDirection q (coefficient P A)

Jet used in constant correction data.

Equations

• One or more equations did not get rendered due to their size.
• EulerConstantCorrection.jet P A 0 = EulerSpatialSobolevInverse.CoefficientJet.zero (EulerConstantCorrection.coefficient P A)

theorem EulerConstantCorrection.jet_boundLevel (P : ℝ) (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (q r : ℕ) : EulerJetProductBounds.boundLevel P (jet P A q) r = if r = 0 then ‖A‖ else 0

theorem EulerConstantCorrection.jet_zero_coefficientBlock (P : ℝ) (q b n : ℕ) : EulerH6Pressure.coefficientBlock P (jet P 0 q) b n = 0

theorem EulerConstantCorrection.jet_positive_coefficientBlock (P : ℝ) (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (q b n : ℕ) (hn : 0 < n) : EulerH6Pressure.coefficientBlock P (jet P A q) b n = 0

theorem EulerConstantCorrection.jet_zero_weightedCoefficient (P : ℝ) (q b N : ℕ) (ρ : ℝ) : EulerSobolevGevreyOperators.weightedCoefficient P (jet P 0 q) b N ρ = 0

theorem EulerConstantCorrection.coefficient_operator_id (P : ℝ) [Fact (0 < P)] : (coefficient P (ContinuousLinearMap.id ℝ EulerSmoothLimit.Space)).operator = ContinuousLinearMap.id ℝ ↥(EulerLiftedGradientSpace.LiftL2 P)

theorem EulerConstantCorrection.coefficient_operator_zero (P : ℝ) [Fact (0 < P)] : (coefficient P 0).operator = 0

noncomputable def EulerConstantCorrection.tower (P : ℝ) [Fact (0 < P)] (T : ℝ) (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerAllOrderCorrectionData.CoefficientTower P T

Tower, bundling coefficient, jet, continuous.

Equations

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

noncomputable def EulerConstantCorrection.data (P : ℝ) [Fact (0 < P)] {T : ℝ} (F R : EulerAllOrderCorrectionData.FieldTower P T) : EulerAllOrderCorrectionData.Data P T

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 EulerConstantCorrection.metricBudget (P : ℝ) [Fact (0 < P)] {T : ℝ} (hT : 0 ≤ T) (F R : EulerAllOrderCorrectionData.FieldTower P T) : EulerCorrectionEnergyData.MetricBudget P T hT (EulerAllOrderCorrectionData.Data.atOrder P (data P F R) 1)

Metric budget, bundling metric, continuous, derivative, hasDeriv and the required compatibility proofs.

Equations

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

def EulerConstantCorrection.pressureBound : ℝ

Pressure bound, given by 9^729.

Equations

• EulerConstantCorrection.pressureBound = 9 ^ 729

theorem EulerConstantCorrection.pressureBound_one_le : 1 ≤ pressureBound

theorem EulerConstantCorrection.identity_base (P : ℝ) (q r : ℕ) : EulerJetProductBounds.boundLevel P (jet P (ContinuousLinearMap.id ℝ EulerSmoothLimit.Space) q) r ≤ 1

theorem EulerConstantCorrection.identity_pressure (P : ℝ) (q : ℕ) (hq : 6 ≤ q) : (EulerH6Pressure.CoefficientJet.restrict (jet P (ContinuousLinearMap.id ℝ EulerSmoothLimit.Space) q) 5 ⋯).pressureConstant 1 ≤ pressureBound ∧ (EulerH6Pressure.CoefficientJet.restrict (jet P (ContinuousLinearMap.id ℝ EulerSmoothLimit.Space) q) 6 hq).pressureConstant 1 ≤ pressureBound

The literal spatial convection of a small smooth cylinder field has a quadratic residual envelope at every Sobolev order. No residual estimate or differential equation is postulated.

noncomputable def EulerSmallCorrection.residualCost (P : ℝ) [Fact (0 < P)] (C R : ℝ) : ℝ

Residual cost, given by 1+108*productBlockConstant P*C^2*R.

Equations

• EulerSmallCorrection.residualCost P C R = 1 + 108 * EulerCylinderPathProduct.productBlockConstant P * C ^ 2 * R

theorem EulerSmallCorrection.residualCost_pos (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hR : 0 ≤ R) : 0 < residualCost P C R

noncomputable def EulerSmallCorrection.residual {P : ℝ} [Fact (0 < P)] {T : ℝ} {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (ε : ℝ) : EulerPacketCylinderField.Field P T fun (z : EulerPacketPointJets.Domain) => (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => (ε • raw) (z.1, y)) z.2) ((ε • raw) z, 0)

Residual, given by (G.smul ε).spatialTransport (G.smul ε).

Equations

• EulerSmallCorrection.residual G ε = (G.smul ε).spatialTransport (G.smul ε)

noncomputable def EulerSmallCorrection.input {P : ℝ} [Fact (0 < P)] {T : ℝ} {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (ε : ℝ) : EulerAllOrderCorrectionData.Data P T

Input, given by data P (G.smul ε).toFieldTower (residual G ε).toFieldTower.

Equations

• EulerSmallCorrection.input G ε = EulerConstantCorrection.data P (G.smul ε).toFieldTower (EulerSmallCorrection.residual G ε).toFieldTower

theorem EulerSmallCorrection.weighted_shift_one {P : ℝ} [Fact (0 < P)] {T : ℝ} {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) {q : ℕ} {R A : ℝ} (hG : G.WordBound q R A 1) (hR : 0 ≤ R) (hA : 0 ≤ A) (s N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (hsmall : ρ * R ≤ 1 / 2) (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedNorm P q N ρ ((G.toFieldTower.realization s) t) ≤ 12 * A * R

theorem EulerSmallCorrection.scaled_word {P : ℝ} [Fact (0 < P)] {T : ℝ} {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) {C R : ℝ} (hG : G.WordBound 6 R C 0) (ε : ℝ) (hε : 0 ≤ ε) : (G.smul ε).WordBound 6 R (ε * C) 0

theorem EulerSmallCorrection.residual_word {P : ℝ} [Fact (0 < P)] {T : ℝ} {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) {C R : ℝ} (hG : G.WordBound 6 R C 0) (hC : 0 ≤ C) (hR : 0 ≤ R) (ε : ℝ) (hε : 0 ≤ ε) : (residual G ε).WordBound 6 R (9 * EulerCylinderPathProduct.productBlockConstant P * (ε * C) * (ε * C)) 1

theorem EulerSmallCorrection.residual_weighted {P : ℝ} [Fact (0 < P)] {T : ℝ} {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) {C R : ℝ} (hG : G.WordBound 6 R C 0) (hC : 0 ≤ C) (hR : 0 ≤ R) (ε : ℝ) (hε : 0 ≤ ε) (s N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (hsmall : ρ * R ≤ 1 / 2) (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedNorm P 6 N ρ (((residual G ε).toFieldTower.realization s) t) ≤ ε ^ 2 * residualCost P C R

An actual exact lifted Euler solution is constructed from any genuine smooth solenoidal L² datum with factorial derivative bounds. The amplitude is an explicit function of the supplied bounds and does not depend on the particular datum realizing them.

A genuine all-order correction budget for small smooth data with the identity metric. Every field and coefficient estimate is derived from the given datum's actual word bound; the amplitude is chosen explicitly.

An explicit positive amplitude puts any finite Gevrey datum and quadratic residual envelope in the all-order correction regime. The growth constant belongs to the identity-metric equation, not to an assumed solution.

noncomputable def EulerSmallCorrection.growth (P : ℝ) [Fact (0 < P)] : ℝ

Growth, given by energyConstant P 0 0 1 1 pressureBound 1 1 0 0 1.

Equations

• EulerSmallCorrection.growth P = EulerNonlinearEnergyConstants.energyConstant P 0 0 1 1 EulerConstantCorrection.pressureBound 1 1 0 0 1

theorem EulerSmallCorrection.growth_pos (P : ℝ) [Fact (0 < P)] : 0 < growth P

noncomputable def EulerSmallCorrection.initialRadius (R : ℝ) : ℝ

Initial radius, given by 1/(2*(R+1)).

Equations

• EulerSmallCorrection.initialRadius R = 1 / (2 * (R + 1))

theorem EulerSmallCorrection.initialRadius_pos (R : ℝ) (hR : 0 ≤ R) : 0 < initialRadius R

theorem EulerSmallCorrection.initialRadius_mul (R : ℝ) (hR : 0 ≤ R) : initialRadius R * R ≤ 1 / 2

structure EulerSmallCorrection.Scale (P : ℝ) [Fact (0 < P)] (C R E : ℝ) : Type

These are scalar smallness inequalities, obtained explicitly below.

• value : ℝ

  Value of Scale, of type ℝ.

• positive : 0 < self.value
• one : self.value ≤ 1
• background : 2 * self.value * C ≤ 1
• derivative : 12 * self.value * C * R ≤ 1
• shrink : 2 * growth P * (8 * self.value * C + self.value) ≤ initialRadius R / 2
• residual : 2 * (self.value ^ 2 * E) * Real.exp (3 * growth P) ≤ self.value / 2

noncomputable def EulerSmallCorrection.scale (P : ℝ) [Fact (0 < P)] (C R E : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hE : 0 < E) : Scale P C R E

Scale as an element of Scale P C R E.

Equations

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

noncomputable def EulerSmallCorrection.Scale.radius (P : ℝ) [Fact (0 < P)] {C R E : ℝ} (S : Scale P C R E) : C(↑(Set.Icc 0 1), ℝ)

Radius as an element of C(Icc (0 : ℝ) 1,ℝ).

Equations

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

theorem EulerSmallCorrection.Scale.radius_bounds (P : ℝ) [Fact (0 < P)] {C R E : ℝ} (S : Scale P C R E) (hC : 0 ≤ C) (t : ↑(Set.Icc 0 1)) : initialRadius R / 2 ≤ (radius P S) t ∧ (radius P S) t ≤ initialRadius R

theorem EulerSmallCorrection.Scale.radius_positive (P : ℝ) [Fact (0 < P)] {C R E : ℝ} (S : Scale P C R E) (hC : 0 ≤ C) (hR : 0 ≤ R) (t : ↑(Set.Icc 0 1)) : 0 < (radius P S) t

theorem EulerSmallCorrection.Scale.radius_small (P : ℝ) [Fact (0 < P)] {C R E : ℝ} (S : Scale P C R E) (hC : 0 ≤ C) (hR : 0 ≤ R) (t : ↑(Set.Icc 0 1)) : (radius P S) t * R ≤ 1 / 2

noncomputable def EulerSmallCorrection.spatialBudget {P : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P 1 raw) {C R : ℝ} (hG : G.WordBound 6 R C 0) (hC : 0 ≤ C) (hR : 0 ≤ R) (S : Scale P C R (residualCost P C R)) (q : ℕ) (hq : 6 ≤ q) : EulerCorrectionEnergyData.SpatialBudget P ⋯ (EulerAllOrderCorrectionData.Data.atOrder P (input G S.value) (q + 1 + 1)) (q - 4) (Scale.radius P S)

Spatial budget, bundling Rc, M, B, B0 and the required compatibility proofs.

Equations

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

noncomputable def EulerSmallCorrection.driftBudget {P : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P 1 raw) {C R : ℝ} (hG : G.WordBound 6 R C 0) (hC : 0 ≤ C) (hR : 0 ≤ R) (S : Scale P C R (residualCost P C R)) (q : ℕ) (hq : 6 ≤ q) : EulerDriftCorrectionBudget.Budget P ⋯ (EulerAllOrderCorrectionData.Data.atOrder P (input G S.value) (q + 1 + 1)) (q - 4) (Scale.radius P S)

Drift budget, bundling full, drift, drift_nonneg, drift_bound and the required compatibility proofs.

Equations

• EulerSmallCorrection.driftBudget G hG hC hR S q hq = { full := EulerSmallCorrection.spatialBudget G hG hC hR S q hq, drift := 8 * S.value * C, drift_nonneg := ⋯, drift_bound := ⋯ }

theorem EulerSmallCorrection.driftBudget_growth {P : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P 1 raw) {C R : ℝ} (hG : G.WordBound 6 R C 0) (hC : 0 ≤ C) (hR : 0 ≤ R) (S : Scale P C R (residualCost P C R)) (q : ℕ) (hq : 6 ≤ q) : EulerCorrectionEnergyMajorants.combinedConstant P (driftBudget G hG hC hR S q hq).full (EulerAllOrderCorrectionData.Data.metricBudget P (input G S.value) driftBudget_growth._proof_1 (EulerConstantCorrection.metricBudget P driftBudget_growth._proof_1 (G.smul S.value).toFieldTower (residual G S.value).toFieldTower) (q + 1)) = growth P

noncomputable def EulerSmallCorrection.budget {P : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P 1 raw) {C R : ℝ} (hG : G.WordBound 6 R C 0) (hC : 0 ≤ C) (hR : 0 ≤ R) (S : Scale P C R (residualCost P C R)) (hdiv : ∀ (t : ↑(Set.Icc 0 1)), G.path t ∈ EulerLiftedGradientSpace.divergenceFreeSpace P 1 0) : EulerAllOrderDriftCorrection.Budget P budget._proof_1 (input G S.value)

Budget, bundling metric, radius, growthCoefficient, delta and the required compatibility proofs.

Equations

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

noncomputable def EulerSmallCorrection.smallBudget {P : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P 1 raw) {C R : ℝ} (hG : G.WordBound 6 R C 0) (hC : 0 ≤ C) (hR : 0 ≤ R) (hdiv : ∀ (t : ↑(Set.Icc 0 1)), G.path t ∈ EulerLiftedGradientSpace.divergenceFreeSpace P 1 0) : EulerAllOrderDriftCorrection.Budget P budget._proof_1 (input G (scale P C R (residualCost P C R) hC hR ⋯).value)

No scalar guard is required of the input: the amplitude is explicitly chosen from its finite actual Gevrey constants.

Equations

• EulerSmallCorrection.smallBudget G hG hC hR hdiv = EulerSmallCorrection.budget G hG hC hR (EulerSmallCorrection.scale P C R (EulerSmallCorrection.residualCost P C R) hC hR ⋯) hdiv

A genuine smooth spatial L² field, embedded as a time-independent, angle-independent cylinder field. Tensor bounds give a fixed mixed Sobolev word bound, and classical divergence zero gives the actual lifted constraint.

noncomputable def EulerStaticCylinder.spatialOrbit (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (a : EulerLiftedGradientSpace.LiftTangent) : ↥(MeasureTheory.Lp EulerSmoothLimit.Space 2 MeasureTheory.volume)

Spatial orbit, given by EulerLpTranslation.translation a.1 u.toLp.

Equations

• EulerStaticCylinder.spatialOrbit u a = (EulerLpTranslation.translation a.1) u.toLp

theorem EulerStaticCylinder.spatialOrbit_smooth (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ContDiff ℝ (↑⊤) (spatialOrbit u)

theorem EulerStaticCylinder.embeddedOrbit_smooth (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ((EulerCylinderSpatialEmbedding.embedding P) u.toLp)

noncomputable def EulerStaticCylinder.field (P T : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : EulerPacketCylinderField.Field P T fun (z : EulerPacketPointJets.Domain) => u.field z.2.1

Field, constructed using Field.ofLifted.

Equations

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

@[simp]

theorem EulerStaticCylinder.field_path (P T : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : (field P T u).path = ContinuousMap.const (↑(Set.Icc 0 T)) ((EulerCylinderSpatialEmbedding.embedding P) u.toLp)

theorem EulerStaticCylinder.field_time (P T : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hT : 0 ≤ T) : EulerPacketCylinderField.TimeDerivative hT (field P T u) (EulerPacketCylinderField.Field.zero P T)

theorem EulerStaticCylinder.field_divergence (P T : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (κ : ℝ) (m : EulerSmoothLimit.Space) (hu : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 T)) : (field P T u).path t ∈ EulerLiftedGradientSpace.divergenceFreeSpace P κ m

theorem EulerStaticCylinder.spatialOrbit_derivative_norm (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (spatialOrbit u) a‖ ≤ ‖u.jetLp n‖

theorem EulerStaticCylinder.field_wordBound (P T : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (q : ℕ) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hb : u.HasJetBound C R) : (field P T u).WordBound q (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) R) (√P * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q R C) 0

For a static approximation the prescribed residual is exactly its spatial convection, at every finite Sobolev order. This verifies the equation input to the correction theorem rather than assuming it.

theorem EulerSmallCorrection.fieldTower_pointField {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (t : ↑(Set.Icc 0 T)) : G.toFieldTower.pointField t = EulerCylinderSmoothOrbit.pointField P G.path ⋯ t

theorem EulerSmallCorrection.nonlinearity_eq_residual {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (ε : ℝ) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCorrectionResidualCancellation.nonlinearity P (EulerAllOrderCorrectionData.Data.atOrder P (input G ε) q) hq t (((G.smul ε).toFieldTower.realization (q + 1)) t) = ((residual G ε).toFieldTower.realization q) t

theorem EulerSmallCorrection.zero_tower {P T : ℝ} [Fact (0 < P)] (q : ℕ) (t : ↑(Set.Icc 0 T)) : ((EulerPacketCylinderField.Field.zero P T).toFieldTower.realization q) t = 0

theorem EulerSmallCorrection.scaled_zero_tower {P T : ℝ} [Fact (0 < P)] (ε : ℝ) (q : ℕ) (t : ↑(Set.Icc 0 T)) : (((EulerPacketCylinderField.Field.zero P T).smul ε).toFieldTower.realization q) t = 0

noncomputable def EulerSmallCorrection.approximationResidual {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (hT : 0 < T) (ε : ℝ) (hstatic : EulerPacketCylinderField.TimeDerivative ⋯ G (EulerPacketCylinderField.Field.zero P T)) : EulerAllOrderDriftCorrection.ApproximationResidual P hT (input G ε)

Approximation residual, bundling pressure, gradient, equation, let and the required compatibility proofs.

Equations

• EulerSmallCorrection.approximationResidual G hT ε hstatic = { pressure := (EulerPacketCylinderField.Field.zero P T).toFieldTower, gradient := ⋯, equation := ⋯ }

def EulerStaticEuler.mixedRadius (R : ℝ) : ℝ

Mixed radius, given by sobolevCoefficientRadius (Fin 4) R.

Equations

• EulerStaticEuler.mixedRadius R = EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) R

noncomputable def EulerStaticEuler.mixedAmplitude (P C R : ℝ) : ℝ

Mixed amplitude, given by Real.sqrt P*sobolevCoefficientAmplitude (Fin 4) 6 R C.

Equations

• EulerStaticEuler.mixedAmplitude P C R = √P * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) 6 R C

theorem EulerStaticEuler.mixedRadius_nonneg (R : ℝ) (hR : 0 ≤ R) : 0 ≤ mixedRadius R

theorem EulerStaticEuler.mixedAmplitude_nonneg (P C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : 0 ≤ mixedAmplitude P C R

noncomputable def EulerStaticEuler.scales (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : EulerSmallCorrection.Scale P (mixedAmplitude P C R) (mixedRadius R) (EulerSmallCorrection.residualCost P (mixedAmplitude P C R) (mixedRadius R))

Scales, given by scale P _ _ _ (mixedAmplitude_nonneg P C R hC hR) (mixedRadius_nonneg R hR) (residualCost_pos P _ _ (mixedRadius_nonneg R hR)).

Equations

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

noncomputable def EulerStaticEuler.amplitude (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : ℝ

Amplitude, given by (scales P C R hC hR).value.

Equations

• EulerStaticEuler.amplitude P C R hC hR = (EulerStaticEuler.scales P C R hC hR).value

theorem EulerStaticEuler.amplitude_pos (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : 0 < amplitude P C R hC hR

theorem EulerStaticEuler.amplitude_le_one (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : amplitude P C R hC hR ≤ 1

noncomputable def EulerStaticEuler.inputData (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : EulerAllOrderCorrectionData.Data P 1

Input data, given by input (EulerStaticCylinder.field P 1 u) (amplitude P C R hC hR).

Equations

• EulerStaticEuler.inputData P u C R hC hR = EulerSmallCorrection.input (EulerStaticCylinder.field P 1 u) (EulerStaticEuler.amplitude P C R hC hR)

noncomputable def EulerStaticEuler.correctionBudget (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : EulerAllOrderDriftCorrection.Budget P EulerSmallCorrection.budget._proof_1 (inputData P u C R hC hR)

Correction budget, constructed using budget.

Equations

• EulerStaticEuler.correctionBudget P u C R hC hR hu hdiv = EulerSmallCorrection.budget (EulerStaticCylinder.field P 1 u) ⋯ ⋯ ⋯ (EulerStaticEuler.scales P C R hC hR) ⋯

noncomputable def EulerStaticEuler.exactPacket (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : EulerAllOrderDriftCorrection.ExactLiftedPacket P EulerSmallCorrection.budget._proof_1 (inputData P u C R hC hR) (correctionBudget P u C R hC hR hu hdiv)

Exact packet, constructed using exactPacketOfResidual.

Equations

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

theorem EulerStaticEuler.exactPacket_initial (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (q : ℕ) : ((exactPacket P u C R hC hR hu hdiv).velocity.realization q) ⟨0, ⋯⟩ = (((EulerStaticCylinder.field P 1 u).smul (amplitude P C R hC hR)).toFieldTower.realization q) ⟨0, ⋯⟩

With spatial scale one and angular direction zero, the zero-angle slice of the actual exact lifted solution solves ordinary three-dimensional Euler. The scalar pressure is the canonical normalized graph potential.

@[instance_reducible]

noncomputable def EulerConstantEuler.instConstantEulerGraph1 : NormedAddCommGroup EulerSmoothLimit.Space

Cache the standard NormedAddCommGroup Space instance to shorten typeclass synthesis.

Equations

• EulerConstantEuler.instConstantEulerGraph1 = inferInstance

@[instance_reducible]

noncomputable def EulerConstantEuler.instConstantEulerGraph2 : NormedSpace ℝ EulerSmoothLimit.Space

Cache the standard NormedSpace ℝ Space instance to shorten typeclass synthesis.

Equations

• EulerConstantEuler.instConstantEulerGraph2 = inferInstance

@[instance_reducible]

noncomputable def EulerConstantEuler.instConstantEulerGraph3 : NormedAddCommGroup EulerLiftedGradientSpace.LiftTangent

Cache the standard NormedAddCommGroup LiftTangent instance to shorten typeclass synthesis.

Equations

• EulerConstantEuler.instConstantEulerGraph3 = inferInstance

@[instance_reducible]

noncomputable def EulerConstantEuler.instConstantEulerGraph4 : NormedSpace ℝ EulerLiftedGradientSpace.LiftTangent

Cache the standard NormedSpace ℝ LiftTangent instance to shorten typeclass synthesis.

Equations

• EulerConstantEuler.instConstantEulerGraph4 = inferInstance

def EulerConstantEuler.inclusion : ℝ × EulerSmoothLimit.Space →L[ℝ] ℝ × EulerLiftedGradientSpace.LiftTangent

Inclusion, given by (ContinuousLinearMap.id ℝ ℝ).prodMap (ContinuousLinearMap.inl ℝ Space ℝ).

Equations

• EulerConstantEuler.inclusion = (ContinuousLinearMap.id ℝ ℝ).prodMap (ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ)

@[simp]

theorem EulerConstantEuler.inclusion_apply (t : ℝ) (x : EulerSmoothLimit.Space) : inclusion (t, x) = (t, x, 0)

noncomputable def EulerConstantEuler.velocity {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (q : ℝ × EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Velocity, given by S.rawVelocity (q.1,(q.2,0)).

Equations

• EulerConstantEuler.velocity S q = S.rawVelocity (q.1, q.2, 0)

noncomputable def EulerConstantEuler.pressure {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (q : ℝ × EulerSmoothLimit.Space) : ℝ

Pressure, given by S.rawGraphPotential 1 q.

Equations

• EulerConstantEuler.pressure S q = S.rawGraphPotential 1 q

noncomputable def EulerConstantEuler.force {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (q : ℝ × EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Force, given by S.rawPressure (q.1,(q.2,0)).

Equations

• EulerConstantEuler.force S q = S.rawPressure (q.1, q.2, 0)

theorem EulerConstantEuler.velocity_hasFDerivAt {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space) : HasFDerivAt (velocity S) (fderiv ℝ S.rawVelocity (t, x, 0) ∘SL inclusion) (t, x)

theorem EulerConstantEuler.velocity_joint_continuous {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) : Continuous (velocity S)

theorem EulerConstantEuler.force_joint_continuous {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) : Continuous (force S)

theorem EulerConstantEuler.pressure_joint_continuous {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) : Continuous (pressure S)

theorem EulerConstantEuler.pressure_smooth {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (t : ℝ) : ContDiff ℝ ↑⊤ fun (x : EulerSmoothLimit.Space) => pressure S (t, x)

theorem EulerConstantEuler.pressure_gradient {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (t : ℝ) (x : EulerSmoothLimit.Space) : gradient (fun (y : EulerSmoothLimit.Space) => pressure S (t, y)) x = force S (t, x)

theorem EulerConstantEuler.pressure_zero {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (t : ℝ) : pressure S (t, 0) = 0

theorem EulerConstantEuler.velocity_divergence {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (t : ℝ) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => velocity S (t, y)) x = 0

theorem EulerConstantEuler.momentum {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space) : EulerLagrangian.momentumResidual (velocity S) (pressure S) (t, x) = 0

noncomputable def EulerConstantEuler.field {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (t : ↑(Set.Icc 0 T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Field, bundling field, smooth, integrable.

Equations

• EulerConstantEuler.field S t = { field := S.velocity.physicalPointField 1 0 t, smooth := ⋯, integrable := ⋯ }

theorem EulerConstantEuler.field_apply {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (field S t).field x = velocity S (↑t, x)

theorem EulerConstantEuler.field_jetLp {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (n : ℕ) (t : ↑(Set.Icc 0 T)) : (field S t).jetLp n = (S.velocity.physicalTensorPath 1 0 n) t

theorem EulerConstantEuler.field_jetLp_continuous {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (field S t).jetLp n

theorem EulerConstantEuler.velocity_smooth {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (t : ℝ) : ContDiff ℝ ↑⊤ fun (x : EulerSmoothLimit.Space) => velocity S (t, x)

theorem EulerConstantEuler.force_smooth {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {F R : EulerAllOrderCorrectionData.FieldTower P T} {B : EulerAllOrderDriftCorrection.Budget P hT (EulerConstantCorrection.data P F R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P hT (EulerConstantCorrection.data P F R) B) (t : ℝ) : ContDiff ℝ ↑⊤ fun (x : EulerSmoothLimit.Space) => force S (t, x)

The genuine Euler time/amplitude scaling. A solution starting from ε u₀ on [0,1] gives a solution starting from u₀ on [0,ε].

noncomputable def EulerTimeRescaling.coordinates {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ε : ℝ) : ℝ × E →L[ℝ] ℝ × E

Coordinates, given by ((ε⁻¹ • ContinuousLinearMap.id ℝ ℝ).comp (fst ℝ ℝ E)).prod (snd ℝ ℝ E).

Equations

• EulerTimeRescaling.coordinates ε = ((ε⁻¹ • ContinuousLinearMap.id ℝ ℝ) ∘SL ContinuousLinearMap.fst ℝ ℝ E).prod (ContinuousLinearMap.snd ℝ ℝ E)

@[simp]

theorem EulerTimeRescaling.coordinates_apply {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ε : ℝ) (q : ℝ × E) : (coordinates ε) q = (ε⁻¹ * q.1, q.2)

noncomputable def EulerTimeRescaling.velocity {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ε : ℝ) (u : ℝ × E → E) (q : ℝ × E) : E

Velocity, given by ε⁻¹ • u (coordinates ε q).

Equations

• EulerTimeRescaling.velocity ε u q = ε⁻¹ • u ((EulerTimeRescaling.coordinates ε) q)

noncomputable def EulerTimeRescaling.pressure {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ε : ℝ) (p : ℝ × E → ℝ) (q : ℝ × E) : ℝ

Pressure, given by (ε⁻¹)^2*p (coordinates ε q).

Equations

• EulerTimeRescaling.pressure ε p q = ε⁻¹ ^ 2 * p ((EulerTimeRescaling.coordinates ε) q)

theorem EulerTimeRescaling.velocity_hasFDerivAt {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ε : ℝ) (u : ℝ × E → E) (q : ℝ × E) (hu : DifferentiableAt ℝ u ((coordinates ε) q)) : HasFDerivAt (velocity ε u) (ε⁻¹ • fderiv ℝ u ((coordinates ε) q) ∘SL coordinates ε) q

theorem EulerTimeRescaling.pressure_gradient {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (ε : ℝ) (p : ℝ × E → ℝ) (q : ℝ × E) (hp : DifferentiableAt ℝ (fun (y : E) => p (ε⁻¹ * q.1, y)) q.2) : gradient (fun (y : E) => pressure ε p (q.1, y)) q.2 = ε⁻¹ ^ 2 • gradient (fun (y : E) => p (ε⁻¹ * q.1, y)) q.2

theorem EulerTimeRescaling.momentumResidual_eq {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (ε : ℝ) (u : ℝ × E → E) (p : ℝ × E → ℝ) (q : ℝ × E) (hu : DifferentiableAt ℝ u ((coordinates ε) q)) (hp : DifferentiableAt ℝ (fun (y : E) => p (ε⁻¹ * q.1, y)) q.2) : EulerLagrangian.momentumResidual (velocity ε u) (pressure ε p) q = ε⁻¹ ^ 2 • EulerLagrangian.momentumResidual u p ((coordinates ε) q)

theorem EulerTimeRescaling.momentumResidual_zero {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (ε : ℝ) (u : ℝ × E → E) (p : ℝ × E → ℝ) (q : ℝ × E) (hu : DifferentiableAt ℝ u ((coordinates ε) q)) (hp : DifferentiableAt ℝ (fun (y : E) => p (ε⁻¹ * q.1, y)) q.2) (he : EulerLagrangian.momentumResidual u p ((coordinates ε) q) = 0) : EulerLagrangian.momentumResidual (velocity ε u) (pressure ε p) q = 0

theorem EulerTimeRescaling.spatial_derivative {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ε : ℝ) (u : ℝ × E → E) (t : ℝ) (x : E) (hu : DifferentiableAt ℝ (fun (y : E) => u (ε⁻¹ * t, y)) x) : fderiv ℝ (fun (y : E) => velocity ε u (t, y)) x = ε⁻¹ • fderiv ℝ (fun (y : E) => u (ε⁻¹ * t, y)) x

noncomputable def EulerTimeRescaling.timeMap (ε : ℝ) (hε : 0 < ε) : C(↑(Set.Icc 0 ε), ↑(Set.Icc 0 1))

Time map, bundling toFun, continuous_toFun.

Equations

• EulerTimeRescaling.timeMap ε hε = { toFun := fun (t : ↑(Set.Icc 0 ε)) => ⟨↑t / ε, ⋯⟩, continuous_toFun := ⋯ }

theorem EulerTimeRescaling.timeMap_initial (ε : ℝ) (hε : 0 < ε) : (timeMap ε hε) ⟨0, ⋯⟩ = ⟨0, ⋯⟩

theorem EulerTimeRescaling.scaled_time_interior (ε : ℝ) (hε : 0 < ε) (t : ℝ) (ht : t ∈ Set.Ioo 0 ε) : ε⁻¹ * t ∈ Set.Ioo 0 1

A positive-time classical Euler solution constructed from a genuine solenoidal Gevrey datum. The initial velocity is the original datum, not its small multiple. All spatial derivative tensors remain continuous L² paths after the actual Euler time/amplitude rescaling.

noncomputable def EulerStaticEuler.localVelocity (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space

Local velocity, given by EulerTimeRescaling.velocity (amplitude P C R hC hR) (EulerConstantEuler.velocity (exactPacket P u C R hC hR hu hdiv)).

Equations

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

noncomputable def EulerStaticEuler.localPressure (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : ℝ × EulerSmoothLimit.Space → ℝ

Local pressure, given by EulerTimeRescaling.pressure (amplitude P C R hC hR) (EulerConstantEuler.pressure (exactPacket P u C R hC hR hu hdiv)).

Equations

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

noncomputable def EulerStaticEuler.localForce (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (q : ℝ × EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Local force as an element of Space.

Equations

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

theorem EulerStaticEuler.unit_initial (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (x : EulerSmoothLimit.Space) : EulerConstantEuler.velocity (exactPacket P u C R hC hR hu hdiv) (0, x) = amplitude P C R hC hR • u.field x

theorem EulerStaticEuler.localVelocity_initial (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (x : EulerSmoothLimit.Space) : localVelocity P u C R hC hR hu hdiv (0, x) = u.field x

theorem EulerStaticEuler.localMomentum (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ℝ) (ht : t ∈ Set.Ioo 0 (amplitude P C R hC hR)) (x : EulerSmoothLimit.Space) : EulerLagrangian.momentumResidual (localVelocity P u C R hC hR hu hdiv) (localPressure P u C R hC hR hu hdiv) (t, x) = 0

theorem EulerStaticEuler.localVelocity_differentiableAt (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ℝ) (ht : t ∈ Set.Ioo 0 (amplitude P C R hC hR)) (x : EulerSmoothLimit.Space) : DifferentiableAt ℝ (localVelocity P u C R hC hR hu hdiv) (t, x)

theorem EulerStaticEuler.localVelocity_divergence (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ℝ) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => localVelocity P u C R hC hR hu hdiv (t, y)) x = 0

theorem EulerStaticEuler.localVelocity_joint_continuous (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : Continuous (localVelocity P u C R hC hR hu hdiv)

theorem EulerStaticEuler.localPressure_joint_continuous (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : Continuous (localPressure P u C R hC hR hu hdiv)

theorem EulerStaticEuler.localForce_joint_continuous (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : Continuous (localForce P u C R hC hR hu hdiv)

theorem EulerStaticEuler.localPressure_gradient (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ℝ) (x : EulerSmoothLimit.Space) : gradient (fun (y : EulerSmoothLimit.Space) => localPressure P u C R hC hR hu hdiv (t, y)) x = localForce P u C R hC hR hu hdiv (t, x)

theorem EulerStaticEuler.localPressure_smooth (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ℝ) : ContDiff ℝ ↑⊤ fun (x : EulerSmoothLimit.Space) => localPressure P u C R hC hR hu hdiv (t, x)

theorem EulerStaticEuler.localPressure_zero (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ℝ) : localPressure P u C R hC hR hu hdiv (t, 0) = 0

noncomputable def EulerStaticEuler.localField (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Local field, constructed using SmoothL2Field.mapField.

Equations

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

theorem EulerStaticEuler.localField_apply (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) (x : EulerSmoothLimit.Space) : (localField P u C R hC hR hu hdiv t).field x = localVelocity P u C R hC hR hu hdiv (↑t, x)

theorem EulerStaticEuler.localField_jetLp_continuous (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) => (localField P u C R hC hR hu hdiv t).jetLp n

theorem EulerStaticEuler.localVelocity_smooth (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) : ContDiff ℝ ↑⊤ fun (x : EulerSmoothLimit.Space) => localVelocity P u C R hC hR hu hdiv (↑t, x)

The locally constructed ordinary Euler solution supplies a concrete first parent, its label budget and its genuine particle inverse. All constants and the positive common horizon depend only on the input Gevrey envelope, not on the particular initial datum.

Actual smooth coefficient paths and their true time derivatives under the Euler amplitude/time scaling. The time interval is shortened by the same positive amplitude used to normalize the initial velocity.

noncomputable def EulerTimeRescaling.coefficient {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (ε : ℝ) (hε : 0 < ε) (A : SmoothTimeField (↑(Set.Icc 0 1)) E V) : SmoothTimeField (↑(Set.Icc 0 ε)) E V

Coefficient, given by (A.compTime (timeMap ε hε)).map (ε⁻¹ • ContinuousLinearMap.id ℝ V).

Equations

• EulerTimeRescaling.coefficient ε hε A = SmoothTimeField.map (ε⁻¹ • ContinuousLinearMap.id ℝ V) (A.compTime (EulerTimeRescaling.timeMap ε hε))

noncomputable def EulerTimeRescaling.derivativeCoefficient {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (ε : ℝ) (hε : 0 < ε) (A : SmoothTimeField (↑(Set.Icc 0 1)) E V) : SmoothTimeField (↑(Set.Icc 0 ε)) E V

Derivative coefficient, given by (A.compTime (timeMap ε hε)).map ((ε⁻¹)^2 • ContinuousLinearMap.id ℝ V).

Equations

• EulerTimeRescaling.derivativeCoefficient ε hε A = SmoothTimeField.map (ε⁻¹ ^ 2 • ContinuousLinearMap.id ℝ V) (A.compTime (EulerTimeRescaling.timeMap ε hε))

theorem EulerTimeRescaling.coefficient_time {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (ε : ℝ) (hε : 0 < ε) (A A₁ : SmoothTimeField (↑(Set.Icc 0 1)) E V) (h : SmoothTimeField.TimeDerivative 1 ⋯ A A₁) : SmoothTimeField.TimeDerivative ε ⋯ (coefficient ε hε A) (derivativeCoefficient ε hε A₁)

The constructed static-datum solution and its actual time derivative have smooth bounded spatial jets continuous in time. This includes the one-sided derivatives at both endpoints.

noncomputable def EulerStaticEuler.unitVelocityCoefficient (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : SmoothTimeField (↑(Set.Icc 0 1)) EulerSmoothLimit.Space EulerSmoothLimit.Space

Unit velocity coefficient as an element of SmoothTimeField (Icc (0 : ℝ) 1) Space Space.

Equations

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

noncomputable def EulerStaticEuler.unitDerivativeCoefficient (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : SmoothTimeField (↑(Set.Icc 0 1)) EulerSmoothLimit.Space EulerSmoothLimit.Space

Unit derivative coefficient as an element of SmoothTimeField (Icc (0 : ℝ) 1) Space Space.

Equations

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

noncomputable def EulerStaticEuler.unitForceCoefficient (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : SmoothTimeField (↑(Set.Icc 0 1)) EulerSmoothLimit.Space EulerSmoothLimit.Space

Unit force coefficient, given by (exactPacket P u C R hC hR hu hdiv).pressure.toSmoothTimeField.precompLinear (ContinuousLinearMap.inl ℝ Space ℝ).

Equations

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

theorem EulerStaticEuler.unitCoefficient_time (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : SmoothTimeField.TimeDerivative 1 ⋯ (unitVelocityCoefficient P u C R hC hR hu hdiv) (unitDerivativeCoefficient P u C R hC hR hu hdiv)

theorem EulerStaticEuler.unitVelocityCoefficient_apply (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 1)) (x : EulerSmoothLimit.Space) : ((unitVelocityCoefficient P u C R hC hR hu hdiv).field t) x = EulerConstantEuler.velocity (exactPacket P u C R hC hR hu hdiv) (↑t, x)

theorem EulerStaticEuler.unitForceCoefficient_apply (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 1)) (x : EulerSmoothLimit.Space) : ((unitForceCoefficient P u C R hC hR hu hdiv).field t) x = EulerConstantEuler.force (exactPacket P u C R hC hR hu hdiv) (↑t, x)

noncomputable def EulerStaticEuler.velocityCoefficient (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : SmoothTimeField (↑(Set.Icc 0 (amplitude P C R hC hR))) EulerSmoothLimit.Space EulerSmoothLimit.Space

Velocity coefficient, given by EulerTimeRescaling.coefficient (amplitude P C R hC hR) (amplitude_pos P C R hC hR) (unitVelocityCoefficient P u C R hC hR hu hdiv).

Equations

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

noncomputable def EulerStaticEuler.derivativeCoefficient (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : SmoothTimeField (↑(Set.Icc 0 (amplitude P C R hC hR))) EulerSmoothLimit.Space EulerSmoothLimit.Space

Derivative coefficient, constructed using EulerTimeRescaling.derivativeCoefficient.

Equations

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

noncomputable def EulerStaticEuler.forceCoefficient (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : SmoothTimeField (↑(Set.Icc 0 (amplitude P C R hC hR))) EulerSmoothLimit.Space EulerSmoothLimit.Space

Force coefficient, constructed using EulerTimeRescaling.derivativeCoefficient.

Equations

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

theorem EulerStaticEuler.coefficient_time (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : SmoothTimeField.TimeDerivative (amplitude P C R hC hR) ⋯ (velocityCoefficient P u C R hC hR hu hdiv) (derivativeCoefficient P u C R hC hR hu hdiv)

Uniform source-only Gevrey bounds for the actual local Euler solution and its genuine time derivative. The same spatial radius works for sup and ordinary L² norms. All constants depend only on P,C,R, not on the particular solenoidal datum realizing the input bounds.

Explicit bounds for the constructed small-data solution. All constants are functions of the datum's supplied Gevrey bounds and the fixed period; none depends on which datum realizes those bounds.

noncomputable def EulerStaticEuler.retainedRadius (R : ℝ) : ℝ

A fixed positive radius retained by the actual correction.

Equations

• EulerStaticEuler.retainedRadius R = EulerSmallCorrection.initialRadius (EulerStaticEuler.mixedRadius R) / 4

noncomputable def EulerStaticEuler.baseErrorFactor : ℝ

Base error factor, given by metricAmplification 1/2.

Equations

• EulerStaticEuler.baseErrorFactor = EulerGevreyMetricEstimate.metricAmplification 1 / 2

theorem EulerStaticEuler.retainedRadius_pos (R : ℝ) (hR : 0 ≤ R) : 0 < retainedRadius R

theorem EulerStaticEuler.retainedRadius_small (R : ℝ) (hR : 0 ≤ R) : retainedRadius R * mixedRadius R ≤ 1 / 2

theorem EulerStaticEuler.baseErrorFactor_nonneg : 0 ≤ baseErrorFactor

noncomputable def EulerStaticEuler.staticSourceCost (P : ℝ) [Fact (0 < P)] (R : ℝ) : ℝ

Static source cost, given by sourceBound P 1 1 0 0 1 baseErrorFactor ((8/EulerSmallCorrection.initialRadius (mixedRadius R))*baseErrorFactor).

Equations

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

noncomputable def EulerStaticEuler.staticTimeCost (P : ℝ) [Fact (0 < P)] (R : ℝ) : ℝ

Static time cost, given by (1+2*pressureBound*(448*1+1))*staticSourceCost P R.

Equations

• EulerStaticEuler.staticTimeCost P R = (1 + 2 * EulerConstantCorrection.pressureBound * (448 * 1 + 1)) * EulerStaticEuler.staticSourceCost P R

noncomputable def EulerStaticEuler.staticPressureCost (P : ℝ) [Fact (0 < P)] (R : ℝ) : ℝ

Static pressure cost, given by 2*pressureBound*staticSourceCost P R.

Equations

• EulerStaticEuler.staticPressureCost P R = 2 * EulerConstantCorrection.pressureBound * EulerStaticEuler.staticSourceCost P R

theorem EulerStaticEuler.staticSourceCost_nonneg (P : ℝ) [Fact (0 < P)] (R : ℝ) (hR : 0 ≤ R) : 0 ≤ staticSourceCost P R

theorem EulerStaticEuler.staticTimeCost_nonneg (P : ℝ) [Fact (0 < P)] (R : ℝ) (hR : 0 ≤ R) : 0 ≤ staticTimeCost P R

theorem EulerStaticEuler.staticPressureCost_nonneg (P : ℝ) [Fact (0 < P)] (R : ℝ) (hR : 0 ≤ R) : 0 ≤ staticPressureCost P R

theorem EulerStaticEuler.budget_retainedRadius (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : EulerAllOrderDriftCorrection.Budget.reducedRadius P (correctionBudget P u C R hC hR hu hdiv) = retainedRadius R

theorem EulerStaticEuler.budget_staticTimeCost (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (q : ℕ) (hq : 6 ≤ q) : EulerAllOrderDriftCorrection.Budget.timeDerivativeCost P (correctionBudget P u C R hC hR hu hdiv) q hq = staticTimeCost P R

theorem EulerStaticEuler.budget_staticPressureCost (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (q : ℕ) (hq : 6 ≤ q) : EulerAllOrderDriftCorrection.Budget.pressureCost P (correctionBudget P u C R hC hR hu hdiv) q hq = staticPressureCost P R

theorem EulerStaticEuler.correction_weighted (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (n : ℕ) (t : ↑(Set.Icc 0 1)) : EulerSobolevGevreyOperators.weightedNorm P 6 n (retainedRadius R) (((EulerAllOrderDriftCorrection.Budget.fieldTower P (correctionBudget P u C R hC hR hu hdiv)).realization (n + 6)) t) ≤ amplitude P C R hC hR * baseErrorFactor

theorem EulerStaticEuler.exact_weighted (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (n : ℕ) (t : ↑(Set.Icc 0 1)) : EulerSobolevGevreyOperators.weightedNorm P 6 n (retainedRadius R) (((exactPacket P u C R hC hR hu hdiv).velocity.realization (n + 6)) t) ≤ amplitude P C R hC hR * (2 * mixedAmplitude P C R + baseErrorFactor)

theorem EulerStaticEuler.time_weighted (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (n : ℕ) (t : ↑(Set.Icc 0 1)) : EulerSobolevGevreyOperators.weightedNorm P 6 n (retainedRadius R) (((EulerAllOrderDriftCorrection.Budget.timeDerivativeTower P (correctionBudget P u C R hC hR hu hdiv)).realization (n + 6)) t) ≤ amplitude P C R hC hR * staticTimeCost P R

theorem EulerStaticEuler.pressure_weighted (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (n : ℕ) (t : ↑(Set.Icc 0 1)) : EulerSobolevGevreyOperators.weightedNorm P 6 n (retainedRadius R) (((EulerAllOrderDriftCorrection.Budget.pressureTower P (correctionBudget P u C R hC hR hu hdiv)).realization (n + 6)) t) ≤ amplitude P C R hC hR * staticPressureCost P R

Quantitative spatial jet bounds under actual Euler time/amplitude rescaling. The constants are explicit and the spatial radius is unchanged.

@[instance_reducible]

noncomputable def EulerTimeRescaling.instSmoothTimeAmplitudeBounds1 {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] V)

Cache the standard NormedAddCommGroup (E [×n]→L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerTimeRescaling.instSmoothTimeAmplitudeBounds1 n = inferInstance

@[instance_reducible]

noncomputable def EulerTimeRescaling.instSmoothTimeAmplitudeBounds2 {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] V)

Cache the standard NormedSpace ℝ (E [×n]→L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerTimeRescaling.instSmoothTimeAmplitudeBounds2 n = inferInstance

@[instance_reducible]

noncomputable def EulerTimeRescaling.instSmoothTimeAmplitudeBounds3 {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction E (E [×n]→L[ℝ] V))

Cache the standard NormedAddCommGroup (E →ᵇ (E [×n]→L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• EulerTimeRescaling.instSmoothTimeAmplitudeBounds3 n = inferInstance

@[instance_reducible]

noncomputable def EulerTimeRescaling.instSmoothTimeAmplitudeBounds4 {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction E (E [×n]→L[ℝ] V))

Cache the standard NormedSpace ℝ (E →ᵇ (E [×n]→L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• EulerTimeRescaling.instSmoothTimeAmplitudeBounds4 n = inferInstance

theorem EulerTimeRescaling.smul_id_norm_le {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℝ) (ha : 0 ≤ a) : ‖a • ContinuousLinearMap.id ℝ V‖ ≤ a

theorem EulerTimeRescaling.coefficient_jet_norm {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (ε : ℝ) (hε : 0 < ε) (A : SmoothTimeField (↑(Set.Icc 0 1)) E V) (n : ℕ) : ‖(coefficient ε hε A).jet n‖ ≤ ε⁻¹ * ‖A.jet n‖

theorem EulerTimeRescaling.derivativeCoefficient_jet_norm {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (ε : ℝ) (hε : 0 < ε) (A : SmoothTimeField (↑(Set.Icc 0 1)) E V) (n : ℕ) : ‖(derivativeCoefficient ε hε A).jet n‖ ≤ ε⁻¹ ^ 2 * ‖A.jet n‖

theorem EulerTimeRescaling.mapField_hasJetBound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℝ) (ha : 0 ≤ a) (F : EulerLpTranslation.SmoothL2Field V) (C R : ℝ) (hF : F.HasJetBound C R) : (EulerLpTranslation.SmoothL2Field.mapField (a • ContinuousLinearMap.id ℝ V) F).HasJetBound (a * C) R

@[instance_reducible]

noncomputable def EulerStaticEuler.instStaticEulerGevrey1 : NormedAddCommGroup EulerSmoothLimit.Space

Cache the standard NormedAddCommGroup Space instance to shorten typeclass synthesis.

Equations

• EulerStaticEuler.instStaticEulerGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerStaticEuler.instStaticEulerGevrey2 : NormedSpace ℝ EulerSmoothLimit.Space

Cache the standard NormedSpace ℝ Space instance to shorten typeclass synthesis.

Equations

• EulerStaticEuler.instStaticEulerGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerStaticEuler.instStaticEulerGevrey3 (n : ℕ) : NormedAddCommGroup (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerStaticEuler.instStaticEulerGevrey3 n = inferInstance

@[instance_reducible]

noncomputable def EulerStaticEuler.instStaticEulerGevrey4 (n : ℕ) : NormedSpace ℝ (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerStaticEuler.instStaticEulerGevrey4 n = inferInstance

@[instance_reducible]

noncomputable def EulerStaticEuler.instStaticEulerGevrey5 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerStaticEuler.instStaticEulerGevrey5 n = inferInstance

@[instance_reducible]

noncomputable def EulerStaticEuler.instStaticEulerGevrey6 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerStaticEuler.instStaticEulerGevrey6 n = inferInstance

noncomputable def EulerStaticEuler.coverRadius (R : ℝ) : ℝ

Cover radius, given by ‖coordinateEquiv.symm.toContinuousLinearMap‖*(retainedRadius R)⁻¹.

Equations

• EulerStaticEuler.coverRadius R = ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * (EulerStaticEuler.retainedRadius R)⁻¹

noncomputable def EulerStaticEuler.outputRadius (R : ℝ) : ℝ

Output radius, given by 1+4*coverRadius R.

Equations

• EulerStaticEuler.outputRadius R = 1 + 4 * EulerStaticEuler.coverRadius R

theorem EulerStaticEuler.coverRadius_nonneg (R : ℝ) (hR : 0 ≤ R) : 0 ≤ coverRadius R

theorem EulerStaticEuler.outputRadius_pos (R : ℝ) (hR : 0 ≤ R) : 0 < outputRadius R

noncomputable def EulerStaticEuler.graphCost (P : ℝ) [Fact (0 < P)] (R : ℝ) : ℝ

Graph cost, given by 1+sobolevEmbeddingConstant P 3+Real.sqrt (2/P+2*P)*(1+coverRadius R).

Equations

• EulerStaticEuler.graphCost P R = 1 + EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 + √(2 / P + 2 * P) * (1 + EulerStaticEuler.coverRadius R)

noncomputable def EulerStaticEuler.outputVelocitySize (P : ℝ) [Fact (0 < P)] (C R : ℝ) : ℝ

Output velocity size, given by graphCost P R*(2*mixedAmplitude P C R+baseErrorFactor).

Equations

• EulerStaticEuler.outputVelocitySize P C R = EulerStaticEuler.graphCost P R * (2 * EulerStaticEuler.mixedAmplitude P C R + EulerStaticEuler.baseErrorFactor)

noncomputable def EulerStaticEuler.outputDerivativeSize (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : ℝ

Output derivative size, given by (amplitude P C R hC hR)⁻¹*graphCost P R*staticTimeCost P R.

Equations

• EulerStaticEuler.outputDerivativeSize P C R hC hR = (EulerStaticEuler.amplitude P C R hC hR)⁻¹ * EulerStaticEuler.graphCost P R * EulerStaticEuler.staticTimeCost P R

theorem EulerStaticEuler.graphCost_nonneg (P : ℝ) [Fact (0 < P)] (R : ℝ) (hR : 0 ≤ R) : 0 ≤ graphCost P R

theorem EulerStaticEuler.outputVelocitySize_nonneg (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : 0 ≤ outputVelocitySize P C R

theorem EulerStaticEuler.outputDerivativeSize_nonneg (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : 0 ≤ outputDerivativeSize P C R hC hR

theorem EulerStaticEuler.unitVelocityCoefficient_graph (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 1)) (x : EulerSmoothLimit.Space) : ((unitVelocityCoefficient P u C R hC hR hu hdiv).field t) x = ((exactPacket P u C R hC hR hu hdiv).velocity.zeroGraphCoefficient.field t) x

theorem EulerStaticEuler.unitDerivativeCoefficient_graph (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 1)) (x : EulerSmoothLimit.Space) : ((unitDerivativeCoefficient P u C R hC hR hu hdiv).field t) x = ((EulerAllOrderDriftCorrection.Budget.timeDerivativeTower P (correctionBudget P u C R hC hR hu hdiv)).zeroGraphCoefficient.field t) x

noncomputable def EulerStaticEuler.localDerivativeField (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Local derivative field, constructed using SmoothL2Field.mapField.

Equations

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

theorem EulerStaticEuler.localDerivativeField_apply (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) (x : EulerSmoothLimit.Space) : (localDerivativeField P u C R hC hR hu hdiv t).field x = ((derivativeCoefficient P u C R hC hR hu hdiv).field t) x

theorem EulerStaticEuler.velocityCoefficient_bound (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (n : ℕ) : ‖(velocityCoefficient P u C R hC hR hu hdiv).jet n‖ ≤ outputVelocitySize P C R * outputRadius R ^ n * ↑n.factorial ^ 2

theorem EulerStaticEuler.derivativeCoefficient_bound (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (n : ℕ) : ‖(derivativeCoefficient P u C R hC hR hu hdiv).jet n‖ ≤ outputDerivativeSize P C R hC hR * outputRadius R ^ n * ↑n.factorial ^ 2

theorem EulerStaticEuler.localField_bound (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) : (localField P u C R hC hR hu hdiv t).HasJetBound (outputVelocitySize P C R) (outputRadius R)

theorem EulerStaticEuler.localDerivativeField_bound (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) : (localDerivativeField P u C R hC hR hu hdiv t).HasJetBound (outputDerivativeSize P C R hC hR) (outputRadius R)

The genuine ordinary flow of a smooth divergence-free velocity gives the first parent particle data. Its horizon can be shortened by an explicit positive amount before applying the uniform flow-jet estimate.

@[instance_reducible]

noncomputable def EulerBaseEulerParent.instBaseEulerParent1 (n : ℕ) : NormedAddCommGroup (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerBaseEulerParent.instBaseEulerParent1 n = inferInstance

@[instance_reducible]

noncomputable def EulerBaseEulerParent.instBaseEulerParent2 (n : ℕ) : NormedSpace ℝ (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerBaseEulerParent.instBaseEulerParent2 n = inferInstance

@[instance_reducible]

noncomputable def EulerBaseEulerParent.instBaseEulerParent3 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerBaseEulerParent.instBaseEulerParent3 n = inferInstance

@[instance_reducible]

noncomputable def EulerBaseEulerParent.instBaseEulerParent4 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerBaseEulerParent.instBaseEulerParent4 n = inferInstance

structure EulerBaseEulerParent.Input : Type

Input data, collecting T, T_pos, field, derivative, time_derivative, divergence and their compatibility conditions.

• T : ℝ

  Time horizon of Input, of type ℝ.

• T_pos : 0 < self.T
• field : SmoothTimeField (↑(Set.Icc 0 self.T)) EulerSmoothLimit.Space EulerSmoothLimit.Space

  Underlying field of Input, of type SmoothTimeField (Icc (0 : ℝ) T) Space Space.

• derivative : SmoothTimeField (↑(Set.Icc 0 self.T)) EulerSmoothLimit.Space EulerSmoothLimit.Space

  Derivative field of Input, of type SmoothTimeField (Icc (0 : ℝ) T) Space Space.

• time_derivative : SmoothTimeField.TimeDerivative self.T ⋯ self.field self.derivative
• divergence (t : ↑(Set.Icc 0 self.T)) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (⇑(self.field.field t)) x = 0
• B : ℝ

  Bound parameter of Input, of type ℝ.

• R : ℝ

  Radius parameter of Input, of type ℝ.

• B_nonneg : 0 ≤ self.B
• R_pos : 0 < self.R
• small : self.B * self.R * self.T ≤ 1 / 8
• bound (n : ℕ) : ‖self.field.jet n‖ ≤ self.B * self.R ^ n * ↑n.factorial ^ 2

noncomputable def EulerBaseEulerParent.Input.displacement (I : Input) : SmoothTimeField (↑(Set.Icc 0 I.T)) EulerSmoothLimit.Space EulerSmoothLimit.Space

Displacement, given by displacementCoefficient I.T I.T_pos.le I.field I.B I.R I.B_nonneg I.R_pos I.small I.bound.

Equations

• I.displacement = EulerSmoothBanachFlow.displacementCoefficient I.T ⋯ I.field I.B I.R ⋯ ⋯ ⋯ ⋯

noncomputable def EulerBaseEulerParent.Input.velocity (I : Input) : SmoothTimeField (↑(Set.Icc 0 I.T)) EulerSmoothLimit.Space EulerSmoothLimit.Space

Velocity, given by I.field.compDisplacement I.displacement.

Equations

• I.velocity = I.field.compDisplacement I.displacement

noncomputable def EulerBaseEulerParent.Input.acceleration (I : Input) : SmoothTimeField (↑(Set.Icc 0 I.T)) EulerSmoothLimit.Space EulerSmoothLimit.Space

Acceleration, given by accelerationCoefficient I.T I.T_pos.le I.field I.B I.R I.B_nonneg I.R_pos I.small I.bound I.derivative.

Equations

• I.acceleration = EulerSmoothBanachFlow.accelerationCoefficient I.T ⋯ I.field I.B I.R ⋯ ⋯ ⋯ ⋯ I.derivative

@[simp]

theorem EulerBaseEulerParent.Input.displacement_apply (I : Input) (t : ↑(Set.Icc 0 I.T)) (x : EulerSmoothLimit.Space) : (I.displacement.field t) x = (EulerSmoothBanachFlow.flowData I.T ⋯ I.field).forward (↑t) x - x

@[simp]

theorem EulerBaseEulerParent.Input.velocity_apply (I : Input) (t : ↑(Set.Icc 0 I.T)) (x : EulerSmoothLimit.Space) : (I.velocity.field t) x = (EulerSmoothBanachFlow.velocityFamily I.T ⋯ I.field x) t

@[simp]

theorem EulerBaseEulerParent.Input.acceleration_apply (I : Input) (t : ↑(Set.Icc 0 I.T)) (x : EulerSmoothLimit.Space) : (I.acceleration.field t) x = (EulerSmoothBanachFlow.accelerationFamily I.T ⋯ I.field I.derivative x) t

theorem EulerBaseEulerParent.Input.displacement_time (I : Input) : SmoothTimeField.TimeDerivative I.T ⋯ I.displacement I.velocity

theorem EulerBaseEulerParent.Input.velocity_time (I : Input) : SmoothTimeField.TimeDerivative I.T ⋯ I.velocity I.acceleration

theorem EulerBaseEulerParent.Input.displacement_initial (I : Input) (x : EulerSmoothLimit.Space) : (I.displacement.field ⟨0, ⋯⟩) x = 0

theorem EulerBaseEulerParent.Input.displacement_det (I : Input) (t : ↑(Set.Icc 0 I.T)) (x : EulerSmoothLimit.Space) : (ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ (⇑(I.displacement.field t)) x).det = 1

noncomputable def EulerBaseEulerParent.Input.parent (I : Input) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.Parent

Parent, bundling T, T_pos, ell, ell_pos and the required compatibility proofs.

Equations

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

theorem EulerBaseEulerParent.Input.parent_position (I : Input) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 I.T)) (x : EulerSmoothLimit.Space) : (I.parent ell hell hell1).position t x = (EulerSmoothBanachFlow.flowData I.T ⋯ I.field).forward (↑t) x

noncomputable def EulerBaseEulerParent.Input.particleInverse (I : Input) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.ParticleInverse (I.parent ell hell hell1)

Particle inverse, bundling field, left_inverse, right_inverse, continuous and the required compatibility proofs.

Equations

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

theorem EulerBaseEulerParent.Input.parent_velocity (I : Input) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 I.T)) (x : EulerSmoothLimit.Space) : ((I.parent ell hell hell1).velocity.field t) x = (I.field.field t) ((I.parent ell hell hell1).position t x)

noncomputable def EulerBaseEulerParent.horizon (T B R : ℝ) : ℝ

Horizon, given by min T (1/(8*(1+B*R))).

Equations

• EulerBaseEulerParent.horizon T B R = min T (1 / (8 * (1 + B * R)))

theorem EulerBaseEulerParent.horizon_pos (T B R : ℝ) (hT : 0 < T) (hB : 0 ≤ B) (hR : 0 ≤ R) : 0 < horizon T B R

theorem EulerBaseEulerParent.horizon_le (T B R : ℝ) : horizon T B R ≤ T

theorem EulerBaseEulerParent.horizon_small (T B R : ℝ) (hT : 0 < T) (hB : 0 ≤ B) (hR : 0 ≤ R) : B * R * horizon T B R ≤ 1 / 8

noncomputable def EulerBaseEulerParent.ofInterval (T : ℝ) (hT : 0 < T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) EulerSmoothLimit.Space EulerSmoothLimit.Space) (htime : SmoothTimeField.TimeDerivative T ⋯ A A₁) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (⇑(A.field t)) x = 0) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) : Input

Of interval, bundling T, T_pos, field, derivative and the required compatibility proofs.

Equations

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

The three actual base-flow fields satisfy the source's fixed-H6 label bound with one explicit constant, independent of derivative order.

Actual ordinary L² displacement, material velocity and acceleration for the base flow. The displacement estimate integrates the real spatial jets of the flow, and the other two estimates use volume preservation.

@[instance_reducible]

noncomputable def EulerBaseEulerParent.instBaseEulerFlowL21 (n : ℕ) : NormedAddCommGroup (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerBaseEulerParent.instBaseEulerFlowL21 n = inferInstance

@[instance_reducible]

noncomputable def EulerBaseEulerParent.instBaseEulerFlowL22 (n : ℕ) : NormedSpace ℝ (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerBaseEulerParent.instBaseEulerFlowL22 n = inferInstance

@[instance_reducible]

noncomputable def EulerBaseEulerParent.instBaseEulerFlowL23 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerBaseEulerParent.instBaseEulerFlowL23 n = inferInstance

@[instance_reducible]

noncomputable def EulerBaseEulerParent.instBaseEulerFlowL24 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerBaseEulerParent.instBaseEulerFlowL24 n = inferInstance

structure EulerBaseEulerParent.L2Data (I : Input) : Type

L² data, collecting velocity, derivative, velocity_match, derivative_match, C, S and their compatibility conditions.

• velocity : ↑(Set.Icc 0 I.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Velocity field of L2Data, of type Icc (0 : ℝ) I.T → SmoothL2Field Space.

• derivative : ↑(Set.Icc 0 I.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Derivative field of L2Data, of type Icc (0 : ℝ) I.T → SmoothL2Field Space.

• velocity_match (t : ↑(Set.Icc 0 I.T)) (x : EulerSmoothLimit.Space) : (self.velocity t).field x = (I.field.field t) x
• derivative_match (t : ↑(Set.Icc 0 I.T)) (x : EulerSmoothLimit.Space) : (self.derivative t).field x = (I.derivative.field t) x
• C : ℝ

  Bound coefficient of L2Data, of type ℝ.

• S : ℝ

  Parameter S of L2Data, of type ℝ.

• C₁ : ℝ

  First-derivative bound coefficient of L2Data, of type ℝ.

• S₁ : ℝ

  Parameter S₁ of L2Data, of type ℝ.

• C_nonneg : 0 ≤ self.C
• S_nonneg : 0 ≤ self.S
• C₁_nonneg : 0 ≤ self.C₁
• S₁_nonneg : 0 ≤ self.S₁
• velocity_bound (t : ↑(Set.Icc 0 I.T)) : (self.velocity t).HasJetBound self.C self.S
• derivative_bound (t : ↑(Set.Icc 0 I.T)) : (self.derivative t).HasJetBound self.C₁ self.S₁

def EulerBaseEulerParent.L2Data.velocityRadius {I : Input} (L : L2Data I) : ℝ

Velocity radius, given by flowRadius I.B I.R I.T L.S.

Equations

• L.velocityRadius = EulerSmoothFlowGevrey.flowRadius I.B I.R I.T L.S

theorem EulerBaseEulerParent.L2Data.velocityRadius_nonneg {I : Input} (L : L2Data I) : 0 ≤ L.velocityRadius

noncomputable def EulerBaseEulerParent.L2Data.velocityField {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Velocity field, constructed using SmoothL2Field.composeField.

Equations

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

theorem EulerBaseEulerParent.L2Data.velocityField_bound {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : (L.velocityField t).HasJetBound L.C L.velocityRadius

theorem EulerBaseEulerParent.L2Data.velocityField_apply {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) (x : EulerSmoothLimit.Space) : (L.velocityField t).field x = (I.velocity.field t) x

theorem EulerBaseEulerParent.L2Data.velocityField_jet {I : Input} (L : L2Data I) (n : ℕ) (t : ↑(Set.Icc 0 I.T)) : iteratedFDeriv ℝ n (L.velocityField t).field = fun (x : EulerSmoothLimit.Space) => ((I.velocity.jet n) t) x

theorem EulerBaseEulerParent.L2Data.displacement_jet_integral {I : Input} (n : ℕ) (t : ↑(Set.Icc 0 I.T)) (x : EulerSmoothLimit.Space) : ((I.displacement.jet n) t) x = ∫ (s : ℝ) in 0..↑t, (EulerVolterraConvolution.extendPath I.T ⋯ (I.velocity.jet n) s) x

theorem EulerBaseEulerParent.L2Data.displacement_memLp_and_bound {I : Input} (L : L2Data I) (n : ℕ) (t : ↑(Set.Icc 0 I.T)) : MeasureTheory.MemLp (iteratedFDeriv ℝ n ⇑(I.displacement.field t)) 2 MeasureTheory.volume ∧ (MeasureTheory.eLpNorm (iteratedFDeriv ℝ n ⇑(I.displacement.field t)) 2 MeasureTheory.volume).toReal ≤ I.T * L.C * L.velocityRadius ^ n * ↑n.factorial ^ 2

noncomputable def EulerBaseEulerParent.L2Data.displacementField {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Displacement field, bundling field, smooth, integrable.

Equations

• L.displacementField t = { field := ⇑(I.displacement.field t), smooth := ⋯, integrable := ⋯ }

theorem EulerBaseEulerParent.L2Data.displacementField_bound {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : (L.displacementField t).HasJetBound (I.T * L.C) L.velocityRadius

def EulerBaseEulerParent.L2Data.accelerationSourceRadius {I : Input} (L : L2Data I) : ℝ

Acceleration source radius, given by 4*I.R+L.S+L.S₁.

Equations

• L.accelerationSourceRadius = 4 * I.R + L.S + L.S₁

theorem EulerBaseEulerParent.L2Data.accelerationSourceRadius_nonneg {I : Input} (L : L2Data I) : 0 ≤ L.accelerationSourceRadius

theorem EulerBaseEulerParent.L2Data.field_derivative_bound {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : EulerGevrey.HasSupBound (fderiv ℝ ⇑(I.field.field t)) (I.B * I.R) L.accelerationSourceRadius

noncomputable def EulerBaseEulerParent.L2Data.accelerationProduct {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Acceleration product, constructed using SmoothL2Field.productField.

Equations

• L.accelerationProduct t = EulerLpTranslation.SmoothL2Field.productField (fderiv ℝ ⇑(I.field.field t)) ⋯ (L.velocity t) (I.B * I.R) L.C L.accelerationSourceRadius ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def EulerBaseEulerParent.L2Data.accelerationSource {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Acceleration source, given by SmoothL2Field.addField (L.derivative t) (L.accelerationProduct t).

Equations

• L.accelerationSource t = (L.derivative t).addField (L.accelerationProduct t)

def EulerBaseEulerParent.L2Data.accelerationAmplitude {I : Input} (L : L2Data I) : ℝ

Acceleration amplitude, given by L.C₁+3*(I.B*I.R)*L.C.

Equations

• L.accelerationAmplitude = L.C₁ + 3 * (I.B * I.R) * L.C

theorem EulerBaseEulerParent.L2Data.accelerationAmplitude_nonneg {I : Input} (L : L2Data I) : 0 ≤ L.accelerationAmplitude

theorem EulerBaseEulerParent.L2Data.accelerationSource_bound {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : (L.accelerationSource t).HasJetBound L.accelerationAmplitude L.accelerationSourceRadius

def EulerBaseEulerParent.L2Data.accelerationRadius {I : Input} (L : L2Data I) : ℝ

Acceleration radius, given by flowRadius I.B I.R I.T L.accelerationSourceRadius.

Equations

• L.accelerationRadius = EulerSmoothFlowGevrey.flowRadius I.B I.R I.T L.accelerationSourceRadius

theorem EulerBaseEulerParent.L2Data.accelerationRadius_nonneg {I : Input} (L : L2Data I) : 0 ≤ L.accelerationRadius

noncomputable def EulerBaseEulerParent.L2Data.accelerationField {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Acceleration field, constructed using SmoothL2Field.composeField.

Equations

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

theorem EulerBaseEulerParent.L2Data.accelerationField_bound {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : (L.accelerationField t).HasJetBound L.accelerationAmplitude L.accelerationRadius

theorem EulerBaseEulerParent.L2Data.accelerationField_apply {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) (x : EulerSmoothLimit.Space) : (L.accelerationField t).field x = (I.acceleration.field t) x

def EulerBaseEulerParent.L2Data.labelCost {I : Input} (L : L2Data I) : ℝ

Label cost, constructed using 1.

Equations

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

theorem EulerBaseEulerParent.L2Data.labelCost_one {I : Input} (L : L2Data I) : 1 ≤ L.labelCost

theorem EulerBaseEulerParent.L2Data.displacement_labelBound {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : EulerPacketParentLabelBounds.HasLabelBound L.labelCost (L.displacementField t)

theorem EulerBaseEulerParent.L2Data.velocity_labelBound {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : EulerPacketParentLabelBounds.HasLabelBound L.labelCost (L.velocityField t)

theorem EulerBaseEulerParent.L2Data.acceleration_labelBound {I : Input} (L : L2Data I) (t : ↑(Set.Icc 0 I.T)) : EulerPacketParentLabelBounds.HasLabelBound L.labelCost (L.accelerationField t)

noncomputable def EulerBaseEulerParent.L2Data.labelData {I : Input} (L : L2Data I) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.LabelData (I.parent ell hell hell1)

Label data, bundling K, K_one, displacement, velocity and the required compatibility proofs.

Equations

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

Odd initial velocity produces the actual odd local Euler velocity and odd pressure force. The scalar pressure, normalized at the origin, is even. These are consequences of correction uniqueness.

Odd static data give the genuine parity hypotheses of the constructed correction. In particular the actual convection residual is odd; this is proved from its derivative formula.

theorem EulerSmallCorrection.residual_odd {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (hodd : EulerPacketCylinderField.JointOdd T raw) (ε : ℝ) : EulerPacketCylinderField.JointOdd T fun (z : EulerPacketPointJets.Domain) => (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => (ε • raw) (z.1, y)) z.2) ((ε • raw) z, 0)

theorem EulerSmallCorrection.parityData {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (hodd : EulerPacketCylinderField.JointOdd T raw) (ε : ℝ) : EulerCorrectionAssembly.ParityData P (input G ε)

theorem EulerStaticEuler.symmetry (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hodd : ∀ (x : EulerSmoothLimit.Space), u.field (-x) = -u.field x) : EulerCorrectionAssembly.ParityData P (inputData P u C R hC hR)

theorem EulerStaticEuler.exactPacket_odd (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (hodd : ∀ (x : EulerSmoothLimit.Space), u.field (-x) = -u.field x) (t : ↑(Set.Icc 0 1)) : -(EulerCylinderReflection.reflection P) ((exactPacket P u C R hC hR hu hdiv).velocity.field t) = (exactPacket P u C R hC hR hu hdiv).velocity.field t

theorem EulerStaticEuler.unit_velocity_odd (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (hodd : ∀ (x : EulerSmoothLimit.Space), u.field (-x) = -u.field x) (t : ℝ) (x : EulerSmoothLimit.Space) : EulerConstantEuler.velocity (exactPacket P u C R hC hR hu hdiv) (t, -x) = -EulerConstantEuler.velocity (exactPacket P u C R hC hR hu hdiv) (t, x)

theorem EulerStaticEuler.unit_pressure_point (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 1)) (x : EulerLiftedGradientSpace.LiftDomain P) : (exactPacket P u C R hC hR hu hdiv).pressure.pointField t x = EulerAllOrderDriftCorrection.Budget.pointPressure P (correctionBudget P u C R hC hR hu hdiv) t x

theorem EulerStaticEuler.unit_force_odd (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (hodd : ∀ (x : EulerSmoothLimit.Space), u.field (-x) = -u.field x) (t : ℝ) (x : EulerSmoothLimit.Space) : EulerConstantEuler.force (exactPacket P u C R hC hR hu hdiv) (t, -x) = -EulerConstantEuler.force (exactPacket P u C R hC hR hu hdiv) (t, x)

theorem EulerStaticEuler.unit_pressure_even (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (hodd : ∀ (x : EulerSmoothLimit.Space), u.field (-x) = -u.field x) (t : ℝ) (x : EulerSmoothLimit.Space) : EulerConstantEuler.pressure (exactPacket P u C R hC hR hu hdiv) (t, -x) = EulerConstantEuler.pressure (exactPacket P u C R hC hR hu hdiv) (t, x)

theorem EulerStaticEuler.localVelocity_odd (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (hodd : ∀ (x : EulerSmoothLimit.Space), u.field (-x) = -u.field x) (t : ℝ) (x : EulerSmoothLimit.Space) : localVelocity P u C R hC hR hu hdiv (t, -x) = -localVelocity P u C R hC hR hu hdiv (t, x)

theorem EulerStaticEuler.localPressure_even (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (hodd : ∀ (x : EulerSmoothLimit.Space), u.field (-x) = -u.field x) (t : ℝ) (x : EulerSmoothLimit.Space) : localPressure P u C R hC hR hu hdiv (t, -x) = localPressure P u C R hC hR hu hdiv (t, x)

The actual local Euler velocity and pressure force agree with the constructed smooth coefficient paths. In particular the local velocity has a true one-sided time derivative at the initial and terminal times.

theorem EulerStaticEuler.velocityCoefficient_apply (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) (x : EulerSmoothLimit.Space) : ((velocityCoefficient P u C R hC hR hu hdiv).field t) x = localVelocity P u C R hC hR hu hdiv (↑t, x)

theorem EulerStaticEuler.forceCoefficient_apply (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) (x : EulerSmoothLimit.Space) : ((forceCoefficient P u C R hC hR hu hdiv).field t) x = localForce P u C R hC hR hu hdiv (↑t, x)

theorem EulerStaticEuler.localVelocity_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => localVelocity P u C R hC hR hu hdiv (s, x)) (((derivativeCoefficient P u C R hC hR hu hdiv).field t) x) (Set.Icc 0 (amplitude P C R hC hR)) ↑t

Oddness of the genuine base velocity propagates through its actual flow to the base parent, using ODE uniqueness.

theorem EulerBaseEulerParent.Input.oddData (I : Input) (hodd : ∀ (t : ↑(Set.Icc 0 I.T)), Function.Odd ⇑(I.field.field t)) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.OddData (I.parent ell hell hell1)

noncomputable def EulerStaticEuler.baseTime (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : ℝ

Base time, given by EulerBaseEulerParent.horizon (amplitude P C R hC hR) (outputVelocitySize P C R) (outputRadius R).

Equations

• EulerStaticEuler.baseTime P C R hC hR = EulerBaseEulerParent.horizon (EulerStaticEuler.amplitude P C R hC hR) (EulerStaticEuler.outputVelocitySize P C R) (EulerStaticEuler.outputRadius R)

theorem EulerStaticEuler.baseTime_pos (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : 0 < baseTime P C R hC hR

theorem EulerStaticEuler.baseTime_le (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : baseTime P C R hC hR ≤ amplitude P C R hC hR

noncomputable def EulerStaticEuler.baseInclusion (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : C(↑(Set.Icc 0 (baseTime P C R hC hR)), ↑(Set.Icc 0 (amplitude P C R hC hR)))

Base inclusion, given by initialInclusion _ _ (baseTime_le P C R hC hR).

Equations

• EulerStaticEuler.baseInclusion P C R hC hR = EulerTimeIntervalRestriction.initialInclusion (EulerStaticEuler.amplitude P C R hC hR) (EulerStaticEuler.baseTime P C R hC hR) ⋯

noncomputable def EulerStaticEuler.baseLabelConstant (P : ℝ) [Fact (0 < P)] (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : ℝ

Base label constant as an element of ℝ.

Equations

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

noncomputable def EulerStaticEuler.baseInput (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : EulerBaseEulerParent.Input

Base input, constructed using EulerBaseEulerParent.ofInterval.

Equations

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

theorem EulerStaticEuler.baseInput_field (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (baseTime P C R hC hR))) (x : EulerSmoothLimit.Space) : ((baseInput P u C R hC hR hu hdiv).field.field t) x = localVelocity P u C R hC hR hu hdiv (↑t, x)

noncomputable def EulerStaticEuler.baseL2Data (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) : EulerBaseEulerParent.L2Data (baseInput P u C R hC hR hu hdiv)

Base L² data, bundling velocity, derivative, velocity_match, derivative_match and the required compatibility proofs.

Equations

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

noncomputable def EulerStaticEuler.baseParent (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.Parent

Base parent, given by (baseInput P u C R hC hR hu hdiv).parent ell hell hell1.

Equations

• EulerStaticEuler.baseParent P u C R hC hR hu hdiv ell hell hell1 = (EulerStaticEuler.baseInput P u C R hC hR hu hdiv).parent ell hell hell1

noncomputable def EulerStaticEuler.baseLabelData (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.LabelData (baseParent P u C R hC hR hu hdiv ell hell hell1)

Base label data, given by (baseL2Data P u C R hC hR hu hdiv).labelData ell hell hell1.

Equations

• EulerStaticEuler.baseLabelData P u C R hC hR hu hdiv ell hell hell1 = (EulerStaticEuler.baseL2Data P u C R hC hR hu hdiv).labelData ell hell hell1

theorem EulerStaticEuler.baseLabelData_constant (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : (baseLabelData P u C R hC hR hu hdiv ell hell hell1).K = baseLabelConstant P C R hC hR

theorem EulerStaticEuler.baseLabelConstant_one (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : 1 ≤ baseLabelConstant P C R hC hR

noncomputable def EulerStaticEuler.baseInverse (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.ParticleInverse (baseParent P u C R hC hR hu hdiv ell hell hell1)

Base inverse, given by (baseInput P u C R hC hR hu hdiv).particleInverse ell hell hell1.

Equations

• EulerStaticEuler.baseInverse P u C R hC hR hu hdiv ell hell hell1 = (EulerStaticEuler.baseInput P u C R hC hR hu hdiv).particleInverse ell hell hell1

theorem EulerStaticEuler.baseParent_velocity_match (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 (baseTime P C R hC hR))) (x : EulerSmoothLimit.Space) : ((baseParent P u C R hC hR hu hdiv ell hell hell1).velocity.field t) x = localVelocity P u C R hC hR hu hdiv (↑t, (baseParent P u C R hC hR hu hdiv ell hell hell1).position t x)

noncomputable def EulerStaticEuler.baseEvolution (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.Evolution (baseParent P u C R hC hR hu hdiv ell hell hell1)

Base evolution, bundling inverse, velocity, pressure, force and the required compatibility proofs.

Equations

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

theorem EulerStaticEuler.baseParent_initial_velocity (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (x : EulerSmoothLimit.Space) : ((baseParent P u C R hC hR hu hdiv ell hell hell1).velocity.field ⟨0, ⋯⟩) x = u.field x

theorem EulerStaticEuler.baseOddData (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (hodd : ∀ (x : EulerSmoothLimit.Space), u.field (-x) = -u.field x) : EulerParentPacketFrames.OddData (baseParent P u C R hC hR hu hdiv ell hell hell1)

The actual compact base datum has factorial bounds uniform in the small transverse parameter. All constants use the fixed cutoff only.

The compact initial velocity in the manuscript is constructed using the fixed factorial-bounded outer cutoff and the actual curl potential.

noncomputable def EulerBaseDatum.potential (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (i : Fin 3) (x : EulerSmoothLimit.Space) : ℝ

Potential, given by outerCutoff x*linearPotential L i x.

Equations

• EulerBaseDatum.potential L i x = EulerSpatialCutoffs.outerCutoff x * EulerVectorCalculus.linearPotential L i x

theorem EulerBaseDatum.potential_smooth (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (i : Fin 3) : ContDiff ℝ (↑⊤) (potential L i)

theorem EulerBaseDatum.potential_support (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (i : Fin 3) : tsupport (potential L i) ⊆ Metric.closedBall 0 2

noncomputable def EulerBaseDatum.velocity (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

Velocity, given by curl (potential L).

Equations

• EulerBaseDatum.velocity L = EulerVectorCalculus.curl (EulerBaseDatum.potential L)

theorem EulerBaseDatum.velocity_smooth (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : ContDiff ℝ (↑⊤) (velocity L)

theorem EulerBaseDatum.velocity_support (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : tsupport (velocity L) ⊆ Metric.closedBall 0 2

theorem EulerBaseDatum.velocity_compact (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : HasCompactSupport (velocity L)

theorem EulerBaseDatum.velocity_divergence (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (velocity L) x = 0

theorem EulerBaseDatum.velocity_odd (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : velocity L (-x) = -velocity L x

theorem EulerBaseDatum.velocity_plateau (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hL : (LinearMap.trace ℝ EulerSmoothLimit.Space) ↑L = 0) (x : EulerSmoothLimit.Space) (hx : ‖x‖ < 1) : velocity L x = L x

theorem EulerBaseDatum.velocity_fderiv_plateau (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hL : (LinearMap.trace ℝ EulerSmoothLimit.Space) ↑L = 0) (x : EulerSmoothLimit.Space) (hx : ‖x‖ < 1) : fderiv ℝ (velocity L) x = L

noncomputable def EulerBaseDatum.field (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Field, bundling field, smooth, integrable.

Equations

• EulerBaseDatum.field L = { field := EulerBaseDatum.velocity L, smooth := ⋯, integrable := ⋯ }

theorem EulerBaseDatum.velocity_memLp (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : MeasureTheory.MemLp (velocity L) 2 MeasureTheory.volume

theorem EulerBaseDatum.field_solenoidal (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : MeasureTheory.MemLp.toLp (velocity L) ⋯ ∈ EulerMeanSolenoidal.solenoidalSpace

noncomputable def EulerBaseDatum.linear (β : ℝ) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Linear, given by (EuclideanSpace.proj 1).smulRight (EuclideanSpace.single 0 1+β • EuclideanSpace.single 2 1).

Equations

• EulerBaseDatum.linear β = ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.single 0 1 + β • EuclideanSpace.single 2 1)

@[simp]

theorem EulerBaseDatum.linear_apply (β : ℝ) (x : EulerSmoothLimit.Space) : (linear β) x = x.ofLp 1 • (EuclideanSpace.single 0 1 + β • EuclideanSpace.single 2 1)

theorem EulerBaseDatum.linear_trace (β : ℝ) : (LinearMap.trace ℝ EulerSmoothLimit.Space) ↑(linear β) = 0

theorem EulerBaseDatum.linear_norm (β : ℝ) : ‖linear β‖ ≤ 1 + |β|

theorem EulerBaseDatum.linear_q (β : ℝ) : (linear β) (EuclideanSpace.single 1 1) = EuclideanSpace.single 0 1 + β • EuclideanSpace.single 2 1

Pointwise factorial estimates suffice when one factor has compact support. In particular polynomial factors need not be globally bounded.

theorem EulerGevreyFunctions.product_bound_at {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f g : E → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (R A B : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) (x : E) (hb₁ : ∀ (n : ℕ), ‖iteratedFDeriv ℝ n f x‖ ≤ A * EulerGevrey.majorant R 0 n) (hb₂ : ∀ (n : ℕ), ‖iteratedFDeriv ℝ n g x‖ ≤ B * EulerGevrey.majorant R 0 n) (n : ℕ) : ‖iteratedFDeriv ℝ n (fun (y : E) => f y * g y) x‖ ≤ 3 * A * B * EulerGevrey.majorant R 0 n

theorem EulerGevreyFunctions.majorant_one_le (R : ℝ) (hR : 1 ≤ R) (n : ℕ) : 1 ≤ EulerGevrey.majorant R 0 n

theorem EulerGevreyFunctions.id_bound_on_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (r R : ℝ) (hr : 1 ≤ r) (hR : 1 ≤ R) (x : E) (hx : ‖x‖ ≤ r) (n : ℕ) : ‖iteratedFDeriv ℝ n id x‖ ≤ r * EulerGevrey.majorant R 0 n

theorem EulerGevreyFunctions.linear_bound_on_ball {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (L : E →L[ℝ] V) (r R : ℝ) (hr : 1 ≤ r) (hR : 1 ≤ R) (x : E) (hx : ‖x‖ ≤ r) (n : ℕ) : ‖iteratedFDeriv ℝ n (⇑L) x‖ ≤ ‖L‖ * r * EulerGevrey.majorant R 0 n

theorem EulerGevreyFunctions.compact_product_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f g : E → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (K : Set E) (hK : tsupport f ⊆ K) (R A B : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) (hb₁ : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ A * EulerGevrey.majorant R 0 n) (hb₂ : ∀ x ∈ K, ∀ (n : ℕ), ‖iteratedFDeriv ℝ n g x‖ ≤ B * EulerGevrey.majorant R 0 n) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (fun (y : E) => f y * g y) x‖ ≤ 3 * A * B * EulerGevrey.majorant R 0 n

Compact support turns actual uniform tensor bounds into the ordinary L² tensor bounds used in the label Sobolev estimates.

theorem EulerLpTranslation.SmoothL2Field.hasJetBound_of_support_sup {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (K : Set EulerSmoothLimit.Space) (hK : MeasureTheory.volume K ≠ ⊤) (hs : tsupport A.field ⊆ K) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hb : EulerGevrey.HasSupBound A.field C R) : A.HasJetBound (C * (MeasureTheory.volume K).toReal ^ (1 / 2)) R

theorem EulerBaseDatum.coordinate_norm_le (i : Fin 3) : ‖EuclideanSpace.proj i‖ ≤ 1

theorem EulerBaseDatum.coordinate_bound_on_ball (i : Fin 3) (x : EulerSmoothLimit.Space) (hx : ‖x‖ ≤ 2) (n : ℕ) : ‖iteratedFDeriv ℝ n (fun (y : EulerSmoothLimit.Space) => y.ofLp i) x‖ ≤ 2 * EulerGevrey.majorant 256 0 n

theorem EulerBaseDatum.linear_coordinate_bound_on_ball (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (i : Fin 3) (x : EulerSmoothLimit.Space) (hx : ‖x‖ ≤ 2) (n : ℕ) : ‖iteratedFDeriv ℝ n (fun (y : EulerSmoothLimit.Space) => (L y).ofLp i) x‖ ≤ 2 * ‖L‖ * EulerGevrey.majorant 256 0 n

theorem EulerBaseDatum.linearPotential_bound (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (i : Fin 3) (x : EulerSmoothLimit.Space) (hx : ‖x‖ ≤ 2) (n : ℕ) : ‖iteratedFDeriv ℝ n (EulerVectorCalculus.linearPotential L i) x‖ ≤ 24 * ‖L‖ * EulerGevrey.majorant 256 0 n

noncomputable def EulerBaseDatum.cutoffAmplitude : ℝ

Cutoff amplitude, given by (9*(1+3/EulerGevreyCutoff.bumpMass)^2)^3.

Equations

• EulerBaseDatum.cutoffAmplitude = (9 * (1 + 3 / EulerGevreyCutoff.bumpMass) ^ 2) ^ 3

theorem EulerBaseDatum.cutoffAmplitude_nonneg : 0 ≤ cutoffAmplitude

noncomputable def EulerBaseDatum.potentialAmplitude (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : ℝ

Potential amplitude, given by 3*cutoffAmplitude*(24*‖L‖).

Equations

• EulerBaseDatum.potentialAmplitude L = 3 * EulerBaseDatum.cutoffAmplitude * (24 * ‖L‖)

theorem EulerBaseDatum.potentialAmplitude_nonneg (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : 0 ≤ potentialAmplitude L

theorem EulerBaseDatum.potential_bound (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (i : Fin 3) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (potential L i) x‖ ≤ potentialAmplitude L * EulerGevrey.majorant 256 0 n

noncomputable def EulerBaseDatum.vectorPotential (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Vector potential, given by ∑ i : Fin 3, potential L i x • EuclideanSpace.single i 1.

Equations

• EulerBaseDatum.vectorPotential L x = ∑ i : Fin 3, EulerBaseDatum.potential L i x • EuclideanSpace.single i 1

@[simp]

theorem EulerBaseDatum.vectorPotential_apply (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (i : Fin 3) : (vectorPotential L x).ofLp i = potential L i x

theorem EulerBaseDatum.vectorPotential_smooth (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : ContDiff ℝ (↑⊤) (vectorPotential L)

noncomputable def EulerBaseDatum.coordinateEmbedding (i : Fin 3) : ℝ →L[ℝ] EulerSmoothLimit.Space

Coordinate embedding, given by (ContinuousLinearMap.id ℝ ℝ).smulRight (EuclideanSpace.single i 1).

Equations

• EulerBaseDatum.coordinateEmbedding i = (ContinuousLinearMap.id ℝ ℝ).smulRight (EuclideanSpace.single i 1)

theorem EulerBaseDatum.coordinateEmbedding_norm (i : Fin 3) : ‖coordinateEmbedding i‖ ≤ 1

theorem EulerBaseDatum.vectorPotential_bound (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (vectorPotential L) x‖ ≤ 3 * potentialAmplitude L * EulerGevrey.majorant 256 0 n

theorem EulerBaseDatum.velocity_eq_curlOperator (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : velocity L = fun (x : EulerSmoothLimit.Space) => EulerPacketPiola.curlOperator (fderiv ℝ (vectorPotential L) x)

noncomputable def EulerBaseDatum.velocityAmplitude (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : ℝ

Velocity amplitude, given by ‖curlOperator‖*(3*potentialAmplitude L*256).

Equations

• EulerBaseDatum.velocityAmplitude L = ‖EulerPacketPiola.curlOperator‖ * (3 * EulerBaseDatum.potentialAmplitude L * 256)

theorem EulerBaseDatum.velocityAmplitude_nonneg (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : 0 ≤ velocityAmplitude L

theorem EulerBaseDatum.velocity_sup_bound (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerGevrey.HasSupBound (velocity L) (velocityAmplitude L) 1024

noncomputable def EulerBaseDatum.volumeFactor : ℝ

Volume factor, given by (volume (Metric.closedBall (0 : Space) 2)).toReal^(1/2 : ℝ).

Equations

• EulerBaseDatum.volumeFactor = (MeasureTheory.volume (Metric.closedBall 0 2)).toReal ^ (1 / 2)

theorem EulerBaseDatum.volumeFactor_nonneg : 0 ≤ volumeFactor

theorem EulerBaseDatum.field_jet_bound (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : (field L).HasJetBound (velocityAmplitude L * volumeFactor) 1024

A single positive time and a single label bound work for every compact base datum with |β|≤1. The parent, inverse and Euler evolution below are the actual constructed objects.

A single factorial budget for every base datum with |β|≤1. In particular this covers β=x₀⁻² with x₀≥1, independently of the eventual frequency and iteration scales.

noncomputable def EulerBaseDatum.uniformAmplitude : ℝ

Uniform amplitude, given by 1+‖curlOperator‖*(3*(3*cutoffAmplitude*(24*2))*256).

Equations

• EulerBaseDatum.uniformAmplitude = 1 + ‖EulerPacketPiola.curlOperator‖ * (3 * (3 * EulerBaseDatum.cutoffAmplitude * (24 * 2)) * 256)

theorem EulerBaseDatum.uniformAmplitude_pos : 0 < uniformAmplitude

theorem EulerBaseDatum.velocityAmplitude_le_uniform (β : ℝ) (hβ : |β| ≤ 1) : velocityAmplitude (linear β) ≤ uniformAmplitude

theorem EulerBaseDatum.velocity_uniform_sup (β : ℝ) (hβ : |β| ≤ 1) : EulerGevrey.HasSupBound (velocity (linear β)) uniformAmplitude 1024

noncomputable def EulerBaseDatum.uniformL2Amplitude : ℝ

Uniform L² amplitude, given by uniformAmplitude*volumeFactor.

Equations

• EulerBaseDatum.uniformL2Amplitude = EulerBaseDatum.uniformAmplitude * EulerBaseDatum.volumeFactor

theorem EulerBaseDatum.uniformL2Amplitude_nonneg : 0 ≤ uniformL2Amplitude

theorem EulerBaseDatum.field_uniform_jet (β : ℝ) (hβ : |β| ≤ 1) : (field (linear β)).HasJetBound uniformL2Amplitude 1024

noncomputable def EulerBaseDatum.uniformLabelBound : ℝ

Uniform label bound, given by 1+sobolevCoefficientAmplitude (Fin 3) 6 1024 uniformL2Amplitude + sobolevCoefficientRadius (Fin 3) 1024.

Equations

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

theorem EulerBaseDatum.uniformLabelBound_one : 1 ≤ uniformLabelBound

theorem EulerBaseDatum.field_uniform_label (β : ℝ) (hβ : |β| ≤ 1) : EulerPacketParentLabelBounds.HasLabelBound uniformLabelBound (field (linear β))

theorem EulerBaseDatum.field_uniform_Hq (β : ℝ) (hβ : |β| ≤ 1) (q n : ℕ) : EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q (field (linear β)).toLp ⋯ n ≤ EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 3) q 1024 uniformL2Amplitude * EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 3) 1024 ^ n * ↑n.factorial ^ 2

theorem EulerBaseDatum.beta_bound (x₀ : ℝ) (hx : 1 ≤ x₀) : |(x₀ ^ 2)⁻¹| ≤ 1

theorem EulerBaseDatum.initial_gradient (x₀ : ℝ) : fderiv ℝ (field (linear (x₀ ^ 2)⁻¹)).field 0 = linear (x₀ ^ 2)⁻¹

theorem EulerBaseDatum.instBaseEulerInput1 : Fact (0 < 1)

noncomputable def EulerBaseDatum.solutionTime : ℝ

Solution time, given by EulerStaticEuler.baseTime 1 uniformL2Amplitude 1024 uniformL2Amplitude_nonneg (by norm_num).

Equations

• EulerBaseDatum.solutionTime = EulerStaticEuler.baseTime 1 EulerBaseDatum.uniformL2Amplitude 1024 EulerBaseDatum.uniformL2Amplitude_nonneg EulerBaseDatum.solutionTime._proof_1

theorem EulerBaseDatum.solutionTime_pos : 0 < solutionTime

noncomputable def EulerBaseDatum.solutionLabelConstant : ℝ

Solution label constant, given by EulerStaticEuler.baseLabelConstant 1 uniformL2Amplitude 1024 uniformL2Amplitude_nonneg (by norm_num).

Equations

• EulerBaseDatum.solutionLabelConstant = EulerStaticEuler.baseLabelConstant 1 EulerBaseDatum.uniformL2Amplitude 1024 EulerBaseDatum.uniformL2Amplitude_nonneg EulerBaseDatum.solutionTime._proof_1

noncomputable def EulerBaseDatum.solutionParent (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.Parent

Solution parent, constructed using EulerStaticEuler.baseParent.

Equations

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

noncomputable def EulerBaseDatum.solutionLabelData (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.LabelData (solutionParent β hβ ell hell hell1)

Solution label data, constructed using EulerStaticEuler.baseLabelData.

Equations

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

noncomputable def EulerBaseDatum.solutionInverse (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.ParticleInverse (solutionParent β hβ ell hell hell1)

Solution inverse, constructed using EulerStaticEuler.baseInverse.

Equations

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

noncomputable def EulerBaseDatum.solutionEvolution (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.Evolution (solutionParent β hβ ell hell hell1)

Solution evolution, constructed using EulerStaticEuler.baseEvolution.

Equations

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

theorem EulerBaseDatum.solutionParent_time (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : (solutionParent β hβ ell hell hell1).T = solutionTime

theorem EulerBaseDatum.solutionLabelData_constant (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : (solutionLabelData β hβ ell hell hell1).K = solutionLabelConstant

theorem EulerBaseDatum.solutionOddData (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.OddData (solutionParent β hβ ell hell hell1)

theorem EulerBaseDatum.solution_initial_velocity (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (x : EulerSmoothLimit.Space) : ((solutionParent β hβ ell hell hell1).velocity.field ⟨0, ⋯⟩) x = velocity (linear β) x

theorem EulerBaseDatum.solution_initial_gradient (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : fderiv ℝ (⇑((solutionParent β hβ ell hell hell1).velocity.field ⟨0, ⋯⟩)) 0 = linear β

theorem EulerBaseDatum.solution_initial_support (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : tsupport ⇑((solutionParent β hβ ell hell hell1).velocity.field ⟨0, ⋯⟩) ⊆ Metric.closedBall 0 2

theorem EulerBaseDatum.solution_origin_fixed (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 solutionTime)) : (solutionParent β hβ ell hell hell1).position t 0 = 0

theorem EulerBaseDatum.solutionLabelConstant_one : 1 ≤ solutionLabelConstant

The actual normalized Euler pressure force has smooth ordinary L² slices, with all derivative tensors continuous in time.

noncomputable def EulerStaticEuler.localForceField (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Local force field, constructed using SmoothL2Field.mapField.

Equations

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

theorem EulerStaticEuler.localForceField_apply (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) (x : EulerSmoothLimit.Space) : (localForceField P u C R hC hR hu hdiv t).field x = localForce P u C R hC hR hu hdiv (↑t, x)

theorem EulerStaticEuler.localForceField_jetLp_continuous (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 (amplitude P C R hC hR))) => (localForceField P u C R hC hR hu hdiv t).jetLp n

The concrete local base evolution has actual continuous L² jets for both velocity and pressure force. Consequently its Euler equation holds strongly in every finite Sobolev order, including endpoint derivatives.

noncomputable def EulerStaticEuler.baseSobolevData (P : ℝ) [Fact (0 < P)] (u : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hu : u.HasJetBound C R) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u.field x = 0) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.SobolevData (baseEvolution P u C R hC hR hu hdiv ell hell hell1)

Base sobolev data, bundling velocity, force, velocity_match, force_match and the required compatibility proofs.

Equations

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

theorem EulerBaseDatum.instBaseEulerSobolev1 : Fact (0 < 1)

noncomputable def EulerBaseDatum.solutionSobolevData (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.SobolevData (solutionEvolution β hβ ell hell hell1)

Solution sobolev data, constructed using EulerStaticEuler.baseSobolevData.

Equations

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

noncomputable def EulerBaseDatum.initialTime : ℝ

Initial time, given by guardTime solutionTime solutionLabelConstant.

Equations

• EulerBaseDatum.initialTime = EulerBaseEulerGuards.guardTime EulerBaseDatum.solutionTime EulerBaseDatum.solutionLabelConstant

theorem EulerBaseDatum.initialTime_pos : 0 < initialTime

theorem EulerBaseDatum.initialTime_le : initialTime ≤ solutionTime

theorem EulerBaseDatum.initialTime_le_one : initialTime ≤ 1

noncomputable def EulerBaseDatum.initialCoefficientCost : ℝ

Initial coefficient cost, given by coefficientCost solutionLabelConstant.

Equations

• EulerBaseDatum.initialCoefficientCost = EulerBaseEulerGuards.coefficientCost EulerBaseDatum.solutionLabelConstant

theorem EulerBaseDatum.initialCoefficientCost_nonneg : 0 ≤ initialCoefficientCost

theorem EulerBaseDatum.initialTime_small : initialCoefficientCost * initialTime ≤ 1 / 4 ∧ EulerPacketFirstPressureSign.firstSignRate initialCoefficientCost initialCoefficientCost * initialTime ≤ 1 / 4

noncomputable def EulerBaseDatum.initialParent (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.Parent

Initial parent, given by (solutionParent β hβ ell hell hell1).restrictTime initialTime initialTime_pos initialTime_le.

Equations

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

noncomputable def EulerBaseDatum.initialLabelData (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.LabelData (initialParent β hβ ell hell hell1)

Initial label data, given by (solutionLabelData β hβ ell hell hell1).restrictTime initialTime initialTime_pos initialTime_le.

Equations

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

noncomputable def EulerBaseDatum.initialInverse (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.ParticleInverse (initialParent β hβ ell hell hell1)

Initial inverse, given by (solutionInverse β hβ ell hell hell1).restrictTime initialTime initialTime_pos initialTime_le.

Equations

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

noncomputable def EulerBaseDatum.initialEvolution (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.Evolution (initialParent β hβ ell hell hell1)

Initial evolution, given by (solutionEvolution β hβ ell hell hell1).restrictTime initialTime initialTime_pos initialTime_le.

Equations

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

noncomputable def EulerBaseDatum.initialSobolevData (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.SobolevData (initialEvolution β hβ ell hell hell1)

Initial sobolev data, given by (solutionSobolevData β hβ ell hell hell1).restrictTime initialTime initialTime_pos initialTime_le.

Equations

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

theorem EulerBaseDatum.initialOddData (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.OddData (initialParent β hβ ell hell hell1)

noncomputable def EulerBaseDatum.initialLowBounds (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.LowBounds (initialParent β hβ ell hell hell1)

Initial low bounds, given by lowBounds (solutionLabelData β hβ ell hell hell1).

Equations

• EulerBaseDatum.initialLowBounds β hβ ell hell hell1 = EulerBaseEulerGuards.lowBounds (EulerBaseDatum.solutionLabelData β hβ ell hell hell1)

theorem EulerBaseDatum.initialLowBounds_values (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : (initialLowBounds β hβ ell hell hell1).Be = initialCoefficientCost ∧ (initialLowBounds β hβ ell hell hell1).Bc = 0 ∧ (initialLowBounds β hβ ell hell hell1).L = 0 ∧ (initialLowBounds β hβ ell hell hell1).r = 0 ∧ (initialLowBounds β hβ ell hell hell1).K = initialCoefficientCost

theorem EulerBaseDatum.initialParent_time (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : (initialParent β hβ ell hell hell1).T = initialTime

theorem EulerBaseDatum.initialLabelData_constant (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : (initialLabelData β hβ ell hell hell1).K = solutionLabelConstant

theorem EulerBaseDatum.initial_velocity (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (x : EulerSmoothLimit.Space) : ((initialParent β hβ ell hell hell1).velocity.field ⟨0, ⋯⟩) x = velocity (linear β) x

theorem EulerBaseDatum.initial_velocity_support (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : tsupport ⇑((initialParent β hβ ell hell hell1).velocity.field ⟨0, ⋯⟩) ⊆ Metric.closedBall 0 2

theorem EulerBaseDatum.solution_initialStrain (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (x : EulerSmoothLimit.Space) (hx : ‖ell • x‖ < 1) : (solutionParent β hβ ell hell hell1).initialStrain.field x = linear β

theorem EulerBaseDatum.initialStrain_plateau (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (x : EulerSmoothLimit.Space) (hx : ‖ell • x‖ < 1) : (initialParent β hβ ell hell hell1).initialStrain.field x = linear β

theorem EulerBaseDatum.initial_strain_bound (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 initialTime)) (x : EulerSmoothLimit.Space) : ‖((initialParent β hβ ell hell hell1).strain.field t) x‖ ≤ initialCoefficientCost

theorem EulerBaseDatum.initial_curvature_bound (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 initialTime)) (x : EulerSmoothLimit.Space) : ‖((initialParent β hβ ell hell hell1).curvature.field t) x‖ ≤ initialCoefficientCost

theorem EulerBaseDatum.initial_origin_fixed (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 initialTime)) : (initialParent β hβ ell hell hell1).position t 0 = 0

theorem EulerBaseDatum.initial_pressure_numerator (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane (EuclideanSpace.single 0 1))) (ξ : U) (hξ : ↑(R ξ) = EuclideanSpace.single 1 1) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (t : ↑(Set.Icc 0 initialTime)) (x : EulerSmoothLimit.Space) (hx : ‖ell • x‖ < 1) : 1 / 2 ≤ inner ℝ ((((initialParent β hβ ell hell hell1).transverseData (EuclideanSpace.single 0 1) initial_pressure_numerator._proof_1 R S hS).normal.field t) x) ((((initialParent β hβ ell hell hell1).strain.field t) x) (EulerPacketForwardFactorization.uncutVelocity ((initialParent β hβ ell hell hell1).transverseData (EuclideanSpace.single 0 1) initial_pressure_numerator._proof_1 R S hS) ξ (↑t) x))

theorem EulerBaseDatum.initial_pressure_numerator_on_support (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane (EuclideanSpace.single 0 1))) (ξ : U) (hξ : ↑(R ξ) = EuclideanSpace.single 1 1) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (t : ↑(Set.Icc 0 initialTime)) (x : EulerSmoothLimit.Space) (hx : x ∈ tsupport EulerSpatialCutoffs.innerCutoff) : 1 / 2 ≤ inner ℝ ((((initialParent β hβ ell hell hell1).transverseData (EuclideanSpace.single 0 1) initial_pressure_numerator._proof_1 R S hS).normal.field t) x) ((((initialParent β hβ ell hell hell1).strain.field t) x) (EulerPacketForwardFactorization.uncutVelocity ((initialParent β hβ ell hell hell1).transverseData (EuclideanSpace.single 0 1) initial_pressure_numerator._proof_1 R S hS) ξ (↑t) x))