The literal corrector of the joined high solution

The actual global velocity and its true time derivative construct Q, Q_t, C and C_t. The returned Field is for the literal raw curlCorrector used by the recursion, including at the history/forward junction.

noncomputable def EulerTransversePacketJoin.potentialPath {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) : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Potential path, given by EulerCylinderPotential.potentialPath P D.potentialCoefficientPath (velocityPath τ hτ hτT B G).

Equations

• EulerTransversePacketJoin.potentialPath τ hτ hτT B G = EulerCylinderPotential.potentialPath P D.potentialCoefficientPath (EulerTransversePacketJoin.velocityPath τ hτ hτT B G)

noncomputable def EulerTransversePacketJoin.potentialTimePath {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) : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Potential time path, constructed using EulerCylinderPotential.potentialDerivative.

Equations

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

theorem EulerTransversePacketJoin.potentialPath_orbit {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) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (potentialPath τ hτ hτT B G)

theorem EulerTransversePacketJoin.potentialTimePath_orbit {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) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (potentialTimePath τ hτ hτT B G)

theorem EulerTransversePacketJoin.potentialPath_time {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)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (potentialPath τ hτ hτT B G)) ((potentialTimePath τ hτ hτT B G) t) (Set.Icc 0 D.T) ↑t

noncomputable def EulerTransversePacketJoin.correctorPath {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) : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Corrector path, given by EulerCylinderSlowCurl.path P D.FInv.field (potentialPath τ hτ hτT B G).

Equations

• EulerTransversePacketJoin.correctorPath τ hτ hτT B G = EulerCylinderSlowCurl.path P D.FInv.field (EulerTransversePacketJoin.potentialPath τ hτ hτT B G)

noncomputable def EulerTransversePacketJoin.correctorTimePath {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) : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Corrector time path, constructed using EulerCylinderSlowCurl.derivative.

Equations

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

theorem EulerTransversePacketJoin.correctorPath_orbit {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) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (correctorPath τ hτ hτT B G)

theorem EulerTransversePacketJoin.correctorTimePath_orbit {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) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (correctorTimePath τ hτ hτT B G)

theorem EulerTransversePacketJoin.correctorPath_time {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)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (correctorPath τ hτ hτT B G)) ((correctorTimePath τ hτ hτT B G) t) (Set.Icc 0 D.T) ↑t

noncomputable def EulerTransversePacketJoin.corrector {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) : EulerPacketProfileRecursion.VectorField

Corrector, defined pointwise by pointField P (correctorPath τ hτ hτT B G) (correctorPath_orbit τ hτ hτT B G) (D.clamp z.1) (z.2.1,(z.2.2 : AddCircle P)).

Equations

• EulerTransversePacketJoin.corrector τ hτ hτT B G z = EulerCylinderSmoothOrbit.pointField P (EulerTransversePacketJoin.correctorPath τ hτ hτT B G) ⋯ (D.clamp z.1) (z.2.1, ↑z.2.2)

noncomputable def EulerTransversePacketJoin.correctorDerivative {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) : EulerPacketProfileRecursion.VectorField

Corrector derivative, defined pointwise by pointField P (correctorTimePath τ hτ hτT B G) (correctorTimePath_orbit τ hτ hτT B G) (D.clamp z.1) (z.2.1,(z.2.2 : AddCircle P)).

Equations

• EulerTransversePacketJoin.correctorDerivative τ hτ hτT B G z = EulerCylinderSmoothOrbit.pointField P (EulerTransversePacketJoin.correctorTimePath τ hτ hτT B G) ⋯ (D.clamp z.1) (z.2.1, ↑z.2.2)

theorem EulerTransversePacketJoin.velocityPath_raw_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, EulerCylinderSmoothOrbit.pointField P (velocityPath τ hτ hτT B G) ⋯ t (x, ↑θ) = 0

theorem EulerTransversePacketJoin.rawPotential_eq {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) (θ : ℝ) : D.rawPotential P (vector τ hτ hτT B G) (↑t, x, θ) = EulerCylinderSmoothOrbit.pointField P (potentialPath τ hτ hτT B G) ⋯ t (x, ↑θ)

theorem EulerTransversePacketJoin.corrector_formula {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) (θ : ℝ) : corrector τ hτ hτT B G (↑t, x, θ) = EulerMeanBoundary.curlMatrix (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P (potentialPath τ hτ hτT B G) ⋯ t) (x, ↑θ) ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL (D.FInv.field t) x)

theorem EulerTransversePacketJoin.curlCorrector_eq {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) (θ : ℝ) : D.curlCorrector P (vector τ hτ hτT B G) (↑t, x, θ) = corrector τ hτ hτT B G (↑t, x, θ)

noncomputable def EulerTransversePacketJoin.correctorField {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) : EulerPacketCylinderField.Field P D.T (D.curlCorrector P (vector τ hτ hτT B G))

Corrector field, bundling path, orbit, raw_eq.

Equations

• EulerTransversePacketJoin.correctorField τ hτ hτT B G = { path := EulerTransversePacketJoin.correctorPath τ hτ hτT B G, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerTransversePacketJoin.correctorDerivativeField {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) : EulerPacketCylinderField.Field P D.T (correctorDerivative τ hτ hτT B G)

Corrector derivative field, bundling path, orbit, raw_eq.

Equations

• EulerTransversePacketJoin.correctorDerivativeField τ hτ hτT B G = { path := EulerTransversePacketJoin.correctorTimePath τ hτ hτT B G, orbit := ⋯, raw_eq := ⋯ }

theorem EulerTransversePacketJoin.correctorField_time {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) : EulerPacketCylinderField.TimeDerivative ⋯ (correctorField τ hτ hτT B G) (correctorDerivativeField τ hτ hτT B G)