Related estimates used together by the same construction modules.

The actual mean pressure enters the lifted gradient closure. Only its genuine L² gradient is embedded; its scalar potential need not be L².

Actual scalar pressures whose lifted gradients are smooth L² fields. The witnesses below are closed under the literal finite packet assembly.

theorem EulerPacketPressure.rawGradient_component (κ : ℝ) (m : EulerSmoothLimit.Space) (p : EulerPacketProfileRecursion.ScalarField) (z : EulerPacketPointJets.Domain) (i : Fin 3) : (rawGradient κ m p z).ofLp i = κ * (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p (z.1, y)) z.2) (EuclideanSpace.single i 1, 0) + (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p (z.1, y)) z.2) (0, 1) * m.ofLp i

theorem EulerPacketPressure.rawGradient_zero (κ : ℝ) (m : EulerSmoothLimit.Space) : rawGradient κ m 0 = 0

theorem EulerPacketPressure.rawGradient_add (κ : ℝ) (m : EulerSmoothLimit.Space) (p q : EulerPacketProfileRecursion.ScalarField) (z : EulerPacketPointJets.Domain) (hp : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p (z.1, y)) z.2) (hq : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => q (z.1, y)) z.2) : rawGradient κ m (p + q) z = rawGradient κ m p z + rawGradient κ m q z

theorem EulerPacketPressure.rawGradient_smul (κ : ℝ) (m : EulerSmoothLimit.Space) (c : ℝ) (p : EulerPacketProfileRecursion.ScalarField) (z : EulerPacketPointJets.Domain) (hp : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p (z.1, y)) z.2) : rawGradient κ m (c • p) z = c • rawGradient κ m p z

theorem EulerPacketPressure.rawGradient_sum {ι : Type u_1} (κ : ℝ) (m : EulerSmoothLimit.Space) (s : Finset ι) (p : ι → EulerPacketProfileRecursion.ScalarField) (z : EulerPacketPointJets.Domain) (hp : ∀ i ∈ s, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p i (z.1, y)) z.2) : rawGradient κ m (∑ i ∈ s, p i) z = ∑ i ∈ s, rawGradient κ m (p i) z

structure EulerPacketPressure.GradientWitness (P T κ : ℝ) [Fact (0 < P)] (m : EulerSmoothLimit.Space) (p : EulerPacketProfileRecursion.ScalarField) : Type

Gradient witness data, collecting smooth, field, gradient_mem.

• smooth (t : ↑(Set.Icc 0 T)) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => p (↑t, y)
• field : EulerPacketCylinderField.Field P T (rawGradient κ m p)

  Underlying field of GradientWitness, of type Field P T (rawGradient κ m p).

• gradient_mem (t : ↑(Set.Icc 0 T)) : self.field.path t ∈ EulerLiftedGradientSpace.gradientSpace P κ m

def EulerPacketPressure.GradientWitness.congr {P T κ : ℝ} [Fact (0 < P)] {m : EulerSmoothLimit.Space} {p q : EulerPacketProfileRecursion.ScalarField} (G : GradientWitness P T κ m p) (h : p = q) : GradientWitness P T κ m q

Congr, given by h ▸ G.

Equations

• G.congr h = h ▸ G

def EulerPacketPressure.GradientWitness.changeTime {P T κ : ℝ} [Fact (0 < P)] {m : EulerSmoothLimit.Space} {p : EulerPacketProfileRecursion.ScalarField} {T' : ℝ} (G : GradientWitness P T κ m p) (h : T = T') : GradientWitness P T' κ m p

Change time, given by h ▸ G.

Equations

• G.changeTime h = h ▸ G

noncomputable def EulerPacketPressure.GradientWitness.zero (P T κ : ℝ) [Fact (0 < P)] (m : EulerSmoothLimit.Space) : GradientWitness P T κ m 0

Zero, bundling smooth, field, gradient_mem.

Equations

• EulerPacketPressure.GradientWitness.zero P T κ m = { smooth := ⋯, field := (EulerPacketCylinderField.Field.zero P T).congr ⋯, gradient_mem := ⋯ }

noncomputable def EulerPacketPressure.GradientWitness.add {P T κ : ℝ} [Fact (0 < P)] {m : EulerSmoothLimit.Space} {p q : EulerPacketProfileRecursion.ScalarField} (G : GradientWitness P T κ m p) (H : GradientWitness P T κ m q) : GradientWitness P T κ m (p + q)

Add, bundling smooth, field, gradient_mem.

Equations

• G.add H = { smooth := ⋯, field := (G.field.add H.field).congr ⋯, gradient_mem := ⋯ }

noncomputable def EulerPacketPressure.GradientWitness.smul {P T κ : ℝ} [Fact (0 < P)] {m : EulerSmoothLimit.Space} {p : EulerPacketProfileRecursion.ScalarField} (G : GradientWitness P T κ m p) (c : ℝ) : GradientWitness P T κ m (c • p)

