Genuine algebraic closure of admissible mean forcing

Admissibility is preserved by finite sums, bounded linear maps, and actual spatial directional derivatives. Every witness consists of literal smooth fields and their continuous L² jets; no inverse or equation is assumed.

noncomputable def EulerMeanPacketProvider.Forcing.ofSlices {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (A : ℝ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 D.T)) => (A ↑t).jetLp n) (heq : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = (A ↑t).field x) : Forcing D raw

The time path is constructed from the actual zeroth L² jet.

Equations

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

noncomputable def EulerMeanPacketProvider.Forcing.zero (D : Data) : Forcing D 0

Zero, given by ofSlices (fun _ => zeroField) (fun _ => continuous_const) (fun _ _ _ => rfl).

Equations

• EulerMeanPacketProvider.Forcing.zero D = EulerMeanPacketProvider.Forcing.ofSlices (fun (x : ℝ) => EulerLpTranslation.SmoothL2Field.zeroField) ⋯ ⋯

noncomputable def EulerMeanPacketProvider.Forcing.add {D : Data} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (H : Forcing D raw') : Forcing D (raw + raw')

Add, constructed using ofSlices.

Equations

• G.add H = EulerMeanPacketProvider.Forcing.ofSlices (fun (t : ℝ) => (G.slices t).addField (H.slices t)) ⋯ ⋯

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

Applying a genuine bounded linear map preserves every actual L² jet.

Equations

• G.map L = EulerMeanPacketProvider.Forcing.ofSlices (fun (t : ℝ) => EulerLpTranslation.SmoothL2Field.mapField L (G.slices t)) ⋯ ⋯

noncomputable def EulerMeanPacketProvider.Forcing.smul {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (c : ℝ) : Forcing D (c • raw)

Smul, given by G.map (c • ContinuousLinearMap.id ℝ Space).

Equations

• G.smul c = G.map (c • ContinuousLinearMap.id ℝ EulerSmoothLimit.Space)

noncomputable def EulerMeanPacketProvider.Forcing.neg {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : Forcing D (-raw)

Neg, given by G.map (-ContinuousLinearMap.id ℝ Space).

Equations

• G.neg = G.map (-ContinuousLinearMap.id ℝ EulerSmoothLimit.Space)

noncomputable def EulerMeanPacketProvider.Forcing.spatialDerivative {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (v : EulerSmoothLimit.Space) : Forcing D fun (z : EulerPacketPointJets.Domain) => (fderiv ℝ (fun (x : EulerSmoothLimit.Space) => raw (z.1, x, z.2.2)) z.2.1) v

The derivative is the ordinary derivative of the prescribed raw field at fixed time and angle.

Equations

• G.spatialDerivative v = EulerMeanPacketProvider.Forcing.ofSlices (fun (t : ℝ) => (G.slices t).directionalField v) ⋯ ⋯

theorem EulerMeanPacketProvider.admissible_finset_sum {ι : Type u_1} (D : Data) (s : Finset ι) (raw : ι → EulerPacketProfileRecursion.VectorField) (h : ∀ i ∈ s, Nonempty (Forcing D (raw i))) : Nonempty (Forcing D (∑ i ∈ s, raw i))

Every actual finite sum of admissible forcing fields is admissible.