The triangular ray system and its perturbation estimates. These results derive ray closeness from the differential equations and coefficient errors.

def EulerPacketRay.norm3 (p q n : ℝ) : ℝ

The sum norm of three scalar coordinates.

Equations

• EulerPacketRay.norm3 p q n = |p| + |q| + |n|

theorem EulerPacketRay.triangular_ray_formula {β T : ℝ} {P Q N f g h : ℝ → ℝ} (hP : ∀ t ∈ Set.Icc 0 T, HasDerivAt P (-Q t + f t) t) (hQ : ∀ t ∈ Set.Icc 0 T, HasDerivAt Q (-2 * β * N t + g t) t) (hN : ∀ t ∈ Set.Icc 0 T, HasDerivAt N (h t) t) (hfc : ContinuousOn f (Set.Icc 0 T)) (hgc : ContinuousOn g (Set.Icc 0 T)) (hhc : ContinuousOn h (Set.Icc 0 T)) (t : ℝ) : t ∈ Set.Icc 0 T → P t = P 0 - t * Q 0 + β * t ^ 2 * N 0 + ∫ (s : ℝ) in 0..t, f s - (t - s) * g s + β * (t - s) ^ 2 * h s ∧ Q t = Q 0 - 2 * β * t * N 0 + ∫ (s : ℝ) in 0..t, g s - 2 * β * (t - s) * h s ∧ N t = N 0 + ∫ (s : ℝ) in 0..t, h s

Exact Duhamel formulas for the triangular ray system.

theorem EulerPacketRay.triangular_ray_kernel_bound {β Θ d p q n : ℝ} (hβ : 0 ≤ β) (hβupper : β ≤ 1) (hΘ : 1 ≤ Θ) (hd : 0 ≤ d) (hdΘ : d ≤ Θ) : norm3 (p - d * q + β * d ^ 2 * n) (q - 2 * β * d * n) n ≤ 4 * Θ ^ 2 * norm3 p q n

The triangular ray propagator has a polynomial norm bound.

theorem EulerPacketRay.triangular_ray_forced_bound {β Θ T : ℝ} {P Q N f g h : ℝ → ℝ} (hβ : 0 ≤ β) (hβupper : β ≤ 1) (hΘ : 1 ≤ Θ) (hT : T ≤ Θ) (hP : ∀ t ∈ Set.Icc 0 T, HasDerivAt P (-Q t + f t) t) (hQ : ∀ t ∈ Set.Icc 0 T, HasDerivAt Q (-2 * β * N t + g t) t) (hN : ∀ t ∈ Set.Icc 0 T, HasDerivAt N (h t) t) (hfc : ContinuousOn f (Set.Icc 0 T)) (hgc : ContinuousOn g (Set.Icc 0 T)) (hhc : ContinuousOn h (Set.Icc 0 T)) (t : ℝ) : t ∈ Set.Icc 0 T → norm3 (P t) (Q t) (N t) ≤ 4 * Θ ^ 2 * norm3 (P 0) (Q 0) (N 0) + 4 * Θ ^ 2 * ∫ (s : ℝ) in 0..t, norm3 (f s) (g s) (h s)

The exact triangular ray equations imply a polynomial Duhamel bound.

theorem EulerPacketRay.triangular_ray_perturbed_bound {β Θ T δ : ℝ} {P Q N f g h : ℝ → ℝ} (hβ : 0 ≤ β) (hβupper : β ≤ 1) (hΘ : 1 ≤ Θ) (hT0 : 0 ≤ T) (hT : T ≤ Θ) (hδ : 0 ≤ δ) (hsmall : 4 * Θ ^ 2 * δ * T ≤ 1 / 2) (hP : ∀ t ∈ Set.Icc 0 T, HasDerivAt P (-Q t + f t) t) (hQ : ∀ t ∈ Set.Icc 0 T, HasDerivAt Q (-2 * β * N t + g t) t) (hN : ∀ t ∈ Set.Icc 0 T, HasDerivAt N (h t) t) (hfc : ContinuousOn f (Set.Icc 0 T)) (hgc : ContinuousOn g (Set.Icc 0 T)) (hhc : ContinuousOn h (Set.Icc 0 T)) (hforcing : ∀ t ∈ Set.Icc 0 T, norm3 (f t) (g t) (h t) ≤ δ * norm3 (P t) (Q t) (N t)) (t : ℝ) : t ∈ Set.Icc 0 T → norm3 (P t) (Q t) (N t) ≤ 8 * Θ ^ 2 * norm3 (P 0) (Q 0) (N 0)

