Actual source profiles for the complete high inverse. The primary datum is a genuine profile with its path/time witnesses; every later forcing is proved admissible and every later profile is constructed by the two source inverses.

The complete history/forward high inverse preserves the actual recursive symmetries.

theorem EulerPacketCylinderField.ProfileParity.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) (E : CoefficientEven M.T O) (eM : EulerMeanPacketProvider.EvenData M) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hDM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hBH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (hp : 2 ≤ p) (G : (i : ℕ) → i < p → ProfileRegularity P M.T ⋯ D.support (a i)) (H : ∀ i < p, ProfileParity M.T (a i)) : ProfileParity M.T (EulerPacketProfileRecursion.step O p a)

All-grade admissibility for the actual history/forward packet recursion.

theorem EulerPacketCylinderField.joined_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) (τ : ℝ) (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) (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.joinedProfileWitness {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) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (p : ℕ) : ProfileRegularity P M.T ⋯ D.support (EulerPacketProfileRecursion.profiles O primary p)

Joined profile witness, given by Classical.choice (joined_profiles_regular M D hT τ hτ hτT B C hmean hhigh hcorrector primary hprimary p).

Equations

• EulerPacketCylinderField.joinedProfileWitness M D hT τ hτ hτT B C hmean hhigh hcorrector primary hprimary p = Classical.choice ⋯

noncomputable def EulerPacketCylinderField.joinedProfilesMeanForcing {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) (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))

Joined profiles mean forcing as an element of EulerMeanPacketProvider.Forcing M (meanForce O p (profiles O primary)).

Equations

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

noncomputable def EulerPacketCylinderField.joinedProfilesHighForcing {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) (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))

Joined profiles high forcing as an element of EulerTransversePacketProvider.Forcing P D (highForce O p (profiles O primary)).

Equations

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

Every grade constructed with the joined inverse has the prescribed joint parity.

theorem EulerPacketCylinderField.joined_profiles_parity {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) (E : CoefficientEven M.T O) (eM : EulerMeanPacketProvider.EvenData M) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hDM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hBH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (hprimaryParity : ProfileParity M.T primary) (p : ℕ) : ProfileParity M.T (EulerPacketProfileRecursion.profiles O primary p)

noncomputable def EulerPacketCylinderField.joinedSourceProfiles (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {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τ ⋯)) (primary : EulerPacketProfileRecursion.Profile) : ℕ → EulerPacketProfileRecursion.Profile

Joined source profiles, given by profiles (joinedSourceOperators P M D τ hτ hτT B) primary.

Equations

• EulerPacketCylinderField.joinedSourceProfiles P M D τ hτ hτT B primary = EulerPacketProfileRecursion.profiles (EulerPacketCylinderField.joinedSourceOperators P M D τ hτ hτT B) primary

noncomputable def EulerPacketCylinderField.joinedSourceProfileWitness (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τ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (p : ℕ) : ProfileRegularity P M.T ⋯ D.support (joinedSourceProfiles P M D τ hτ hτT B primary p)

Joined source profile witness, given by joinedProfileWitness M D hT τ hτ hτT B (joinedSourceCoefficientData P M D τ hτ hτT B hT) rfl rfl rfl primary hprimary p.

Equations

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

noncomputable def EulerPacketCylinderField.joinedSourceMeanForcing (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τ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (p : ℕ) (hp : 2 ≤ p) : EulerMeanPacketProvider.Forcing M (EulerPacketProfileRecursion.meanForce (joinedSourceOperators P M D τ hτ hτT B) p (joinedSourceProfiles P M D τ hτ hτT B primary))

Joined source mean forcing, given by joinedProfilesMeanForcing M D hT τ hτ hτT B (joinedSourceCoefficientData P M D τ hτ hτT B hT) rfl rfl rfl primary hprimary p hp.

Equations

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

noncomputable def EulerPacketCylinderField.joinedSourceHighForcing (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τ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (p : ℕ) (hp : 2 ≤ p) : EulerTransversePacketProvider.Forcing P D (EulerPacketProfileRecursion.highForce (joinedSourceOperators P M D τ hτ hτT B) p (joinedSourceProfiles P M D τ hτ hτT B primary))

Joined source high forcing, given by joinedProfilesHighForcing M D hT τ hτ hτT B (joinedSourceCoefficientData P M D τ hτ hτT B hT) rfl rfl rfl primary hprimary p hp.

Equations

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

theorem EulerPacketCylinderField.joinedSourceCoefficientEven (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {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τ ⋯)) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) : CoefficientEven M.T (joinedSourceOperators P M D τ hτ hτT B)

theorem EulerPacketCylinderField.joinedSourceProfiles_parity (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τ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (eM : EulerMeanPacketProvider.EvenData M) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hDM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hBH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hprimaryParity : ProfileParity M.T primary) (p : ℕ) : ProfileParity M.T (joinedSourceProfiles P M D τ hτ hτT B primary p)