A genuine recursion step using the full history/forward transverse inverse.

Support and zero angular mean of the literal joined corrector and its actual time derivative.

theorem EulerTransversePacketJoin.derivativePath_mean_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) : (EulerCylinderAngleAverage.average P) ((derivativePath τ hτ hτT B G) t) = 0

theorem EulerTransversePacketJoin.potentialPath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) : (potentialPath τ hτ hτT B G) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketJoin.potentialTimePath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) : (potentialTimePath τ hτ hτT B G) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketJoin.correctorPath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) : (correctorPath τ hτ hτT B G) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketJoin.correctorTimePath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) : (correctorTimePath τ hτ hτT B G) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketJoin.potentialPath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : (EulerCylinderAngleAverage.pathAverage P) (potentialPath τ hτ hτT B G) = 0

theorem EulerTransversePacketJoin.potentialTimePath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : (EulerCylinderAngleAverage.pathAverage P) (potentialTimePath τ hτ hτT B G) = 0

theorem EulerTransversePacketJoin.correctorPath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : (EulerCylinderAngleAverage.pathAverage P) (correctorPath τ hτ hτT B G) = 0

theorem EulerTransversePacketJoin.correctorTimePath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : (EulerCylinderAngleAverage.pathAverage P) (correctorTimePath τ hτ hτT B G) = 0

theorem EulerTransversePacketJoin.corrector_zero_outside {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ℝ) (x : EulerSmoothLimit.Space) (hx : x ∉ D.support) (θ : ℝ) : corrector τ hτ hτT B G (t, x, θ) = 0

theorem EulerTransversePacketJoin.correctorDerivative_zero_outside {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ℝ) (x : EulerSmoothLimit.Space) (hx : x ∉ D.support) (θ : ℝ) : correctorDerivative τ hτ hτT B G (t, x, θ) = 0

theorem EulerTransversePacketJoin.curlCorrector_mean_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, D.curlCorrector P (vector τ hτ hτT B G) (↑t, x, θ) = 0

noncomputable def EulerPacketCylinderField.ProfileRegularity.joinedStep {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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {O : EulerPacketProfileRecursion.Operators} (C : CoefficientData P M.T O) (hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M) (hhigh : O.highSolve = EulerTransversePacketJoin.highSolve τ hτ hτT B) (hcorrector : O.curlCorrector = D.curlCorrector P) {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (hp : 2 ≤ p) (G : (i : ℕ) → i < p → ProfileRegularity P M.T ⋯ D.support (a i)) : ProfileRegularity P M.T ⋯ D.support (EulerPacketProfileRecursion.step O p a)

Joined step as an element of ProfileRegularity P M.T M.T_pos.le D.support (EulerPacketProfileRecursion.step O p a).

Equations

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