Smul, bundling smooth, field, gradient_mem.

Equations

• G.smul c = { smooth := ⋯, field := (G.field.smul c).congr ⋯, gradient_mem := ⋯ }

noncomputable def EulerPacketPressure.GradientWitness.finsetSum {P T κ : ℝ} [Fact (0 < P)] {m : EulerSmoothLimit.Space} {ι : Type u_1} (s : Finset ι) (p : ι → EulerPacketProfileRecursion.ScalarField) (G : (i : ι) → GradientWitness P T κ m (p i)) : GradientWitness P T κ m (∑ i ∈ s, p i)

Finset sum, bundling smooth, simpa, field, gradient_mem and the required compatibility proofs.

Equations

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

noncomputable def EulerPacketPressure.GradientWitness.truncateFamily {P T κ : ℝ} [Fact (0 < P)] {m : EulerSmoothLimit.Space} (N : ℕ) (p : ℕ → EulerPacketProfileRecursion.ScalarField) (G : (i : ℕ) → i ≤ N → GradientWitness P T κ m (p i)) (n : ℕ) : GradientWitness P T κ m (EulerFiniteGrades.truncate N p n)

Truncate family as an element of GradientWitness P T κ m (truncate N p n).

Equations

• EulerPacketPressure.GradientWitness.truncateFamily N p G n = if hn : n ≤ N then (G n hn).congr ⋯ else (EulerPacketPressure.GradientWitness.zero P T κ m).congr ⋯

noncomputable def EulerPacketPressure.GradientWitness.assembleFamily {P T κ : ℝ} [Fact (0 < P)] {m : EulerSmoothLimit.Space} (N : ℕ) (p q : ℕ → EulerPacketProfileRecursion.ScalarField) (G : (i : ℕ) → i ≤ N → GradientWitness P T κ m (p i)) (H : (i : ℕ) → i ≤ N → GradientWitness P T κ m (q i)) (n : ℕ) : GradientWitness P T κ m (EulerFiniteGrades.assemble N p q n)

Assemble family used in packet pressure witness.

Equations

• One or more equations did not get rendered due to their size.
• EulerPacketPressure.GradientWitness.assembleFamily N p q G H 0 = (EulerPacketPressure.GradientWitness.truncateFamily N p G 0).congr ⋯

noncomputable def EulerPacketPressure.GradientWitness.evaluateFamily {P T κ : ℝ} [Fact (0 < P)] {m : EulerSmoothLimit.Space} (N : ℕ) (r : ℝ) (p : ℕ → EulerPacketProfileRecursion.ScalarField) (G : (i : ℕ) → GradientWitness P T κ m (p i)) : GradientWitness P T κ m (EulerPacketPointJets.fieldSum N r p)

Evaluate family as an element of GradientWitness P T κ m (fieldSum N r p).

Equations

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

