The genuine base parent can be restricted to one explicit positive time on which the low-order source guards hold. The constants depend only on its fixed label envelope; the initial core is empty.

Positivity of the first packet's actual pressure numerator on a short base interval. The normal and uncut velocity are the constructed source trajectories; their equations and the parent Riccati equation give the bound.

def EulerPacketFirstPressureSign.firstSignRate (CM CH : ℝ) : ℝ

First sign rate, given by 4*(3*CM^2+CH).

Equations

• EulerPacketFirstPressureSign.firstSignRate CM CH = 4 * (3 * CM ^ 2 + CH)

theorem EulerPacketFirstPressureSign.uncut_numerator_variation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (ξ : U) (x : EulerSmoothLimit.Space) (H : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (CM CH : ℝ) (hCM : 0 ≤ CM) (hCH : 0 ≤ CH) (hM : ∀ (t : ↑(Set.Icc 0 D.T)), ‖(D.M.field t) x‖ ≤ CM) (hH : ∀ (t : ↑(Set.Icc 0 D.T)), ‖H t‖ ≤ CH) (hRiccati : ∀ (t : ↑(Set.Icc 0 D.T)), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath D.T ⋯ D.M.field s) x) (-(D.M.field t) x ∘SL (D.M.field t) x - H t) (Set.Icc 0 D.T) ↑t) (hm0 : ‖(D.normal.field ⟨0, ⋯⟩) x‖ = 1) (hv0 : ‖((D.frame.field ⟨0, ⋯⟩) x) ξ‖ = 1) (h0 : inner ℝ ((D.normal.field ⟨0, ⋯⟩) x) (((D.M.field ⟨0, ⋯⟩) x) (((D.frame.field ⟨0, ⋯⟩) x) ξ)) = 1) (hshort : CM * D.T ≤ 1 / 2) (t : ↑(Set.Icc 0 D.T)) : |inner ℝ ((D.normal.field t) x) (((D.M.field t) x) (EulerPacketForwardFactorization.uncutVelocity D ξ (↑t) x)) - 1| ≤ firstSignRate CM CH * ↑t

theorem EulerPacketFirstPressureSign.uncut_numerator_pos {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (ξ : U) (x : EulerSmoothLimit.Space) (H : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (CM CH : ℝ) (hCM : 0 ≤ CM) (hCH : 0 ≤ CH) (hM : ∀ (t : ↑(Set.Icc 0 D.T)), ‖(D.M.field t) x‖ ≤ CM) (hH : ∀ (t : ↑(Set.Icc 0 D.T)), ‖H t‖ ≤ CH) (hRiccati : ∀ (t : ↑(Set.Icc 0 D.T)), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath D.T ⋯ D.M.field s) x) (-(D.M.field t) x ∘SL (D.M.field t) x - H t) (Set.Icc 0 D.T) ↑t) (hm0 : ‖(D.normal.field ⟨0, ⋯⟩) x‖ = 1) (hv0 : ‖((D.frame.field ⟨0, ⋯⟩) x) ξ‖ = 1) (h0 : inner ℝ ((D.normal.field ⟨0, ⋯⟩) x) (((D.M.field ⟨0, ⋯⟩) x) (((D.frame.field ⟨0, ⋯⟩) x) ξ)) = 1) (hshort : CM * D.T ≤ 1 / 2) (hsmall : firstSignRate CM CH * D.T ≤ 1 / 2) (t : ↑(Set.Icc 0 D.T)) : 1 / 2 ≤ inner ℝ ((D.normal.field t) x) (((D.M.field t) x) (EulerPacketForwardFactorization.uncutVelocity D ξ (↑t) x))

noncomputable def EulerBaseEulerGuards.coefficientCost (K : ℝ) : ℝ

Coefficient cost, given by 27*(frameAmplitude K)^2*gradientAmplitude K.

Equations

• EulerBaseEulerGuards.coefficientCost K = 27 * EulerPacketParentLabelBounds.frameAmplitude K ^ 2 * EulerPacketParentLabelBounds.gradientAmplitude K

theorem EulerBaseEulerGuards.coefficientCost_nonneg (K : ℝ) : 0 ≤ coefficientCost K

noncomputable def EulerBaseEulerGuards.guardTime (T K : ℝ) : ℝ

Guard time, given by min T (min 1 (1/(4*(1+coefficientCost K + firstSignRate (coefficientCost K) (coefficientCost K))))).

Equations

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

theorem EulerBaseEulerGuards.guardTime_pos (T K : ℝ) (hT : 0 < T) : 0 < guardTime T K

theorem EulerBaseEulerGuards.guardTime_le (T K : ℝ) : guardTime T K ≤ T

theorem EulerBaseEulerGuards.guardTime_le_one (T K : ℝ) : guardTime T K ≤ 1

theorem EulerBaseEulerGuards.guardTime_small (T K : ℝ) : coefficientCost K * guardTime T K ≤ 1 / 4 ∧ EulerPacketFirstPressureSign.firstSignRate (coefficientCost K) (coefficientCost K) * guardTime T K ≤ 1 / 4

theorem EulerBaseEulerGuards.inner_bounds_of_norm (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (C : ℝ) (hA : ‖A‖ ≤ C) (v : EulerSmoothLimit.Space) : -C * ‖v‖ ^ 2 ≤ inner ℝ (A v) v ∧ inner ℝ (A v) v ≤ C * ‖v‖ ^ 2

theorem EulerBaseEulerGuards.strain_norm {G : EulerParentPacketFrames.Parent} (L : EulerParentPacketFrames.LabelData G) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : ‖(G.strain.field t) x‖ ≤ coefficientCost L.K

theorem EulerBaseEulerGuards.curvature_norm {G : EulerParentPacketFrames.Parent} (L : EulerParentPacketFrames.LabelData G) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : ‖(G.curvature.field t) x‖ ≤ coefficientCost L.K

theorem EulerBaseEulerGuards.initialStrain_norm {G : EulerParentPacketFrames.Parent} (L : EulerParentPacketFrames.LabelData G) (x : EulerSmoothLimit.Space) : ‖G.initialStrain.field x‖ ≤ coefficientCost L.K

noncomputable def EulerBaseEulerGuards.lowBoundsOn {G : EulerParentPacketFrames.Parent} (L : EulerParentPacketFrames.LabelData G) (S : ℝ) (hS : 0 < S) (hST : S ≤ G.T) (hSone : S ≤ 1) (hsmall : coefficientCost L.K * S ≤ 1 / 4) : EulerParentPacketFrames.LowBounds (G.restrictTime S hS hST)

Low bounds on, bundling Be, Bc, L, r and the required compatibility proofs.

Equations

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

noncomputable def EulerBaseEulerGuards.lowBounds {G : EulerParentPacketFrames.Parent} (L : EulerParentPacketFrames.LabelData G) : EulerParentPacketFrames.LowBounds (G.restrictTime (guardTime G.T L.K) ⋯ ⋯)

Low bounds, given by lowBoundsOn L _ _ _ (guardTime_le_one G.T L.K) (guardTime_small G.T L.K).1.

Equations

• EulerBaseEulerGuards.lowBounds L = EulerBaseEulerGuards.lowBoundsOn L (EulerBaseEulerGuards.guardTime G.T L.K) ⋯ ⋯ ⋯ ⋯