A small perturbation of the triangular ray system remains polynomially bounded on the whole interval.

theorem EulerPacketRay.triangular_ray_difference_bound {β Θ T δ η : ℝ} {P Q N f g h : ℝ → ℝ} (hβ : 0 ≤ β) (hβupper : β ≤ 1) (hΘ : 1 ≤ Θ) (hT0 : 0 ≤ T) (hT : T ≤ Θ) (hδ : 0 ≤ δ) (hη : 0 ≤ η) (hsmall : 4 * Θ ^ 2 * δ * T ≤ 1 / 2) (hP : ∀ t ∈ Set.Icc 0 T, HasDerivAt P (-Q t + f t) t) (hQ : ∀ t ∈ Set.Icc 0 T, HasDerivAt Q (-2 * β * N t + g t) t) (hN : ∀ t ∈ Set.Icc 0 T, HasDerivAt N (h t) t) (hfc : ContinuousOn f (Set.Icc 0 T)) (hgc : ContinuousOn g (Set.Icc 0 T)) (hhc : ContinuousOn h (Set.Icc 0 T)) (hforcing : ∀ t ∈ Set.Icc 0 T, norm3 (f t) (g t) (h t) ≤ δ * norm3 (P t) (Q t) (N t)) (hinitial : norm3 (P 0) (Q 0) (N 0 - 1) ≤ η) (t : ℝ) : t ∈ Set.Icc 0 T → norm3 (P t - β * t ^ 2) (Q t + 2 * β * t) (N t - 1) ≤ 4 * Θ ^ 2 * η + 32 * δ * Θ ^ 5 * (1 + η)

Ray closeness is derived from the ODE and the forcing bound, with a polynomial loss and arbitrary small initial ray error.

def EulerPacketRay.idealRayEntry (β : ℝ) (i j : Fin 3) : ℝ

Entries of the triangular ideal ray generator.

Equations

• EulerPacketRay.idealRayEntry β i j = if i = 0 ∧ j = 1 then -1 else if i = 1 ∧ j = 2 then -2 * β else 0

theorem EulerPacketRay.three_term_bound {a b c p q n e : ℝ} (ha : |a| ≤ e) (hb : |b| ≤ e) (hc : |c| ≤ e) : |a * p + b * q + c * n| ≤ e * norm3 p q n

theorem EulerPacketRay.ray_closeness_of_coefficient_error {β Θ T e : ℝ} {A : ℝ → Fin 3 → Fin 3 → ℝ} {P Q N : ℝ → ℝ} (hβ : 0 ≤ β) (hβupper : β ≤ 1) (hΘ : 1 ≤ Θ) (hT0 : 0 ≤ T) (hT : T ≤ Θ) (he : 0 ≤ e) (hsmall : 400 * e * Θ ^ 5 ≤ 1) (hAc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => A t i j) (Set.Icc 0 T)) (hP : ∀ t ∈ Set.Icc 0 T, HasDerivAt P (A t 0 0 * P t + A t 0 1 * Q t + A t 0 2 * N t) t) (hQ : ∀ t ∈ Set.Icc 0 T, HasDerivAt Q (A t 1 0 * P t + A t 1 1 * Q t + A t 1 2 * N t) t) (hN : ∀ t ∈ Set.Icc 0 T, HasDerivAt N (A t 2 0 * P t + A t 2 1 * Q t + A t 2 2 * N t) t) (hclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |A t i j - idealRayEntry β i j| ≤ e) (hinitial : norm3 (P 0) (Q 0) (N 0 - 1) ≤ e) (t : ℝ) : t ∈ Set.Icc 0 T → norm3 (P t - β * t ^ 2) (Q t + 2 * β * t) (N t - 1) ≤ 200 * e * Θ ^ 5 ∧ 1 / 2 ≤ N t