noncomputable def EulerPacketPressure.GradientWitness.compact {P T κ : ℝ} [Fact (0 < P)] {m : EulerSmoothLimit.Space} (p : EulerPacketProfileRecursion.ScalarField) (q : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), p (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P q hq t (x, ↑θ)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (hz : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ S, ∀ (θ : ℝ), p (↑t, x, θ) = 0) : GradientWitness P T κ m p

Compact, bundling smooth, field, gradient_mem.

Equations

• EulerPacketPressure.GradientWitness.compact p q hq he S hS hz = { smooth := ⋯, field := EulerPacketPressure.liftedGradientField P p q hq he κ m, gradient_mem := ⋯ }

noncomputable def EulerPacketCoordinates.pressureField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (hk : k ≠ 0) {p : EulerPacketProfileRecursion.ScalarField} (G : EulerPacketPressure.GradientWitness P D.T k⁻¹ D.m₀ p) : EulerPacketCylinderField.Field P D.T (coordinatePressure D k p)

Pressure field as an element of Field P D.T (coordinatePressure D k p).

Equations

• EulerPacketCoordinates.pressureField D k hk G = (G.field.smul (k ^ 2)).congr ⋯

theorem EulerPacketCoordinates.pressureField_mem {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (hk : k ≠ 0) {p : EulerPacketProfileRecursion.ScalarField} (G : EulerPacketPressure.GradientWitness P D.T k⁻¹ D.m₀ p) (t : ↑(Set.Icc 0 D.T)) : (pressureField D k hk G).path t ∈ EulerLiftedGradientSpace.gradientSpace P k⁻¹ D.m₀

The actual constant-angle embedding preserves the closed gradient spaces. Compact ordinary scalar tests give compact cylinder scalar tests, and the bounded embedding carries their closures into one another.

def EulerCylinderSpatialEmbedding.scalarLift (P : ℝ) (φ : EulerSmoothLimit.Space → ℝ) : EulerLiftedGradientSpace.LiftDomain P → ℝ

Scalar lift, defined pointwise by φ z.1.

Equations

• EulerCylinderSpatialEmbedding.scalarLift P φ z = φ z.1

theorem EulerCylinderSpatialEmbedding.scalarLift_compact (P : ℝ) [Fact (0 < P)] (φ : EulerSmoothLimit.Space → ℝ) (hφ : HasCompactSupport φ) : HasCompactSupport (scalarLift P φ)

theorem EulerCylinderSpatialEmbedding.scalarLift_smooth (P : ℝ) (φ : EulerSmoothLimit.Space → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (z : EulerLiftedGradientSpace.LiftDomain P) : ContDiff ℝ (↑⊤) (EulerLiftedGradientSpace.localLift P (scalarLift P φ) z)

theorem EulerCylinderSpatialEmbedding.gradient_component (φ : EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) (i : Fin 3) : (gradient φ x).ofLp i = (fderiv ℝ φ x) (EuclideanSpace.single i 1)

theorem EulerCylinderSpatialEmbedding.scalarLift_gradient (P κ : ℝ) (m : EulerSmoothLimit.Space) (φ : EulerSmoothLimit.Space → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (z : EulerLiftedGradientSpace.LiftDomain P) : EulerLiftedGradientSpace.liftedGradient P κ m (scalarLift P φ) z = κ • gradient φ z.1

theorem EulerCylinderSpatialEmbedding.smul_embedding_gradient_mem (P : ℝ) [Fact (0 < P)] (κ : ℝ) (m : EulerSmoothLimit.Space) (g : ↥EulerMeanSolenoidal.L2) (hg : g ∈ EulerMeanSolenoidal.gradientSpace) : κ • (embedding P) g ∈ EulerLiftedGradientSpace.gradientSpace P κ m

theorem EulerCylinderSpatialEmbedding.embedding_gradient_mem (P : ℝ) [Fact (0 < P)] (κ : ℝ) (hκ : κ ≠ 0) (m : EulerSmoothLimit.Space) (g : ↥EulerMeanSolenoidal.L2) (hg : g ∈ EulerMeanSolenoidal.gradientSpace) : (embedding P) g ∈ EulerLiftedGradientSpace.gradientSpace P κ m

theorem EulerMeanPacketProvider.Forcing.path_ae_raw_zeroAngle {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) : ↑↑(G.path t) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => raw (↑t, x, 0)

theorem EulerMeanPacketProvider.Forcing.scalarGradient_path_eq {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) : G.scalarGradientForcing.path t = (ContinuousLinearMap.adjoint (D.opF t)) (G.pressureForcePath t)

The classical gradient constructed from the radial potential is the same ordinary L² element as the projected pressure residual.

theorem EulerMeanPacketProvider.Forcing.scalarGradient_path_mem {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) : G.scalarGradientForcing.path t ∈ EulerMeanSolenoidal.gradientSpace

theorem EulerMeanPacketProvider.Forcing.pressureGradient_eq_scalarGradient {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketCylinderField.pressureGradient G.scalar (↑t, x, θ) = G.scalarGradient (↑t, x, θ)

noncomputable def EulerMeanPacketProvider.Forcing.pressureGradientWitness {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (P κ : ℝ) [Fact (0 < P)] (m : EulerSmoothLimit.Space) : EulerPacketPressure.GradientWitness P D.T κ m G.scalar

This witness uses the actual projected mean equation to prove membership, without any compact-support or integrability premise on the scalar potential.

Equations

• G.pressureGradientWitness P κ m = { smooth := ⋯, field := ((EulerMeanPacketProvider.Forcing.toCylinderField P G.scalarGradientForcing).smul κ).congr ⋯, gradient_mem := ⋯ }

The actual coordinate residual identity in every finite Sobolev space. This discharges the approximation equation, using the source coefficients and the genuine packet Fields rather than an assumed residual equation.

@[instance_reducible]

noncomputable def EulerPacketCoordinates.instPacketCoordinateSobolev1 : NormedAddCommGroup EulerSmoothLimit.Space

Cache the standard NormedAddCommGroup Space instance to shorten typeclass synthesis.

Equations

• EulerPacketCoordinates.instPacketCoordinateSobolev1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCoordinates.instPacketCoordinateSobolev2 : NormedSpace ℝ EulerSmoothLimit.Space

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

Equations

• EulerPacketCoordinates.instPacketCoordinateSobolev2 = inferInstance

noncomputable def EulerPacketCoordinates.normalizedResidual {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (W : EulerPacketProfileRecursion.VectorField) (p : EulerPacketProfileRecursion.ScalarField) (z : EulerPacketPointJets.Domain) : EulerSmoothLimit.Space

Normalized residual, given by k • rawInverse D z (slicedMomentumResidual (Icc (0 : ℝ) D.T) k⁻¹ (rawInverse D z) (D.strain z) (D.normalField z) W p z).

Equations

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

noncomputable def EulerPacketCoordinates.coordinateData {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (hκ : |k⁻¹| ≤ 1) {W : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T W) (p : EulerPacketProfileRecursion.ScalarField) (R : EulerPacketCylinderField.Field P D.T (normalizedResidual D k W p)) : EulerAllOrderCorrectionData.Data P D.T

The data used for cancellation has the literal normalized packet field and residual. Its coefficients are the original deformation coefficients.

Equations

• EulerPacketCoordinates.coordinateData D k hκ G p R = EulerPacketCorrectionCoefficients.correctionDataOfFields D P k⁻¹ hκ (EulerPacketCoordinates.coordinateField D G k) R

theorem EulerPacketCoordinates.sobolev_residual_identity {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (hk : k ≠ 0) (hκ : |k⁻¹| ≤ 1) {W Wt : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T W) (Gt : EulerPacketCylinderField.Field P D.T Wt) (hW : EulerPacketCylinderField.TimeDerivative ⋯ G Gt) (p : EulerPacketProfileRecursion.ScalarField) (R : EulerPacketCylinderField.Field P D.T (normalizedResidual D k W p)) (Pa : EulerPacketCylinderField.Field P D.T (coordinatePressure D k p)) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 D.T)) : (R.toFieldTower.realization q) t = ((coordinateTimeField D G Gt k).toFieldTower.realization q) t + EulerCorrectionResidualCancellation.nonlinearity P (EulerAllOrderCorrectionData.Data.atOrder P (coordinateData D k hκ G p R) q) hq t (((coordinateField D G k).toFieldTower.realization (q + 1)) t) + (EulerSobolevCoefficientPressure.coefficientSobolevOperator P ((EulerPacketCorrectionCoefficients.metricTower D P).jet q t)) ((Pa.toFieldTower.realization q) t)

theorem EulerPacketCoordinates.approximation_hasDerivWithinAt {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (hk : k ≠ 0) (hκ : |k⁻¹| ≤ 1) {W Wt : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T W) (Gt : EulerPacketCylinderField.Field P D.T Wt) (hW : EulerPacketCylinderField.TimeDerivative ⋯ G Gt) (p : EulerPacketProfileRecursion.ScalarField) (R : EulerPacketCylinderField.Field P D.T (normalizedResidual D k W p)) (Pa : EulerPacketCylinderField.Field P D.T (coordinatePressure D k p)) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 D.T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ ((coordinateData D k hκ G p R).approximation.realization q)) (((coordinateData D k hκ G p R).residual.realization q) t - EulerCorrectionResidualCancellation.nonlinearity P (EulerAllOrderCorrectionData.Data.atOrder P (coordinateData D k hκ G p R) q) hq t (((coordinateData D k hκ G p R).approximation.realization (q + 1)) t) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator P ((coordinateData D k hκ G p R).metric.jet q t)) ((Pa.toFieldTower.realization q) t)) (Set.Icc 0 D.T) ↑t

The approximation's actual all-order derivative is its literal residual minus the full nonlinearity and its own actual pressure.

theorem EulerPacketCoordinates.approximation_hasDerivAt {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (hk : k ≠ 0) (hκ : |k⁻¹| ≤ 1) {W Wt : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T W) (Gt : EulerPacketCylinderField.Field P D.T Wt) (hW : EulerPacketCylinderField.TimeDerivative ⋯ G Gt) (p : EulerPacketProfileRecursion.ScalarField) (R : EulerPacketCylinderField.Field P D.T (normalizedResidual D k W p)) (Pa : EulerPacketCylinderField.Field P D.T (coordinatePressure D k p)) (q : ℕ) (hq : 6 ≤ q) (t : ℝ) (ht : t ∈ Set.Ioo 0 D.T) : HasDerivAt (EulerVolterraConvolution.extendPath D.T ⋯ ((coordinateData D k hκ G p R).approximation.realization q)) (((coordinateData D k hκ G p R).residual.realization q) ⟨t, ⋯⟩ - EulerCorrectionResidualCancellation.nonlinearity P (EulerAllOrderCorrectionData.Data.atOrder P (coordinateData D k hκ G p R) q) hq ⟨t, ⋯⟩ (((coordinateData D k hκ G p R).approximation.realization (q + 1)) ⟨t, ⋯⟩) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator P ((coordinateData D k hκ G p R).metric.jet q ⟨t, ⋯⟩)) ((Pa.toFieldTower.realization q) ⟨t, ⋯⟩)) t