The genuine homogeneous high-mode solution supplies the primary profile's regularity.

def EulerPacketCylinderField.ProfileRegularity.changeTime {P T : ℝ} [Fact (0 < P)] {T' : ℝ} {hT : 0 ≤ T} {S : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} (G : ProfileRegularity P T hT S a) (h : T = T') (hT' : 0 ≤ T') : ProfileRegularity P T' hT' S a

Change time as an element of ProfileRegularity P T' hT' S a.

Equations

• G.changeTime h hT' = Eq.ndrec (motive := fun {T' : ℝ} => (hT' : 0 ≤ T') → EulerPacketCylinderField.ProfileRegularity P T' hT' S a) (fun (hT' : 0 ≤ T) => G) h hT'

noncomputable def EulerPacketCylinderField.ProfileRegularity.primary {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (O : EulerPacketProfileRecursion.Operators) (hcorrector : O.curlCorrector = D.curlCorrector P) : ProfileRegularity P D.T ⋯ D.support (EulerPacketProfileRecursion.primaryProfile O (G.vector I) (G.scalar I))

Primary, bundling high, mean, corrector, pressure and the required compatibility proofs.

Equations

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

noncomputable def EulerPacketCylinderField.homogeneousForcing {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : EulerTransversePacketProvider.Forcing P D 0

Zero forcing is an actual supported smooth cylinder path with zero angular integral.

Equations

• EulerPacketCylinderField.homogeneousForcing D = EulerPacketCylinderField.Field.transverseForcingOfRaw D (EulerPacketCylinderField.Field.zero P D.T) ⋯ ⋯

noncomputable def EulerPacketCylinderField.homogeneousPrimary {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (I : EulerTransversePacketProvider.InitialData P D) (O : EulerPacketProfileRecursion.Operators) : EulerPacketProfileRecursion.Profile

Homogeneous primary, given by primaryProfile O ((homogeneousForcing (P := P) D).vector I) ((homogeneousForcing (P := P) D).scalar I).

Equations

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

noncomputable def EulerPacketCylinderField.homogeneousPrimaryRegularity {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (I : EulerTransversePacketProvider.InitialData P D) (O : EulerPacketProfileRecursion.Operators) (hcorrector : O.curlCorrector = D.curlCorrector P) : ProfileRegularity P D.T ⋯ D.support (homogeneousPrimary D I O)

Homogeneous primary regularity, given by ProfileRegularity.primary (homogeneousForcing D) I O hcorrector.

Equations

• EulerPacketCylinderField.homogeneousPrimaryRegularity D I O hcorrector = EulerPacketCylinderField.ProfileRegularity.primary (EulerPacketCylinderField.homogeneousForcing D) I O hcorrector