Actual coefficient equations of the recursively constructed packet fields.

The constructed recursive forcing equals the full nonlinear coefficient forcing.

@[simp]

theorem EulerPacketProfileRecursion.zero_high : Profile.high 0 = 0

@[simp]

theorem EulerPacketProfileRecursion.zero_mean : Profile.mean 0 = 0

@[simp]

theorem EulerPacketProfileRecursion.zero_corrector : Profile.corrector 0 = 0

@[simp]

theorem EulerPacketProfileRecursion.zero_highPressure : Profile.highPressure 0 = 0

@[simp]

theorem EulerPacketProfileRecursion.zero_meanPressure : Profile.meanPressure 0 = 0

theorem EulerPacketProfileRecursion.slicedJet_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (z : EulerPacketPointJets.Domain) : EulerPacketPointJets.slicedJet s 0 z = 0

noncomputable def EulerPacketProfileRecursion.assembledJets (O : Operators) (N : ℕ) (a : ℕ → Profile) (z : EulerPacketPointJets.Domain) : ℕ → EulerPacketPointJets.VectorJet

Assembled jets, constructed using assemble.

Equations

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

theorem EulerPacketProfileRecursion.assembledJets_eq_velocityJet (O : Operators) (N : ℕ) (a : ℕ → Profile) (ha : a 0 = 0) (z : EulerPacketPointJets.Domain) (i : ℕ) (hi : i ≤ N) : assembledJets O N a z i = velocityJet O.interval a z i

theorem EulerPacketProfileRecursion.velocityJet_primary (O : Operators) (a : ℕ → Profile) (ha : a 0 = 0) (hmean : (a 1).mean = 0) (z : EulerPacketPointJets.Domain) : velocityJet O.interval a z 1 = EulerPacketPointJets.slicedJet O.interval (a 1).high z

theorem EulerPacketProfileRecursion.nonlinearGrade_cutoff (M K p : ℕ) (hM : p + 1 ≤ M) (hK : p + 1 ≤ K) (FInv : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : ℕ → EulerPacketPointJets.VectorJet) : EulerPacketPointJets.nonlinearGrade M p FInv m u = EulerPacketPointJets.nonlinearGrade K p FInv m u

theorem EulerPacketProfileRecursion.assembled_nonlinear_eq_known (O : Operators) (N p : ℕ) (hp : 2 ≤ p) (hpN : p ≤ N) (a : ℕ → Profile) (ha : a 0 = 0) (hmean : (a 1).mean = 0) (z : EulerPacketPointJets.Domain) (hprimary : inner ℝ (O.normal z) ((a 1).high z) = 0) (hhigh : inner ℝ (O.normal z) ((a p).high z) = 0) : EulerPacketPointJets.nonlinearGrade (N + 1) p (O.inverseFrame z) (O.normal z) (assembledJets O N a z) = EulerPacketPointJets.nonlinearGrade (p + 1) p (O.inverseFrame z) (O.normal z) (knownJets O p a z) + ((EulerPacketPointJets.fastAdvection (O.normal z)) (EulerPacketPointJets.slicedJet O.interval (a p).mean z)) (EulerPacketPointJets.slicedJet O.interval (a 1).high z)

Substituting the newly solved mean is the only change from the known forcing.

noncomputable def EulerPacketProfileRecursion.fullForce (O : Operators) (N p : ℕ) (a : ℕ → Profile) : VectorField

Full force as an element of VectorField.

Equations

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

theorem EulerPacketProfileRecursion.knownForce_sub_interaction (O : Operators) (N p : ℕ) (hp : 2 ≤ p) (hpN : p ≤ N) (a : ℕ → Profile) (ha : a 0 = 0) (hmean : (a 1).mean = 0) (z : EulerPacketPointJets.Domain) (hprimary : inner ℝ (O.normal z) ((a 1).high z) = 0) (hhigh : inner ℝ (O.normal z) ((a p).high z) = 0) : knownForce O p a z - ((EulerPacketPointJets.fastAdvection (O.normal z)) (EulerPacketPointJets.slicedJet O.interval (a p).mean z)) (EulerPacketPointJets.slicedJet O.interval (a 1).high z) = fullForce O N p a z

theorem EulerPacketProfileRecursion.recursive_forces_sum (O : Operators) (primary : Profile) (hmean : primary.mean = 0) (N p : ℕ) (hp : 2 ≤ p) (hpN : p ≤ N) (z : EulerPacketPointJets.Domain) (hprimary : inner ℝ (O.normal z) (primary.high z) = 0) (hhigh : inner ℝ (O.normal z) ((profiles O primary p).high z) = 0) : meanForce O p (profiles O primary) z + highForce O p (profiles O primary) z = fullForce O N p (profiles O primary) z

The two right-hand sides actually generated by recursion sum to source (14).

def EulerPacketProfileRecursion.assembledVelocity (N : ℕ) (a : ℕ → Profile) : ℕ → VectorField

Assembled velocity, given by assemble N (fun i => (a i).high+(a i).mean) (fun i => (a i).corrector).

Equations