The ray closeness estimate follows from entrywise coefficient error. No closeness of the ray itself is assumed. The third component stays away from zero, as required to eliminate the third velocity coordinate.

def EulerPacketRay.frameSkew (B : Fin 3 → Fin 3 → ℝ) (i j : Fin 3) : ℝ

The skew matrix of the moving orthonormal frame in the source.

Equations

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

def EulerPacketRay.parentEntry (B E : Fin 3 → Fin 3 → ℝ) (h : ℝ) (i j : Fin 3) : ℝ

The older gradient plus rank-one parent shear and error.

Equations

• EulerPacketRay.parentEntry B E h i j = B i j + E i j + if i = 1 ∧ j = 0 then h else 0

def EulerPacketRay.rayScale (ε : ℝ) (i : Fin 3) : ℝ

Coordinate scaling for the normalized ray.

Equations

• EulerPacketRay.rayScale ε i = if i = 1 then ε else 1

noncomputable def EulerPacketRay.scaledRayEntry (a ε : ℝ) (M S : Fin 3 → Fin 3 → ℝ) (i j : Fin 3) : ℝ

Coefficients after the moving-frame transformation and the scaling m/s₀=(P,εQ,N), dt/dτ=ε/a.

Equations

• EulerPacketRay.scaledRayEntry a ε M S i j = -(ε / a) * (EulerPacketRay.rayScale ε j / EulerPacketRay.rayScale ε i) * (M j i - S j i)

def EulerPacketRay.normalizedRayEntry (ε H κ : ℝ) (B E : Fin 3 → Fin 3 → ℝ) (i j : Fin 3) : ℝ

The scaled moving-frame ray entries in normalized coefficients.

Equations

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

theorem EulerPacketRay.scaled_ray_entry_identity {a ε h : ℝ} {B E : Fin 3 → Fin 3 → ℝ} (ha : a ≠ 0) (hε : ε ≠ 0) (i j : Fin 3) : scaledRayEntry a ε (parentEntry B E h) (frameSkew B) i j = normalizedRayEntry ε (ε ^ 2 * h / a) (B 2 1 / a) (fun (i j : Fin 3) => ε * B i j / a) (fun (i j : Fin 3) => E i j / a) i j

Exact entries of the scaled moving-frame ray matrix.

theorem EulerPacketRay.normalized_ray_entry_error {ε H κ β e : ℝ} {B E : Fin 3 → Fin 3 → ℝ} (hε : 0 ≤ ε) (hεupper : ε ≤ 1) (he : 0 ≤ e) (hB : ∀ (i j : Fin 3), |B i j| ≤ e) (hE : ∀ (i j : Fin 3), |E i j| ≤ e) (hH : |H - 1| ≤ e) (hκ : |κ - β| ≤ e) (i j : Fin 3) : |normalizedRayEntry ε H κ B E i j - idealRayEntry β i j| ≤ 4 * e

Each scaled matrix entry is close to the triangular ideal matrix when the normalized older-gradient, error, shear, and coupling coefficients are small.

theorem EulerPacketRay.scaled_ray_entry_error {a ε h β e : ℝ} {B E : Fin 3 → Fin 3 → ℝ} (ha : a ≠ 0) (hε : 0 < ε) (hεupper : ε ≤ 1) (he : 0 ≤ e) (hB : ∀ (i j : Fin 3), |ε * B i j / a| ≤ e) (hE : ∀ (i j : Fin 3), |E i j / a| ≤ e) (hH : |ε ^ 2 * h / a - 1| ≤ e) (hκ : |B 2 1 / a - β| ≤ e) (i j : Fin 3) : |scaledRayEntry a ε (parentEntry B E h) (frameSkew B) i j - idealRayEntry β i j| ≤ 4 * e

