The literal recursive high forcing is admissible for the constructed transverse inverse.

Support of the literal recursive high forcing

Exterior pure-mean interactions are angle-independent and are removed by the actual angular mean. The remaining terms use only the already supported prefix high fields, correctors and physical pressure gradients.

theorem EulerPacketCylinderField.Field.timeDerivative_zero_outside {P T : ℝ} [Fact (0 < P)] {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw_t) (hT : 0 < T) (hd : TimeDerivative ⋯ G H) (S : Set EulerSmoothLimit.Space) (hs : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ S, ∀ (θ : ℝ), raw (↑t, x, θ) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (hx : x ∉ S) (θ : ℝ) : raw_t (↑t, x, θ) = 0

theorem EulerPacketCylinderField.PrefixFields.knownForce_angleIndependent {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 1 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (S : Set EulerSmoothLimit.Space) (hS : IsClosed S) (L : PrefixLocality T p a S) (hpressure : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ S, ∀ (θ : ℝ), pressureGradient (a (p - 1)).highPressure (↑t, x, θ) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (hx : x ∉ S) (θ : ℝ) : EulerPacketProfileRecursion.knownForce O p a (↑t, x, θ) = EulerPacketProfileRecursion.knownForce O p a (↑t, x, 0)

theorem EulerPacketCylinderField.PrefixFields.highForce_zero_outside {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 2 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (S : Set EulerSmoothLimit.Space) (hS : IsClosed S) (L : PrefixLocality T p a S) (hpressure : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ S, ∀ (θ : ℝ), pressureGradient (a (p - 1)).highPressure (↑t, x, θ) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (hx : x ∉ S) (θ : ℝ) : EulerPacketProfileRecursion.highForce O p a (↑t, x, θ) = 0

def EulerPacketCylinderField.Field.changeTime {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {T' : ℝ} (G : Field P T raw) (h : T = T') : Field P T' raw

Change time, given by h ▸ G.

Equations

• G.changeTime h = h ▸ G

theorem EulerPacketCylinderField.Field.changeTime_derivative {P T : ℝ} [Fact (0 < P)] {raw raw_t : EulerPacketProfileRecursion.VectorField} {T' : ℝ} (G : Field P T raw) (H : Field P T raw_t) (h : T = T') (hT : 0 ≤ T) (hT' : 0 ≤ T') (hd : TimeDerivative hT G H) : TimeDerivative hT' (G.changeTime h) (H.changeTime h)

noncomputable def EulerPacketCylinderField.Field.transverseForcingOfRawTime {P T : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : T = D.T) (hs : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ D.support, ∀ (θ : ℝ), raw (↑t, x, θ) = 0) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, raw (↑t, x, θ) = 0) : EulerTransversePacketProvider.Forcing P D raw

Transverse forcing of raw time as an element of EulerTransversePacketProvider.Forcing P D raw.

Equations

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

noncomputable def EulerPacketCylinderField.PrefixFields.highForcing {P : ℝ} [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P M.T p a) (C : CoefficientData P M.T O) (hp : 2 ≤ p) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P M.T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P M.T (pressureGradient (a (p - 1)).highPressure)) (hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M) (L : PrefixLocality M.T p a D.support) (hpressure : ∀ (t : ↑(Set.Icc 0 M.T)), ∀ x ∉ D.support, ∀ (θ : ℝ), pressureGradient (a (p - 1)).highPressure (↑t, x, θ) = 0) : EulerTransversePacketProvider.Forcing P D (EulerPacketProfileRecursion.highForce O p a)

Every hypothesis concerns already constructed prefix fields or the actual prescribed coefficients.

Equations

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