Genuine regularity through the full literal profile recursion

Strong induction applies the constructed mean and high solvers at each grade. Only the primary profile is supplied; later forcing admissibility is proved.

theorem EulerPacketCylinderField.profiles_regular {P : ℝ} [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I : EulerTransversePacketProvider.InitialData P D) {O : EulerPacketProfileRecursion.Operators} (C : CoefficientData P M.T O) (hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M) (hhigh : O.highSolve = EulerTransversePacketProvider.highSolve P D I) (hcorrector : O.curlCorrector = D.curlCorrector P) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (p : ℕ) : Nonempty (ProfileRegularity P M.T ⋯ D.support (EulerPacketProfileRecursion.profiles O primary p))

noncomputable def EulerPacketCylinderField.profileWitness {P : ℝ} [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I : EulerTransversePacketProvider.InitialData P D) {O : EulerPacketProfileRecursion.Operators} (C : CoefficientData P M.T O) (hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M) (hhigh : O.highSolve = EulerTransversePacketProvider.highSolve P D I) (hcorrector : O.curlCorrector = D.curlCorrector P) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (p : ℕ) : ProfileRegularity P M.T ⋯ D.support (EulerPacketProfileRecursion.profiles O primary p)

Profile witness, given by Classical.choice (profiles_regular M D hT I C hmean hhigh hcorrector primary hprimary p).

Equations

• EulerPacketCylinderField.profileWitness M D hT I C hmean hhigh hcorrector primary hprimary p = Classical.choice ⋯

noncomputable def EulerPacketCylinderField.profilesMeanForcing {P : ℝ} [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I : EulerTransversePacketProvider.InitialData P D) {O : EulerPacketProfileRecursion.Operators} (C : CoefficientData P M.T O) (hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M) (hhigh : O.highSolve = EulerTransversePacketProvider.highSolve P D I) (hcorrector : O.curlCorrector = D.curlCorrector P) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (p : ℕ) (hp : 2 ≤ p) : EulerMeanPacketProvider.Forcing M (EulerPacketProfileRecursion.meanForce O p (EulerPacketProfileRecursion.profiles O primary))

The literal mean forcing at every nonprimary grade has actual smooth spatial L² slices.

Equations

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

noncomputable def EulerPacketCylinderField.profilesHighForcing {P : ℝ} [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I : EulerTransversePacketProvider.InitialData P D) {O : EulerPacketProfileRecursion.Operators} (C : CoefficientData P M.T O) (hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M) (hhigh : O.highSolve = EulerTransversePacketProvider.highSolve P D I) (hcorrector : O.curlCorrector = D.curlCorrector P) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (p : ℕ) (hp : 2 ≤ p) : EulerTransversePacketProvider.Forcing P D (EulerPacketProfileRecursion.highForce O p (EulerPacketProfileRecursion.profiles O primary))

The actual supported zero-mean transverse input is built from the already generated profiles.

Equations

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