The original moving-frame entries imply the coefficient hypothesis of ray_closeness_of_coefficient_error.

theorem EulerPacketRay.abs_product_difference {a b c d ea eb A B : ℝ} (ha : |a - c| ≤ ea) (hb : |b - d| ≤ eb) (hc : |c| ≤ A) (hd : |b| ≤ B) : |a * b - c * d| ≤ ea * B + A * eb

A product difference estimate used to control the projection denominator.

noncomputable def EulerPacketRay.velocityThird (P Q N U V : ℝ) : ℝ

The third velocity coordinate imposed by ray orthogonality.

Equations

• EulerPacketRay.velocityThird P Q N U V = -(P * U + Q * V) / N

def EulerPacketRay.rayDenominator (ε P Q N : ℝ) : ℝ

Squared norm of the scaled ray.

Equations

• EulerPacketRay.rayDenominator ε P Q N = P ^ 2 + ε ^ 2 * Q ^ 2 + N ^ 2

theorem EulerPacketRay.ray_geometric_bounds {Θ ρ ε P Q N P₀ Q₀ U V : ℝ} (hΘ : 1 ≤ Θ) (hρ : 0 ≤ ρ) (hρupper : ρ ≤ 1 / 2) (hP₀ : |P₀| ≤ Θ ^ 2) (hQ₀ : |Q₀| ≤ 2 * Θ ^ 2) (hP : |P - P₀| ≤ ρ) (hQ : |Q - Q₀| ≤ ρ) (hN : |N - 1| ≤ ρ) : 1 / 2 ≤ N ∧ |P| ≤ 2 * Θ ^ 2 ∧ |Q| ≤ 3 * Θ ^ 2 ∧ |N| ≤ 2 ∧ |velocityThird P Q N U V| ≤ 6 * Θ ^ 2 * (|U| + |V|) ∧ 1 / 4 ≤ rayDenominator ε P Q N ∧ |rayDenominator ε P Q N - (1 + P₀ ^ 2)| ≤ 6 * ρ * Θ ^ 2 + 9 * ε ^ 2 * Θ ^ 4

Elimination of the third velocity component and the denominator estimate are consequences of the proved ray error.

def EulerPacketRay.normalizedVelocityEntry (ε H α κ : ℝ) (B E : Fin 3 → Fin 3 → ℝ) (i j : Fin 3) : ℝ

The three rows entering J_v, with the middle row multiplied by ε.

Equations

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

def EulerPacketRay.idealVelocityEntry (β : ℝ) (i j : Fin 3) : ℝ

The ideal scaled parent action on velocity coordinates.

Equations

• EulerPacketRay.idealVelocityEntry β i j = if i = 0 ∧ j = 1 ∨ i = 1 ∧ j = 0 then 1 else if i = 2 ∧ j = 1 then β else 0

noncomputable def EulerPacketRay.scaledVelocityEntry (a ε : ℝ) (M : Fin 3 → Fin 3 → ℝ) (i j : Fin 3) : ℝ

Parent-gradient entries after ray and velocity rescaling.

Equations

• EulerPacketRay.scaledVelocityEntry a ε M i j = ((if i = 1 then ε else 1) * if j = 1 then 1 else ε) * M i j / a

theorem EulerPacketRay.scaled_velocity_entry_identity {a ε h : ℝ} {B E : Fin 3 → Fin 3 → ℝ} (ha : a ≠ 0) (i j : Fin 3) : scaledVelocityEntry a ε (parentEntry B E h) i j = normalizedVelocityEntry ε (ε ^ 2 * h / a) (B 0 1 / a) (B 2 1 / a) (fun (i j : Fin 3) => ε * B i j / a) (fun (i j : Fin 3) => E i j / a) i j

