Every actual compact high/corrector pair is a member of the closed lifted solenoidal space.

def EulerPacketCylinderField.packetInverseCoefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : MatrixCoefficient D.T fun (z : EulerPacketPointJets.Domain) => (D.FInv.field (D.clamp z.1)) z.2.1

Packet inverse coefficient, bundling path, orbit, raw_eq.

Equations

• EulerPacketCylinderField.packetInverseCoefficient D = { path := D.FInv.field, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerPacketCylinderField.piolaPairRaw {P : ℝ} {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (κ : ℝ) (raw : EulerPacketProfileRecursion.VectorField) (p : ℕ) : EulerPacketProfileRecursion.VectorField

Piola pair raw, defined pointwise by D.FInv.field (D.clamp z.1) z.2.1 (κ^p • raw z+κ^(p+1) • D.curlCorrector P raw z).

Equations

• EulerPacketCylinderField.piolaPairRaw D κ raw p z = ((D.FInv.field (D.clamp z.1)) z.2.1) (κ ^ p • raw z + κ ^ (p + 1) • D.curlCorrector P raw z)

noncomputable def EulerPacketCylinderField.piolaPairField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {raw : EulerPacketProfileRecursion.VectorField} (G : Field P D.T raw) (C : Field P D.T (D.curlCorrector P raw)) (κ : ℝ) (p : ℕ) : Field P D.T (piolaPairRaw D κ raw p)

Piola pair field, given by (packetInverseCoefficient D).multiply ((G.smul (κ^p)).add (C.smul (κ^(p+1)))).

Equations

• EulerPacketCylinderField.piolaPairField D G C κ p = (EulerPacketCylinderField.packetInverseCoefficient D).multiply ((G.smul (κ ^ p)).add (C.smul (κ ^ (p + 1))))

theorem EulerPacketCylinderField.piolaPairField_mem {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {raw : EulerPacketProfileRecursion.VectorField} (G : Field P D.T raw) (C : Field P D.T (D.curlCorrector P raw)) (κ : ℝ) (p : ℕ) (t : ↑(Set.Icc 0 D.T)) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hF : ∀ (x : EulerSmoothLimit.Space), fderiv ℝ Ξ x = (D.F.field t) x) (hdet : ∀ (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hs : G.path t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯) (hm : ∀ (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, raw (↑t, x, θ) = 0) (htan : ∀ (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (D.normalField (↑t, x, θ)) (raw (↑t, x, θ)) = 0) : (piolaPairField D G C κ p).path t ∈ EulerLiftedGradientSpace.divergenceFreeSpace P κ D.m₀