• EulerPacketProfileRecursion.assembledVelocity N a = EulerFiniteGrades.assemble N (fun (i : ℕ) => (a i).high + (a i).mean) fun (i : ℕ) => (a i).corrector

def EulerPacketProfileRecursion.assembledPressure (N : ℕ) (a : ℕ → Profile) : ℕ → ScalarField

Assembled pressure, given by assemble N (fun i => (a i).meanPressure) (fun i => (a i).highPressure).

Equations

• EulerPacketProfileRecursion.assembledPressure N a = EulerFiniteGrades.assemble N (fun (i : ℕ) => (a i).meanPressure) fun (i : ℕ) => (a i).highPressure

noncomputable def EulerPacketProfileRecursion.pressureJets (N : ℕ) (a : ℕ → Profile) (z : EulerPacketPointJets.Domain) : ℕ → EulerPacketPointJets.ScalarJet

Pressure jets, given by assemble N (fun i => pressureJet (a i).meanPressure z) (fun i => pressureJet (a i).highPressure z).

Equations

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

noncomputable def EulerPacketProfileRecursion.recursiveGrade (O : Operators) (N : ℕ) (a : ℕ → Profile) (z : EulerPacketPointJets.Domain) (p : ℕ) : EulerSmoothLimit.Space

Recursive grade, constructed using coefficient.

Equations

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

theorem EulerPacketProfileRecursion.slicedJet_assembledVelocity (O : Operators) (N : ℕ) (a : ℕ → Profile) (z : EulerPacketPointJets.Domain) (hA : ∀ (i : ℕ), EulerPacketPointJets.SliceDifferentiable O.interval (a i).high z) (hB : ∀ (i : ℕ), EulerPacketPointJets.SliceDifferentiable O.interval (a i).mean z) (hC : ∀ (i : ℕ), EulerPacketPointJets.SliceDifferentiable O.interval (a i).corrector z) (i : ℕ) : EulerPacketPointJets.slicedJet O.interval (assembledVelocity N a i) z = assembledJets O N a z i

theorem EulerPacketProfileRecursion.pressureJet_assembledPressure (N : ℕ) (a : ℕ → Profile) (z : EulerPacketPointJets.Domain) (hq : ∀ (i : ℕ), DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => (a i).meanPressure (z.1, y)) z.2) (hπ : ∀ (i : ℕ), DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => (a i).highPressure (z.1, y)) z.2) (i : ℕ) : EulerPacketPointJets.pressureJet (assembledPressure N a i) z = pressureJets N a z i

theorem EulerPacketProfileRecursion.recursiveGrade_eq_actual (O : Operators) (N : ℕ) (a : ℕ → Profile) (z : EulerPacketPointJets.Domain) (hA : ∀ (i : ℕ), EulerPacketPointJets.SliceDifferentiable O.interval (a i).high z) (hB : ∀ (i : ℕ), EulerPacketPointJets.SliceDifferentiable O.interval (a i).mean z) (hC : ∀ (i : ℕ), EulerPacketPointJets.SliceDifferentiable O.interval (a i).corrector z) (hq : ∀ (i : ℕ), DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => (a i).meanPressure (z.1, y)) z.2) (hπ : ∀ (i : ℕ), DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => (a i).highPressure (z.1, y)) z.2) (p : ℕ) : EulerPacketPointJets.slicedMomentumGrade O.interval (N + 1) (O.inverseFrame z) (O.strain z) (O.normal z) (assembledVelocity N a) (assembledPressure N a) z p = recursiveGrade O N a z p

The coefficient is that of the literal finite sum, with actual interval derivatives.

theorem EulerPacketProfileRecursion.recursiveGrade_eq_zero (O : Operators) (primary : Profile) (hm : primary.mean = 0) (N p : ℕ) (hp : 2 ≤ p) (hpN : p ≤ N) (z : EulerPacketPointJets.Domain) (hprimary : inner ℝ (O.normal z) (primary.high z) = 0) (hhigh : inner ℝ (O.normal z) ((profiles O primary p).high z) = 0) (hqθ : ∀ i ≤ N, (EulerPacketPointJets.fastPressure (O.normal z)) (EulerPacketPointJets.pressureJet (profiles O primary i).meanPressure z) = 0) (hmeanEquation : (EulerPacketPointJets.linearPart (O.strain z)) (EulerPacketPointJets.slicedJet O.interval (profiles O primary p).mean z) + (EulerPacketPointJets.slowPressure (O.inverseFrame z)) (EulerPacketPointJets.pressureJet (profiles O primary p).meanPressure z) = meanForce O p (profiles O primary) z) (hhighEquation : (EulerPacketPointJets.linearPart (O.strain z)) (EulerPacketPointJets.slicedJet O.interval (profiles O primary p).high z) + (EulerPacketPointJets.fastPressure (O.normal z)) (EulerPacketPointJets.pressureJet (profiles O primary p).highPressure z) = highForce O p (profiles O primary) z) : recursiveGrade O N (profiles O primary) z p = 0

Solving the two linear equations used by the recursion cancels the whole grade.