theorem EulerPacketRay.normalized_velocity_entry_error {ε H α κ β e : ℝ} {B E : Fin 3 → Fin 3 → ℝ} (hε : 0 ≤ ε) (hεupper : ε ≤ 1) (he : 0 ≤ e) (hB : ∀ (i j : Fin 3), |B i j| ≤ e) (hE : ∀ (i j : Fin 3), |E i j| ≤ e) (hH : |H - 1| ≤ e) (hα : |α - 1| ≤ e) (hκ : |κ - β| ≤ e) (i j : Fin 3) : |normalizedVelocityEntry ε H α κ B E i j - idealVelocityEntry β i j| ≤ 3 * e

def EulerPacketRay.velocityNumerator (A : Fin 3 → Fin 3 → ℝ) (P Q N U V W : ℝ) : ℝ

The scalar pressure numerator in the scaled coordinates.

Equations

• EulerPacketRay.velocityNumerator A P Q N U V W = P * (A 0 0 * U + A 0 1 * V + A 0 2 * W) + Q * (A 1 0 * U + A 1 1 * V + A 1 2 * W) + N * (A 2 0 * U + A 2 1 * V + A 2 2 * W)

theorem EulerPacketRay.velocity_numerator_error {A : Fin 3 → Fin 3 → ℝ} {Θ ρ e β P Q N P₀ Q₀ U V W : ℝ} (hΘ : 1 ≤ Θ) (hρ : 0 ≤ ρ) (he : 0 ≤ e) (hβ : |β| ≤ 1) (hA : ∀ (i j : Fin 3), |A i j - idealVelocityEntry β i j| ≤ e) (hp : |P| ≤ 2 * Θ ^ 2) (hq : |Q| ≤ 3 * Θ ^ 2) (hn : |N| ≤ 2) (hP : |P - P₀| ≤ ρ) (hQ : |Q - Q₀| ≤ ρ) (hN : |N - 1| ≤ ρ) (hw : |W| ≤ 6 * Θ ^ 2 * (|U| + |V|)) : |velocityNumerator A P Q N U V W - ((P₀ + β) * V + Q₀ * U)| ≤ (49 * e * Θ ^ 4 + 2 * ρ) * (|U| + |V|)

def EulerPacketRay.normalizedUnprojectedEntry (ε H α : ℝ) (B E : Fin 3 → Fin 3 → ℝ) (i j : Fin 3) : ℝ

The first two velocity rows before pressure projection.

Equations

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

def EulerPacketRay.idealUnprojectedEntry (i j : Fin 3) : ℝ

Ideal entries of the unprojected two-component velocity equation.

Equations

• EulerPacketRay.idealUnprojectedEntry i j = if i = 0 then if j = 1 then 2 else 0 else if j = 0 then 1 else 0

theorem EulerPacketRay.scaled_unprojected_entry_identity {a ε h : ℝ} {B E : Fin 3 → Fin 3 → ℝ} (ha : a ≠ 0) (j : Fin 3) : scaledVelocityEntry a ε (fun (i j : Fin 3) => parentEntry B E h i j + frameSkew B i j) 0 j = normalizedUnprojectedEntry ε (ε ^ 2 * h / a) (B 0 1 / a) (fun (i j : Fin 3) => ε * B i j / a) (fun (i j : Fin 3) => E i j / a) 0 j ∧ scaledVelocityEntry a ε (fun (i j : Fin 3) => parentEntry B E h i j + frameSkew B i j) 1 j = normalizedUnprojectedEntry ε (ε ^ 2 * h / a) (B 0 1 / a) (fun (i j : Fin 3) => ε * B i j / a) (fun (i j : Fin 3) => E i j / a) 1 j

Exact first and second rows of the moving-frame velocity operator.

theorem EulerPacketRay.normalized_unprojected_entry_error {ε H α e : ℝ} {B E : Fin 3 → Fin 3 → ℝ} (hε : 0 ≤ ε) (hεe : ε ≤ e) (he : 0 ≤ e) (heupper : e ≤ 1) (hB : ∀ (i j : Fin 3), |B i j| ≤ e) (hE : ∀ (i j : Fin 3), |E i j| ≤ e) (hH : |H - 1| ≤ e) (hα : |α - 1| ≤ e) (i j : Fin 3) : |normalizedUnprojectedEntry ε H α B E i j - idealUnprojectedEntry i j| ≤ 5 * e

