On the short base interval the actual normal and homogeneous velocity have absolute size at most two. This gives the first packet's size and sign estimates without any amplification-stage hypotheses.

noncomputable def EulerPacketFirstLowBounds.firstRatio : ℝ

First ratio, given by 4*cutoffBound.

Equations

• EulerPacketFirstLowBounds.firstRatio = 4 * EulerPacketGeometryLowBounds.cutoffBound

theorem EulerPacketFirstLowBounds.firstRatio_pos : 0 < firstRatio

theorem EulerPacketFirstLowBounds.normal_norm_le_two {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (CM : ℝ) (hCM : 0 ≤ CM) (x : EulerSmoothLimit.Space) (hM : ∀ (t : ↑(Set.Icc 0 D.T)), ‖(D.M.field t) x‖ ≤ CM) (hshort : CM * D.T ≤ 1 / 2) (hzero : ‖(D.normal.field ⟨0, ⋯⟩) x‖ = 1) (t : ↑(Set.Icc 0 D.T)) : ‖(D.normal.field t) x‖ ≤ 2

theorem EulerPacketFirstLowBounds.uncut_norm_le_two {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (CM : ℝ) (hCM : 0 ≤ CM) (x : EulerSmoothLimit.Space) (hM : ∀ (t : ↑(Set.Icc 0 D.T)), ‖(D.M.field t) x‖ ≤ CM) (hshort : CM * D.T ≤ 1 / 2) [CompleteSpace U] (ξ : U) (hzero : ‖((D.frame.field ⟨0, ⋯⟩) x) ξ‖ = 1) (t : ↑(Set.Icc 0 D.T)) : ‖EulerPacketForwardFactorization.uncutVelocity D ξ (↑t) x‖ ≤ 2

theorem EulerPacketFirstLowBounds.primary_size_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (CM : ℝ) (hCM : 0 ≤ CM) (x : EulerSmoothLimit.Space) (hM : ∀ (t : ↑(Set.Icc 0 D.T)), ‖(D.M.field t) x‖ ≤ CM) (hshort : CM * D.T ≤ 1 / 2) [CompleteSpace U] (ξ : U) (hn : ‖(D.normal.field ⟨0, ⋯⟩) x‖ = 1) (hv : ‖((D.frame.field ⟨0, ⋯⟩) x) ξ‖ = 1) (t : ↑(Set.Icc 0 D.T)) : ‖(D.normal.field t) x‖ * ‖EulerPacketForwardFactorization.canonicalVelocity D ξ (↑t) x‖ ≤ firstRatio

theorem EulerPacketFirstLowBounds.primary_flux_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (x : EulerSmoothLimit.Space) [CompleteSpace U] (ξ : U) (t : ↑(Set.Icc 0 D.T)) (hflux : x ∈ tsupport EulerSpatialCutoffs.innerCutoff → 0 ≤ inner ℝ ((D.normal.field t) x) (((D.M.field t) x) (EulerPacketForwardFactorization.uncutVelocity D ξ (↑t) x))) : 0 ≤ inner ℝ ((D.normal.field t) x) (((D.M.field t) x) (EulerPacketForwardFactorization.canonicalVelocity D ξ (↑t) x))