The well-founded profile recursion in (14), on literal time/space/angle fields. Every new mean is computed before the new high coefficient. The supplied linear inverse maps are the interface to the analytic source constructions; this file proves the recursion and its dependence only on earlier grades.

The actual nonlinear packet operators have the triangular dependence claimed in (14).

Which unknown coefficients can enter the slow and fast quadratic terms.

theorem EulerFiniteGrades.convolution_strict_congr {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (M p : ℕ) (hp : 0 < p) (hMp : p ≤ M) (B : V →ₗ[ℝ] V →ₗ[ℝ] W) (u u' : ℕ → V) (hu0 : u 0 = 0) (hu : ∀ i < p, u' i = u i) : convolution M B u' u' p = convolution M B u u p

With zero constant coefficient, the slow grade p depends only on grades below p.

theorem EulerFiniteGrades.convolution_next_delta {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (M p : ℕ) (hp : 2 ≤ p) (hMp : p + 1 ≤ M) (B : V →ₗ[ℝ] V →ₗ[ℝ] W) (u u' : ℕ → V) (δ : V) (hu0 : u 0 = 0) (hu : ∀ i < p, u' i = u i) (hδ : u' p = u p + δ) : convolution M B u' u' (p + 1) = convolution M B u u (p + 1) + (B δ) (u 1) + (B (u 1)) δ

The fast grade p has exactly two possible dependencies on the new grade p.

theorem EulerPacketPointJets.fastAdvection_tangent_left (m : EulerSmoothLimit.Space) (J K : VectorJet) (hJ : inner ℝ m J.1 = 0) : ((fastAdvection m) J) K = 0

theorem EulerPacketPointJets.fastAdvection_angleConstant_right (m : EulerSmoothLimit.Space) (J K : VectorJet) (hK : K.2 angleDirection = 0) : ((fastAdvection m) J) K = 0

noncomputable def EulerPacketPointJets.nonlinearGrade (M p : ℕ) (FInv : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : ℕ → VectorJet) : EulerSmoothLimit.Space

Nonlinear grade, given by convolution M (slowAdvection FInv) u u p + convolution M (fastAdvection m) u u (p+1).

Equations

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

theorem EulerPacketPointJets.nonlinearGrade_update (M p : ℕ) (hp : 2 ≤ p) (hMp : p + 1 ≤ M) (FInv : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u u' : ℕ → VectorJet) (A B : VectorJet) (hu0 : u 0 = 0) (hu : ∀ i < p, u' i = u i) (hnew : u' p = u p + (A + B)) (hprimary : inner ℝ m (u 1).1 = 0) (hA : inner ℝ m A.1 = 0) : nonlinearGrade M p FInv m u' = nonlinearGrade M p FInv m u + ((fastAdvection m) B) (u 1)

Changing the new high coefficient and mean coefficient leaves just the mean-primary interaction.

theorem EulerPacketPointJets.nonlinearGrade_update_formula (M p : ℕ) (hp : 2 ≤ p) (hMp : p + 1 ≤ M) (FInv : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u u' : ℕ → VectorJet) (A B : VectorJet) (hu0 : u 0 = 0) (hu : ∀ i < p, u' i = u i) (hnew : u' p = u p + (A + B)) (hprimary : inner ℝ m (u 1).1 = 0) (hA : inner ℝ m A.1 = 0) : nonlinearGrade M p FInv m u' = nonlinearGrade M p FInv m u + inner ℝ m B.1 • (u 1).2 angleDirection

The surviving unknown term is literally (m dot B) times the primary angular derivative.

The known forcing at a recursive grade uses only previously constructed coefficients.

noncomputable def EulerPacketPointJets.history (p : ℕ) (u : ℕ → VectorJet) (previousCorrector : VectorJet) (i : ℕ) : VectorJet

History, with branches according to i<p.

Equations

• EulerPacketPointJets.history p u previousCorrector i = if i < p then u i else if i = p then previousCorrector else 0

theorem EulerPacketPointJets.history_congr (p : ℕ) (u v : ℕ → VectorJet) (c : VectorJet) (huv : ∀ i < p, u i = v i) : history p u c = history p v c

No unspecified coefficient at or above p enters the known part.

theorem EulerPacketPointJets.nonlinearGrade_eq_history (M p : ℕ) (hp : 2 ≤ p) (hMp : p + 1 ≤ M) (FInv : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : ℕ → VectorJet) (A B c : VectorJet) (hu0 : u 0 = 0) (hnew : u p = c + (A + B)) (hprimary : inner ℝ m (u 1).1 = 0) (hA : inner ℝ m A.1 = 0) : nonlinearGrade M p FInv m u = nonlinearGrade M p FInv m (history p u c) + ((fastAdvection m) B) (u 1)

The only new nonlinear term is the mean coefficient against the primary angular derivative.

theorem EulerPacketPointJets.mean_primary_interaction_zero (P : ℝ) (m B : EulerSmoothLimit.Space) (A Aθ : ℝ → EulerSmoothLimit.Space) (hA : ∀ (θ : ℝ), HasDerivAt A (Aθ θ) θ) (hAθ : Continuous Aθ) (hper : Function.Periodic A P) : ∫ (θ : ℝ) in 0..P, inner ℝ m B • Aθ θ = 0

The unknown mean-primary interaction has exactly zero angular mean.

@[reducible, inline]

abbrev EulerPacketProfileRecursion.VectorField : Type

Vector field: an abbreviation for Domain → Space.

Equations

• EulerPacketProfileRecursion.VectorField = (EulerPacketPointJets.Domain → EulerSmoothLimit.Space)

@[reducible, inline]

abbrev EulerPacketProfileRecursion.ScalarField : Type

Scalar field: an abbreviation for Domain → ℝ.

Equations

• EulerPacketProfileRecursion.ScalarField = (EulerPacketPointJets.Domain → ℝ)

structure EulerPacketProfileRecursion.Profile : Type

Profile data, collecting high, mean, corrector, highPressure, meanPressure, instance.

• high : VectorField

  High-frequency field of Profile, of type VectorField.

• mean : VectorField

  Mean field of Profile, of type VectorField.

• corrector : VectorField

  Correction field of Profile, of type VectorField.

• highPressure : ScalarField

  High-frequency pressure of Profile, of type ScalarField.

• meanPressure : ScalarField

  Mean pressure of Profile, of type ScalarField.

@[instance_reducible]

instance EulerPacketProfileRecursion.instZeroProfile : Zero Profile

Equations

• EulerPacketProfileRecursion.instZeroProfile = { zero := { high := 0, mean := 0, corrector := 0, highPressure := 0, meanPressure := 0 } }

structure EulerPacketProfileRecursion.Operators : Type

Operators data, collecting interval, period, inverseFrame, strain, normal, meanSolve and their compatibility conditions.

• interval : Set ℝ

  Interval of Operators, of type Set ℝ.

• period : ℝ

  Period of Operators, of type ℝ.

• inverseFrame : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

  Inverse frame of Operators, of type Domain → Space →L[ℝ] Space.

• strain : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

  Strain of Operators, of type Domain → Space →L[ℝ] Space.

• normal : VectorField

  Normal of Operators, of type VectorField.

• meanSolve : VectorField → VectorField × ScalarField

  Mean solve of Operators, of type VectorField → VectorField × ScalarField.

• highSolve : VectorField → VectorField × ScalarField

  High solve of Operators, of type VectorField → VectorField × ScalarField.

• curlCorrector : VectorField → VectorField

  Curl corrector of Operators, of type VectorField → VectorField.

noncomputable def EulerPacketProfileRecursion.angleMean (P : ℝ) (f : VectorField) : VectorField

Literal angular averaging at each time and spatial label.

Equations

• EulerPacketProfileRecursion.angleMean P f z = P⁻¹ • ∫ (θ : ℝ) in 0..P, f (z.1, z.2.1, θ)

noncomputable def EulerPacketProfileRecursion.velocityJet (s : Set ℝ) (a : ℕ → Profile) (z : EulerPacketPointJets.Domain) (i : ℕ) : EulerPacketPointJets.VectorJet

The stored coefficients determine the jets of V_i=A_i+B_i+C_{i-1}.

Equations

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

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

Known jets, given by history p (velocityJet O.interval a z) (slicedJet O.interval (a (p-1)).corrector z).

Equations

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

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

All terms of the grade-p forcing that are already determined.

Equations

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

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

Mean force, given by angleMean O.period (knownForce O p a).

Equations

• EulerPacketProfileRecursion.meanForce O p a = EulerPacketProfileRecursion.angleMean O.period (EulerPacketProfileRecursion.knownForce O p a)

noncomputable def EulerPacketProfileRecursion.meanResult (O : Operators) (p : ℕ) (a : ℕ → Profile) : VectorField × ScalarField

Mean result, given by O.meanSolve (meanForce O p a).

Equations

• EulerPacketProfileRecursion.meanResult O p a = O.meanSolve (EulerPacketProfileRecursion.meanForce O p a)

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

The sole new mean-primary interaction is added after solving the mean.

Equations

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

noncomputable def EulerPacketProfileRecursion.step (O : Operators) (p : ℕ) (a : ℕ → Profile) : Profile

Step, given by let b := meanResult O p a let h := O.highSolve (highForce O p a) ⟨h.1,b.1,O.curlCorrector h.1,h.2,b.2⟩.

Equations

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

theorem EulerPacketProfileRecursion.velocityJet_congr (s : Set ℝ) (p : ℕ) (a b : ℕ → Profile) (h : ∀ i < p, a i = b i) (z : EulerPacketPointJets.Domain) (i : ℕ) (hi : i < p) : velocityJet s a z i = velocityJet s b z i

theorem EulerPacketProfileRecursion.knownJets_congr (O : Operators) (p : ℕ) (hp : 1 ≤ p) (a b : ℕ → Profile) (h : ∀ i < p, a i = b i) (z : EulerPacketPointJets.Domain) : knownJets O p a z = knownJets O p b z

theorem EulerPacketProfileRecursion.knownForce_congr (O : Operators) (p : ℕ) (hp : 1 ≤ p) (a b : ℕ → Profile) (h : ∀ i < p, a i = b i) : knownForce O p a = knownForce O p b

theorem EulerPacketProfileRecursion.step_congr (O : Operators) (p : ℕ) (hp : 2 ≤ p) (a b : ℕ → Profile) (h : ∀ i < p, a i = b i) : step O p a = step O p b

At p≥2 the complete new profile depends only on the strict prefix.

noncomputable def EulerPacketProfileRecursion.recursionStep (O : Operators) (primary : Profile) (p : ℕ) (a : (i : ℕ) → i < p → Profile) : Profile

Recursion step, with branches according to p=0.

Equations

• EulerPacketProfileRecursion.recursionStep O primary p a = if p = 0 then 0 else if p = 1 then primary else EulerPacketProfileRecursion.step O p fun (i : ℕ) => if hi : i < p then a i hi else 0

noncomputable def EulerPacketProfileRecursion.profiles (O : Operators) (primary : Profile) : ℕ → Profile

All finite profile families are restrictions of this one well-founded sequence.

Equations

• EulerPacketProfileRecursion.profiles O primary t = Nat.strongRec (EulerPacketProfileRecursion.recursionStep O primary) t

theorem EulerPacketProfileRecursion.profiles_unfold (O : Operators) (primary : Profile) (p : ℕ) : profiles O primary p = recursionStep O primary p fun (i : ℕ) (x : i < p) => profiles O primary i

@[simp]

theorem EulerPacketProfileRecursion.profiles_zero (O : Operators) (primary : Profile) : profiles O primary 0 = 0

@[simp]

theorem EulerPacketProfileRecursion.profiles_one (O : Operators) (primary : Profile) : profiles O primary 1 = primary

theorem EulerPacketProfileRecursion.profiles_step (O : Operators) (primary : Profile) (p : ℕ) (hp : 2 ≤ p) : profiles O primary p = step O p (profiles O primary)

This is an actual recursive construction, not an existence assumption on profiles.

theorem EulerPacketProfileRecursion.profiles_mean (O : Operators) (primary : Profile) (p : ℕ) (hp : 2 ≤ p) : (profiles O primary p).mean = (meanResult O p (profiles O primary)).1

theorem EulerPacketProfileRecursion.profiles_high (O : Operators) (primary : Profile) (p : ℕ) (hp : 2 ≤ p) : (profiles O primary p).high = (O.highSolve (highForce O p (profiles O primary))).1

theorem EulerPacketProfileRecursion.profiles_corrector (O : Operators) (primary : Profile) (p : ℕ) (hp : 2 ≤ p) : (profiles O primary p).corrector = O.curlCorrector (profiles O primary p).high