Nonlinear closure of actual admissible mean forcing

Sobolev evaluation supplies bounded coefficients from one actual smooth L² factor. Consequently finite-dimensional bilinear products preserve the literal spatial L² jets and their time continuity without an extra product regularity assumption.

Actual multiplication closure for admissible mean forcing.

noncomputable def EulerMeanPacketProvider.Forcing.multiply {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (A : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 D.T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) : Forcing D fun (z : EulerPacketPointJets.Domain) => ((A.field (D.clamp z.1)) z.2.1) (raw z)

Multiplying the raw field by a genuinely bounded smooth coefficient path preserves all actual L² spatial jets and their time continuity.

Equations

• G.multiply A = EulerMeanPacketProvider.Forcing.ofSlices (fun (r : ℝ) => EulerLpSmoothCoefficientProduct.product A (D.clamp r) (G.slices r)) ⋯ ⋯

def EulerMeanPacketProvider.Forcing.congr {D : Data} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (heq : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = raw (↑t, x, θ)) : Forcing D raw'

Admissibility depends only on the raw field on the actual time interval.

Equations

• G.congr heq = { slices := G.slices, jets_continuous := ⋯, path := G.path, path_eq := ⋯, raw_eq := ⋯ }

noncomputable def EulerMeanPacketProvider.Forcing.bilinear {D : Data} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (H : Forcing D raw') (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : Forcing D fun (z : EulerPacketPointJets.Domain) => (B (raw z)) (raw' z)

A literal bilinear product of two admissible fields is admissible.

Equations

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

theorem EulerMeanPacketProvider.admissible_bilinear (D : Data) (raw raw' : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) (h' : Nonempty (Forcing D raw')) (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : Nonempty (Forcing D fun (z : EulerPacketPointJets.Domain) => (B (raw z)) (raw' z))