LeanPool.NavierStokesAndEuler.Euler.PacketGeometryData

Literal physical data and scale guards for one geometric propagation stage. The record contains no amplification, sign, size, or frame-renewal conclusion.

Bounds for the actual source choice of the packet amplitude.

source

noncomputable def EulerPacketMovingFrame.primaryAmplitude (δ hchild : ℝ) (r w : ℝ → EulerSmoothLimit.Space) (t : ℝ) :

ℝ

Primary amplitude, given by δ*hchild/(‖r t‖*‖w t‖).

Equations

EulerPacketMovingFrame.primaryAmplitude δ hchild r w t = δ * hchild / (‖r t‖ * ‖w t‖)

Instances For

source

theorem EulerPacketMovingFrame.primaryAmplitude_nonneg (δ hchild : ℝ) (r w : ℝ → EulerSmoothLimit.Space) (t : ℝ) (hδ : 0 ≤ δ) (hh : 0 ≤ hchild) :

0 ≤ primaryAmplitude δ hchild r w t

source

theorem EulerPacketMovingFrame.primaryAmplitude_target_identity (δ hchild : ℝ) (r w : ℝ → EulerSmoothLimit.Space) (t : ℝ) (ht : 0 < ‖r t‖ * ‖w t‖) :

primaryAmplitude δ hchild r w t * (‖r t‖ * ‖w t‖) = δ * hchild

source

theorem EulerPacketMovingFrame.primaryAmplitude_exponential_bound (r w : ℝ → EulerSmoothLimit.Space) {δ hchild s₀ Θ x t : ℝ} (hδ : 0 ≤ δ) (hh : 0 ≤ hchild) (hs₀ : 0 < s₀) (hΘ : 0 < Θ) (hgrowth : s₀ * Real.exp x ≤ 4 * Θ * (‖r t‖ * ‖w t‖)) :

primaryAmplitude δ hchild r w t ≤ 4 * Θ * δ * hchild / s₀ * Real.exp (-x)

source

theorem EulerPacketMovingFrame.primaryAmplitude_profile_bound (r w : ℝ → EulerSmoothLimit.Space) {δ hchild s₀ σ T H targetTime : ℝ} {Z Z₁ : ℝ → ℝ} (hδ : 0 ≤ δ) (hh : 0 ≤ hchild) (hs₀ : 0 < s₀) (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hT : 1 ≤ T) (hshort : H - T ≤ 1) (hZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hZ0 : Z 0 = 1) (hZ₁0 : 0 ≤ Z₁ 0) (hlower : s₀ * idealPrimarySize σ Z T / 4 ≤ ‖r targetTime‖ * ‖w targetTime‖) (τ : ℝ) :

τ ∈ Set.Icc 0 H → primaryAmplitude δ hchild r w targetTime * Z τ ≤ 8 * Real.exp 6 * δ * hchild / s₀

The profile-weighted amplitude is bounded uniformly on the full forward horizon, including before scaled time one.

source

structure EulerPacketMovingFrame.PhysicalGeometryData (α : Type u_1) :

Type u_1

Physical geometry data, collecting center, B, B₁, M, E, m and their compatibility conditions.