theorem EulerPacketRay.quotient_difference_bound {P P₀ D D₀ ρ d A : ℝ} (hD : 1 / 4 ≤ D) (hD₀ : 1 ≤ D₀) (hP : |P - P₀| ≤ ρ) (hP₀ : |P₀| ≤ A) (hDD : |D - D₀| ≤ d) : |P / D - P₀ / D₀| ≤ 4 * ρ + 4 * A * d

A quotient difference bound requiring only the quantitative lower bounds actually available for the ray denominator.

theorem EulerPacketRay.velocity_projection_error {Θ ρ d j ε P Q D P₀ D₀ J J₀ U V : ℝ} (hΘ : 1 ≤ Θ) (hρ : 0 ≤ ρ) (hd : 0 ≤ d) (_hj : 0 ≤ j) (hjupper : j ≤ 1) (hD : 1 / 4 ≤ D) (hD₀ : 1 ≤ D₀) (hP : |P - P₀| ≤ ρ) (hP₀ : |P₀| ≤ Θ ^ 2) (hp : |P| ≤ 2 * Θ ^ 2) (hq : |Q| ≤ 3 * Θ ^ 2) (hDD : |D - D₀| ≤ d) (hJ : |J - J₀| ≤ j * (|U| + |V|)) (hJ₀ : |J₀| ≤ 2 * Θ ^ 2 * (|U| + |V|)) : |2 * P * J / D - 2 * P₀ * J₀ / D₀| + |2 * ε ^ 2 * Q * J / D| ≤ (16 * Θ ^ 2 * j + 16 * ρ * Θ ^ 2 + 16 * Θ ^ 4 * d + 72 * ε ^ 2 * Θ ^ 4) * (|U| + |V|)

Quantitative stability of the two pressure projection components.

noncomputable def EulerPacketRay.velocityFirstRhs (A C : Fin 3 → Fin 3 → ℝ) (ε P Q N U V : ℝ) : ℝ

The first normalized velocity equation with pressure projection.

Equations

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

noncomputable def EulerPacketRay.velocitySecondRhs (A C : Fin 3 → Fin 3 → ℝ) (ε P Q N U V : ℝ) : ℝ

The second normalized velocity equation with pressure projection.

Equations

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

theorem EulerPacketRay.velocity_rhs_error {A C : Fin 3 → Fin 3 → ℝ} {Θ e ε β P Q N P₀ Q₀ U V : ℝ} (hΘ : 1 ≤ Θ) (he : 0 ≤ e) (hε : 0 ≤ ε) (hεe : ε ≤ e) (hsmall : 10000 * e * Θ ^ 5 ≤ 1) (hβ : |β| ≤ 1) (hA : ∀ (i j : Fin 3), |A i j - idealVelocityEntry β i j| ≤ 3 * e) (hC : ∀ (i j : Fin 3), |C i j - idealUnprojectedEntry i j| ≤ 5 * e) (hP₀ : |P₀| ≤ Θ ^ 2) (hQ₀ : |Q₀| ≤ 2 * Θ ^ 2) (hP : |P - P₀| ≤ 800 * e * Θ ^ 5) (hQ : |Q - Q₀| ≤ 800 * e * Θ ^ 5) (hN : |N - 1| ≤ 800 * e * Θ ^ 5) : |velocityFirstRhs A C ε P Q N U V - (-2 * V + 2 * P₀ * ((P₀ + β) * V + Q₀ * U) / (1 + P₀ ^ 2))| + |velocitySecondRhs A C ε P Q N U V + U| ≤ 200000 * e * Θ ^ 12 * (|U| + |V|)

The full pressure projection is a small matrix perturbation, with an explicit constant and the power of Θ used in the source.