center : α
Center of PhysicalGeometryData, of type α.
B : ℝ → EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space
Bound parameter of PhysicalGeometryData, of type ℝ → Space →L[ℝ] Space.
B₁ : ℝ → EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space
B₁ of PhysicalGeometryData, of type ℝ → Space →L[ℝ] Space.
M : α → ℝ → EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space
M of PhysicalGeometryData, of type α → ℝ → Space →L[ℝ] Space.
E : α → ℝ → EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space
E of PhysicalGeometryData, of type α → ℝ → Space →L[ℝ] Space.
m : ℝ → EulerSmoothLimit.Space
M of PhysicalGeometryData, of type ℝ → Space.
v : ℝ → EulerSmoothLimit.Space
V of PhysicalGeometryData, of type ℝ → Space.
r : α → ℝ → EulerSmoothLimit.Space
R of PhysicalGeometryData, of type α → ℝ → Space.
w : α → ℝ → EulerSmoothLimit.Space
W of PhysicalGeometryData, of type α → ℝ → Space.
c : ℝ
C of PhysicalGeometryData, of type ℝ.
s₀ : ℝ
S₀ of PhysicalGeometryData, of type ℝ.
t₀ : ℝ
T₀ of PhysicalGeometryData, of type ℝ.
a : ℝ
A of PhysicalGeometryData, of type ℝ.
ε : ℝ
Ε of PhysicalGeometryData, of type ℝ.
σ : ℝ
Σ of PhysicalGeometryData, of type ℝ.
y : ℝ
Y of PhysicalGeometryData, of type ℝ.
Θ : ℝ
Θ of PhysicalGeometryData, of type ℝ.
H : ℝ
H of PhysicalGeometryData, of type ℝ.
G : ℝ
Geometric data of PhysicalGeometryData, of type ℝ.
d : ℝ
D of PhysicalGeometryData, of type ℝ.
lam : ℝ
Lam of PhysicalGeometryData, of type ℝ.
δ : ℝ
Δ of PhysicalGeometryData, of type ℝ.
hchild : ℝ
Hchild of PhysicalGeometryData, of type ℝ.
S : Set ℝ
Parameter S of PhysicalGeometryData, of type Set ℝ.
sigma_pos : 0 < self.σ
sigma_small : self.σ ≤ 1 / 4
y_pos : 0 < self.y
y_small : self.y ≤ 1 / 2
target_le_horizon : self.y⁻¹ / self.σ ≤ self.H
horizon_le_Theta : self.H ≤ self.Θ
short_extension : self.H - self.y⁻¹ / self.σ ≤ 1
a_lower : 1 / 2 ≤ self.a
epsilon_pos : 0 < self.ε
Theta_lower : 1 ≤ self.Θ
G_lower : 1 ≤ self.G
d_nonneg : 0 ≤ self.d
ray_scale_pos : 0 < self.s₀
slope_nonneg : 0 ≤ self.lam
delta_nonneg : 0 ≤ self.δ
child_nonneg : 0 ≤ self.hchild
small : 1000000 * neighborStabilityConstant * (16 * (self.ε * self.Θ * (4 * self.G) ^ 2 + self.d)) * self.Θ ^ 40 ≤ 1
compression_guard : 60 * (self.G + self.d) * (self.y⁻¹ / self.σ) * self.ε < self.a
time_maps : Set.MapsTo (physicalTime self.t₀ self.a self.ε) (Set.Icc 0 self.Θ) self.S
M_continuous (ξ : α) : ContinuousOn (self.M ξ) self.S
B_derivative (t : ℝ) : t ∈ self.S → HasDerivWithinAt self.B (self.B₁ t) self.S t
old_ray_equation (t : ℝ) : t ∈ self.S → HasDerivWithinAt self.m (-(ContinuousLinearMap.adjoint (self.B t)) (self.m t)) self.S t
old_velocity_equation (t : ℝ) : t ∈ self.S → HasDerivWithinAt self.v (-(self.B t) (self.v t) + (2 * inner ℝ (self.m t) ((self.B t) (self.v t)) / ‖self.m t‖ ^ 2) • self.m t) self.S t
ray_equation (ξ : α) (t : ℝ) : t ∈ self.S → HasDerivWithinAt (self.r ξ) (-(ContinuousLinearMap.adjoint (self.M ξ t)) (self.r ξ t)) self.S t
velocity_equation (ξ : α) (t : ℝ) : t ∈ self.S → HasDerivWithinAt (self.w ξ) (-(self.M ξ t) (self.w ξ t) + (2 * inner ℝ (self.r ξ t) ((self.M ξ t) (self.w ξ t)) / ‖self.r ξ t‖ ^ 2) • self.r ξ t) self.S t
old_ray_nonzero (t : ℝ) : t ∈ self.S → self.m t ≠ 0
old_velocity_nonzero (t : ℝ) : t ∈ self.S → self.v t ≠ 0
old_tangent (t : ℝ) : t ∈ self.S → inner ℝ (self.m t) (self.v t) = 0
initial_tangent (ξ : α) : inner ℝ (self.r ξ self.t₀) (self.w ξ self.t₀) = 0
B_bound (t : ℝ) : t ∈ self.S → ‖self.B t‖ ≤ self.G
B_derivative_bound (t : ℝ) : t ∈ self.S → ‖self.B₁ t‖ ≤ self.G ^ 2
E_bound (ξ : α) (t : ℝ) : t ∈ self.S → ‖self.E ξ t‖ ≤ self.d
parent_decomposition (ξ : α) (t : ℝ) : t ∈ self.S → self.M ξ t = self.B t + primaryShear self.c self.m self.v t • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (self.v t))) (EulerPacketNormalizedPrimary.unit (self.m t)) + self.E ξ t
initial_coupling : rescaledFrame self.B self.m self.v self.t₀ self.a self.ε 0 0 1 = self.a
initial_tilt : rescaledFrame self.B self.m self.v self.t₀ self.a self.ε 0 2 1 = self.a * self.σ ^ 2
initial_shear : rescaledShear self.c self.m self.v self.t₀ self.a self.ε 0 = self.a / self.ε ^ 2
initial_ray_error (ξ : α) : EulerPacketRay.norm3 (scaledRay self.m self.v (self.r ξ) self.s₀ self.t₀ self.a self.ε 0 0) (scaledRay self.m self.v (self.r ξ) self.s₀ self.t₀ self.a self.ε 0 1) (scaledRay self.m self.v (self.r ξ) self.s₀ self.t₀ self.a self.ε 0 2 - 1) ≤ 16 * (self.ε * self.Θ * (4 * self.G) ^ 2 + self.d)
initial_velocity_error (ξ : α) : |scaledVelocity self.m self.v (self.w ξ) self.t₀ self.a self.ε 0 1 - 1| + |scaledVelocity self.m self.v (self.w ξ) self.t₀ self.a self.ε 0 0 + self.lam| ≤ 16 * (self.ε * self.Θ * (4 * self.G) ^ 2 + self.d)